diff options
Diffstat (limited to 'plugins')
74 files changed, 1095 insertions, 956 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 4d817625f5..1bdedcaf26 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -196,7 +196,7 @@ module Btauto = struct let assign = List.combine penv var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let sigma, env = Pfedit.get_current_context () in + let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 575d964158..048ec56dee 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -17,6 +17,7 @@ open Pp open Names open Sorts open Constr +open Context open Vars open Goptions open Tacmach @@ -26,10 +27,6 @@ let init_size=5 let cc_verbose=ref false -let print_constr t = - let sigma, env = Pfedit.get_current_context () in - Printer.pr_econstr_env env sigma t - let debug x = if !cc_verbose then Feedback.msg_debug (x ()) @@ -421,11 +418,11 @@ let new_representative typ = let _A_ = Name (Id.of_string "A") let _B_ = Name (Id.of_string "A") -let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) +let _body_ = mkProd(make_annot Anonymous Sorts.Relevant,mkRel 2,mkRel 2) let cc_product s1 s2 = - mkLambda(_A_,mkSort(s1), - mkLambda(_B_,mkSort(s2),_body_)) + mkLambda(make_annot _A_ Sorts.Relevant,mkSort(s1), + mkLambda(make_annot _B_ Sorts.Relevant,mkSort(s2),_body_)) let rec constr_of_term = function Symb s-> s @@ -452,11 +449,11 @@ let rec canonize_name sigma c = let canon_mind = MutInd.make1 (MutInd.canonical kn) in mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> - mkProd (na,func t, func ct) + mkProd (na,func t, func ct) | Lambda (na,t,ct) -> - mkLambda (na, func t,func ct) + mkLambda (na, func t,func ct) | LetIn (na,b,t,ct) -> - mkLetIn (na, func b,func t,func ct) + mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.Smart.map func l) | Proj(p,c) -> @@ -483,11 +480,11 @@ let rec inst_pattern subst = function (fun spat f -> Appli (f,inst_pattern subst spat)) args t -let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" +let pr_idx_term env sigma uf i = str "[" ++ int i ++ str ":=" ++ + Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" -let pr_term t = str "[" ++ - print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" +let pr_term env sigma t = str "[" ++ + Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -602,16 +599,16 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ - pr_term s ++ str " == " ++ pr_term t ++ str "]")); + (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ + pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]")); add_equality state prf s t end else begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ - pr_term s ++ str " <> " ++ pr_term t ++ str "]")); + (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ + pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]")); add_disequality state (Hyp prf) s t end end @@ -639,8 +636,8 @@ let join_path uf i j= min_path (down_path uf i [],down_path uf j []) let union state i1 i2 eq= - debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++ - str " and " ++ pr_idx_term state.uf i2 ++ str "."); + debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ + str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in link state.uf i1 i2 eq; @@ -680,8 +677,8 @@ let union state i1 i2 eq= let merge eq state = (* merge and no-merge *) debug - (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++ - str " and " ++ pr_idx_term state.uf eq.rhs ++ str "."); + (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++ + str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str "."); let uf=state.uf in let i=find uf eq.lhs and j=find uf eq.rhs in @@ -693,7 +690,7 @@ let merge eq state = (* merge and no-merge *) let update t state = (* update 1 and 2 *) debug - (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str "."); + (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let (i,j) as sign = signature state.uf t in let (u,v) = subterms state.uf t in let rep = get_representative state.uf i in @@ -755,7 +752,7 @@ let process_constructor_mark t i rep pac state = let process_mark t m state = debug - (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str "."); + (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in match m with @@ -776,8 +773,8 @@ let check_disequalities state = else (str "No", check_aux q) in let _ = debug - (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++ - pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in + (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++ + pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in ans | [] -> None in @@ -806,7 +803,8 @@ let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in let id = Namegen.next_ident_away __eps__ ids in - state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env; + let r = Sorts.Relevant in (* TODO relevance *) + state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env; id let complete_one_class state i= @@ -814,9 +812,9 @@ let complete_one_class state i= Partial pac -> let rec app t typ n = if n<=0 then t else - let _,etyp,rest= destProd typ in + let _,etyp,rest= destProd typ in let id = new_state_var (EConstr.of_constr etyp) state in - app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in + app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in let _c = EConstr.Unsafe.to_constr _c in diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index d52e83dc31..978969bf59 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option -val pr_idx_term : forest -> int -> Pp.t +val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t val empty_forest: unit -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 1f1fa9c99a..4f46f8327a 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -94,65 +94,65 @@ let pinject p c n a = p_rhs=nth_arg p.p_rhs (n-a); p_rule=Inject(p,c,n,a)} -let rec equal_proof uf i j= - debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); +let rec equal_proof env sigma uf i j= + debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in - ptrans (path_proof uf i li) (psym (path_proof uf j lj)) + ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj)) -and edge_proof uf ((i,j),eq)= - debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); - let pi=equal_proof uf i eq.lhs in - let pj=psym (equal_proof uf j eq.rhs) in +and edge_proof env sigma uf ((i,j),eq)= + debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + let pi=equal_proof env sigma uf i eq.lhs in + let pj=psym (equal_proof env sigma uf j eq.rhs) in let pij= match eq.rule with Axiom (s,reversed)-> if reversed then psymax (axioms uf) s else pax (axioms uf) s - | Congruence ->congr_proof uf eq.lhs eq.rhs + | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) - let p=ind_proof uf ti ipac tj jpac in + let p=ind_proof env sigma uf ti ipac tj jpac in let cinfo= get_constructor_info uf ipac.cnode in pinject p cinfo.ci_constr cinfo.ci_nhyps k in ptrans (ptrans pi pij) pj -and constr_proof uf i ipac= - debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20)); +and constr_proof env sigma uf i ipac= + debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); let t=find_oldest_pac uf i ipac in - let eq_it=equal_proof uf i t in + let eq_it=equal_proof env sigma uf i t in if ipac.args=[] then eq_it else let fipac=tail_pac ipac in let (fi,arg)=subterms uf t in let targ=term uf arg in - let p=constr_proof uf fi fipac in + let p=constr_proof env sigma uf fi fipac in ptrans eq_it (pcongr p (prefl targ)) -and path_proof uf i l= - debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++ +and path_proof env sigma uf i l= + debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); match l with | [] -> prefl (term uf i) - | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x) + | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x) -and congr_proof uf i j= - debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); +and congr_proof env sigma uf i j= + debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in - pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2) + pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2) -and ind_proof uf i ipac j jpac= - debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); - let p=equal_proof uf i j - and p1=constr_proof uf i ipac - and p2=constr_proof uf j jpac in +and ind_proof env sigma uf i ipac j jpac= + debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + let p=equal_proof env sigma uf i j + and p1=constr_proof env sigma uf i ipac + and p2=constr_proof env sigma uf j jpac in ptrans (psym p1) (ptrans p p2) -let build_proof uf= +let build_proof env sigma uf= function - | `Prove (i,j) -> equal_proof uf i j - | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj + | `Prove (i,j) -> equal_proof env sigma uf i j + | `Discr (i,ci,j,cj)-> ind_proof env sigma uf i ci j cj diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index bebef241e1..9ea31259c1 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -41,20 +41,20 @@ val pinject : proof -> pconstructor -> int -> int -> proof (** Proof building functions *) -val equal_proof : forest -> int -> int -> proof +val equal_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof -val edge_proof : forest -> (int*int)*equality -> proof +val edge_proof : Environ.env -> Evd.evar_map -> forest -> (int*int)*equality -> proof -val path_proof : forest -> int -> ((int*int)*equality) list -> proof +val path_proof : Environ.env -> Evd.evar_map -> forest -> int -> ((int*int)*equality) list -> proof -val congr_proof : forest -> int -> int -> proof +val congr_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof -val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof +val ind_proof : Environ.env -> Evd.evar_map -> forest -> int -> pa_constructor -> int -> pa_constructor -> proof (** Main proof building function *) val build_proof : - forest -> + Environ.env -> Evd.evar_map -> forest -> [ `Discr of int * pa_constructor * int * pa_constructor | `Prove of int * int ] -> proof diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 055d36747d..50fc2448fc 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -15,6 +15,7 @@ open Names open Inductiveops open Declarations open Constr +open Context open EConstr open Vars open Tactics @@ -151,19 +152,19 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match EConstr.kind sigma (whd_delta env sigma term) with - Prod (id,atom,ff) -> + Prod (id,atom,ff) -> if is_global sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts let litteral_of_constr env sigma term= match EConstr.kind sigma (whd_delta env sigma term) with - | Prod (id,atom,ff) -> + | Prod (id,atom,ff) -> if is_global sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) @@ -171,7 +172,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -233,7 +234,7 @@ let build_projection intype (cstr:pconstructor) special default gls= let sigma = project gls in let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in - sigma, mkLambda(Name id,intype,body) + sigma, mkLambda(make_annot (Name id) Sorts.Relevant,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -318,7 +319,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of tx1) (fun typx -> refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in - let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in + let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = @@ -377,7 +378,7 @@ let convert_to_goal_tac c t1 t2 p = let neweq= app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in - let identity=mkLambda (Name x,sort,mkRel 1) in + let identity=mkLambda (make_annot (Name x) Sorts.Relevant,sort,mkRel 1) in let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] @@ -432,7 +433,7 @@ let cc_tactic depth additionnal_terms = debug (fun () -> Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> - let p=build_proof uf (`Discr (i,ipac,j,jpac)) in + let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> @@ -461,7 +462,8 @@ let cc_tactic depth additionnal_terms = Pp.str " replacing metavariables by arbitrary terms."); Tacticals.New.tclFAIL 0 (str "Incomplete") | Contradiction dis -> - let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in + let env = Proofview.Goal.env gl in + let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in let ta=term uf dis.lhs and tb=term uf dis.rhs in match dis.rule with Goal -> proof_tac p diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index d06a241969..afdbfa1999 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -9,6 +9,7 @@ (************************************************************************) open Constr +open Context open Context.Named.Declaration let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) @@ -39,7 +40,7 @@ let start_deriving f suchthat lemma = TCons ( env , sigma , f_type , (fun sigma ef -> let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b59e3b608c..0fa9be21c9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -150,7 +150,7 @@ let check_fix env sg cb i = | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = - Array.equal Name.equal na1 na2 && + Array.equal (Context.eq_annot Name.equal) na1 na2 && Array.equal (EConstr.eq_constr sg) ca1 ca2 && Array.equal (EConstr.eq_constr sg) ta1 ta2 diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 204f889f90..c9cfd74362 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -13,6 +13,7 @@ open Util open Names open Term open Constr +open Context open Declarations open Declareops open Environ @@ -73,13 +74,18 @@ type flag = info * scheme (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) +let info_of_family = function + | InSProp | InProp -> Logic + | InSet | InType -> Info + +let info_of_sort s = info_of_family (Sorts.family s) + let rec flag_of_type env sg t : flag = let t = whd_all env sg t in match EConstr.kind sg t with | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c - | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) - | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) + | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme) + | _ -> (info_of_family (sort_of env sg t),Default) (*s Two particular cases of [flag_of_type]. *) @@ -179,7 +185,7 @@ let rec type_sign_vl env sg c = | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in if not (is_info_scheme env sg t) then Kill Kprop::s, vl - else Keep::s, (make_typvar n vl) :: vl + else Keep::s, (make_typvar n.binder_name vl) :: vl | _ -> [],[] let rec nb_default_params env sg c = @@ -259,14 +265,14 @@ let rec extract_type env sg db j c args = (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> - (match args with + (match args with | [] -> assert false (* A lambda cannot be a type. *) | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args) | Prod (n,t,d) -> - assert (List.is_empty args); - let env' = push_rel_assum (n,t) env in + assert (List.is_empty args); + let env' = push_rel_assum (n,t) env in (match flag_of_type env sg t with - | (Info, Default) -> + | (Info, Default) -> (* Standard case: two [extract_type] ... *) let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with @@ -291,7 +297,7 @@ let rec extract_type env sg db j c args = (match EConstr.lookup_rel n env with | LocalDef (_,t,_) -> extract_type env sg db j (EConstr.Vars.lift n t) args - | _ -> + | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown else let n' = List.nth db (n-1) in @@ -492,8 +498,8 @@ and extract_really_ind env kn mib = (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with - | Prod(n,_,t) -> n::(names_prod t) - | LetIn(_,_,_,t) -> names_prod t + | Prod(n,_,t) -> n::(names_prod t) + | LetIn(_,_,_,t) -> names_prod t | Cast(t,_,_) -> names_prod t | _ -> [] in @@ -506,9 +512,9 @@ and extract_really_ind env kn mib = | [],[] -> [] | _::l, typ::typs when isTdummy (expand env typ) -> select_fields l typs - | Anonymous::l, typ::typs -> + | {binder_name=Anonymous}::l, typ::typs -> None :: (select_fields l typs) - | Name id::l, typ::typs -> + | {binder_name=Name id}::l, typ::typs -> let knp = Constant.make2 mp (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((==) Keep) (type2signature env typ) @@ -551,8 +557,8 @@ and extract_really_ind env kn mib = and extract_type_cons env sg db dbmap c i = match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let env' = push_rel_assum (n,t) env in - let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in + let env' = push_rel_assum (n,t) env in + let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in let l = extract_type_cons env' sg db' dbmap d (i+1) in (extract_type env sg db 0 t []) :: l | _ -> [] @@ -615,17 +621,18 @@ let rec extract_term env sg mle mlt c args = | App (f,a) -> extract_term env sg mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> - let id = id_of_name n in + let id = map_annot id_of_name n in + let idna = map_annot Name.mk_name id in (match args with | a :: l -> (* We make as many [LetIn] as possible. *) let l' = List.map (EConstr.Vars.lift 1) l in - let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in + let d' = EConstr.mkLetIn (idna,a,t,applistc d l') in extract_term env sg mle mlt d' [] - | [] -> - let env' = push_rel_assum (Name id, t) env in + | [] -> + let env' = push_rel_assum (idna, t) env in let id, a = - try check_default env sg t; Id id, new_meta() + try check_default env sg t; Id id.binder_name, new_meta() with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in @@ -634,9 +641,9 @@ let rec extract_term env sg mle mlt c args = let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> - let id = id_of_name n in - let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in - (* We directly push the args inside the [LetIn]. + let id = map_annot id_of_name n in + let env' = EConstr.push_rel (LocalDef (map_annot Name.mk_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 (EConstr.Vars.lift 1) args in (try @@ -649,7 +656,7 @@ let rec extract_term env sg mle mlt c args = then Mlenv.push_gen mle a else Mlenv.push_type mle a in - MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args') + MLletin (Id id.binder_name, c1', extract_term env' sg mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' sg mle' mlt c2 args')) @@ -913,7 +920,7 @@ and extract_fix env sg mle i (fi,ti,ci as recd) mlt = metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in - MLfix (i, Array.map id_of_name fi, ei) + MLfix (i, Array.map (fun x -> id_of_name x.binder_name) fi, ei) (*S ML declarations. *) @@ -989,7 +996,7 @@ let extract_std_constant env sg kn body typ = (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in (* The lambdas names. *) - let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in + let ids = List.map (fun (n,_) -> Id (id_of_name n.binder_name)) rels in (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) @@ -1044,7 +1051,9 @@ let fake_match_projection env p = let indu = mkIndU (ind,u) in let ctx, paramslet = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + let (ctx, cty) = mip.mind_nf_lc.(0) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in List.chop mip.mind_consnrealdecls.(0) rctx in let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in @@ -1053,12 +1062,15 @@ let fake_match_projection env p = ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; ci_cstr_nargs = mip.mind_consnrealargs; + ci_relevance = Declareops.relevance_of_projection_repr mib p; ci_pp_info; } in let x = match mib.mind_record with | NotRecord | FakeRecord -> assert false - | PrimRecord info -> Name (pi1 info.(snd ind)) + | PrimRecord info -> + let x, _, _, _ = info.(snd ind) in + make_annot (Name x) mip.mind_relevance in let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in let rec fold arg j subst = function @@ -1066,7 +1078,7 @@ let fake_match_projection env p = | LocalAssum (na,ty) :: rem -> let ty = Vars.substl subst (liftn 1 j ty) in if arg != proj_arg then - let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in + let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem else diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2058837b8e..399a77c596 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -449,11 +449,11 @@ let argnames_of_global r = let typ, _ = Typeops.type_of_global_in_context env r in let rels,_ = decompose_prod (Reduction.whd_all env typ) in - List.rev_map fst rels + List.rev_map (fun x -> Context.binder_name (fst x)) rels let msg_of_implicit = function | Kimplicit (r,i) -> - let name = match List.nth (argnames_of_global r) (i-1) with + let name = match (List.nth (argnames_of_global r) (i-1)) with | Anonymous -> "" | Name id -> "(" ^ Id.to_string id ^ ") " in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index a60a966cec..56b3dc97cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -13,7 +13,6 @@ open Names open Constr open EConstr open Vars -open Termops open Util open Declarations open Globnames @@ -100,9 +99,8 @@ let kind_of_formula env sigma term = else let has_realargs=(n>0) in let is_trivial= - let is_constant c = - Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - Array.exists is_constant mip.mind_nf_lc in + let is_constant n = Int.equal n 0 in + Array.exists is_constant mip.mind_consnrealargs in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 286021d68e..1c9ab2e3bd 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance env evmap id idc m t = (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd evmap (whd_all env evmap typ) in - match nam with + match nam.Context.binder_name with Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in @@ -115,7 +115,7 @@ let mk_open_instance env evmap id idc m t = if Int.equal n 0 then evmap, decls else let nid=(fresh_id_in_env avoid var_id env) in let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = LocalAssum (Name nid, c) in + let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m Id.Set.empty env evmap [] in (evmap, decls, revt) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 832a98b7f8..7f06ab6777 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -163,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in let open Vars in - let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc = mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in + let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b, + mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (cut c) [tclTHENLIST diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 5958fe8203..01b18e2f30 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -235,7 +235,7 @@ let print_cmap map= str "| " ++ prlist Printer.pr_global l ++ str " : " ++ - Ppconstr.pr_constr_expr xc ++ + Ppconstr.pr_constr_expr env sigma xc ++ cut () ++ s in (v 0 diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d63fe9d799..0c958ddee3 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -65,13 +65,13 @@ let unif evd t1 t2= bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige - | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> + | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; let l=Array.length va in - if not (Int.equal l (Array.length vb)) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..16f376931e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -2,6 +2,7 @@ open Printer open CErrors open Util open Constr +open Context open EConstr open Vars open Namegen @@ -44,10 +45,6 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) -let pr_leconstr_fp = - let sigma, env = Pfedit.get_current_context () in - Printer.pr_leconstr_env env sigma - let debug_queue = Stack.create () let rec print_debug_queue e = @@ -163,7 +160,7 @@ let rec incompatible_constructor_terms sigma t1 t2 = List.exists2 (incompatible_constructor_terms sigma) arg1 arg2 ) -let is_incompatible_eq sigma t = +let is_incompatible_eq env sigma t = let res = try match EConstr.kind sigma t with @@ -175,7 +172,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -238,7 +235,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; @@ -300,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let old_context_length = List.length context + 1 in let witness_fun = - mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t, + mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t, mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) ) in @@ -310,7 +309,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl, + witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -426,7 +426,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = else if isProd sigma type_of_hyp then begin - let (x,t_x,t') = destProd sigma type_of_hyp in + let (x,t_x,t') = destProd sigma type_of_hyp in let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property sigma ptes_infos t_x actual_real_type_of_hyp then begin @@ -476,7 +476,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (* ); *) raise TOREMOVE; (* False -> .. useless *) end - else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) + else if is_incompatible_eq env sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) else if eq_constr sigma t_x coq_True (* Trivial => we remove this precons *) then (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) @@ -539,7 +539,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with NoChange -> (* Last thing todo : push the rel in the context and continue *) - scan_type (LocalAssum (x,t_x) :: context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -608,7 +608,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = anomaly (Pp.str "cannot compute new term value.") in let fun_body = - mkLambda(Anonymous, + mkLambda(make_annot Anonymous Sorts.Relevant, pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) @@ -722,7 +722,7 @@ let build_proof (treat_new_case ptes_infos nb_instantiate_partial - (build_proof do_finalize) + (build_proof env sigma do_finalize) t dyn_infos) g' @@ -733,8 +733,8 @@ let build_proof ] g in - build_proof do_finalize_t {dyn_infos with info = t} g - | Lambda(n,t,b) -> + build_proof env sigma do_finalize_t {dyn_infos with info = t} g + | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with | Prod _ -> @@ -749,7 +749,7 @@ let build_proof in let new_infos = {dyn_infos with info = new_term} in let do_prove new_hyps = - build_proof do_finalize + build_proof env sigma do_finalize {new_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps @@ -762,7 +762,7 @@ let build_proof do_finalize dyn_infos g end | Cast(t,_,_) -> - build_proof do_finalize {dyn_infos with info = t} g + build_proof env sigma do_finalize {dyn_infos with info = t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> do_finalize dyn_infos g | App(_,_) -> @@ -778,7 +778,7 @@ let build_proof info = (f,args) } in - build_proof_args do_finalize new_infos g + build_proof_args env sigma do_finalize new_infos g | Const (c,_) when not (List.mem_f Constant.equal c fnames) -> let new_infos = { dyn_infos with @@ -786,13 +786,13 @@ let build_proof } in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) - build_proof_args do_finalize new_infos g + build_proof_args env sigma do_finalize new_infos g | Const _ -> do_finalize dyn_infos g | Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in - build_proof do_finalize {dyn_infos with info = new_term} + build_proof env sigma do_finalize {dyn_infos with info = new_term} g | LetIn _ -> let new_infos = @@ -805,11 +805,11 @@ let build_proof h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof do_finalize new_infos + build_proof env sigma do_finalize new_infos ] g | Cast(b,_,_) -> - build_proof do_finalize {dyn_infos with info = b } g + build_proof env sigma do_finalize {dyn_infos with info = b } g | Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = @@ -817,9 +817,9 @@ let build_proof info = dyn_infos.info,args } in - build_proof_args do_finalize new_infos + build_proof_args env sigma do_finalize new_infos in - build_proof new_finalize {dyn_infos with info = f } g + build_proof env sigma new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) @@ -839,13 +839,13 @@ let build_proof (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof do_finalize new_infos + build_proof env sigma do_finalize new_infos ] g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") - and build_proof do_finalize dyn_infos g = + and build_proof env sigma do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g - and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = + observe_tac_stream (str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + and build_proof_args env sigma do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in let tac : tactic = @@ -861,12 +861,12 @@ let build_proof let do_finalize dyn_infos = let new_arg = dyn_infos.info in (* tclTRYD *) - (build_proof_args + (build_proof_args env sigma do_finalize {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} ) in - build_proof do_finalize + build_proof env sigma do_finalize {dyn_infos with info = arg } g in @@ -878,7 +878,10 @@ let build_proof finish_proof dyn_infos) in (* observe_tac "build_proof" *) - (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) + fun g -> + let env = pf_env g in + let sigma = project g in + build_proof env sigma (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g @@ -1147,7 +1150,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let fix_offset = List.length princ_params in let ptes_to_fix,infos = match EConstr.kind (project g) fbody_with_full_params with - | Fix((idxs,i),(names,typess,bodies)) -> + | Fix((idxs,i),(names,typess,bodies)) -> let bodies_with_all_params = Array.map (fun body -> @@ -1162,7 +1165,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.Name.get_id (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i).binder_name); types = types; offset = fix_offset; nb_realargs = @@ -1193,9 +1196,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with - | Fix((_,num),(_,_,bs)) -> + | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) - ( + ( (applist (substl (List.rev @@ -1512,7 +1515,7 @@ let is_valid_hypothesis sigma predicates_name = let rec is_valid_hypothesis typ = is_pte typ || match EConstr.kind sigma typ with - | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' + | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' | _ -> false in is_valid_hypothesis @@ -1563,7 +1566,7 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id + | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index ca09cad1f3..1217ba0eba 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,7 @@ open Term open Sorts open Util open Constr +open Context open Vars open Namegen open Names @@ -72,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -137,14 +138,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Rel n -> begin try match Environ.lookup_rel n env with - | LocalAssum (_,t) | LocalDef (_,_,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 - | Prod(x,t,b) -> - compute_new_princ_type_for_binder remove mkProd env x t b - | Lambda(x,t,b) -> - compute_new_princ_type_for_binder remove mkLambda env x t b + | Prod(x,t,b) -> + compute_new_princ_type_for_binder remove mkProd env x t b + | Lambda(x,t,b) -> + compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> let var_to_be_removed = destRel (Array.last args) in @@ -164,8 +165,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in applistc new_f new_args, list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove - | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin remove env x v t b + | LetIn(x,v,t,b) -> + compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in (* let _ = match Constr.kind pre_princ with *) @@ -181,14 +182,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin 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 (LocalAssum (x,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x 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 (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - bind_fun(new_x,new_t,new_b), + bind_fun(new_x,new_t,new_b), list_union_eq Constr.equal binders_to_remove_from_t @@ -210,14 +211,14 @@ 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_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 (LocalDef (x,v,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x 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 (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - mkLetIn(new_x,new_v,new_t,new_b), + mkLetIn(new_x,new_v,new_t,new_b), list_union_eq Constr.equal (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) @@ -250,8 +251,11 @@ 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 (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)) + pre_res (List.map (function + | Context.Named.Declaration.LocalAssum (id,b) -> + LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b) + | Context.Named.Declaration.LocalDef (id,t,b) -> + LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b)) new_predicates) ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) @@ -264,7 +268,7 @@ let change_property_sort evd toSort princ princName = let princ_info = compute_elim_sig evd princ in let change_sort_in_predicate decl = LocalAssum - (get_name decl, + (get_annot decl, let args,ty = decompose_prod (EConstr.Unsafe.to_constr (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); @@ -414,7 +418,7 @@ let get_funs_constant mp = | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> - match na with + match na.binder_name with | Name id -> let const = Constant.make2 mp (Label.of_id id) in const,i @@ -451,7 +455,8 @@ let get_funs_constant mp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> + eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params) then user_err Pp.(str "Not a mutal recursive block") ) l_params @@ -461,7 +466,7 @@ let get_funs_constant mp = try let extract_info is_first body = match Constr.kind body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) + | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec @@ -469,9 +474,9 @@ let get_funs_constant mp = in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) - let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = - Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 + let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = + Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 && + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then user_err Pp.(str "Not a mutal recursive block") diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index c4f8843e51..6f67ab4d8b 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -29,10 +29,10 @@ DECLARE PLUGIN "recdef_plugin" { -let pr_fun_ind_using prc prlc _ opt_c = +let pr_fun_ind_using env sigma prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -47,15 +47,15 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = let env = Global.env () in let evd = Evd.from_env env in let (_, b) = b env evd in - spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) + spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) b) } ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option PRINTED BY { pr_fun_ind_using_typed } - RAW_PRINTED BY { pr_fun_ind_using } - GLOB_PRINTED BY { pr_fun_ind_using } + RAW_PRINTED BY { pr_fun_ind_using env sigma } + GLOB_PRINTED BY { pr_fun_ind_using env sigma } | [ "using" constr_with_bindings(c) ] -> { Some c } | [ ] -> { None } END @@ -119,26 +119,26 @@ END { -let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc +let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma) } ARGUMENT EXTEND constr_comma_sequence' TYPED AS constr list - PRINTED BY { pr_constr_comma_sequence } + PRINTED BY { pr_constr_comma_sequence env sigma } | [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l } | [ constr(c) ] -> { [c] } END { -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc +let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma) } ARGUMENT EXTEND auto_using' TYPED AS constr list - PRINTED BY { pr_auto_using } + PRINTED BY { pr_auto_using env sigma } | [ "using" constr_comma_sequence'(l) ] -> { l } | [ ] -> { [] } END @@ -170,7 +170,7 @@ END { let () = - let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in + let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer } diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ba0a3bbb5c..f4807954a7 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,6 +2,7 @@ open Printer open Pp open Names open Constr +open Context open Vars open Glob_term open Glob_ops @@ -343,20 +344,21 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let na = make_annot id Sorts.Relevant in (* TODO relevance *) (match raw_value with | None -> - EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env + EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env | Some value -> - EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) + EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env) -let add_pat_variables pat typ env : Environ.env = +let add_pat_variables sigma pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match DAst.get pat with - | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) @@ -373,18 +375,19 @@ let add_pat_variables pat typ env : Environ.env = Context.Rel.fold_outside (fun decl (env,ctxt) -> let open Context.Rel.Declaration in - let sigma, _ = Pfedit.get_current_context () in match decl with - | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false - | LocalAssum (Name id, t) -> + | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false + | LocalAssum ({binder_name=Name id} as na, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> + (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt) + | LocalDef ({binder_name=Name id} as na, v, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ @@ -394,7 +397,7 @@ let add_pat_variables pat typ env : Environ.env = str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -472,7 +475,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function *) -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = +let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with @@ -484,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) (fun arg ctxt_argsl -> - let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in + let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in combine_results combine_args arg_res ctxt_argsl ) args @@ -503,7 +506,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | _ -> GApp(t,l) in - build_entry_lc env funnames avoid (aux f args) + build_entry_lc env sigma funnames avoid (aux f args) | GVar id when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], @@ -567,7 +570,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in build_entry_lc env - funnames + sigma + funnames avoid (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> @@ -575,7 +579,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = we first compute the result from the case and then combine each of them with each of args one *) - let f_res = build_entry_lc env funnames args_res.to_avoid f in + let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in combine_results combine_app f_res args_res | GCast(b,_) -> (* for an applied cast we just trash the cast part @@ -583,7 +587,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = WARNING: We need to restart since [b] itself should be an application term *) - build_entry_lc env funnames avoid (mkGApp(b,args)) + build_entry_lc env sigma funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") | GInt _ -> user_err Pp.(str "Cannot apply an integer") @@ -595,14 +599,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the type and combine the two result *) - let t_res = build_entry_lc env funnames avoid t in + let t_res = build_entry_lc env sigma funnames avoid t in let new_n = match n with | Name _ -> n | Anonymous -> Name (Indfun_common.fresh_id [] "_x") in let new_env = raw_push_named (new_n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in + let b_res = build_entry_lc new_env sigma funnames avoid b in combine_results (combine_lam new_n) t_res b_res | GProd(n,_,t,b) -> (* we first compute the list of constructor @@ -610,9 +614,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the type and combine the two result *) - let t_res = build_entry_lc env funnames avoid t in + let t_res = build_entry_lc env sigma funnames avoid t in let new_env = raw_push_named (n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in + let b_res = build_entry_lc new_env sigma funnames avoid b in if List.length t_res.result = 1 && List.length b_res.result = 1 then combine_results (combine_prod2 n) t_res b_res else combine_results (combine_prod n) t_res b_res @@ -623,22 +627,23 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in - let v_res = build_entry_lc env funnames avoid v in + let v_res = build_entry_lc env sigma funnames avoid v in 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 v_r = Sorts.Relevant in (* TODO relevance *) let new_env = match n with Anonymous -> env - | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env - in - let b_res = build_entry_lc new_env funnames avoid b in + | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env + in + let b_res = build_entry_lc new_env sigma funnames avoid b in combine_results (combine_letin n) v_res b_res | GCases(_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in - build_entry_lc_from_case env funnames make_discr el brl avoid + build_entry_lc_from_case env sigma funnames make_discr el brl avoid | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in @@ -661,7 +666,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = mkGCases(None,[(b,(Anonymous,None))],brl) in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) - build_entry_lc env funnames avoid match_expr + build_entry_lc env sigma funnames avoid match_expr | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = @@ -685,13 +690,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Int.equal (Array.length case_pats) 1); let br = CAst.make ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in - build_entry_lc env funnames avoid match_expr + build_entry_lc env sigma funnames avoid match_expr end | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> - build_entry_lc env funnames avoid b -and build_entry_lc_from_case env funname make_discr + build_entry_lc env sigma funnames avoid b +and build_entry_lc_from_case env sigma funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : glob_constr build_entry_return = @@ -709,7 +714,7 @@ and build_entry_lc_from_case env funname make_discr let case_resl = List.fold_right (fun (case_arg,_) ctxt_argsl -> - let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in + let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in combine_results combine_args arg_res ctxt_argsl ) el @@ -726,7 +731,7 @@ and build_entry_lc_from_case env funname make_discr List.map (fun ca -> let res = build_entry_lc_from_case_term - env types + env sigma types funname (make_discr) [] brl case_resl.to_avoid @@ -743,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr [] results } -and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid +and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid matched_expr = match brl with | [] -> (* computed_branches *) {result = [];to_avoid = avoid} @@ -754,14 +759,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) *) - let new_env = List.fold_right2 add_pat_variables patl types env in + let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> let renamed_pat,_,_ = alpha_pat avoid pat in let pat_ids = get_pattern_id renamed_pat in - let env_with_pat_ids = add_pat_variables pat typ new_env in + let env_with_pat_ids = add_pat_variables sigma pat typ new_env in List.fold_right (fun id acc -> let typ_of_id = @@ -793,6 +798,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let brl'_res = build_entry_lc_from_case_term env + sigma types funname make_discr @@ -857,7 +863,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve ) in (* We compute the result of the value returned by the branch*) - let return_res = build_entry_lc new_env funname new_avoid return in + let return_res = build_entry_lc new_env sigma funname new_avoid return in (* and combine it with the preconds computed for this branch *) let this_branch_res = List.map @@ -890,8 +896,7 @@ let same_raw_term rt1 rt2 = | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2 | GHole _, GHole _ -> true | _ -> false -let decompose_raw_eq lhs rhs = - let _, env = Pfedit.get_current_context () in +let decompose_raw_eq env lhs rhs = let rec decompose_raw_eq lhs rhs acc = observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); let (rhd,lrhs) = glob_decompose_app rhs in @@ -939,9 +944,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in - let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -974,9 +980,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_args = List.map (replace_var_by_term id rt) args in let subst_b = if is_in_b then b else replace_var_by_term id rt b - in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1057,8 +1064,9 @@ 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 - EConstr.push_rel (LocalAssum (n,t')) env - in + let r = Sorts.Relevant in (* TODO relevance *) + EConstr.push_rel (LocalAssum (make_annot n r,t')) env + in let new_b,id_to_exclude = rebuild_cons new_env @@ -1078,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = -> begin try - let l = decompose_raw_eq rt1 rt2 in + let l = decompose_raw_eq env rt1 rt2 in if List.length l > 1 then let new_rt = @@ -1095,8 +1103,9 @@ 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_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1111,8 +1120,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1132,8 +1142,9 @@ 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 = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname (args@[mkGVar id])new_crossed_types @@ -1158,7 +1169,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let type_t' = Typing.unsafe_type_of env evd t' in let t' = EConstr.Unsafe.to_constr t' in let type_t' = EConstr.Unsafe.to_constr type_t' in - let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in + let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1182,8 +1193,9 @@ 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 = EConstr.push_rel (LocalAssum (na,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args (t::crossed_types) @@ -1320,7 +1332,7 @@ let do_build_inductive let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in let t = EConstr.Unsafe.to_constr t in evd, - Environ.push_named (LocalAssum (id,t)) + Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t)) env ) funnames @@ -1334,7 +1346,7 @@ let do_build_inductive resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt ) rta in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = @@ -1364,7 +1376,8 @@ let do_build_inductive Util.Array.fold_left2 (fun env rel_name rel_ar -> let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in let rex = EConstr.Unsafe.to_constr rex in - Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities + let r = Sorts.Relevant in (* TODO relevance *) + Environ.push_named (LocalAssum (make_annot rel_name r,rex)) 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 42dc66dcf4..b69ca7080c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -3,6 +3,7 @@ open Sorts open Util open Names open Constr +open Context open EConstr open Pp open Indfun_common @@ -49,7 +50,8 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction information on "++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - match Tacticals.elimination_sort_of_goal g with + match Tacticals.elimination_sort_of_goal g with + | InSProp -> finfo.sprop_lemma | InProp -> finfo.prop_lemma | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma @@ -169,7 +171,8 @@ let build_newrecursive let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in - (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) + let r = Sorts.Relevant in (* TODO relevance *) + (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) @@ -621,8 +624,8 @@ let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in - let constr_expr_typel = + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in + let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index cba3cc3d42..e34323abf4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -199,6 +199,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -249,6 +250,7 @@ let subst_Function (subst,finfos) = let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in + let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -256,7 +258,8 @@ let subst_Function (subst,finfos) = completeness_lemma' == finfos.completeness_lemma && rect_lemma' == finfos.rect_lemma && rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma + prop_lemma' == finfos.prop_lemma && + sprop_lemma' == finfos.sprop_lemma then finfos else { function_constant = function_constant'; @@ -267,17 +270,16 @@ let subst_Function (subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + sprop_lemma = sprop_lemma'; is_general = finfos.is_general } let discharge_Function (_,finfos) = Some finfos -let pr_ocst c = - let sigma, env = Pfedit.get_current_context () in +let pr_ocst env sigma c = Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) -let pr_info f_info = - let sigma, env = Pfedit.get_current_context () in +let pr_info env sigma f_info = str "function_constant := " ++ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ @@ -285,17 +287,17 @@ let pr_info f_info = Printer.pr_lconstr_env env sigma (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ - str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ - str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ - str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ - str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ - str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ - str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ + str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++ + str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++ + str "correctness_lemma := " ++ pr_ocst env sigma f_info.correctness_lemma ++ fnl () ++ + str "rect_lemma := " ++ pr_ocst env sigma f_info.rect_lemma ++ fnl () ++ + str "rec_lemma := " ++ pr_ocst env sigma f_info.rec_lemma ++ fnl () ++ + str "prop_lemma := " ++ pr_ocst env sigma f_info.prop_lemma ++ fnl () ++ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () -let pr_table tb = +let pr_table env sigma tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in - Pp.prlist_with_sep fnl pr_info l + Pp.prlist_with_sep fnl (pr_info env sigma) l let in_Function : function_info -> Libobject.obj = let open Libobject in @@ -333,6 +335,7 @@ let add_Function is_general f = and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect") and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec") and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") + and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") @@ -345,6 +348,7 @@ let add_Function is_general f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; + sprop_lemma = sprop_lemma; graph_ind = graph_ind; is_general = is_general @@ -352,7 +356,7 @@ let add_Function is_general f = in update_Function finfos -let pr_table () = pr_table !from_function +let pr_table env sigma = pr_table env sigma !from_function (*********************************) (* Debuging *) let functional_induction_rewrite_dependent_proofs = ref true diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 1e0b95df34..12facc5744 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -70,6 +70,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; } @@ -82,8 +83,8 @@ val update_Function : function_info -> unit (** debugging *) -val pr_info : function_info -> Pp.t -val pr_table : unit -> Pp.t +val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t +val pr_table : Environ.env -> Evd.evar_map -> Pp.t (* val function_debug : bool ref *) @@ -109,9 +110,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> - (Names.Name.t * EConstr.t) list * EConstr.t -val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t -val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t +val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t +val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t type tcc_lemma_value = | Undefined diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 95e2e9f6e5..37dbfec4c9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Constr +open Context open EConstr open Vars open Pp @@ -142,12 +143,13 @@ 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 = - LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt + LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) :: + LocalDef (make_annot (Name fv_id) Sorts.Relevant, 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 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 + then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -270,10 +272,10 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let type_of_hid = pf_unsafe_type_of g (mkVar hid) in let sigma = project g in match EConstr.kind sigma type_of_hid with - | Prod(_,_,t') -> + | Prod(_,_,t') -> begin match EConstr.kind sigma t' with - | Prod(_,t'',t''') -> + | Prod(_,t'',t''') -> begin match EConstr.kind sigma t'',EConstr.kind sigma t''' with | App(eq,args), App(graph',_) @@ -358,17 +360,16 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* end of branche proof *) let lemmas = Array.map - (fun ((_,(ctxt,concl))) -> - match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") - | hres::res::decl::ctxt -> - let res = EConstr.it_mkLambda_or_LetIn - (EConstr.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) - in - res - ) - lemmas_types_infos + (fun ((_,(ctxt,concl))) -> + match ctxt with + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") + | hres::res::decl::ctxt -> + let res = EConstr.it_mkLambda_or_LetIn + (EConstr.it_mkProd_or_LetIn concl [hres;res]) + (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt) + in + res) + lemmas_types_infos in let param_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in @@ -429,7 +430,7 @@ let generalize_dependent_of x hyp g = let open Context.Named.Declaration in tclMAP (function - | LocalAssum (id,t) when not (Id.equal id hyp) && + | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) @@ -456,7 +457,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = let eq_ind = make_eq () in let sigma = project g in match EConstr.kind sigma (pf_concl g) with - | Prod(_,t,t') -> + | Prod(_,t,t') -> begin match EConstr.kind sigma t with | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8746c37309..e19741a4e9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -12,6 +12,7 @@ module CVars = Vars open Constr +open Context open EConstr open Vars open Namegen @@ -57,10 +58,6 @@ let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] let arith_Lt = ["Coq"; "Arith";"Lt"] -let pr_leconstr_rd = - let sigma, env = Pfedit.get_current_context () in - Printer.pr_leconstr_env env sigma - let coq_init_constant s = EConstr.of_constr ( UnivGen.constr_of_monomorphic_global @@ @@ -182,7 +179,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = ) in let context = List.map - (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al)) + (fun (x, c) -> LocalAssum (make_annot (Name x) Sorts.Relevant, c)) (List.combine rev_x_id_l (List.rev al)) in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = @@ -302,7 +299,7 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = (* [check_not_nested forbidden e] checks that [e] does not contains any variable of [forbidden] *) -let check_not_nested sigma forbidden e = +let check_not_nested env sigma forbidden e = let rec check_not_nested e = match EConstr.kind sigma e with | Rel _ -> () @@ -329,7 +326,6 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - let _, env = Pfedit.get_current_context () in user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) @@ -388,9 +384,9 @@ let add_vars sigma forbidden e = let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = fun g -> let rev_context,b = decompose_lam_n (project g) nb_lam e in - let ids = List.fold_left (fun acc (na,_) -> + let ids = List.fold_left (fun acc (na,_) -> let pre_id = - match na with + match na.binder_name with | Name x -> x | Anonymous -> ano_id in @@ -433,10 +429,10 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") | Proj _ -> user_err Pp.(str "Function cannot treat projections") - | LetIn(na,b,t,e) -> + | LetIn(na,b,t,e) -> begin let new_continuation_tac = - jinfo.letiN (na,b,t,e) expr_info continuation_tac + jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac in travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} g @@ -445,15 +441,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | Prod _ -> begin try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end - | Lambda(n,t,b) -> + | Lambda(n,t,b) -> begin try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) @@ -506,10 +502,11 @@ and travel_args jinfo is_final continuation_tac infos = in travel jinfo new_continuation_tac {infos with info=arg;is_final=false} -and travel jinfo continuation_tac expr_info = - observe_tac - (str jinfo.message ++ pr_leconstr_rd expr_info.info) - (travel_aux jinfo continuation_tac expr_info) +and travel jinfo continuation_tac expr_info = + fun g -> + observe_tac + (str jinfo.message ++ Printer.pr_leconstr_env (pf_env g) (project g) expr_info.info) + (travel_aux jinfo continuation_tac expr_info) g (* Termination proof *) @@ -651,7 +648,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info g = let new_forbidden = let forbid = try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b; + check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) b; true with e when CErrors.noncritical e -> false in @@ -710,7 +707,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in let f_is_present = try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a; + check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) a; false with e when CErrors.noncritical e -> true @@ -739,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let terminate_app_rec (f,args) expr_info continuation_tac _ g = let sigma = project g in - List.iter (check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids)) + List.iter (check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids)) args; begin try @@ -853,8 +850,8 @@ let rec prove_le g = EConstr.is_global sigma (le ()) c | _ -> false in - let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) - in + let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in + let h = h.binder_name in let y = let _,args = decompose_app sigma t in List.hd (List.tl args) @@ -877,10 +874,10 @@ let rec make_rewrite_list expr_info max = function let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true @@ -903,10 +900,10 @@ let make_rewrite expr_info l hp max = let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences @@ -986,13 +983,19 @@ let rec intros_values_eq expr_info acc = )) let equation_others _ expr_info continuation_tac infos = + fun g -> + let env = pf_env g in + let sigma = project g in if expr_info.is_final && expr_info.is_main_branch - then - observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) + then + observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) + (fun g -> + let env = pf_env g in + let sigma = project g in + observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []) g)) g + else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) g let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1054,20 +1057,19 @@ let compute_terminate_type nb_args func = let right = mkRel 5 in let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in - let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in + let result = (mkProd (make_annot (Name def_id) Sorts.Relevant, lift 4 a_arrow_b, equality)) in let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in let nb_iter = mkApp(delayed_force ex, [|delayed_force nat; (mkLambda - (Name - p_id, + (make_annot (Name p_id) Sorts.Relevant, delayed_force nat, - (mkProd (Name k_id, delayed_force nat, - mkArrow cond result))))|])in + (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, + mkArrow cond Sorts.Relevant result))))|])in let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), [|b; - (mkLambda (Name v_id, b, nb_iter))|]) in + (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1165,15 +1167,15 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let func_body = EConstr.of_constr func_body in let (f_name, _, body1) = destLambda sigma func_body in let f_id = - match f_name with + match f_name.binder_name with | Name f_id -> next_ident_away_in_goal f_id ids | Anonymous -> anomaly (Pp.str "Anonymous function.") in let n_names_types,_ = decompose_lam_n sigma nb_args body1 in let n_ids,ids = List.fold_left - (fun (n_ids,ids) (n_name,_) -> - match n_name with + (fun (n_ids,ids) (n_name,_) -> + match n_name.binder_name with | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids @@ -1270,12 +1272,12 @@ let is_rec_res id = let clear_goals sigma = let rec clear_goal t = match EConstr.kind sigma t with - | Prod(Name id as na,t',b) -> + | Prod({binder_name=Name id} as na,t',b) -> let b' = clear_goal b in if noccurn sigma 1 b' && (is_rec_res id) then Vars.lift (-1) b' else if b' == b then t - else mkProd(na,t',b') + else mkProd(na,t',b') | _ -> EConstr.map sigma clear_goal t in List.map clear_goal @@ -1417,7 +1419,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evd, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in (* XXX *) Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook; @@ -1469,7 +1471,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evd, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in (* XXX *) let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in @@ -1519,7 +1521,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in - let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let function_r = Sorts.Relevant in (* TODO relevance *) + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot function_name function_r,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in @@ -1537,7 +1540,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> - mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) + mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars eq_fix)) | _ -> failwith "Recursive Definition (res not eq)" in let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index b0277e9cc2..050fdcb608 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -11,6 +11,7 @@ open Util open Names open Constr +open Context open CErrors open Evar_refiner open Tacmach @@ -62,7 +63,7 @@ let instantiate_tac n c ido = evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with - | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) + | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) | _ -> user_err Pp.(str "Not a defined hypothesis.")) in if List.length evl < n then user_err Pp.(str "Not enough uninstantiated existential variables."); @@ -108,5 +109,6 @@ let hget_evar n = if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in - Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl)) + let r = Retyping.relevance_of_type (Proofview.Goal.env gl) sigma ev_type in + Tactics.change_concl (mkLetIn (make_annot Name.Anonymous r,mkEvar ev,ev_type,concl)) end diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 5d5d45c58f..eb9cacb975 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -145,31 +145,30 @@ END let pr_occurrences = pr_occurrences () () () -let pr_gen prc _prlc _prtac c = prc c +let pr_gen env sigma prc _prlc _prtac x = prc env sigma x -let pr_globc _prc _prlc _prtac (_,glob) = - let _, env = Pfedit.get_current_context () in +let pr_globc env sigma _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) let glob_glob = Tacintern.intern_constr -let pr_lconstr _ prc _ c = prc c +let pr_lconstr env sigma _ prc _ c = prc env sigma c let subst_glob = Tacsubst.subst_glob_constr_and_expr } ARGUMENT EXTEND glob - PRINTED BY { pr_globc } + PRINTED BY { pr_globc env sigma } INTERPRETED BY { interp_glob } GLOBALIZED BY { glob_glob } SUBSTITUTED BY { subst_glob } - RAW_PRINTED BY { pr_gen } - GLOB_PRINTED BY { pr_gen } + RAW_PRINTED BY { pr_gen env sigma } + GLOB_PRINTED BY { pr_gen env sigma } | [ constr(c) ] -> { c } END @@ -181,20 +180,20 @@ let l_constr = Pcoq.Constr.lconstr ARGUMENT EXTEND lconstr TYPED AS constr - PRINTED BY { pr_lconstr } + PRINTED BY { pr_lconstr env sigma } | [ l_constr(c) ] -> { c } END ARGUMENT EXTEND lglob TYPED AS glob - PRINTED BY { pr_globc } + PRINTED BY { pr_globc env sigma } INTERPRETED BY { interp_glob } GLOBALIZED BY { glob_glob } SUBSTITUTED BY { subst_glob } - RAW_PRINTED BY { pr_gen } - GLOB_PRINTED BY { pr_gen } + RAW_PRINTED BY { pr_gen env sigma } + GLOB_PRINTED BY { pr_gen env sigma } | [ lconstr(c) ] -> { c } END @@ -207,7 +206,7 @@ let interp_casted_constr ist gl c = ARGUMENT EXTEND casted_constr TYPED AS constr - PRINTED BY { pr_gen } + PRINTED BY { pr_gen env sigma } INTERPRETED BY { interp_casted_constr } | [ constr(c) ] -> { c } END @@ -296,23 +295,23 @@ END { -let pr_by_arg_tac _prc _prlc prtac opt_c = +let pr_by_arg_tac env sigma _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t) } ARGUMENT EXTEND by_arg_tac TYPED AS tactic option - PRINTED BY { pr_by_arg_tac } + PRINTED BY { pr_by_arg_tac env sigma } | [ "by" tactic3(c) ] -> { Some c } | [ ] -> { None } END { -let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c +let pr_by_arg_tac env sigma prtac opt_c = pr_by_arg_tac env sigma () () prtac opt_c let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 0509d6ae71..7f9eecbef5 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -65,8 +65,9 @@ val wit_by_arg_tac : glob_tactic_expr option, Geninterp.Val.t option) Genarg.genarg_type -val pr_by_arg_tac : - (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> +val pr_by_arg_tac : + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ffd8b71e5d..0428f08138 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -12,6 +12,7 @@ open Pp open Constr +open Context open Genarg open Stdarg open Tacarg @@ -674,7 +675,7 @@ let hResolve id c occ t = let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) + (change_concl (mkLetIn (make_annot Name.Anonymous Sorts.Relevant,t_constr,t_constr_type,concl))) end let hResolve_auto id c t = diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 663537f3e8..3a4b0571d4 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -62,21 +62,19 @@ let eval_uconstrs ist cs = let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs -let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> - let _, env = Pfedit.get_current_context () in +let pr_auto_using_raw env sigma _ _ _ = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma +let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr_env env c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using - (let sigma, env = Pfedit.get_current_context () in - Printer.pr_closed_glob_env env sigma) +let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@ + Printer.pr_closed_glob_env env sigma } ARGUMENT EXTEND auto_using TYPED AS uconstr list - PRINTED BY { pr_auto_using } - RAW_PRINTED BY { pr_auto_using_raw } - GLOB_PRINTED BY { pr_auto_using_glob } + PRINTED BY { pr_auto_using env sigma } + RAW_PRINTED BY { pr_auto_using_raw env sigma } + GLOB_PRINTED BY { pr_auto_using_glob env sigma } | [ "using" ne_uconstr_list_sep(l, ",") ] -> { l } | [ ] -> { [] } END diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 9ecc36bdf3..3f2fabeeee 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -99,8 +99,19 @@ TACTIC EXTEND is_ground | [ "is_ground" constr(ty) ] -> { is_ground ty } END +{ +let deprecated_autoapply_using = + CWarnings.create + ~name:"autoapply-using" ~category:"deprecated" + (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.") +} + TACTIC EXTEND autoapply -| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +| [ "autoapply" constr(c) "using" preident(i) ] -> { + deprecated_autoapply_using (); + autoapply c i + } +| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i } END { diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 4c24f51b1e..a348e2cea4 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -514,7 +514,7 @@ END let pr_ltac_ref = Libnames.pr_qualid -let pr_tacdef_body tacdef_body = +let pr_tacdef_body env sigma tacdef_body = let id, redef, body = match tacdef_body with | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body @@ -528,12 +528,12 @@ let pr_tacdef_body tacdef_body = prlist (function Name.Anonymous -> str " _" | Name.Name id -> spc () ++ Id.print id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) - ++ Pptactic.pr_raw_tactic body + ++ Pptactic.pr_raw_tactic env sigma body } VERNAC ARGUMENT EXTEND ltac_tacdef_body -PRINTED BY { pr_tacdef_body } +PRINTED BY { pr_tacdef_body env sigma } | [ tacdef_body(t) ] -> { t } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index cdee012a82..a12dee48a8 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -162,9 +162,9 @@ END (* Declare a printer for the content of Program tactics *) let () = - let printer _ _ _ = function + let printer env sigma _ _ _ = function | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic env sigma tac in Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index db8d1b20d8..86a227415a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -41,13 +41,11 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = - let _, env = Pfedit.get_current_context () in +let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr_env env (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = - let _, env = Pfedit.get_current_context () in +let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr_env env (fst (fst ge)) -let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) +let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l let subst_glob_constr_with_bindings s c = @@ -56,14 +54,14 @@ let subst_glob_constr_with_bindings s c = } ARGUMENT EXTEND glob_constr_with_bindings - PRINTED BY { pr_glob_constr_with_bindings_sign } + PRINTED BY { pr_glob_constr_with_bindings_sign env sigma } INTERPRETED BY { interp_glob_constr_with_bindings } GLOBALIZED BY { glob_glob_constr_with_bindings } SUBSTITUTED BY { subst_glob_constr_with_bindings } - RAW_PRINTED BY { pr_constr_expr_with_bindings } - GLOB_PRINTED BY { pr_glob_constr_with_bindings } + RAW_PRINTED BY { pr_constr_expr_with_bindings env sigma } + GLOB_PRINTED BY { pr_glob_constr_with_bindings env sigma } | [ constr_with_bindings(bl) ] -> { bl } END @@ -80,17 +78,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" -let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in - Rewrite.pr_strategy prc prr s -let pr_glob_strategy prc prlc _ (s : glob_strategy) = - let prr = Pptactic.pr_red_expr +let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) = + let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in + Rewrite.pr_strategy (prc env sigma) prr s +let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) = + let prr = Pptactic.pr_red_expr env sigma (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in - Rewrite.pr_strategy prc prr s + Rewrite.pr_strategy (prc env sigma) prr s } @@ -101,8 +99,8 @@ ARGUMENT EXTEND rewstrategy GLOBALIZED BY { glob_strategy } SUBSTITUTED BY { subst_strategy } - RAW_PRINTED BY { pr_raw_strategy } - GLOB_PRINTED BY { pr_glob_strategy } + RAW_PRINTED BY { pr_raw_strategy env sigma } + GLOB_PRINTED BY { pr_glob_strategy env sigma } | [ glob(c) ] -> { StratConstr (c, true) } | [ "<-" constr(c) ] -> { StratConstr (c, false) } @@ -224,7 +222,7 @@ let wit_binders = let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) let () = - let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in + let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer } diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 5e3f4df192..1bdba699f7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -71,40 +71,46 @@ let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab type 'a raw_extra_genarg_printer = - (constr_expr -> Pp.t) -> - (constr_expr -> Pp.t) -> - (tolerability -> raw_tactic_expr -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> Pp.t) -> - (glob_constr_and_expr -> Pp.t) -> - (tolerability -> glob_tactic_expr -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.constr -> Pp.t) -> - (EConstr.constr -> Pp.t) -> - (tolerability -> Val.t -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = - (constr_expr -> Pp.t) -> - (constr_expr -> Pp.t) -> - (tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = - (glob_constr_and_expr -> Pp.t) -> - (glob_constr_and_expr -> Pp.t) -> - (tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = - (EConstr.constr -> Pp.t) -> - (EConstr.constr -> Pp.t) -> - (tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function @@ -160,27 +166,27 @@ let string_of_genarg_arg (ArgumentType arg) = | _ -> default let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c - let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c + let pr_red_expr env sigma pr c = Ppred.pr_red_expr_env env sigma pr keyword c - let pr_may_eval test prc prlc pr2 pr3 = function + let pr_may_eval env sigma test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> hov 0 (keyword "eval" ++ brk (1,1) ++ - pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ - keyword "in" ++ spc() ++ prc c) + pr_red_expr env sigma (prc,prlc,pr2,pr3) r ++ spc () ++ + keyword "in" ++ spc() ++ prc env sigma c) | ConstrContext ({CAst.v=id},c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ - str "[ " ++ prlc c ++ str " ]") + str "[ " ++ prlc env sigma c ++ str " ]") | ConstrTypeOf c -> - hov 1 (keyword "type of" ++ spc() ++ prc c) + hov 1 (keyword "type of" ++ spc() ++ prc env sigma c) | ConstrTerm c when test c -> - h 0 (str "(" ++ prc c ++ str ")") + h 0 (str "(" ++ prc env sigma c ++ str ")") | ConstrTerm c -> - prc c + prc env sigma c - let pr_may_eval a = - pr_may_eval (fun _ -> false) a + let pr_may_eval env sigma a = + pr_may_eval env sigma (fun _ -> false) a let pr_arg pr x = spc () ++ pr x @@ -647,15 +653,15 @@ let pr_goal_selector ~toplevel s = type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> Pp.t; - pr_constr : 'trm -> Pp.t; - pr_lconstr : 'trm -> Pp.t; - pr_dconstr : 'dtrm -> Pp.t; - pr_pattern : 'pat -> Pp.t; - pr_lpattern : 'pat -> Pp.t; + pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; + pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; + pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t; + pr_pattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t; + pr_lpattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t; pr_constant : 'cst -> Pp.t; pr_reference : 'ref -> Pp.t; pr_name : 'nam -> Pp.t; - pr_generic : 'lev generic_argument -> Pp.t; + pr_generic : Environ.env -> Evd.evar_map -> 'lev generic_argument -> Pp.t; pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t; pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t; } @@ -671,14 +677,14 @@ let pr_goal_selector ~toplevel s = level :'lev > - let pr_atom pr strip_prod_binders tag_atom = - let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in + let pr_atom env sigma pr strip_prod_binders tag_atom = + let pr_with_bindings = pr_with_bindings (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in let pr_with_bindings_arg_full = pr_with_bindings_arg in - let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in - let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in + let pr_with_bindings_arg = pr_with_bindings_arg (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in + let pr_red_expr = pr_red_expr env sigma (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in - let _pr_constrarg c = spc () ++ pr.pr_constr c in - let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in + let _pr_constrarg c = spc () ++ pr.pr_constr env sigma c in + let pr_lconstrarg c = spc () ++ pr.pr_lconstr env sigma c in let pr_intarg n = spc () ++ int n in (* Some printing combinators *) @@ -688,7 +694,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr env sigma t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -723,7 +729,7 @@ let pr_goal_selector ~toplevel s = in hov 1 (str"(" ++ pr_id id ++ prlist pr_binder_fix bll ++ annot ++ str" :" ++ - pr_lconstrarg ty ++ str")") in + (pr_lconstrarg ty) ++ str")") in (* spc() ++ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg c) @@ -747,13 +753,13 @@ let pr_goal_selector ~toplevel s = hov 1 (primitive (if ev then "eintros" else "intros") ++ (match p with | [{CAst.v=IntroForthcoming false}] -> mt () - | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern @@ pr.pr_dconstr env sigma) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ primitive (with_evars ev "apply") ++ spc () ++ prlist_with_sep pr_comma pr_with_bindings_arg cb ++ - pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp + pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp ) | TacElim (ev,cb,cbo) -> hov 1 ( @@ -774,28 +780,28 @@ let pr_goal_selector ~toplevel s = | TacAssert (ev,b,Some tac,ipat,c) -> hov 1 ( primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ - pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ + pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) | TacAssert (ev,_,None,ipat,c) -> hov 1 ( primitive (if ev then "epose proof" else "pose proof") - ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c + ++ pr_assertion (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ) | TacGeneralize l -> hov 1 ( primitive "generalize" ++ spc () ++ prlist_with_sep pr_comma (fun (cl,na) -> - pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) + pr_with_occurrences (pr.pr_constr env sigma) cl ++ pr_as_name na) l ) | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c) | TacLetTac (ev,na,c,cl,b,e) -> hov 1 ( primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++ - (if b then pr_pose pr.pr_constr pr.pr_lconstr na c - else pr_pose_as_style pr.pr_constr na c) ++ + (if b then pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c + else pr_pose_as_style (pr.pr_constr env sigma) na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl) (* | TacInstantiate (n,c,ConclLocation ()) -> @@ -815,8 +821,8 @@ let pr_goal_selector ~toplevel s = primitive (with_evars ev (if isrec then "induction" else "destruct")) ++ spc () ++ prlist_with_sep pr_comma (fun (h,ids,cl) -> - pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++ - pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++ + pr_destruction_arg (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) h ++ + pr_non_empty_arg (pr_with_induction_names (pr.pr_dconstr env sigma)) ids ++ pr_opt (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) @@ -835,9 +841,9 @@ let pr_goal_selector ~toplevel s = None -> mt () | Some p -> - pr.pr_pattern p ++ spc () + pr.pr_pattern env sigma p ++ spc () ++ keyword "with" ++ spc () - ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h + ) ++ pr.pr_dconstr env sigma c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) (* Equality and inversion *) @@ -848,7 +854,7 @@ let pr_goal_selector ~toplevel s = (fun () -> str ","++spc()) (fun (b,m,c) -> pr_orient b ++ pr_multi m ++ - pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) + pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac @@ -857,28 +863,28 @@ let pr_goal_selector ~toplevel s = hov 1 ( primitive "dependent " ++ pr_inversion_kind k ++ spc () ++ pr_quantified_hypothesis hyp - ++ pr_with_inversion_names pr.pr_dconstr ids - ++ pr_with_constr pr.pr_constr c + ++ pr_with_inversion_names (pr.pr_dconstr env sigma) ids + ++ pr_with_constr (pr.pr_constr env sigma) c ) | TacInversion (NonDepInversion (k,cl,ids),hyp) -> hov 1 ( pr_inversion_kind k ++ spc () ++ pr_quantified_hypothesis hyp - ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids + ++ pr_non_empty_arg (pr_with_inversion_names @@ pr.pr_dconstr env sigma) ids ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl ) | TacInversion (InversionUsing (c,cl),hyp) -> hov 1 ( primitive "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ spc () - ++ keyword "using" ++ spc () ++ pr.pr_constr c + ++ keyword "using" ++ spc () ++ pr.pr_constr env sigma c ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl ) ) in pr_atom1 - let make_pr_tac pr strip_prod_binders tag_atom tag = + let make_pr_tac env sigma pr strip_prod_binders tag_atom tag = let extract_binders = function | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) @@ -898,7 +904,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc + pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -908,7 +914,7 @@ let pr_goal_selector ~toplevel s = ++ pr_tac ltop t ++ spc () ++ keyword "with" ++ prlist (fun r -> fnl () ++ str "| " - ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r + ++ pr_match_rule true (pr_tac ltop) (pr.pr_lpattern env sigma) r ) lrul ++ fnl() ++ keyword "end"), lmatch @@ -918,7 +924,7 @@ let pr_goal_selector ~toplevel s = ++ keyword (if lr then "match reverse goal with" else "match goal with") ++ prlist (fun r -> fnl () ++ str "| " - ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r + ++ pr_match_rule false (pr_tac ltop) (pr.pr_lpattern env sigma) r ) lrul ++ fnl() ++ keyword "end"), lmatch | TacFun (lvar,body) -> @@ -1041,17 +1047,17 @@ let pr_goal_selector ~toplevel s = | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom { CAst.loc; v=t } -> - pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom + pr_with_comments ?loc (hov 1 (pr_atom env sigma pr strip_prod_binders tag_atom t)), ltatom | TacArg { CAst.v=Tacexp e } -> pr_tac inherited e, latom | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } -> - keyword "constr:" ++ pr.pr_constr c, latom + keyword "constr:" ++ pr.pr_constr env sigma c, latom | TacArg { CAst.v=ConstrMayEval c } -> - pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval + pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval | TacArg { CAst.v=TacFreshId l } -> primitive "fresh" ++ pr_fresh_ids l, latom | TacArg { CAst.v=TacGeneric arg } -> - pr.pr_generic arg, latom + pr.pr_generic env sigma arg, latom | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } -> pr.pr_reference f, latom | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } -> @@ -1074,11 +1080,11 @@ let pr_goal_selector ~toplevel s = | Reference r -> pr.pr_reference r | ConstrMayEval c -> - pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c + pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c | TacFreshId l -> keyword "fresh" ++ pr_fresh_ids l | TacPretype c -> - keyword "type_term" ++ pr.pr_constr c + keyword "type_term" ++ pr.pr_constr env sigma c | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> @@ -1098,9 +1104,9 @@ let pr_goal_selector ~toplevel s = let raw_printers = (strip_prod_binders_expr) - let rec pr_raw_tactic_level n (t:raw_tactic_expr) = + let rec pr_raw_tactic_level env sigma n (t:raw_tactic_expr) = let pr = { - pr_tactic = pr_raw_tactic_level; + pr_tactic = pr_raw_tactic_level env sigma; pr_constr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; @@ -1109,16 +1115,16 @@ let pr_goal_selector ~toplevel s = pr_constant = pr_or_by_notation pr_qualid; pr_reference = pr_qualid; pr_name = pr_lident; - pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); - pr_extend = pr_raw_extend_rec pr_raw_tactic_level; - pr_alias = pr_raw_alias pr_raw_tactic_level; + pr_generic = Pputils.pr_raw_generic; + pr_extend = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma; + pr_alias = pr_raw_alias @@ pr_raw_tactic_level env sigma; } in - make_pr_tac + make_pr_tac env sigma pr raw_printers tag_raw_atomic_tactic_expr tag_raw_tactic_expr n t - let pr_raw_tactic = pr_raw_tactic_level ltop + let pr_raw_tactic env sigma = pr_raw_tactic_level env sigma ltop let pr_and_constr_expr pr (c,_) = pr c @@ -1131,19 +1137,19 @@ let pr_goal_selector ~toplevel s = let rec prtac n (t:glob_tactic_expr) = let pr = { pr_tactic = prtac; - pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); - pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); - pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); - pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); + pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); + pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)); + pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env)); pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; - pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg); + pr_generic = Pputils.pr_glb_generic; pr_extend = pr_glob_extend_rec prtac; pr_alias = pr_glob_alias prtac; } in - make_pr_tac + make_pr_tac env (Evd.from_env env) pr glob_printers tag_glob_atomic_tactic_expr tag_glob_tactic_expr n t @@ -1158,7 +1164,7 @@ let pr_goal_selector ~toplevel s = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Constr.kind ty with | Constr.Prod(na,a,b) -> - strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([CAst.make na.Context.binder_name],EConstr.of_constr a)::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1166,11 +1172,11 @@ let pr_goal_selector ~toplevel s = let prtac (t:atomic_tactic_expr) = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); - pr_constr = (fun c -> pr_econstr_env env sigma c); - pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); - pr_lconstr = (fun c -> pr_leconstr_env env sigma c); - pr_pattern = pr_constr_pattern_env env sigma; - pr_lpattern = pr_lconstr_pattern_env env sigma; + pr_constr = pr_econstr_env; + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); + pr_lconstr = pr_leconstr_env; + pr_pattern = pr_constr_pattern_env; + pr_lpattern = pr_lconstr_pattern_env; pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; @@ -1180,7 +1186,7 @@ let pr_goal_selector ~toplevel s = pr_alias = (fun _ _ _ -> assert false); } in - pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t + pr_atom env sigma pr strip_prod_binders_constr tag_atomic_tactic_expr t in prtac t @@ -1188,9 +1194,9 @@ let pr_goal_selector ~toplevel s = let pr_glb_generic = Pputils.pr_glb_generic - let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level + let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma - let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env) + let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env) let pr_alias pr lev key args = pr_alias_gen (fun _ arg -> pr arg) lev key args @@ -1209,16 +1215,17 @@ let declare_extra_genarg_pprule wit | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = - Genprint.PrinterBasic (fun () -> - f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in + Genprint.PrinterBasic (fun env sigma -> + f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = - Genprint.PrinterBasic (fun () -> - let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) + Genprint.PrinterBasic (fun env sigma -> + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + (fun env sigma -> pr_glob_tactic_level env) x) in let h x = Genprint.TopPrinterNeedsContext (fun env sigma -> - h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) + h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h @@ -1235,27 +1242,28 @@ let declare_extra_genarg_pprule_with_level wit PrinterNeedsLevel { default_already_surrounded = default_surrounded; default_ensure_surrounded = default_non_surrounded; - printer = (fun n -> - f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + printer = (fun env sigma n -> + f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in let g x = - let env = Global.env () in PrinterNeedsLevel { default_already_surrounded = default_surrounded; default_ensure_surrounded = default_non_surrounded; - printer = (fun n -> - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + printer = (fun env sigma n -> + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + (fun env sigma -> pr_glob_tactic_level env) n x) } in let h x = TopPrinterNeedsContextAndLevel { default_already_surrounded = default_surrounded; default_ensure_surrounded = default_non_surrounded; printer = (fun env sigma n -> - h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") n x) } in Genprint.register_print0 wit f g h let declare_extra_vernac_genarg_pprule wit f = - let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in + let f x = Genprint.PrinterBasic (fun env sigma -> f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) @@ -1265,8 +1273,8 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> Miscprint.pr_intro_pattern print_constr p) let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> - pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, - pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) + pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env, + pr_evaluable_reference_env env, pr_constr_pattern_env) r) let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in @@ -1292,19 +1300,18 @@ let make_constr_printer f c = Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} -let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift f a = Genprint.PrinterBasic (fun env sigma -> f a) +let lift_env f a = Genprint.PrinterBasic (fun env sigma -> f env sigma a) let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) -let pr_glob_constr_pptac c = - let _, env = Pfedit.get_current_context () in +let pr_glob_constr_pptac env sigma c = pr_glob_constr_env env c -let pr_lglob_constr_pptac c = - let _, env = Pfedit.get_current_context () in +let pr_lglob_constr_pptac env sigma c = pr_lglob_constr_env env c let () = @@ -1318,8 +1325,8 @@ let () = register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intro_pattern - (lift (Miscprint.pr_intro_pattern pr_constr_expr)) - (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) + (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)) + (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl @@ -1329,47 +1336,55 @@ let () = ; Genprint.register_print0 wit_constr - (lift Ppconstr.pr_lconstr_expr) - (lift (fun (c, _) -> pr_lglob_constr_pptac c)) + (lift_env Ppconstr.pr_lconstr_expr) + (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - (lift Ppconstr.pr_constr_expr) - (lift (fun (c,_) -> pr_glob_constr_pptac c)) + (lift_env Ppconstr.pr_constr_expr) + (lift_env (fun env sigma (c,_) -> pr_glob_constr_pptac env sigma c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - (lift Ppconstr.pr_constr_expr) - (lift (fun (c, _) -> pr_glob_constr_pptac c)) + (lift_env Ppconstr.pr_constr_expr) + (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr - (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) - (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) + (lift_env (fun env sigma -> pr_red_expr env sigma (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) + (lift_env (fun env sigma -> pr_red_expr env sigma + ((fun env sigma -> pr_and_constr_expr @@ pr_glob_constr_pptac env sigma), + (fun env sigma -> pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma), + pr_or_var (pr_and_short_name pr_evaluable_reference), + (fun env sigma -> pr_pat_and_constr_expr @@ pr_glob_constr_pptac env sigma)))) pr_red_expr_env ; register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; register_print0 wit_bindings - (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) - (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_constr_expr env sigma) + (pr_lconstr_expr env sigma))) + (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma))) pr_bindings_env ; register_print0 wit_constr_with_bindings - (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) - (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma))) + (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) + (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma))) pr_with_bindings_env ; register_print0 wit_open_constr_with_bindings - (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) - (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma))) + (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) + (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma))) pr_with_bindings_env ; register_print0 Tacarg.wit_destruction_arg - (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) - (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + (lift_env (fun env sigma -> pr_destruction_arg (pr_constr_expr env sigma) (pr_lconstr_expr env sigma))) + (lift_env (fun env sigma -> pr_destruction_arg (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) + (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma))) pr_destruction_arg_env ; register_basic_print0 Stdarg.wit_int int int int; @@ -1379,12 +1394,12 @@ let () = register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac in + let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_tactic printer printer printer ltop (0,E) let () = - let pr_unit _ _ _ _ () = str "()" in - let printer _ _ prtac = prtac in + let pr_unit _env _sigma _ _ _ _ () = str "()" in + let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index bc47036d92..70af09833d 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -26,40 +26,46 @@ type 'a grammar_tactic_prod_item_expr = | TacNonTerm of ('a * Names.Id.t option) Loc.located type 'a raw_extra_genarg_printer = - (constr_expr -> Pp.t) -> - (constr_expr -> Pp.t) -> - (tolerability -> raw_tactic_expr -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> Pp.t) -> - (glob_constr_and_expr -> Pp.t) -> - (tolerability -> glob_tactic_expr -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.t -> Pp.t) -> - (EConstr.t -> Pp.t) -> - (tolerability -> Val.t -> Pp.t) -> - 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = - (constr_expr -> Pp.t) -> - (constr_expr -> Pp.t) -> - (tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = - (glob_constr_and_expr -> Pp.t) -> - (glob_constr_and_expr -> Pp.t) -> - (tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = - (EConstr.constr -> Pp.t) -> - (EConstr.constr -> Pp.t) -> - (tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -91,12 +97,13 @@ val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t -val pr_red_expr : - ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> +val pr_red_expr : env -> Evd.evar_map -> + (env -> Evd.evar_map -> 'a -> Pp.t) * (env -> Evd.evar_map -> 'a -> Pp.t) * ('b -> Pp.t) * (env -> Evd.evar_map -> 'c -> Pp.t) -> ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t val pr_may_eval : - ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> - ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t + env -> Evd.evar_map -> + (env -> Evd.evar_map -> 'a -> Pp.t) -> (env -> Evd.evar_map -> 'a -> Pp.t) -> ('b -> Pp.t) -> + (env -> Evd.evar_map -> 'c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t @@ -111,14 +118,14 @@ val pr_clauses : (* default: *) bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t (* Some true = default is concl; Some false = default is all; None = no default *) -val pr_raw_generic : env -> rlevel generic_argument -> Pp.t +val pr_raw_generic : env -> Evd.evar_map -> rlevel generic_argument -> Pp.t -val pr_glb_generic : env -> glevel generic_argument -> Pp.t +val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t -val pr_raw_extend: env -> int -> +val pr_raw_extend: env -> Evd.evar_map -> int -> ml_tactic_entry -> raw_tactic_arg list -> Pp.t -val pr_glob_extend: env -> int -> +val pr_glob_extend: env -> Evd.evar_map -> int -> ml_tactic_entry -> glob_tactic_arg list -> Pp.t val pr_extend : @@ -131,9 +138,9 @@ val pr_alias : (Val.t -> Pp.t) -> val pr_ltac_constant : ltac_constant -> Pp.t -val pr_raw_tactic : raw_tactic_expr -> Pp.t +val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t +val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d833a2cde..b1d5c0252f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -15,6 +15,7 @@ open Names open Nameops open Namegen open Constr +open Context open EConstr open Vars open Reduction @@ -220,23 +221,23 @@ end) = struct let rec aux env evars ty l = let t = Reductionops.whd_all env (goalevars evars) ty in match EConstr.kind (goalevars evars) t, l with - | Prod (na, ty, b), obj :: cstrs -> + | Prod (na, ty, b), obj :: cstrs -> let b = Reductionops.nf_betaiota env (goalevars evars) b in - if noccurn (goalevars evars) 1 b (* non-dependent product *) then + if noccurn (goalevars evars) 1 b (* non-dependent product *) then let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in let evars, relty = mk_relty evars env ty obj in let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in - evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs + evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs else let (evars, b, arg, cstrs) = - aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs + aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in let ty = Reductionops.nf_betaiota env (goalevars evars) ty in - let pred = mkLambda (na, ty, b) in - let liftarg = mkLambda (na, ty, arg) in - let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in - if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs + let pred = mkLambda (na, ty, b) in + let liftarg = mkLambda (na, ty, arg) in + let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in + if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.") | _, [] -> @@ -253,7 +254,7 @@ end) = struct let unfold_impl sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (Anonymous, a, lift 1 b) + mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -279,7 +280,7 @@ end) = struct (app_poly env evd arrow [| a; b |]), unfold_impl (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) (app_poly env evd arrow [| a; b |]), unfold_impl @@ -308,7 +309,8 @@ end) = struct app_poly env evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |] else app_poly env evd forall_relation - [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |] + [| t; mkLambda (make_annot n Sorts.Relevant, t, car); + mkLambda (make_annot n Sorts.Relevant, t, rel) |] let lift_cstr env evars (args : constr list) c ty cstr = let start evars env car = @@ -323,15 +325,15 @@ end) = struct else let sigma = goalevars evars in match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with - | Prod (na, ty, b) -> + | Prod (na, ty, b) -> if noccurn sigma 1 b then let b' = lift (-1) b in let evars, rb = aux evars env b' (pred n) in app_poly env evars pointwise_relation [| ty; b'; rb |] else - let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in + let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in app_poly env evars forall_relation - [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |] + [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |] | _ -> raise Not_found in let rec find env c ty = function @@ -449,7 +451,7 @@ let evd_convertible env evd x y = unsolvable constraints remain, so we check that this unification does not introduce any new problem. *) let _, pbs = Evd.extract_all_conv_pbs evd in - let evd' = Evarconv.the_conv_x env x y evd in + let evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None @@ -481,8 +483,9 @@ let rec decompose_app_rel env evd t = | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Typing.unsafe_type_of env evd argl in - let f'' = mkLambda (Name default_dependent_ident, ty, - mkLambda (Name (Id.of_string "y"), lift 1 ty, + let r = Retyping.relevance_of_type env evd ty in + let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, + mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', argl, argr) | App (f, args) -> @@ -522,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with + match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") @@ -803,7 +806,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation in EConstr.push_named - (LocalDef (Id.of_string "do_subrelation", + (LocalDef (make_annot (Id.of_string "do_subrelation") Sorts.Relevant, snd (app_poly_sort b env evars dosub [||]), snd (app_poly_nocheck env evars appsub [||]))) env @@ -906,7 +909,7 @@ let make_leibniz_proof env c ty r = let prf = e_app_poly env evars coq_f_equal [| r.rew_car; ty; - mkLambda (Anonymous, r.rew_car, c); + mkLambda (make_annot Anonymous Sorts.Relevant, r.rew_car, c); r.rew_from; r.rew_to; prf |] in RewPrf (rel, prf) | RewCast k -> r.rew_prf @@ -1103,7 +1106,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* else *) | Prod (n, dom, codom) -> - let lam = mkLambda (n, dom, codom) in + let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = if eq_constr (fst evars) ty mkProp then (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all @@ -1149,9 +1152,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in let open Context.Rel.Declaration in - let env' = EConstr.push_rel (LocalAssum (n', t)) env in + let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ; @@ -1166,15 +1169,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let point = if prop then PropGlobal.pointwise_or_dep_relation else TypeGlobal.pointwise_or_dep_relation in - let evars, rel = point env r.rew_evars n' t r.rew_car rel in - let prf = mkLambda (n', t, prf) in + let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in + let prf = mkLambda (n', t, prf) in { r with rew_prf = RewPrf (rel, prf); rew_evars = evars } | x -> r in Success { r with - rew_car = mkProd (n, t, r.rew_car); - rew_from = mkLambda(n, t, r.rew_from); - rew_to = mkLambda (n, t, r.rew_to) } + rew_car = mkProd (n, t, r.rew_car); + rew_from = mkLambda(n, t, r.rew_from); + rew_to = mkLambda (n, t, r.rew_to) } | Fail | Identity -> b' in state, res @@ -1516,7 +1519,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Some (t, ty) -> let t = Reductionops.nf_evar evars' t in let ty = Reductionops.nf_evar evars' ty in - mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |]) + mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) Sorts.Relevant, ty, p), [| t |]) in let proof = match is_hyp with | None -> term @@ -1542,7 +1545,8 @@ let assert_replacing id newt tac = let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env sigma + (LocalAssum (make_annot (NamedDecl.get_id d) Sorts.Relevant, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~typecheck:true begin fun sigma -> @@ -1586,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (id, newt)) <*> + convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1905,7 +1909,7 @@ let build_morphism_signature env sigma m = let cstrs = let rec aux t = match EConstr.kind sigma t with - | Prod (na, a, b) -> + | Prod (na, a, b) -> None :: aux b | _ -> [] in aux t diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 026c00b849..fcab98c7e8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,7 +199,8 @@ let id_of_name = function basename | Sort s -> begin - match ESorts.kind sigma s with + match ESorts.kind sigma s with + | Sorts.SProp -> Label.to_id (Label.make "SProp") | Sorts.Prop -> Label.to_id (Label.make "Prop") | Sorts.Set -> Label.to_id (Label.make "Set") | Sorts.Type _ -> Label.to_id (Label.make "Type") diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04..543d4de0fe 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 30f716d764..eac84f0543 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 99b9e881f6..52a83a038f 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -19,11 +19,9 @@ let prtac x = Pptactic.pr_glob_tactic (Global.env()) x let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp -let prmatchrl rl = +let prmatchrl env sigma rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> - let sigma, env = Pfedit.get_current_context () in - Printer.pr_constr_pattern_env env sigma p) rl + (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -246,13 +244,13 @@ let db_constr debug env sigma c = else return () (* Prints the pattern rule *) -let db_pattern_rule debug num r = +let db_pattern_rule debug env sigma num r = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then begin msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++ - str "|" ++ spc () ++ prmatchrl r) + str "|" ++ spc () ++ prmatchrl env sigma r) end else return () diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 91e8510b92..74ea4e6b74 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + debug_info -> env -> evar_map -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 54924f1644..2b5e496168 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -12,6 +12,7 @@ (lazy)match and (lazy)match goal. *) open Names +open Context open Tacexpr open Context.Named.Declaration @@ -299,8 +300,8 @@ module PatternMatching (E:StaticEnvironment) = struct | LocalDef (id,body,hyp) -> pattern_match_term false bodypat body () <*> pattern_match_term true typepat hyp () <*> - put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> - return id + put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*> + return id.binder_name | LocalAssum (id,hyp) -> fail (** [hyp_match pat hyps] dispatches to diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 19256e054d..4c65445b89 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -142,7 +142,7 @@ let flatten_contravariant_conj _ ist = ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let newtyp = List.fold_right mkArrow args c in + let newtyp = List.fold_right (fun a b -> mkArrow a Sorts.Relevant b) args c in let intros = tclMAP (fun _ -> intro) args in let by = tclTHENLIST [intros; apply hyp; split; assumption] in tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)] @@ -173,7 +173,7 @@ let flatten_contravariant_disj _ ist = typ with | Some (_,args) -> let map i arg = - let typ = mkArrow arg c in + let typ = mkArrow arg Sorts.Relevant c in let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7adae148bd..7db47e13a5 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Context open Tactypes (** @@ -876,11 +877,9 @@ struct * This is the big generic function for expression parsers. *) - let parse_expr sigma parse_constant parse_exp ops_spec env term = + let parse_expr cenv sigma parse_constant parse_exp ops_spec env term = if debug - then ( - let _, env = Pfedit.get_current_context () in - Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env cenv sigma term); (* let constant_or_variable env term = @@ -999,8 +998,7 @@ struct | _ -> raise ParseError - let rconstant sigma term = - let _, env = Pfedit.get_current_context () in + let rconstant env sigma term = if debug then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in @@ -1009,7 +1007,7 @@ struct res - let parse_zexpr sigma = parse_expr sigma + let parse_zexpr env sigma = parse_expr env sigma (zconstant sigma) (fun expr x -> let exp = (parse_z sigma x) in @@ -1018,7 +1016,7 @@ struct | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) zop_spec - let parse_qexpr sigma = parse_expr sigma + let parse_qexpr env sigma = parse_expr env sigma (qconstant sigma) (fun expr x -> let exp = parse_z sigma x in @@ -1033,8 +1031,8 @@ struct Mc.PEpow(expr,exp)) qop_spec - let parse_rexpr sigma = parse_expr sigma - (rconstant sigma) + let parse_rexpr env sigma = parse_expr env sigma + (rconstant env sigma) (fun expr x -> let exp = Mc.N.of_nat (parse_nat sigma x) in Mc.PEpow(expr,exp)) @@ -1047,8 +1045,8 @@ struct match EConstr.kind sigma cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr sigma env lhs in - let (e2,env) = parse_expr sigma env rhs in + let (e1,env) = parse_expr gl.env sigma env lhs in + let (e2,env) = parse_expr gl.env sigma env rhs in ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) | _ -> failwith "error : parse_arith(2)" @@ -1243,7 +1241,7 @@ let dump_rexpr = lazy let prodn n env b = let rec prodrec = function | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) + | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (make_annot v Sorts.Relevant,t,b)) | _ -> assert false in prodrec (n,env,b) @@ -1293,8 +1291,8 @@ let make_goal_of_formula sigma dexpr form = | FF -> Lazy.force coq_False | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) + | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (xdump (pi+1) (xi+1) y) + | N(x) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) | A(x,_,_) -> dump_cstr xi x | X(t) -> let idx = Env.get_rank props sigma t in EConstr.mkRel (pi+idx) in @@ -1327,7 +1325,7 @@ let make_goal_of_formula sigma dexpr form = | (e::l) -> let (name,expr,typ) = e in xset (EConstr.mkNamedLetIn - (Names.Id.of_string name) + (make_annot (Names.Id.of_string name) Sorts.Relevant) expr typ acc) l in xset concl l @@ -1614,7 +1612,7 @@ let abstract_formula hyps f = | I(f1,hyp,f2) -> (match xabs f1 , hyp, xabs f2 with | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) + | X a1 , None , X a2 -> X (EConstr.mkArrow a1 Sorts.Relevant a2) | af1 , _ , af2 -> I(af1,hyp,af2) ) | FF -> FF diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index b91feb3984..d1776b8ca4 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -20,3 +20,9 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic + + +(** {5 Use Micromega independently from tactics. } *) + +(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *) +val dump_proof_term : Micromega.zArithProof -> EConstr.t diff --git a/plugins/micromega/micromega_plugin.mlpack b/plugins/micromega/micromega_plugin.mlpack index 2baf6608a4..e3aa0dab7d 100644 --- a/plugins/micromega/micromega_plugin.mlpack +++ b/plugins/micromega/micromega_plugin.mlpack @@ -1,8 +1,8 @@ +Micromega Mutils Itv Vect Sos_types -Micromega Polynomial Mfourier Simplex diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index dff25b3a42..4802608fda 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -19,6 +19,7 @@ open CErrors open Util open Names open Constr +open Context open Nameops open EConstr open Tacticals.New @@ -431,8 +432,8 @@ let destructurate_prop sigma t = | Ind (isp,_), args -> Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id - | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") + | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) + | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo let nf = Tacred.simpl @@ -499,13 +500,13 @@ let context sigma operation path (t : constr) = | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in - v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) | ((P_TYPE :: p), Prod (n,t,c)) -> - (mkProd (n,loop i p t,c)) + (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> - (mkLambda (n,loop i p t,c)) + (mkLambda (n,loop i p t,c)) | ((P_TYPE :: p), LetIn (n,b,t,c)) -> - (mkLetIn (n,b,loop i p t,c)) + (mkLetIn (n,b,loop i p t,c)) | (p, _) -> failwith ("abstract_path " ^ string_of_int(List.length p)) in @@ -528,7 +529,7 @@ let occurrence sigma path (t : constr) = let abstract_path sigma typ path t = let term_occur = ref (mkRel 0) in let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur + mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur let focused_simpl path = let open Tacmach.New in @@ -604,10 +605,10 @@ let clever_rewrite_base_poly typ p result theorem = let t = applist (mkLambda - (Name (Id.of_string "P"), - mkArrow typ mkProp, + (make_annot (Name (Id.of_string "P")) Sorts.Relevant, + mkArrow typ Sorts.Relevant mkProp, mkLambda - (Name (Id.of_string "H"), + (make_annot (Name (Id.of_string "H")) Sorts.Relevant, applist (mkRel 1,[result]), mkApp (Lazy.force coq_eq_ind_r, [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), @@ -1264,7 +1265,7 @@ let replay_history tactic_normalisation = mkApp (Lazy.force coq_ex, [| Lazy.force coq_Z; mkLambda - (Name vid, + (make_annot (Name vid) Sorts.Relevant, Lazy.force coq_Z, mk_eq (mkRel 1) eq1) |]) in @@ -1725,11 +1726,11 @@ let destructure_hyps = try match destructurate_type env sigma typ with | Kapp(Nat,_) | Kapp(Z,_) -> - let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in - let hty = mk_gen_eq typ (mkVar i) body in + let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in + let hty = mk_gen_eq typ (mkVar i.binder_name) body in tclTHEN (assert_by (Name hid) hty reflexivity) - (loop (LocalAssum (hid, hty) :: lit)) + (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit)) | _ -> loop lit with e when catchable_exception e -> loop lit end @@ -1742,18 +1743,20 @@ let destructure_hyps = | Kapp(Or,[t1;t2]) -> (tclTHENS (elim_id i) - [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); - onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) + [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit))); + onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) + loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) :: + LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) + loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) :: + LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) @@ -1764,7 +1767,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit)))) ] else loop lit @@ -1775,7 +1778,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in @@ -1784,7 +1787,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in @@ -1794,7 +1797,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2)) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2)) (mk_and (mk_not t1) t2)) :: lit)))) ] | Kimp(t1,t2) -> @@ -1806,14 +1809,14 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit)))) ] | Kapp(Not,[t]) -> let d = decidability t in tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) + (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit)))) ] | Kapp(op,[t1;t2]) -> (try diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 751f0d8334..c2dec264ad 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -294,10 +294,10 @@ Qed. End Store. -Arguments PNone [A]. +Arguments PNone {A}. Arguments PSome [A] _. -Arguments Tempty [A]. +Arguments Tempty {A}. Arguments Branch0 [A] _ _. Arguments Branch1 [A] _ _ _. @@ -311,7 +311,7 @@ Arguments mkStore [A] index contents. Arguments index [A] s. Arguments contents [A] s. -Arguments empty [A]. +Arguments empty {A}. Arguments get [A] i S. Arguments push [A] a S. @@ -319,7 +319,7 @@ Arguments get_empty [A] i. Arguments get_push_Full [A] i a S _. Arguments Full [A] _. -Arguments F_empty [A]. +Arguments F_empty {A}. Arguments F_push [A] a S _. Arguments In [A] x S F. diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index a6b6c57ff9..89528fe357 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,6 +16,7 @@ open CErrors open Util open Term open Constr +open Context open Proof_search open Context.Named.Declaration @@ -127,7 +128,7 @@ let rec make_hyps env sigma atom_env lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps env sigma atom_env (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id.binder_name c) lenv || (Retyping.get_sort_family_of env sigma typ != InProp) then hrec @@ -291,7 +292,7 @@ let rtauto_tac = build_form formula; build_proof [] 0 prf|]) in let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in let build_end_time=System.get_time () in let () = if !verbose then begin diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 49b5ee5ac7..3de0ba44df 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -23,6 +23,6 @@ val make_hyps -> atom_env -> EConstr.types list -> EConstr.named_context - -> (Names.Id.t * Proof_search.form) list + -> (Names.Id.t Context.binder_annot * Proof_search.form) list val rtauto_tac : unit Proofview.tactic diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index dba72337b2..f5d13053b1 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1789,5 +1789,5 @@ End Field. End Complete. -Arguments FEO [C]. -Arguments FEI [C]. +Arguments FEO {C}. +Arguments FEI {C}. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 9ef24144d2..12f716c496 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1507,5 +1507,5 @@ Qed. End MakeRingPol. -Arguments PEO [C]. -Arguments PEI [C]. +Arguments PEO {C}. +Arguments PEI {C}. diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index f59ca4cef4..3ce6478700 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -38,24 +38,24 @@ END open Pptactic open Ppconstr -let pr_ring_mod = function - | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test +let pr_ring_mod env sigma = function + | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test | Ring_kind Abstract -> str "abstract" - | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph - | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" + | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph + | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" - | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" - | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t - | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t + | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]" + | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" + | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]" + | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t + | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t } VERNAC ARGUMENT EXTEND ring_mod - PRINTED BY { pr_ring_mod } + PRINTED BY { pr_ring_mod env sigma } | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) } | [ "abstract" ] -> { Ring_kind Abstract } | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) } @@ -74,12 +74,12 @@ END { -let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) +let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l) } VERNAC ARGUMENT EXTEND ring_mods - PRINTED BY { pr_ring_mods } + PRINTED BY { pr_ring_mods env sigma } | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods } END @@ -104,26 +104,26 @@ END { -let pr_field_mod = function - | Ring_mod m -> pr_ring_mod m - | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj +let pr_field_mod env sigma = function + | Ring_mod m -> pr_ring_mod env sigma m + | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj } VERNAC ARGUMENT EXTEND field_mod - PRINTED BY { pr_field_mod } + PRINTED BY { pr_field_mod env sigma } | [ ring_mod(m) ] -> { Ring_mod m } | [ "completeness" constr(inj) ] -> { Inject inj } END { -let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l) +let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l) } VERNAC ARGUMENT EXTEND field_mods - PRINTED BY { pr_field_mods } + PRINTED BY { pr_field_mods env sigma } | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods } END diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index ed4ff2aa66..d6b7371647 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -813,21 +813,21 @@ Proof. by case b1; case b2; constructor; auto. Qed. End ReflectConnectives. -Arguments idP [b1]. -Arguments idPn [b1]. -Arguments negP [b1]. -Arguments negPn [b1]. -Arguments negPf [b1]. -Arguments andP [b1 b2]. -Arguments and3P [b1 b2 b3]. -Arguments and4P [b1 b2 b3 b4]. -Arguments and5P [b1 b2 b3 b4 b5]. -Arguments orP [b1 b2]. -Arguments or3P [b1 b2 b3]. -Arguments or4P [b1 b2 b3 b4]. -Arguments nandP [b1 b2]. -Arguments norP [b1 b2]. -Arguments implyP [b1 b2]. +Arguments idP {b1}. +Arguments idPn {b1}. +Arguments negP {b1}. +Arguments negPn {b1}. +Arguments negPf {b1}. +Arguments andP {b1 b2}. +Arguments and3P {b1 b2 b3}. +Arguments and4P {b1 b2 b3 b4}. +Arguments and5P {b1 b2 b3 b4 b5}. +Arguments orP {b1 b2}. +Arguments or3P {b1 b2 b3}. +Arguments or4P {b1 b2 b3 b4}. +Arguments nandP {b1 b2}. +Arguments norP {b1 b2}. +Arguments implyP {b1 b2}. Prenex Implicits idP idPn negP negPn negPf. Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP. @@ -953,7 +953,7 @@ Proof. by case: a; case: b. Qed. Lemma addbP a b : reflect (~~ a = b) (a (+) b). Proof. by case: a; case: b; constructor. Qed. -Arguments addbP [a b]. +Arguments addbP {a b}. (** Resolution tactic for blindly weeding out common terms from boolean @@ -1158,8 +1158,8 @@ Definition clone_pred U := End Predicates. -Arguments pred0 [T]. -Arguments predT [T]. +Arguments pred0 {T}. +Arguments predT {T}. Prenex Implicits pred0 predT predI predU predC predD preim relU. Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) @@ -1357,7 +1357,7 @@ Variant qualifier (q : nat) T := Qualifier of predPredType T. Coercion has_quality n T (q : qualifier n T) : pred_class := fun x => let: Qualifier _ p := q in p x. -Arguments has_quality n [T]. +Arguments has_quality n {T}. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 0961edb6cb..6956120a6a 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -15,6 +15,7 @@ open Names open Evd open Term open Constr +open Context open Termops open Printer open Locusops @@ -429,15 +430,16 @@ let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Prod(_,src,tgt) -> - Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl + | Prod(x,src,tgt) -> + let x = {x with binder_name = !orig_name_ref} in + Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (x,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") (* Reduction that preserves the Prod/Let spine of the "in" tactical. *) let inc_safe n = if n = 0 then n else n + 1 let rec safe_depth s c = match EConstr.kind s c with -| LetIn (Name x, _, _, c') when is_discharged_id x -> safe_depth s c' + 1 +| LetIn ({binder_name=Name x}, _, _, c') when is_discharged_id x -> safe_depth s c' + 1 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth s c') | _ -> 0 @@ -529,7 +531,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let concl = EConstr.Unsafe.to_constr evi.evar_concl in let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function - | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) + | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in @@ -552,7 +554,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | _ -> Constr.map_with_binders ((+) 1) get i c in let rec loop c i = function | (_, (n, t)) :: evl -> - loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl + loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, get (i - 1) t, c)) (i - 1) evl | [] -> c in List.length evlist, EConstr.of_constr (loop (get 1 c0) 1 evlist), List.map fst evlist, ucst @@ -590,7 +592,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let concl = EConstr.Unsafe.to_constr evi.evar_concl in let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function - | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) + | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in @@ -646,7 +648,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in - loopP evlist (mkProd (n, t, c)) (i - 1) evl + loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function | (_, (n, t, _)) :: evl -> @@ -658,7 +660,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) (List.rev t_evplist) in let c = if extra_args = [] then c else app extra_args 1 c in - loop (mkLambda (mk_evar_name n, t, c)) (i - 1) evl + loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl | [] -> c in let res = loop (get evlist 1 c0) 1 evlist in pp(lazy(str"res= " ++ pr_constr res)); @@ -679,6 +681,9 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let pfe_type_relevance_of gl t = + let gl, ty = pfe_type_of gl t in + gl, ty, pf_apply Retyping.relevance_of_term gl t let pf_type_of gl t = let sigma, ty = pf_type_of gl (EConstr.of_constr t) in re_sig (sig_it gl) sigma, EConstr.Unsafe.to_constr ty @@ -710,13 +715,13 @@ let pf_abs_cterm gl n c0 = | _ -> [], strip i c in let rec strip_evars i c = match Constr.kind c with | Lambda (x, t1, c1) when i < n -> - let na = nb_evar_deps x in + let na = nb_evar_deps x.binder_name in let dl, t2 = strip_ndeps (i + na) i t1 in let na' = List.length dl in eva.(i) <- Array.of_list (na - na' :: dl); let x' = if na' = 0 then Name (pf_type_id gl (EConstr.of_constr t2)) else mk_evar_name na' in - mkLambda (x', t2, strip_evars (i + 1) c1) + mkLambda ({x with binder_name=x'}, t2, strip_evars (i + 1) c1) (* if noccurn 1 c2 then lift (-1) c2 else mkLambda (Name (pf_type_id gl t2), t2, c2) *) | _ -> strip i c in @@ -739,9 +744,9 @@ let rec constr_name sigma c = match EConstr.kind sigma c with | _ -> Anonymous let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = - let gl, t = pfe_type_of gl c in - if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (name, t, cl) else - gl, EConstr.mkProd (Name (pf_type_id gl t), t, cl) + let gl, t, r = pfe_type_relevance_of gl c in + if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (make_annot name r, t, cl) else + gl, EConstr.mkProd (make_annot (Name (pf_type_id gl t)) r, t, cl) let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) @@ -783,13 +788,17 @@ let mkRefl t c gl = let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in - match pf_get_hyp gl id, mode with - | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) + let decl = pf_get_hyp gl id in + match decl, mode with + | NamedDecl.LocalAssum _, _ | NamedDecl.LocalDef _, "(" -> + let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true + (EConstr.of_constr (mkProd (id', NamedDecl.get_type decl, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> + let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in Proofview.V82.of_tactic - (convert_concl (EConstr.of_constr (mkLetIn (Name id', v, t, cl')))) gl + (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl (* wildcard names *) let clear_wilds wilds gl = @@ -983,7 +992,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = let rec loop sigma bo args = function (* saturate with metas *) | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma | n -> match EConstr.kind sigma bo with - | Lambda (_, ty, bo) -> + | Lambda (_, ty, bo) -> if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in @@ -1019,7 +1028,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with - | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id + | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id.binder_name | _ -> if red then Tacticals.New.tclZEROMSG (str"No product even after head-reduction.") else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac) end @@ -1122,14 +1131,14 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = errorstrm (str "@ can be used with variables only") else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only") - | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (Name name,b,ty,cl),c,clr,ucst,gl + | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl),c,clr,ucst,gl else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else - let gl, pty = pfe_type_of gl p in - false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl + let gl, pty, rp = pfe_type_relevance_of gl p in + false, pat, EConstr.mkProd (make_annot (constr_name (project gl) c) rp, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) @@ -1223,7 +1232,7 @@ let abs_wgen keep_let f gen (gl,args,c) = let evar_closed t p = if occur_existential sigma t then CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect" - (pr_constr_pat (EConstr.Unsafe.to_constr t) ++ + (pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ str" contains holes and matches no subterm of the goal") in match gen with | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) -> @@ -1235,7 +1244,10 @@ let abs_wgen keep_let f gen (gl,args,c) = (EConstr.Vars.subst_var x c) | _, Some ((x, _), None) -> let x = hoi_id x in - gl, EConstr.mkVar x :: args, EConstr.mkProd (Name (f x),Tacmach.pf_get_hyp_typ gl x, EConstr.Vars.subst_var x c) + let hyp = Tacmach.pf_get_hyp gl x in + let x' = make_annot (Name (f x)) (NamedDecl.get_relevance hyp) in + let prod = EConstr.mkProd (x', NamedDecl.get_type hyp, EConstr.Vars.subst_var x c) in + gl, EConstr.mkVar x :: args, prod | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in @@ -1246,8 +1258,8 @@ let abs_wgen keep_let f gen (gl,args,c) = let t = EConstr.of_constr t in evar_closed t p; let ut = red_product_skip_id env sigma t in - let gl, ty = pfe_type_of gl t in - pf_merge_uc ucst gl, args, EConstr.mkLetIn(Name (f x), ut, ty, c) + let gl, ty, r = pfe_type_relevance_of gl t in + pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c) | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in @@ -1257,8 +1269,8 @@ let abs_wgen keep_let f gen (gl,args,c) = let c = EConstr.of_constr c in let t = EConstr.of_constr t in evar_closed t p; - let gl, ty = pfe_type_of gl t in - pf_merge_uc ucst gl, t :: args, EConstr.mkProd(Name (f x), ty, c) + let gl, ty, r = pfe_type_relevance_of gl t in + pf_merge_uc ucst gl, t :: args, EConstr.mkProd(make_annot (Name (f x)) r, ty, c) | _ -> gl, args, c let clr_of_wgen gen clrs = match gen with @@ -1321,8 +1333,8 @@ let unsafe_intro env decl b = end let set_decl_id id = let open Context in function - | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum(id,ty) - | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef(id,ty,t) + | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum({name with binder_name=id},ty) + | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef({name with binder_name=id},ty,t) let rec decompose_assum env sigma orig_goal = let open Context in @@ -1400,8 +1412,8 @@ let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with - | Prod(_,src,tgt) -> - convert_concl_no_check EConstr.(mkProd (name,src,tgt)) + | Prod(x,src,tgt) -> + convert_concl_no_check EConstr.(mkProd ({x with binder_name = name},src,tgt)) | _ -> CErrors.anomaly (Pp.str "rename_hd_prod: no head product") end @@ -1429,11 +1441,12 @@ let tacMKPROD c ?name cl = tacCONSTR_NAME ?name c >>= fun name -> Goal.enter_one ~__LOC__ begin fun g -> let sigma, env = Goal.sigma g, Goal.env g in + let r = Retyping.relevance_of_term env sigma c in if name <> Names.Name.Anonymous || EConstr.Vars.noccurn sigma 1 cl - then tclUNIT (EConstr.mkProd (name, t, cl)) + then tclUNIT (EConstr.mkProd (make_annot name r, t, cl)) else let name = Names.Id.of_string (Namegen.hdchar env sigma t) in - tclUNIT (EConstr.mkProd (Names.Name.Name name, t, cl)) + tclUNIT (EConstr.mkProd (make_annot (Name.Name name) r, t, cl)) end let tacINTERP_CPATTERN cp = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e642b5e788..9662daa7c7 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -155,7 +155,7 @@ val pf_e_type_of : val splay_open_constr : Goal.goal Evd.sigma -> evar_map * EConstr.t -> - (Names.Name.t * EConstr.t) list * EConstr.t + (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool val mk_term : ssrtermkind -> constr_expr -> ssrterm @@ -205,6 +205,9 @@ val pf_type_of : val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types +val pfe_type_relevance_of : + Goal.goal Evd.sigma -> + EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance val pf_abs_prod : Name.t -> Goal.goal Evd.sigma -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..3fc05437da 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -15,6 +15,7 @@ open Names open Printer open Term open Constr +open Context open Termops open Tactypes open Tacmach @@ -132,7 +133,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p)); + ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); @@ -209,7 +210,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in @@ -237,8 +239,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elimty = Reductionops.whd_all env (project gl) elimty in seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in - ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat (EConstr.Unsafe.to_constr elim))); - ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat (EConstr.Unsafe.to_constr elimty))); + ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elim))); + ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elimty))); let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in @@ -283,8 +285,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) - let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern p) in - let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl t)) in + let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in + let pp_inf_pat gl (_,_,t,_) = pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl t)) in let patterns, clr, gl = let rec loop patterns clr i = function | [],[] -> patterns, clr, gl @@ -298,7 +300,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr c))); + ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr c))); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -321,11 +323,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elim_pred, gen_eq_tac, clr, gl = let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++ spc()++pp_term gl t++spc()++str"while the inferred pattern"++ - spc()++pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in + spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then - let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern p)) in + let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in cl, gl, post @ [h, p, inf_t, occ] else try let c, cl, ucst = match_pat env p occ h cl in @@ -363,14 +365,14 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let gl, eq = get_eq_type gl in let gen_eq_tac, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in - let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in + let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in apply_type new_concl [erefl], gl in let rel = k + if c_is_head_p then 1 else 0 in let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in - let concl = EConstr.mkArrow src (EConstr.Vars.lift 1 concl) in + let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl | _ -> concl, Tacticals.tclIDTAC, clr, gl in @@ -406,7 +408,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = if not (Evar.Set.is_empty inter) then begin let i = Evar.Set.choose inter in let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in - errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat (EConstr.Unsafe.to_constr pat)++spc()++ + errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++ str"was not completely instantiated and one of its variables"++spc()++ str"occurs in the type of another non-instantiated pattern variable"); end @@ -445,7 +447,7 @@ let injecteq_id = mk_internal_id "injection equation" let revtoptac n0 gl = let n = pf_nb_prod gl - n0 in let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in - let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in + let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl @@ -485,7 +487,7 @@ let perform_injection c gl = CErrors.user_err (Pp.str "can't decompose a quantified equality") else let cl = pf_concl gl in let n = List.length dc in let c_eq = mkEtaApp c n 2 in - let cl1 = EConstr.mkLambda EConstr.(Anonymous, mkArrow eqt cl, mkApp (mkRel 1, [|c_eq|])) in + let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (EConstr.mkVar id, NoBindings) in let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 64e023c68a..15480c7a45 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Constr +open Context open Vars open Locus open Printer @@ -136,7 +137,7 @@ let newssrcongrtac arg ist gl = (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in - let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in + let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|]) (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist)) (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow"))) @@ -198,13 +199,13 @@ let simplintac occ rdx sim gl = | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl | _ -> simpltac sim gl -let rec get_evalref sigma c = match EConstr.kind sigma c with +let rec get_evalref env sigma c = match EConstr.kind sigma c with | Var id -> EvalVarRef id | Const (k,_) -> EvalConstRef k - | App (c', _) -> get_evalref sigma c' - | Cast (c', _, _) -> get_evalref sigma c' + | App (c', _) -> get_evalref env sigma c' + | Cast (c', _, _) -> get_evalref env sigma c' | Proj(c,_) -> EvalConstRef(Projection.constant c) - | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable") + | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with @@ -229,7 +230,7 @@ let unfoldintac occ rdx t (kt,_) gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let (sigma, t), const = strip_unfold_term env0 t kt in let body env t c = - Tacred.unfoldn [AllOccurrences, get_evalref sigma t] env sigma0 c in + Tacred.unfoldn [AllOccurrences, get_evalref env sigma t] env sigma0 c in let easy = occ = None && rdx = None in let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in @@ -243,7 +244,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), + ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -269,12 +270,12 @@ let unfoldintac occ rdx t (kt,_) gl = else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) - with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)) in + with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat env0 sigma (EConstr.Unsafe.to_constr t)) in let _ = conclude () in Proofview.V82.of_tactic (convert_concl concl) gl ;; @@ -297,8 +298,8 @@ let foldtac occ rdx ft gl = try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t) - with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc () - ++ str "does not match redex " ++ pr_constr_pat c)), + with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat env sigma t ++ spc () + ++ str "does not match redex " ++ pr_constr_pat env sigma c)), fake_pmatcher_end in let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in @@ -335,7 +336,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in (sigma, ev) in - let pred = EConstr.mkNamedLambda pattern_id rdx_ty pred in + let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in @@ -362,7 +363,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let names = let rec aux t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in match EConstr.kind_of_type sigma t with - | ProdType (name, _, t) -> name :: aux t (n-1) + | ProdType (name, _, t) -> name.binder_name :: aux t (n-1) | _ -> assert false in aux hd_ty (Array.length args) in hd_ty, Util.List.map_filter (fun (t, name) -> let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in @@ -403,7 +404,7 @@ let rwcltac cl rdx dir sr gl = let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> - let cl' = EConstr.mkApp (EConstr.mkNamedLambda pattern_id rdxt cl, [|rdx|]) in + let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl @@ -411,10 +412,10 @@ let rwcltac cl rdx dir sr gl = let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> - errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) + errorstrm Pp.(str "no cast from " ++ pr_constr_pat (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr)) ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in - let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in - let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in + let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in + let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in @@ -426,7 +427,9 @@ let rwcltac cl rdx dir sr gl = if occur_existential (project gl) (Tacmach.pf_concl gl) then errorstrm Pp.(str "Rewriting impacts evars") else errorstrm Pp.(str "Dependent type error in rewrite of " - ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) + ++ pr_constr_env (pf_env gl) (project gl) + (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant) + (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) in tclTHEN cvtac' rwtac gl @@ -470,7 +473,7 @@ let rwprocess_rule dir rule gl = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat (EConstr.Unsafe.to_constr t))); + ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in @@ -529,8 +532,8 @@ let rwprocess_rule dir rule gl = sigma, (d, r', lhs, rhs) :: rs | _ -> if red = 0 then loop d sigma r t rs 1 - else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat (EConstr.Unsafe.to_constr t) - ++ spc() ++ str "in rule " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd rule))) + else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) + ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule))) in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in @@ -544,9 +547,9 @@ let rwrxtac occ rdx_pat dir rule gl = let find_rule rdx = let rec rwtac = function | [] -> - errorstrm Pp.(str "pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr rdx) ++ + errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++ str " does not match " ++ pr_dir_side dir ++ - str " of " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd rule))) + str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule))) | (d, r, lhs, rhs) :: rs -> try let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in @@ -637,7 +640,7 @@ let ssrrewritetac ist rwargs = let unfoldtac occ ko t kt gl = let env = pf_env gl in let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in - let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref (project gl) c] gl c) cl in + let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in Proofview.V82.of_tactic (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8c1363020a..be9586fdd7 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -13,6 +13,7 @@ open Pp open Names open Constr +open Context open Tacmach open Ssrmatching_plugin.Ssrmatching @@ -49,12 +50,12 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ - pr_constr_pat (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++ + pr_constr_pat env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++ str"Did you mean pose?") else let c, (gl, cty) = match EConstr.kind sigma c with | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in - let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in + let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util @@ -162,7 +163,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -190,10 +191,10 @@ let havetac ist Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)) | _,true,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in - gl, EConstr.mkArrow ty concl, hint, itac, clr + gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, itac, clr | _,false,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in - gl, EConstr.mkArrow ty concl, hint, id, itac_c + gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c | _, false, false -> let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac @@ -233,7 +234,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let gens = List.filter (function _, Some _ -> true | _ -> false) gens in let concl = pf_concl gl in let c = EConstr.mkProp in - let c = if cut_implies_goal then EConstr.mkArrow c concl else c in + let c = if cut_implies_goal then EConstr.mkArrow c Sorts.Relevant concl else c in let gl, args, c = List.fold_right mkabs gens (gl,[],c) in let env, _ = List.fold_left (fun (env, c) _ -> @@ -245,10 +246,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let fake_gl = {Evd.it = k; Evd.sigma = sigma} in let _, ct, _, uc = pf_interp_ty ist fake_gl ct in let rec var2rel c g s = match EConstr.kind sigma c, g with - | Prod(Anonymous,_,c), [] -> EConstr.mkProd(Anonymous, EConstr.Vars.subst_vars s ct, c) + | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c) | Sort _, [] -> EConstr.Vars.subst_vars s ct - | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) - | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) + | LetIn({binder_name=Name id} as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) + | Prod({binder_name=Name id} as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index a8dfd69240..e9fe1f3e48 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -13,6 +13,7 @@ open Ssrmatching_plugin open Util open Names open Constr +open Context open Proofview open Proofview.Notations @@ -393,12 +394,12 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let sigma, m = Evarutil.new_evar env sigma abstract_ty in sigma, (m, abstract_ty) in let sigma, kont = - let rd = Context.Rel.Declaration.LocalAssum (Name id, abstract_ty) in + let rd = Context.Rel.Declaration.LocalAssum (make_annot (Name id) Sorts.Relevant, abstract_ty) in let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in sigma, ev in let term = - EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont),[|abstract_proof|])) in + EConstr.(mkApp (mkLambda(make_annot (Name id) Sorts.Relevant,abstract_ty,kont),[|abstract_proof|])) in let sigma, _ = Typing.type_of env sigma term in sigma, term end in @@ -608,7 +609,7 @@ let with_defective maintac deps clr = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in let top_id = match EConstr.kind_of_type sigma concl with - | Term.ProdType (Name id, _, _) + | Term.ProdType ({binder_name=Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> Ssrcommon.top_id in let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in @@ -683,7 +684,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = let name = Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in let new_concl = - mkProd (Name name, case_ty, mkArrow refl (Vars.lift 2 concl)) in + mkProd (make_annot (Name name) Sorts.Relevant, case_ty, mkArrow refl Sorts.Relevant (Vars.lift 2 concl)) in let erefl, sigma = mkCoqRefl case_ty case env sigma in Proofview.Unsafe.tclEVARS sigma <*> Tactics.apply_type ~typecheck:true new_concl [case;erefl] @@ -707,7 +708,7 @@ let mkEq dir cl c t n env sigma = eqargs.(Ssrequality.dir_org dir) <- mkRel n; let eq, sigma = mkCoqEq env sigma in let refl, sigma = mkCoqRefl t c env sigma in - mkArrow (mkApp (eq, eqargs)) (Vars.lift 1 cl), refl, sigma + mkArrow (mkApp (eq, eqargs)) Sorts.Relevant (Vars.lift 1 cl), refl, sigma (** in [tac/v: last gens..] the first (last to be run) generalization is "special" in that is it also the main argument of [tac] and is eventually @@ -743,7 +744,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only") | Context.Named.Declaration.LocalDef (name, b, ty) -> Unsafe.tclEVARS sigma <*> - tclUNIT (true, EConstr.mkLetIn (Name name,b,ty,cl), c, clr) + tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr) else Unsafe.tclEVARS sigma <*> Ssrcommon.tacMKPROD c cl >>= fun ccl -> @@ -757,7 +758,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Unsafe.tclEVARS sigma <*> Ssrcommon.tacTYPEOF p >>= fun pty -> (* TODO: check bug: cl0 no lift? *) - let ccl = EConstr.mkProd (Ssrcommon.constr_name sigma c, pty, cl0) in + let ccl = EConstr.mkProd (make_annot (Ssrcommon.constr_name sigma c) Sorts.Relevant, pty, cl0) in tclUNIT (false, ccl, p, clr) else Ssrcommon.errorstrm Pp.(str "generalized term didn't match") diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 2a2cd73df2..0ec5f1673a 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -74,11 +74,11 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let tacltop = (5,Notation_gram.E) -let pr_ssrtacarg _ _ prt = prt tacltop +let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop } -ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg } +ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } | [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram @@ -89,12 +89,12 @@ END { (* Lexically closed tactic for tacticals. *) -let pr_ssrtclarg _ _ prt tac = prt tacltop tac +let pr_ssrtclarg env sigma _ _ prt tac = prt env sigma tacltop tac } ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg - PRINTED BY { pr_ssrtclarg } + PRINTED BY { pr_ssrtclarg env sigma } | [ ssrtacarg(tac) ] -> { tac } END @@ -109,7 +109,7 @@ let add_genarg tag pr = let glob ist x = (ist, x) in let subst _ x = x in let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in - let gen_pr _ _ _ = pr in + let gen_pr env sigma _ _ _ = pr env sigma in let () = Genintern.register_intern0 wit glob in let () = Genintern.register_subst0 wit subst in let () = Geninterp.register_interp0 wit interp in @@ -146,7 +146,7 @@ let pr_list = prlist_with_sep let pr_ssrhyp _ _ _ = pr_hyp -let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp +let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in @@ -168,7 +168,7 @@ END let pr_hoi = hoik pr_hyp let pr_ssrhoi _ _ _ = pr_hoi -let wit_ssrhoirep = add_genarg "ssrhoirep" pr_hoi +let wit_ssrhoirep = add_genarg "ssrhoirep" (fun env sigma -> pr_hoi) let intern_ssrhoi ist = function | Hyp h -> Hyp (intern_hyp ist h) @@ -212,13 +212,13 @@ END let pr_rwdir = function L2R -> mt() | R2L -> str "-" -let wit_ssrdir = add_genarg "ssrdir" pr_dir +let wit_ssrdir = add_genarg "ssrdir" (fun env sigma -> pr_dir) (** Simpl switch *) let pr_ssrsimpl _ _ _ = pr_simpl -let wit_ssrsimplrep = add_genarg "ssrsimplrep" pr_simpl +let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl) let test_ssrslashnum b1 b2 strm = match Util.stream_nth 0 strm with @@ -413,7 +413,7 @@ END let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt () -let wit_ssrmmod = add_genarg "ssrmmod" pr_mmod +let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod) let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);; } @@ -643,7 +643,7 @@ and map_block map_id = function | SuffixNum _ as x -> x type ssripatrep = ssripat -let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat +let wit_ssripatrep = add_genarg "ssripatrep" (fun env sigma -> pr_ipat) let pr_ssripat _ _ _ = pr_ipat let pr_ssripats _ _ _ = pr_ipats @@ -950,13 +950,13 @@ END { -let pr_ssrintrosarg _ _ prt (tac, ipats) = - prt tacltop tac ++ pr_intros spc ipats +let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) = + prt env sigma tacltop tac ++ pr_intros spc ipats } ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) - PRINTED BY { pr_ssrintrosarg } + PRINTED BY { pr_ssrintrosarg env sigma } | [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END @@ -1007,22 +1007,22 @@ GRAMMAR EXTEND Gram { -let pr_ortacs prt = +let pr_ortacs env sigma prt = let rec pr_rec = function | [None] -> spc() ++ str "|" ++ spc() | None :: tacs -> spc() ++ str "|" ++ pr_rec tacs - | Some tac :: tacs -> spc() ++ str "| " ++ prt tacltop tac ++ pr_rec tacs + | Some tac :: tacs -> spc() ++ str "| " ++ prt env sigma tacltop tac ++ pr_rec tacs | [] -> mt() in function | [None] -> spc() | None :: tacs -> pr_rec tacs - | Some tac :: tacs -> prt tacltop tac ++ pr_rec tacs + | Some tac :: tacs -> prt env sigma tacltop tac ++ pr_rec tacs | [] -> mt() -let pr_ssrortacs _ _ = pr_ortacs +let pr_ssrortacs env sigma _ _ = pr_ortacs env sigma } -ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs } +ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs env sigma } | [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> { Some tac :: tacs } | [ ssrtacarg(tac) "|" ] -> { [Some tac; None] } | [ ssrtacarg(tac) ] -> { [Some tac] } @@ -1032,34 +1032,34 @@ END { -let pr_hintarg prt = function - | true, tacs -> hv 0 (str "[ " ++ pr_ortacs prt tacs ++ str " ]") - | false, [Some tac] -> prt tacltop tac +let pr_hintarg env sigma prt = function + | true, tacs -> hv 0 (str "[ " ++ pr_ortacs env sigma prt tacs ++ str " ]") + | false, [Some tac] -> prt env sigma tacltop tac | _, _ -> mt() -let pr_ssrhintarg _ _ = pr_hintarg +let pr_ssrhintarg env sigma _ _ = pr_hintarg env sigma } -ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg } +ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma } | [ "[" "]" ] -> { nullhint } | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } | [ ssrtacarg(arg) ] -> { mk_hint arg } END -ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg } +ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma } | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } END { -let pr_hint prt arg = - if arg = nohint then mt() else str "by " ++ pr_hintarg prt arg -let pr_ssrhint _ _ = pr_hint +let pr_hint env sigma prt arg = + if arg = nohint then mt() else str "by " ++ pr_hintarg env sigma prt arg +let pr_ssrhint env sigma _ _ = pr_hint env sigma } -ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint } +ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint env sigma } | [ ] -> { nohint } END (** The "in" pseudo-tactical *) @@ -1117,7 +1117,7 @@ let pr_clseq = function | InHypsSeq -> str " |-" | InAllHyps -> str "* |-" -let wit_ssrclseq = add_genarg "ssrclseq" pr_clseq +let wit_ssrclseq = add_genarg "ssrclseq" (fun env sigma -> pr_clseq) let pr_clausehyps = pr_list pr_spc pr_wgen let pr_ssrclausehyps _ _ _ = pr_clausehyps @@ -1220,7 +1220,7 @@ let pr_fwdkind = function | FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc () let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk -let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt +let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" (fun env sigma -> pr_fwdfmt) (* type ssrfwd = ssrfwdfmt * ssrterm *) @@ -1283,11 +1283,11 @@ END { -let pr_ssrbvar prc _ _ v = prc v +let pr_ssrbvar env sigma prc _ _ v = prc env sigma v } -ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar } +ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar env sigma } | [ ident(id) ] -> { mkCVar ~loc id } | [ "_" ] -> { mkCHole (Some loc) } END @@ -1299,11 +1299,11 @@ let bvar_lname = let open CAst in function CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous -let pr_ssrbinder prc _ _ (_, c) = prc c +let pr_ssrbinder env sigma prc _ _ (_, c) = prc env sigma c } -ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder } +ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder env sigma } | [ ssrbvar(bv) ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), @@ -1474,11 +1474,11 @@ END { -let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint +let pr_ssrhavefwd env sigma _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint env sigma prt hint } -ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd } +ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd env sigma } | [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint } | [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint } | [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint } @@ -1503,14 +1503,14 @@ let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)] | _ -> anomaly "ssrbinder is not a binder")) -let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = - pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint +let pr_ssrhavefwdwbinders env sigma _ _ prt (tr,((hpats, (fwd, hint)))) = + pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint } ARGUMENT EXTEND ssrhavefwdwbinders TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint))) - PRINTED BY { pr_ssrhavefwdwbinders } + PRINTED BY { pr_ssrhavefwdwbinders env sigma } | [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] -> { let tr, pats = trpats in let ((clr, pats), binders), simpl = pats in @@ -1522,14 +1522,14 @@ END { -let pr_ssrdoarg prc _ prt (((n, m), tac), clauses) = - pr_index n ++ pr_mmod m ++ pr_hintarg prt tac ++ pr_clauses clauses +let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) = + pr_index n ++ pr_mmod m ++ pr_hintarg env sigma prt tac ++ pr_clauses clauses } ARGUMENT EXTEND ssrdoarg TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses) - PRINTED BY { pr_ssrdoarg } + PRINTED BY { pr_ssrdoarg env sigma } | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END @@ -1537,22 +1537,22 @@ END (* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *) -let pr_seqtacarg prt = function +let pr_seqtacarg env sigma prt = function | (is_first, []), _ -> str (if is_first then "first" else "last") | tac, Some dtac -> - hv 0 (pr_hintarg prt tac ++ spc() ++ str "|| " ++ prt tacltop dtac) - | tac, _ -> pr_hintarg prt tac + hv 0 (pr_hintarg env sigma prt tac ++ spc() ++ str "|| " ++ prt env sigma tacltop dtac) + | tac, _ -> pr_hintarg env sigma prt tac -let pr_ssrseqarg _ _ prt = function - | ArgArg 0, tac -> pr_seqtacarg prt tac - | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg prt tac +let pr_ssrseqarg env sigma _ _ prt = function + | ArgArg 0, tac -> pr_seqtacarg env sigma prt tac + | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg env sigma prt tac } (* We must parse the index separately to resolve the conflict with *) (* an unindexed tactic. *) ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option)) - PRINTED BY { pr_ssrseqarg } + PRINTED BY { pr_ssrseqarg env sigma } | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END @@ -2278,7 +2278,7 @@ let pr_rwkind = function | RWdef -> str "/" | RWeq -> mt () -let wit_ssrrwkind = add_genarg "ssrrwkind" pr_rwkind +let wit_ssrrwkind = add_genarg "ssrrwkind" (fun env sigma -> pr_rwkind) let pr_rule = function | RWred s, _ -> pr_simpl s @@ -2520,13 +2520,13 @@ END { -let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) = - pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint +let pr_ssrsufffwdwbinders env sigma _ _ prt (hpats, (fwd, hint)) = + pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint } ARGUMENT EXTEND ssrsufffwd - TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders } + TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders env sigma } | [ ssrhpats(pats) ssrbinder_list(bs) ":" ast_closure_lterm(t) ssrhint(hint) ] -> { let ((clr, pats), binders), simpl = pats in let allbs = intro_id_to_binder binders @ bs in diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 7844050272..4a872be6a5 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -14,13 +14,15 @@ open Ltac_plugin val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c +val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> + (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd +val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> + (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd -val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type +val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type (* Parsing witnesses, needed to serialize ssreflect syntax *) open Ssrmatching_plugin diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 38f5b7d107..5d8c94e49b 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -57,11 +57,17 @@ let pr_guarded guard prc c = let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c -let prl_constr_expr = Ppconstr.pr_lconstr_expr +let prl_constr_expr = + let env = Global.env () in + let sigma = Evd.from_env env in + Ppconstr.pr_lconstr_expr env sigma let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c let pr_glob_constr_and_expr = function - | _, Some c -> Ppconstr.pr_constr_expr c + | _, Some c -> + let env = Global.env () in + let sigma = Evd.from_env env in + Ppconstr.pr_constr_expr env sigma c | c, None -> pr_glob_constr c let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c @@ -91,7 +97,10 @@ let pr_simpl = function (* New terms *) -let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body +let pr_ast_closure_term { body } = + let env = Global.env () in + let sigma = Evd.from_env env in + Ppconstr.pr_constr_expr env sigma body let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index f12f9fac0f..bbe7bde78b 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -12,6 +12,7 @@ open Names open Constr +open Context open Termops open Tacmach @@ -102,10 +103,10 @@ let endclausestac id_map clseq gl_id cl0 gl = forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with | Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Prod (Name id, t, c') when List.mem_assoc id id_map -> - EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> - EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') + | Prod ({binder_name=Name id} as na, t, c') when List.mem_assoc id id_map -> + EConstr.mkProd ({na with binder_name=Name (orig_id id)}, unmark t, unmark c') + | LetIn ({binder_name=Name id} as na, v, t, c') when List.mem_assoc id id_map -> + EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d083d34b52..d3f89147fa 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -152,7 +152,7 @@ let declare_one_prenex_implicit locality f = with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> - (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' + Impargs.MaximallyImplicit :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in @@ -165,7 +165,7 @@ let declare_one_prenex_implicit locality f = | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> - Impargs.declare_manual_implicits locality fref ~enriching:false [impls] + Impargs.set_implicits locality fref [impls] } @@ -198,13 +198,13 @@ type raw_glob_search_about_item = | RGlobSearchSubPattern of constr_expr | RGlobSearchString of Loc.t * string * string option -let pr_search_item = function +let pr_search_item env sigma = function | RGlobSearchString (_,s,_) -> str s - | RGlobSearchSubPattern p -> pr_constr_expr p + | RGlobSearchSubPattern p -> pr_constr_expr env sigma p let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item -let pr_ssr_search_item _ _ _ = pr_search_item +let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma (* Workaround the notation API that can only print notations *) @@ -316,7 +316,7 @@ let interp_search_notation ?loc tag okey = } ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem - PRINTED BY { pr_ssr_search_item } + PRINTED BY { pr_ssr_search_item env sigma } | [ string(s) ] -> { RGlobSearchString (loc,s,None) } | [ string(s) "%" preident(key) ] -> { RGlobSearchString (loc,s,Some key) } | [ constr_pattern(p) ] -> { RGlobSearchSubPattern p } @@ -324,14 +324,14 @@ END { -let pr_ssr_search_arg _ _ _ = - let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item p in +let pr_ssr_search_arg env sigma _ _ _ = + let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in pr_list spc pr_item } ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list - PRINTED BY { pr_ssr_search_arg } + PRINTED BY { pr_ssr_search_arg env sigma } | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> { (false, p) :: a } | [ ssr_search_item(p) ssr_search_arg(a) ] -> { (true, p) :: a } | [ ] -> { [] } @@ -432,7 +432,7 @@ let interp_search_arg arg = let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m -let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc +let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc) let pr_ssr_modlocs _ _ _ ml = if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml @@ -491,24 +491,23 @@ END { -let pr_raw_ssrhintref prc _ _ = let open CAst in function +let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function | { v = CAppExpl ((None, r,x), args) } when isCHoles args -> - prc (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args) - | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc c + prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args) + | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc env sigma c | { v = CApp ((_, c), args) } when isCxHoles args -> - prc c ++ str "|" ++ int (List.length args) - | c -> prc c + prc env sigma c ++ str "|" ++ int (List.length args) + | c -> prc env sigma c -let pr_rawhintref c = - let _, env = Pfedit.get_current_context () in +let pr_rawhintref env sigma c = match DAst.get c with | GApp (f, args) when isRHoles args -> pr_glob_constr_env env f ++ str "|" ++ int (List.length args) | _ -> pr_glob_constr_env env c -let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c +let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c -let pr_ssrhintref prc _ _ = prc +let pr_ssrhintref env sigma prc _ _ = prc env sigma let mkhintref ?loc c n = match c.CAst.v with | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n) @@ -518,9 +517,9 @@ let mkhintref ?loc c n = match c.CAst.v with ARGUMENT EXTEND ssrhintref TYPED AS constr - PRINTED BY { pr_ssrhintref } - RAW_PRINTED BY { pr_raw_ssrhintref } - GLOB_PRINTED BY { pr_glob_ssrhintref } + PRINTED BY { pr_ssrhintref env sigma } + RAW_PRINTED BY { pr_raw_ssrhintref env sigma } + GLOB_PRINTED BY { pr_glob_ssrhintref env sigma } | [ constr(c) ] -> { c } | [ constr(c) "|" natural(n) ] -> { mkhintref ~loc c n } END @@ -559,19 +558,22 @@ END { -let print_view_hints kind l = +let print_view_hints env sigma kind l = let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in - let pp_hints = pr_list spc pr_rawhintref l in + let pp_hints = pr_list spc (pr_rawhintref env sigma) l in Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY | [ "Print" "Hint" "View" ssrviewpos(i) ] -> - { match i with - | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k) + { + let sigma, env = Pfedit.get_current_context () in + match i with + | Some k -> + print_view_hints env sigma k (Ssrview.AdaptorDb.get k) | None -> - List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k)) + List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; Ssrview.AdaptorDb.Equivalence ] diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 2794696017..537fd7d7b4 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -10,6 +10,7 @@ open Util open Names +open Context open Ltac_plugin @@ -95,7 +96,7 @@ let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in let id = (* We keep the orig name for checks in "in" tcl *) match EConstr.kind_of_type (Goal.sigma gl) concl with - | Term.ProdType(Name.Name id, _, _) + | Term.ProdType({binder_name=Name.Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 552a4048b1..5eb106cc26 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -16,6 +16,7 @@ open Pp open Genarg open Stdarg open Term +open Context module CoqConstr = Constr open CoqConstr open Vars @@ -96,14 +97,20 @@ let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr let pr_constr_expr = pr_constr_expr -let prl_glob_constr_and_expr = function - | _, Some c -> prl_constr_expr c +let prl_glob_constr_and_expr env sigma = function + | _, Some c -> prl_constr_expr env sigma c | c, None -> prl_glob_constr c -let pr_glob_constr_and_expr = function - | _, Some c -> pr_constr_expr c +let pr_glob_constr_and_expr env sigma = function + | _, Some c -> pr_constr_expr env sigma c | c, None -> pr_glob_constr c -let pr_term (k, c, _) = pr_guarded (guard_term k) pr_glob_constr_and_expr c -let prl_term (k, c, _) = pr_guarded (guard_term k) prl_glob_constr_and_expr c +let pr_term (k, c, _) = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c +let prl_term (k, c, _) = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = @@ -112,7 +119,7 @@ let add_genarg tag pr = let glob ist x = (ist, x) in let subst _ x = x in let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in - let gen_pr _ _ _ = pr in + let gen_pr env sigma _ _ _ = pr env sigma in let () = Genintern.register_intern0 wit glob in let () = Genintern.register_subst0 wit subst in let () = Geninterp.register_interp0 wit interp in @@ -213,7 +220,7 @@ let unif_EQ_args env sigma pa a = loop 0 let unif_HO env ise p c = - try Evarconv.the_conv_x env p c ise + try Evarconv.unify_delay env ise p c with Evarconv.UnableToUnify(ise, err) -> raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) @@ -361,10 +368,9 @@ let isRigid c = match kind c with | _ -> false let hole_var = mkVar (Id.of_string "_") -let pr_constr_pat c0 = +let pr_constr_pat env sigma c0 = let rec wipe_evar c = if isEvar c then hole_var else map wipe_evar c in - let sigma, env = Pfedit.get_current_context () in pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) @@ -383,7 +389,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = | Context.Named.Declaration.LocalDef (x, b, t) -> d, mkNamedLetIn x (put b) (put t) c | Context.Named.Declaration.LocalAssum (x, t) -> - mkVar x :: d, mkNamedProd x (put t) c in + mkVar x.binder_name :: d, mkNamedProd x (put t) c in let a, t = Context.Named.fold_inside abs_dc ~init:([], (put @@ EConstr.Unsafe.to_constr evi.evar_concl)) @@ -416,7 +422,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir - ++ str " in " ++ pr_constr_pat rule)) + ++ str " in " ++ pr_constr_pat env ise rule)) | LetIn (_, v, _, b) -> if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a | Lambda _ -> KpatLam, f, a @@ -548,7 +554,7 @@ let match_upats_FO upats env sigma0 ise orig_c = if skip || not (closed0 c') then () else try let _ = match u.up_k with | KpatFlex -> - let kludge v = mkLambda (Anonymous, mkProp, v) in + let kludge v = mkLambda (make_annot Anonymous Sorts.Relevant, mkProp, v) in unif_FO env ise (kludge u.up_FO) (kludge c') | KpatLet -> let kludge vla = @@ -636,8 +642,8 @@ let assert_done r = let assert_done_multires r = match !r with | None -> CErrors.anomaly (str"do_once never called.") - | Some (n, xs) -> - r := Some (n+1,xs); + | Some (e, n, xs) -> + r := Some (e, n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch type subst = Environ.env -> constr -> constr -> int -> constr @@ -683,14 +689,15 @@ let mk_tpattern_matcher ?(all_instances=false) | _ -> false) | _ -> unif_EQ env sigma u.up_f in let p2t p = mkApp(p.up_f,p.up_a) in -let source () = match upats_origin, upats with +let source env = match upats_origin, upats with | None, [p] -> (if fixed_upat ise p then str"term " else str"partial term ") ++ - pr_constr_pat (p2t p) ++ spc() + pr_constr_pat env ise (p2t p) ++ spc() | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ - pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl() + pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ + pr_constr_pat env ise (p2t p) ++ fnl() | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ - pr_constr_pat rule ++ spc() + pr_constr_pat env ise rule ++ spc() | _, [] | None, _::_::_ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in let on_instance, instances = @@ -720,23 +727,23 @@ let rec uniquize = function if not all_instances then match_upats_FO upats env sigma0 ise c; failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c; raise NoMatch - with FoundUnif sigma_u -> 0,[sigma_u] + with FoundUnif sigma_u -> env,0,[sigma_u] | (NoMatch|NoProgress) when all_instances && instances () <> [] -> - 0, uniquize (instances ()) + env, 0, uniquize (instances ()) | NoMatch when (not raise_NoMatch) -> if !failed_because_of_TC then - errorstrm (source ()++strbrk"matches but type classes inference fails") + errorstrm (source env++strbrk"matches but type classes inference fails") else - errorstrm (source () ++ str "does not match any subterm of the goal") + errorstrm (source env ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in - errorstrm (str"all matches of "++source()++ + errorstrm (str"all matches of "++source env++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); let sigma, _, ({up_f = pf; up_a = pa} as u) = if all_instances then assert_done_multires upat_that_matched - else List.hd (snd(assert_done upat_that_matched)) in + else List.hd (pi3(assert_done upat_that_matched)) in (* pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *) if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else let match_EQ = match_EQ env sigma u in @@ -765,18 +772,18 @@ let rec uniquize = function mkApp (f', Array.map_left (subst_loop acc) a) in subst_loop (env,h) c) : find_P), ((fun () -> - let sigma, uc, ({up_f = pf; up_a = pa} as u) = + let env, (sigma, uc, ({up_f = pf; up_a = pa} as u)) = match !upat_that_matched with - | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch + | Some (env,_,x) -> env,List.hd x | None when raise_NoMatch -> raise NoMatch | None -> CErrors.anomaly (str"companion function never called.") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ str(String.plural !nocc " occurrence") ++ match upats_origin with - | None -> str" of" ++ spc() ++ pr_constr_pat p' + | None -> str" of" ++ spc() ++ pr_constr_pat env sigma p' | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++ - ws 4 ++ pr_constr_pat p' ++ fnl () ++ - str"of " ++ pr_constr_pat rule)) : conclude) + ws 4 ++ pr_constr_pat env sigma p' ++ fnl () ++ + str"of " ++ pr_constr_pat env sigma rule)) : conclude) type ('ident, 'term) ssrpattern = | T of 'term @@ -815,11 +822,11 @@ let pr_pattern_aux pr_constr = function pr_constr e ++ str " in " ++ pr_constr x ++ str " in " ++ pr_constr t | E_As_X_In_T (e,x,t) -> pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t -let pp_pattern (sigma, p) = - pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p +let pp_pattern env (sigma, p) = + pr_pattern_aux (fun t -> pr_constr_pat env sigma (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p let pr_cpattern = pr_term -let wit_rpatternty = add_genarg "rpatternty" pr_pattern +let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern) let glob_ssrterm gs = function | k, (_, Some c), None -> @@ -1246,8 +1253,10 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = if sigma' != sigma0 then raise NoMatch else cl, (Evd.merge_universe_context sigma' uc, t') with _ -> - errorstrm (str "partial term " ++ pr_constr_pat (EConstr.Unsafe.to_constr t) - ++ str " does not match any subterm of the goal") + errorstrm (str "partial term " ++ + pr_constr_pat env sigma + (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) ++ + str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in @@ -1286,7 +1295,7 @@ let ssrpatterntac _ist arg gl = let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index ff2c900130..1143bcc813 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -46,7 +46,7 @@ type ('ident, 'term) ssrpattern = | E_As_X_In_T of 'term * 'ident * 'term type pattern = evar_map * (constr, constr) ssrpattern -val pp_pattern : pattern -> Pp.t +val pp_pattern : env -> pattern -> Pp.t (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) @@ -222,7 +222,7 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern -val pr_constr_pat : constr -> Pp.t +val pr_constr_pat : env -> evar_map -> constr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 13e0bcbd47..73a2b99434 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -37,5 +37,6 @@ END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + { let (sigma, env) = Pfedit.get_current_context () in + vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index 1e06cd8ddb..171e0e213d 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -21,5 +21,6 @@ open Stdarg VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } + { let (sigma, env) = Pfedit.get_current_context () in + vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) } END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 0c6d2ac0d1..525056e5f1 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -77,8 +77,7 @@ let locate_int63 () = Some (mkRefC q_int63) else None -let has_type f ty = - let (sigma, env) = Pfedit.get_current_context () in +let has_type env sigma f ty = let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false @@ -95,7 +94,7 @@ let type_error_of g ty = str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).") -let vernac_numeral_notation local ty f g scope opts = +let vernac_numeral_notation env sigma local ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in @@ -112,35 +111,35 @@ let vernac_numeral_notation local ty f g scope opts = (* Check the type of f *) let to_kind = match int_ty with - | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct - | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option - | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option + | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option | _ -> match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct - | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option + | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct - | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option + | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct + | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option | _ -> type_error_to f ty in (* Check the type of g *) let of_kind = match int_ty with - | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct - | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option - | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option + | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option | _ -> match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct - | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option + | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct - | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option + | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct + | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option | _ -> type_error_of g ty in let o = { to_kind; to_ty; of_kind; of_ty; diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index f96b8321f8..b14ed18497 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -14,4 +14,6 @@ open Notation (** * Numeral notation *) -val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit +val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag -> + qualid -> qualid -> qualid -> + Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 12ee4c6eda..5fae696d58 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -32,8 +32,7 @@ let q_option () = qualid_of_ref "core.option.type" let q_list () = qualid_of_ref "core.list.type" let q_byte () = qualid_of_ref "core.byte.type" -let has_type f ty = - let (sigma, env) = Pfedit.get_current_context () in +let has_type env sigma f ty = let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false @@ -48,7 +47,7 @@ let type_error_of g ty = (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") -let vernac_string_notation local ty f g scope = +let vernac_string_notation env sigma local ty f g scope = let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in let cbyte = cref (q_byte ()) in @@ -66,18 +65,18 @@ let vernac_string_notation local ty f g scope = let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = - if has_type f (arrow clist_byte cty) then ListByte, Direct - else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option - else if has_type f (arrow cbyte cty) then Byte, Direct - else if has_type f (arrow cbyte (opt cty)) then Byte, Option + if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct + else if has_type env sigma f (arrow clist_byte (opt cty)) then ListByte, Option + else if has_type env sigma f (arrow cbyte cty) then Byte, Direct + else if has_type env sigma f (arrow cbyte (opt cty)) then Byte, Option else type_error_to f ty in (* Check the type of g *) let of_kind = - if has_type g (arrow cty clist_byte) then ListByte, Direct - else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option - else if has_type g (arrow cty cbyte) then Byte, Direct - else if has_type g (arrow cty (opt cbyte)) then Byte, Option + if has_type env sigma g (arrow cty clist_byte) then ListByte, Direct + else if has_type env sigma g (arrow cty (opt clist_byte)) then ListByte, Option + else if has_type env sigma g (arrow cty cbyte) then Byte, Direct + else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option else type_error_of g ty in let o = { to_kind = to_kind; diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli index 9a0174abf2..e81de603d9 100644 --- a/plugins/syntax/string_notation.mli +++ b/plugins/syntax/string_notation.mli @@ -13,4 +13,6 @@ open Vernacexpr (** * String notation *) -val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit +val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag -> + qualid -> qualid -> qualid -> + Notation_term.scope_name -> unit |