diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/cc/ccalgo.ml | 2 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 8 | ||||
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 25 | ||||
-rw-r--r-- | plugins/derive/derive.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 9 | ||||
-rw-r--r-- | plugins/firstorder/formula.ml | 11 | ||||
-rw-r--r-- | plugins/firstorder/instances.ml | 3 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 6 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 6 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 60 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 39 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 52 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 8 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 40 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 24 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 18 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 37 | ||||
-rw-r--r-- | plugins/rtauto/refl_tauto.ml | 5 | ||||
-rw-r--r-- | plugins/rtauto/refl_tauto.mli | 2 |
21 files changed, 205 insertions, 158 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc3d9ed56..359157a4c 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -824,7 +824,7 @@ let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in let {it=gl ; sigma=sigma} = state.gls in - let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in + let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in state.gls<- gls; id diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 09d9cf019..e5b68af8e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,6 +23,7 @@ open Pp open Errors open Util open Proofview.Notations +open Context.Rel.Declaration let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -152,7 +153,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff + quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -167,7 +168,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff + quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -188,7 +189,8 @@ let make_prb gls depth additionnal_terms = let t = decompose_term env sigma c in ignore (add_term state t)) additionnal_terms; List.iter - (fun (id,_,e) -> + (fun decl -> + let (id,_,e) = Context.Named.Declaration.to_tuple decl in begin let cid=mkVar id in match litteral_of_constr env sigma e with diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2a44dca21..7cfca53c5 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)= match hyp with (Hprop st | Hvar st) -> match st.st_label with - Name id -> Environ.push_named (id,None,st.st_it) env0 + Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0 | _ -> env in let nenv = List.fold_right push_one locvars env in nenv,res diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index acee3d6c2..f9399d682 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -116,7 +116,7 @@ let get_top_stack pts = let get_stack pts = Proof.get_at_focus proof_focus pts let get_last env = match Environ.named_context env with - | (id,_,_)::_ -> id + | decl :: _ -> Context.Named.Declaration.get_id decl | [] -> error "no previous statement to use" diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index f47b35541..22a646b3f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -30,6 +30,7 @@ open Namegen open Goptions open Misctypes open Sigma.Notations +open Context.Named.Declaration (* Strictness option *) @@ -229,7 +230,8 @@ let close_previous_case pts = (* automation *) let filter_hyps f gls = - let filter_aux (id,_,_) = + let filter_aux id = + let id = get_id id in if f id then tclIDTAC else @@ -331,11 +333,12 @@ let enstack_subsubgoals env se stack gls= let rc,_ = Reduction.dest_prod env apptype in let rec meta_aux last lenv = function [] -> (last,lenv,[]) - | (nam,_,typ)::q -> + | decl::q -> let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in - (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + let open Context.Rel.Declaration in + (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in @@ -411,7 +414,7 @@ let concl_refiner metas body gls = let _A = subst_meta subst typ in let x = id_of_name_using_hdchar env _A Anonymous in let _x = fresh_id avoid x gls in - let nenv = Environ.push_named (_x,None,_A) env in + let nenv = Environ.push_named (LocalAssum (_x,_A)) env in let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in let nsubst = (n,mkVar _x)::subst in if List.is_empty rest then @@ -606,7 +609,7 @@ let assume_tac hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_hyps_or_theses hyps gls = @@ -616,7 +619,7 @@ let assume_hyps_or_theses hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam) | Hprop {st_label=nam;st_it=Thesis (tk)} -> tclTHEN (push_intro_tac @@ -628,7 +631,7 @@ let assume_st hyps gls = (fun st -> tclTHEN (push_intro_tac - (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) + (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_st_letin hyps gls = @@ -637,7 +640,7 @@ let assume_st_letin hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label)) hyps tclIDTAC gls (* suffices *) @@ -731,7 +734,7 @@ let rec consider_match may_intro introduced available expected gls = error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) + tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) begin match st.st_label with Anonymous -> @@ -799,8 +802,8 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with This id -> - let (_,body,_) = pf_get_hyp gls id in - Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls + let body = pf_get_hyp gls id |> get_value in + Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index a47dc5b2f..5d1551106 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Context.Named.Declaration + let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> @@ -32,7 +34,7 @@ let start_deriving f suchthat lemma = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> - let env' = Environ.push_named (f , (Some ef) , f_type) env in + let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in let evdref = ref sigma in let suchthat = Constrintern.interp_type_evars env' evdref suchthat in TCons ( env' , !evdref , suchthat , (fun sigma _ -> diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 38aef62e1..6c57bc2bb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -25,6 +25,7 @@ open Globnames open Miniml open Table open Mlutil +open Context.Rel.Declaration (*i*) exception I of inductive_kind @@ -74,7 +75,7 @@ type flag = info * scheme let rec flag_of_type env t : flag = let t = whd_betadeltaiota env none t in match kind_of_term t with - | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c + | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) @@ -247,7 +248,7 @@ let rec extract_type env db j c args = | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with - | (_,Some t,_) -> extract_type env db j (lift n t) args + | LocalDef (_,t,_) -> extract_type env db j (lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown @@ -560,7 +561,7 @@ let rec extract_term env mle mlt c args = put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (Name id, Some c1, t1) env in + let env' = push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (lift 1) args in @@ -835,7 +836,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let decomp_lams_eta_n n m env c t = let rels = fst (splay_prod_n env none n t) in - let rels = List.map (fun (id,_,c) -> (id,c)) rels in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index ae2d059fa..2ed436c6b 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,6 +15,7 @@ open Tacmach open Util open Declarations open Globnames +open Context.Rel.Declaration let qflag=ref true @@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm = negative:= unsigned :: !negative end; let v = ind_hyps 0 i l gl in - let g i _ (_,_,t) = - build_rec env polarity (lift i t) in + let g i _ decl = + build_rec env polarity (lift i (get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm = | Exists(i,l)-> let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in - let g i _ (_,_,t) = - build_rec (var::env) polarity (lift i t) in + let g i _ decl = + build_rec (var::env) polarity (lift i (get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in + let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a717cc91e..797f43f2a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Context.Rel.Declaration let compare_instance inst1 inst2= match inst1,inst2 with @@ -117,7 +118,7 @@ let mk_open_instance id idc gl m t= if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = (Name nid,None,c) in + let decl = LocalAssum (Name nid,c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index e676a8a93..b0e8f7d25 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -19,6 +19,7 @@ open Formula open Sequent open Globnames open Locus +open Context.Named.Declaration type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -34,12 +35,13 @@ let wrap n b continue seq gls= if i<=0 then seq else match nc with []->anomaly (Pp.str "Not the expected number of hyps") - | ((id,_,typ) as nd)::q-> + | nd::q-> + let id = get_id nd in if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4c0aa6c75..8bc84608e 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -445,7 +445,11 @@ let is_ineq (h,t) = ;; *) -let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; +let list_of_sign s = + let open Context.Named.Declaration in + List.map (function LocalAssum (name, typ) -> name, typ + | LocalDef (name, _, typ) -> name, typ) + s;; let mkAppL a = let l = Array.to_list a in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4eab5f912..28982c37f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -15,6 +15,7 @@ open Tactics open Indfun_common open Libnames open Globnames +open Context.Rel.Declaration (* let msgnl = Pp.msgnl *) @@ -304,11 +305,11 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = in let new_type_of_hyp,ctxt_size,witness_fun = List.fold_left_i - (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> + (fun i (end_of_type,ctxt_size,witness_fun) decl -> try let witness = Int.Map.find i sub in - if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) + if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); + (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with Failure "NoChange" -> (* Last thing todo : push the rel in the context and continue *) - scan_type ((x,None,t_x)::context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -736,7 +737,8 @@ let build_proof tclTHEN (Proofview.V82.of_tactic intro) (fun g' -> - let (id,_,_) = pf_last_hyp g' in + let open Context.Named.Declaration in + let id = pf_last_hyp g' |> get_id in let new_term = pf_nf_betaiota g' (mkApp(dyn_infos.info,[|mkVar id|])) @@ -921,7 +923,9 @@ let generalize_non_dep hyp g = let env = Global.env () in let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = - Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> + let open Context.Named.Declaration in + Environ.fold_named_context_reverse (fun (clear,keep) decl -> + let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env hyp) keep || Termops.occur_var env hyp hyp_typ @@ -936,7 +940,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl (na,_,_) = (Nameops.out_name na) +let id_of_decl decl = Nameops.out_name (get_name decl) let var_of_decl decl = mkVar (id_of_decl decl) let revert idl = tclTHEN @@ -1044,7 +1048,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a ( fun g' -> let just_introduced = nLastDecls nb_intro_to_do g' in - let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in + let open Context.Named.Declaration in + let just_introduced_id = List.map get_id just_introduced in tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g' ) @@ -1069,11 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = - (fun (na,b,t) -> - (fresh_id na,b,t) - ) - in + let fresh_decl = map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1120,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1166,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let pte_to_fix,rev_info = List.fold_left_i - (fun i (acc_map,acc_info) (pte,_,_) -> + (fun i (acc_map,acc_info) decl -> + let pte = get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1259,7 +1261,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) - let args_id = List.map (fun (id,_,_) -> id) args in + let open Context.Named.Declaration in + let args_id = List.map get_id args in let dyn_infos = { nb_rec_hyps = -100; @@ -1276,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params)) + (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1317,8 +1320,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam [ tclDO nb_args (Proofview.V82.of_tactic intro); (fun g -> (* replacement of the function by its body *) - let args = nLastDecls nb_args g in - let args_id = List.map (fun (id,_,_) -> id) args in + let args = nLastDecls nb_args g in + let open Context.Named.Declaration in + let args_id = List.map get_id args in let dyn_infos = { nb_rec_hyps = -100; @@ -1520,7 +1524,7 @@ let prove_principle_for_gen avoid := new_id :: !avoid; Name new_id in - let fresh_decl (na,b,t) = (fresh_id na,b,t) in + let fresh_decl = map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1550,11 +1554,11 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (Name id,_,_)::_ -> id + | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in @@ -1582,7 +1586,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in + let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in let lemma = match !tcc_lemma_ref with | None -> error "No tcc proof !!" @@ -1629,7 +1633,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (fun (na,_,_) -> Nameops.out_name na) + (List.rev_map (fun decl -> Nameops.out_name (get_name decl)) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1667,7 +1671,7 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates + List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates in let pte_info = { proving_tac = @@ -1683,7 +1687,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (fun (na,_,_) -> (Nameops.out_name na)) + (fun decl -> (Nameops.out_name (get_name decl))) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1712,7 +1716,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches) + (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e2c3bbb97..7a933c04b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -8,6 +8,7 @@ open Names open Pp open Entries open Tactics +open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs open Misctypes @@ -32,11 +33,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = match predicates with | [] -> [] - |(Name x,v,t)::predicates -> - let id = Namegen.next_ident_away x avoid in - Hashtbl.add tbl id x; - (Name id,v,t)::(change_predicates_names (id::avoid) predicates) - | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ") + | decl :: predicates -> + (match Context.Rel.Declaration.get_name decl with + | Name x -> + let id = Namegen.next_ident_away x avoid in + Hashtbl.add tbl id x; + set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -46,15 +49,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in (* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *) (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) - let change_predicate_sort i (x,_,t) = + let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod t in + let args,_ = decompose_prod (get_type decl) in let real_args = if princ_type_info.indarg_in_concl then List.tl args else args in - Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) + Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), + compose_prod real_args (mkSort new_sort)) in let new_predicates = List.map_i @@ -69,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | _ -> error "Not a valid predicate" ) in - let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in + let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> @@ -114,7 +118,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Rel n -> begin try match Environ.lookup_rel n env with - | _,_,t when is_dom t -> raise Toberemoved + | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved | _ -> pre_princ,[] with Not_found -> assert false end @@ -159,7 +163,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_x : Name.t = get_name (Termops.ids_of_context env) x in - let new_env = Environ.push_rel (x,None,t) env in + let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b @@ -188,7 +192,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in let new_x : Name.t = get_name (Termops.ids_of_context env) x in - let new_env = Environ.push_rel (x,Some v,t) env in + let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b @@ -227,7 +231,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in it_mkProd_or_LetIn (it_mkProd_or_LetIn - pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) + pre_res (List.map (function Context.Named.Declaration.LocalAssum (id,b) -> LocalAssum (Name (Hashtbl.find tbl id), b) + | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b)) new_predicates) ) princ_type_info.params @@ -235,10 +240,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let change_property_sort evd toSort princ princName = + let open Context.Rel.Declaration in let princ_info = compute_elim_sig princ in - let change_sort_in_predicate (x,v,t) = - (x,None, - let args,ty = decompose_prod t in + let change_sort_in_predicate decl = + LocalAssum + (get_name decl, + let args,ty = decompose_prod (get_type decl) in let s = destSort ty in Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty); compose_prod args (mkSort toSort) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 80de8e764..8a0a1a064 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -335,15 +335,17 @@ let raw_push_named (na,raw_value,raw_typ) env = | Name id -> let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in - Environ.push_named (id,value,typ) env + let open Context.Named.Declaration in + Environ.push_named (of_tuple (id,value,typ)) env let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = + let open Context.Rel.Declaration in observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (na,None,typ) env + | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) typ @@ -351,15 +353,16 @@ let add_pat_variables pat typ env : Environ.env = in let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in let new_env = add_pat_variables env pat typ in let res = fst ( Context.Rel.fold_outside - (fun (na,v,t) (env,ctxt) -> - match na with + (fun decl (env,ctxt) -> + let _,v,t = Context.Rel.Declaration.to_tuple decl in + match Context.Rel.Declaration.get_name decl with | Anonymous -> assert false | Name id -> let new_t = substl ctxt t in @@ -370,7 +373,8 @@ let add_pat_variables pat typ env : Environ.env = Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) ); - (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) + let open Context.Named.Declaration in + (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -398,7 +402,8 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + let open Context.Rel.Declaration in + let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -597,9 +602,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = + let open Context.Named.Declaration in match n with Anonymous -> env - | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env + | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res @@ -875,7 +881,7 @@ exception Continue *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); - + let open Context.Rel.Declaration in match rt with | GProd(_,n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in @@ -895,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -926,7 +932,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let subst_b = if is_in_b then b else replace_var_by_term id rt b in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -970,9 +976,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let (na,_,_) = - Environ.lookup_rel (destRel var_as_constr) env - in + let open Context.Rel.Declaration in + let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> @@ -1010,7 +1015,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let new_env = let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in - Environ.push_rel (n,None,t') env + Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons @@ -1048,7 +1053,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1064,7 +1069,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1085,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1108,7 +1113,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd t' in - let new_env = Environ.push_rel (n,Some t',type_t') env in + let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1132,7 +1137,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = depth t in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (na,None,t') env in + let new_env = Environ.push_rel (LocalAssum (na,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1254,12 +1259,13 @@ let do_build_inductive let relnames = Array.map mk_rel_id funnames in let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in (* Construction of the pseudo constructors *) + let open Context.Named.Declaration in let evd,env = Array.fold_right2 (fun id c (evd,env) -> let evd,t = Typing.type_of env evd (mkConstU c) in evd, - Environ.push_named (id,None,t) + Environ.push_named (LocalAssum (id,t)) (* try *) (* Typing.e_type_of env evd (mkConstU c) *) (* with Not_found -> *) @@ -1298,8 +1304,8 @@ let do_build_inductive *) let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (rel_name,None, - fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities + Environ.push_named (LocalAssum (rel_name, + fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d1e109825..86abf9e2e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,4 @@ +open Context.Rel.Declaration open Errors open Util open Names @@ -13,10 +14,10 @@ open Decl_kinds open Sigma.Notations let is_rec_info scheme_info = - let test_branche min acc (_,_,br) = + let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br @@ -153,7 +154,8 @@ let build_newrecursive let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in - (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb81..56bc4328d 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + open Tacexpr open Declarations open Errors @@ -20,6 +21,7 @@ open Indfun_common open Tacmach open Misctypes open Termops +open Context.Rel.Declaration (* Some pretty printing function for debugging purpose *) @@ -134,18 +136,21 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type + | decl :: fun_ctxt -> fun_ctxt, get_type decl in let rec args_from_decl i accu = function | [] -> accu - | (_, Some _, _) :: l -> + | LocalDef _ :: l -> args_from_decl (succ i) accu l | _ :: l -> let t = mkRel i in args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in + let filter = fun decl -> match get_name decl with + | Name id -> Some id + | Anonymous -> None + in let named_ctxt = List.map_filter filter fun_ctxt in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in @@ -171,12 +176,12 @@ let generate_type evd g_to_f f graph i = \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) let pre_ctxt = - (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt + LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt in (*i and we can return the solution depending on which lemma type we are defining i*) if g_to_f - then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph - else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph + then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -260,10 +265,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* and built the intro pattern for each of them *) let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) ) branches in @@ -390,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun ((_,(ctxt,concl))) -> match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") - | hres::res::(x,_,t)::ctxt -> + | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - ((x,None,t)::ctxt) + (LocalAssum (get_name decl, get_type decl) :: ctxt) in res ) @@ -408,8 +413,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let bindings = let params_bindings,avoid = List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -418,8 +423,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in let lemmas_bindings = List.rev (fst (List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -455,9 +460,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes generalize every hypothesis which depends of [x] but [hyp] *) let generalize_dependent_of x hyp g = + let open Context.Named.Declaration in tclMAP (function - | (id,None,t) when not (Id.equal id hyp) && + | LocalAssum (id,t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) @@ -663,10 +669,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let branches = List.rev princ_infos.branches in let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type)) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 57782dd71..c71d9a9ca 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -24,6 +24,7 @@ open Declarations open Glob_term open Glob_termops open Decl_kinds +open Context.Rel.Declaration (** {1 Utilities} *) @@ -134,9 +135,9 @@ let showind (id:Id.t) = let cstrid = Constrintern.global_reference id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in - List.iter (fun (nm, optcstr, tp) -> - print_string (string_of_name nm^":"); - prconstr tp; print_string "\n") + List.iter (fun decl -> + print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); + prconstr (get_type decl); print_string "\n") ib1.mind_arity_ctxt; Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri @@ -459,11 +460,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in let _ = prstr "\notherprms1:\n" in let _ = - List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); + prconstr (get_type decl); prstr "\n") otherprms1 in let _ = prstr "\notherprms2:\n" in let _ = - List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n") otherprms2 in { ident=id; @@ -823,9 +825,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = List.fold_left - (fun (acc,env) (nm,_,c) -> + (fun (acc,env) decl -> + let nm = Context.Rel.Declaration.get_name decl in + let c = get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in - let newenv = Environ.push_rel (nm,None,c) env in + let newenv = Environ.push_rel (LocalAssum (nm,c)) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @@ -852,10 +856,10 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with - | (nme,None,t) -> + | LocalAssum (nme,t) -> let traw = Detyping.detype false [] (Global.env()) Evd.empty t in GProd (Loc.ghost,nme,Explicit,traw,t2) - | (_,Some _,_) -> assert false + | LocalDef _ -> assert false (** [merge_inductive ind1 ind2 lnk] merges two graphs, linking @@ -969,7 +973,7 @@ let funify_branches relinfo nfuns branch = | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) | _ -> false in (* FIXME: *) - (Anonymous,Some mkProp,mkProp) + LocalDef (Anonymous,mkProp,mkProp) let relprinctype_to_funprinctype relprinctype nfuns = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b09678341..09c5aa567 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -40,7 +40,7 @@ open Eauto open Indfun_common open Sigma.Notations - +open Context.Rel.Declaration (* Ugly things which should not be here *) @@ -181,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) = ) in let context = List.map - (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al)) + (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al)) in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = @@ -678,8 +678,10 @@ let mkDestructEq : let hyps = pf_hyps g in let to_revert = Util.List.map_filter - (fun (id, _, t) -> - if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) + (fun decl -> + let open Context.Named.Declaration in + let id = get_id decl in + if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in @@ -1253,7 +1255,7 @@ let clear_goals = then Termops.pop b' else if b' == b then t else mkProd(na,t',b') - | _ -> map_constr clear_goal t + | _ -> Term.map_constr clear_goal t in List.map clear_goal @@ -1489,7 +1491,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = ref (Evd.from_env env) in let function_type = interp_type_evars env evd type_of_f in - let env = push_named (function_name,None,function_type) env in + let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let ty = interp_type_evars env evd ~impls:rec_impls eq in let evm, nf = Evarutil.nf_evars_and_universes !evd in @@ -1497,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let function_type = nf function_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in - let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in + let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in let eq' = nf_zeta env_eq' eq' in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) @@ -1515,7 +1517,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in - let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in + let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr env_with_pre_rec_args diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 7e38109d6..b740649e9 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -28,6 +28,7 @@ open Nametab open Contradiction open Misctypes open Proofview.Notations +open Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1695,25 +1696,26 @@ let destructure_hyps = let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) - | (i,body,t)::lit -> + | decl::lit -> + let (i,_,t) = to_tuple decl in begin try match destructurate_prop t with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> (Tacticals.New.tclTHENS (elim_id i) - [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); - onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) + [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); + onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop ((i1,None,t1)::(i2,None,t2)::lit))) + loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit))) + loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) @@ -1724,7 +1726,7 @@ let destructure_hyps = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> - (loop ((i,None,mk_or (mk_not t1) t2)::lit)))) + (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) ] else loop lit @@ -1735,7 +1737,7 @@ let destructure_hyps = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> - (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) + (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in @@ -1744,7 +1746,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))) + (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in @@ -1754,9 +1756,8 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> - (loop ((i,None, - mk_or (mk_and t1 (mk_not t2)) - (mk_and (mk_not t1) t2))::lit)))) + (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2)) + (mk_and (mk_not t1) t2)) :: lit)))) ] | Kimp(t1,t2) -> (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. @@ -1767,14 +1768,14 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) + (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit)))) ] | Kapp(Not,[t]) -> let d = decidability t in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop ((i,None,t)::lit)))) + (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) ] | Kapp(op,[t1;t2]) -> (try @@ -1807,15 +1808,13 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|])))) + (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) + (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 9c22b5adb..2f3a3e551 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -13,6 +13,7 @@ open Util open Term open Tacmach open Proof_search +open Context.Named.Declaration let force count lazc = incr count;Lazy.force lazc @@ -128,9 +129,9 @@ let rec make_form atom_env gls term = let rec make_hyps atom_env gls lenv = function [] -> [] - | (_,Some body,typ)::rest -> + | LocalDef (_,body,typ)::rest -> make_hyps atom_env gls (typ::body::lenv) rest - | (id,None,typ)::rest -> + | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in if List.exists (Termops.dependent (mkVar id)) lenv || diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index c9e591bbd..9a14ac6c7 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -18,7 +18,7 @@ val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> Term.types list -> - (Names.Id.t * Term.types option * Term.types) list -> + Context.Named.t -> (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic |