From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/auto_ind_decl.ml | 125 ++++++++++++++++++++++++---------------------- 1 file changed, 66 insertions(+), 59 deletions(-) (limited to 'toplevel/auto_ind_decl.ml') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index b3144fa9..0561fc4b 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -10,7 +10,7 @@ decidable equality, created by Vincent Siles, Oct 2007 *) open Tacmach -open Errors +open CErrors open Util open Pp open Term @@ -25,6 +25,7 @@ open Tactics open Ind_tables open Misctypes open Proofview.Notations +open Context.Rel.Declaration let out_punivs = Univ.out_punivs @@ -53,7 +54,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported @@ -85,7 +86,7 @@ let destruct_on c = destruct false None c None None let destruct_on_using c id = destruct false None c - (Some (dl,[[dl,IntroNaming IntroAnonymous]; + (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous]; [dl,IntroNaming (IntroIdentifier id)]])) None @@ -102,12 +103,12 @@ let mkFullInd (ind,u) n = context_chop (nparams-nparrec) mib.mind_params_ctxt in if nparrec > 0 then mkApp (mkIndU (ind,u), - Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) + Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec)) else mkIndU (ind,u) let check_bool_is_defined () = try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in () - with e when Errors.noncritical e -> raise (UndefinedCst "bool") + with e when CErrors.noncritical e -> raise (UndefinedCst "bool") let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -137,7 +138,7 @@ let build_beq_scheme mode kn = | Name s -> Id.of_string ("eq_"^(Id.to_string s)) | Anonymous -> Id.of_string "eq_A" in - let ext_rel_list = extended_rel_list 0 lnamesparrec in + let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in let lift_cnt = ref 0 in let eqs_typ = List.map (fun aa -> let a = lift !lift_cnt aa in @@ -146,17 +147,17 @@ let build_beq_scheme mode kn = ) ext_rel_list in let eq_input = List.fold_left2 - ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *) + ( fun a b decl -> (* mkLambda(n,b,a) ) *) (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (eqName n) b a ) + mkNamedLambda (eqName (get_name decl)) b a ) c (List.rev eqs_typ) lnamesparrec in - List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *) + List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) (* Same here , hoping the auto renaming will do something good ;) *) mkNamedLambda - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let make_one_eq cur = let u = Univ.Instance.empty in @@ -180,7 +181,13 @@ let build_beq_scheme mode kn = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants + | Var x -> + let eid = id_of_string ("eq_"^(string_of_id x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (VarRef x)) + in + mkVar eid, Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> @@ -208,7 +215,7 @@ let build_beq_scheme mode kn = | LetIn _ -> raise (EqUnknown "LetIn") | Const kn -> (match Environ.constant_opt_value_in env kn with - | None -> raise (ParameterWithoutEquality (fst kn)) + | None -> raise (ParameterWithoutEquality (ConstRef (fst kn))) | Some c -> aux (applist (c,a))) | Proj _ -> raise (EqUnknown "Proj") | Construct _ -> raise (EqUnknown "Construct") @@ -233,7 +240,7 @@ let build_beq_scheme mode kn = Cn => match Y with ... end |] part *) let ci = make_case_info env (fst ind) MatchStyle in let constrs n = get_constructors env (make_ind_family (ind, - extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in + Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in @@ -248,7 +255,7 @@ let build_beq_scheme mode kn = | 0 -> Lazy.force tt | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in for ndx = 0 to nb_cstr_args-1 do - let _,_,cc = List.nth constrsi.(i).cs_args ndx in + let cc = get_type (List.nth constrsi.(i).cs_args ndx) in let eqA, eff' = compute_A_equality rel_list nparrec (nparrec+3+2*nb_cstr_args) @@ -267,14 +274,14 @@ let build_beq_scheme mode kn = (Array.sub eqs 1 (nb_cstr_args - 1)) ) in - (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc + (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc (constrsj.(j).cs_args) ) - else ar2.(j) <- (List.fold_left (fun a (p,q,r) -> - mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + else ar2.(j) <- (List.fold_left (fun a decl -> + mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) done; - ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) + ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) (mkCase (ci,do_predicate rel_list nb_cstr_args, mkVar (Id.of_string "Y") ,ar2)) (constrsi.(i).cs_args)) @@ -343,7 +350,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* if this happen then the args have to be already declared as a Parameter*) ( @@ -354,7 +361,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ))) ) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = @@ -384,7 +391,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace p q ; apply app ; Auto.default_auto] - end + end } (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = @@ -401,7 +408,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* if this happen then the args have to be already declared as a Parameter*) ( @@ -416,13 +423,13 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 (* trick so that the good sequence is returned*) - with e when Errors.noncritical e -> indu,[||] + with e when CErrors.noncritical e -> indu,[||] in if eq_ind (fst u) ind then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ] else ( @@ -457,7 +464,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = aux q1 q2 ] ) ) - end + end } | ([],[]) -> Proofview.tclUNIT () | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in @@ -487,8 +494,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = create, from a list of ids [i1,i2,...,in] the list [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] *) -let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = - match n with +let list_id l = List.fold_left ( fun a decl -> let s' = + match get_name decl with Name s -> Id.to_string s | Anonymous -> "A" in (Id.of_string s',Id.of_string ("eq_"^s'), @@ -535,9 +542,9 @@ let compute_bl_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -564,7 +571,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -580,25 +587,25 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTRY ( Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); - Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp)); + simpl_in_hyp (freshz,Locus.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [ Simple.apply_in freshz (andb_prop()); - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in - (destruct_on_as (mkVar freshz) - [[dl,IntroNaming (IntroIdentifier fresht); + destruct_on_as (mkVar freshz) + (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht); dl,IntroNaming (IntroIdentifier freshz)]]) - end + end } ]); (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.nf_enter { enter = begin fun gls -> let gl = Proofview.Goal.concl gls in match (kind_of_term gl) with | App (c,ca) -> ( @@ -617,10 +624,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end + end } ] - end + end } let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -678,9 +685,9 @@ let compute_lb_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) lb_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match (get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -707,7 +714,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -724,13 +731,13 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj None false None (mkVar freshz,NoBindings); - intros; (Proofview.V82.tactic simpl_in_concl); + intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [apply (andb_true_intro()); simplest_split ;Auto.default_auto ] ); - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.nf_enter { enter = begin fun gls -> let gl = Proofview.Goal.concl gls in (* assume the goal to be eq (eq_type ...) = true *) match (kind_of_term gl) with @@ -746,9 +753,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end + end } ] - end + end } let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -779,7 +786,7 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind let check_not_is_defined () = try ignore (Coqlib.build_coq_not ()) - with e when Errors.noncritical e -> raise (UndefinedCst "not") + with e when CErrors.noncritical e -> raise (UndefinedCst "not") (* {n=m}+{n<>m} part *) let compute_dec_goal ind lnamesparrec nparrec = @@ -819,9 +826,9 @@ let compute_dec_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -854,7 +861,7 @@ let compute_dec_tact ind lnamesparrec nparrec = avoid := fresh::(!avoid); fresh end gl in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -885,7 +892,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ) (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto); - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let freshH2 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [ (* left *) @@ -897,11 +904,11 @@ let compute_dec_tact ind lnamesparrec nparrec = ; (*right *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; - Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref)); + unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all (); assert_by (Name freshH3) @@ -919,11 +926,11 @@ let compute_dec_tact ind lnamesparrec nparrec = true; Equality.discr_tac false None ] - end + end } ] - end + end } ] - end + end } let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in -- cgit v1.2.3