From 846b74275511bd89c2f3abe19245133050d2199c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2017 20:11:01 +0100 Subject: [constrexpr] Make patterns use Loc.located for location information This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created. --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d335836dfc..daa5cbb3fb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -760,7 +760,7 @@ let rec add_args id new_args b = List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal + List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc:loc @@ (cpl,add_args id new_args e)) cal ) | CLetTuple(loc,nal,(na,b_option),b1,b2) -> CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), -- cgit v1.2.3 From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Jan 2017 01:27:40 +0100 Subject: [location] Use Loc.located for constr_expr. This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. --- plugins/funind/glob_term_to_relation.ml | 31 +++++----- plugins/funind/indfun.ml | 105 ++++++++++++++++---------------- plugins/funind/merge.ml | 4 +- 3 files changed, 67 insertions(+), 73 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7dc8691311..4b942c989e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1247,16 +1247,15 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_ in List.rev !l -let rec rebuild_return_type rt = +let rec rebuild_return_type (loc, rt) = match rt with - | Constrexpr.CProdN(loc,n,t') -> - Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,v,t,t') -> - Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') - | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], - Constrexpr.Default Decl_kinds.Explicit,rt], - Constrexpr.CSort(Loc.ghost,GType [])) - + | Constrexpr.CProdN(n,t') -> + Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t') + | Constrexpr.CLetIn(na,v,t,t') -> + Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.ghost,Anonymous], + Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt], + Loc.tag @@ Constrexpr.CSort(GType [])) let do_build_inductive evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) @@ -1307,13 +1306,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + Loc.tag @@ Constrexpr.CProdN + ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1375,13 +1373,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + Loc.tag @@ Constrexpr.CProdN + ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index daa5cbb3fb..6ee7553231 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -469,8 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in let unbounded_eq = let f_app_args = - Constrexpr.CAppExpl - (Loc.ghost, + Loc.tag @@ Constrexpr.CAppExpl( (None,(Ident (Loc.ghost,fname)),None) , (List.map (function @@ -481,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), + Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in @@ -589,15 +588,15 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) -> rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal,typ with + match nal, snd typ with | [], _ -> rebuild_bl (aux,assoc) bl' typ - | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ - | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> + | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ + | _,CProdN((nal',bk',nal't)::rest,typ') -> let lnal' = List.length nal' in if lnal' >= lnal then @@ -607,15 +606,15 @@ let rec rebuild_bl (aux,assoc) bl typ = rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' - else if List.is_empty new_nal' - then CProdN(Loc.ghost,rest,typ') - else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ')) + else Loc.tag @@ if List.is_empty new_nal' + then CProdN(rest,typ') + else CProdN(((new_nal',bk',nal't)::rest),typ')) else let captured_nal,non_captured_nal = List.chop lnal' nal in let nassoc = make_assoc assoc nal' captured_nal in let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) + bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ')) | _ -> assert false let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ @@ -726,67 +725,65 @@ let do_generate_principle pconstants on_error register_built interactive_proof in () -let rec add_args id new_args b = - match b with - | CRef (r,_) -> - begin match r with +let rec add_args id new_args = Loc.map (function + | CRef (r,_) as b -> + begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> - CAppExpl(Loc.ghost,(None,r,None),new_args) + CAppExpl((None,r,None),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") - | CProdN(loc,nal,b1) -> - CProdN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + | CProdN(nal,b1) -> + CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLambdaN(loc,nal,b1) -> - CLambdaN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + | CLambdaN(nal,b1) -> + CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,t,b2) -> - CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl(loc,(pf,r,us),exprl) -> + | CLetIn(na,b1,t,b2) -> + CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) + | CAppExpl((pf,r,us),exprl) -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> - CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl) + CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) + | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) end - | CApp(loc,(pf,b),bl) -> - CApp(loc,(pf,add_args id new_args b), + | CApp((pf,b),bl) -> + CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) - | CCases(loc,sty,b_option,cel,cal) -> - CCases(loc,sty,Option.map (add_args id new_args) b_option, + | CCases(sty,b_option,cel,cal) -> + CCases(sty,Option.map (add_args id new_args) b_option, List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc:loc @@ (cpl,add_args id new_args e)) cal + List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc @@ (cpl,add_args id new_args e)) cal ) - | CLetTuple(loc,nal,(na,b_option),b1,b2) -> - CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), + | CLetTuple(nal,(na,b_option),b1,b2) -> + CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), add_args id new_args b1, add_args id new_args b2 ) - | CIf(loc,b1,(na,b_option),b2,b3) -> - CIf(loc,add_args id new_args b1, + | CIf(b1,(na,b_option),b2,b3) -> + CIf(add_args id new_args b1, (na,Option.map (add_args id new_args) b_option), add_args id new_args b2, add_args id new_args b3 ) - | CHole _ -> b - | CPatVar _ -> b - | CEvar _ -> b - | CSort _ -> b - | CCast(loc,b1,b2) -> - CCast(loc,add_args id new_args b1, + | CHole _ + | CPatVar _ + | CEvar _ + | CPrim _ + | CSort _ as b -> b + | CCast(b1,b2) -> + CCast(add_args id new_args b1, Miscops.map_cast_type (add_args id new_args) b2) - | CRecord (loc, pars) -> - CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CRecord pars -> + CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") - | CPrim _ -> b | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") + ) exception Stop of Constrexpr.constr_expr @@ -797,8 +794,8 @@ let rec chop_n_arrow n t = if n <= 0 then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) - match t with - | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : + match snd t with + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -816,8 +813,8 @@ let rec chop_n_arrow n t = then aux (n - nal_l) nal_ta' else - let new_t' = - Constrexpr.CProdN(Loc.ghost, + let new_t' = Loc.tag @@ + Constrexpr.CProdN( ((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') @@ -832,8 +829,8 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = - match b with - | Constrexpr.CLambdaN (loc, (nal_ta), b') -> + match snd b with + | Constrexpr.CLambdaN ((nal_ta), b') -> begin let n = (List.fold_left (fun n (nal,_,_) -> @@ -872,8 +869,8 @@ let make_graph (f_ref:global_reference) = in let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = - match b with - | Constrexpr.CFix(loc,l_id,fixexprl) -> + match snd b with + | Constrexpr.CFix(l_id,fixexprl) -> let l = List.map (fun (id,(n,recexp),bl,t,b) -> @@ -885,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> + (fun (loc,n) -> Loc.tag ~loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f1ca575856..29de56478b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -73,7 +73,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in + let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.ghost,id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when CErrors.noncritical e -> false @@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + Loc.tag @@ CProdN ([[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in -- cgit v1.2.3 From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Jan 2017 13:02:55 +0100 Subject: [location] Move Glob_term.cases_pattern to located. We continue the uniformization pass. No big news here, trying to be minimally invasive. --- plugins/funind/glob_term_to_relation.ml | 15 +++++---- plugins/funind/glob_termops.ml | 59 +++++++++++++++++---------------- plugins/funind/recdef.ml | 6 ++-- 3 files changed, 41 insertions(+), 39 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4b942c989e..85d465a4bb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -345,12 +345,12 @@ let raw_push_named (na,raw_value,raw_typ) env = let add_pat_variables pat typ env : Environ.env = - let rec add_pat_variables env pat typ : Environ.env = + let rec add_pat_variables env (loc, pat) typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env - | PatCstr(_,c,patl,na) -> + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false @@ -398,11 +398,11 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term_and_type env typ = Loc.with_unloc (function + | PatVar Anonymous -> assert false + | PatVar (Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) @@ -430,6 +430,7 @@ let rec pattern_to_term_and_type env typ = function mkGApp(mkGRef(ConstructRef constr), implicit_args@patl_as_term ) + ) (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 99f50437b9..51ca8c4717 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -194,19 +194,19 @@ let change_vars = -let rec alpha_pat excluded pat = +let rec alpha_pat excluded (loc, pat) = match pat with - | PatVar(loc,Anonymous) -> + | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty - | PatVar(loc,Name id) -> + (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - PatVar(loc,Name new_id),(new_id::excluded), + (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else pat,excluded,Id.Map.empty - | PatCstr(loc,constr,patl,na) -> + else (Loc.tag ~loc pat),excluded,Id.Map.empty + | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> @@ -223,7 +223,7 @@ let rec alpha_pat excluded pat = ([],new_excluded,map) patl in - PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map + (Loc.tag ~loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -241,12 +241,12 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = - let rec get_pattern_id pat = + let rec get_pattern_id (loc, pat) = match pat with - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> + | PatVar(Anonymous) -> assert false + | PatVar(Name id) -> [id] - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> List.fold_right (fun pat idl -> let idl' = get_pattern_id pat in @@ -425,11 +425,11 @@ let is_free_in id = -let rec pattern_to_term = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term pt = Loc.with_unloc (function + | PatVar Anonymous -> assert false + | PatVar(Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) @@ -448,7 +448,7 @@ let rec pattern_to_term = function mkGApp(mkGRef(Globnames.ConstructRef constr), implicit_args@patl_as_term ) - + ) pt let replace_var_by_term x_id term = @@ -533,8 +533,8 @@ let rec are_unifiable_aux = function | [] -> () | eq::eqs -> match eq with - | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs + | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -555,8 +555,8 @@ let rec eq_cases_pattern_aux = function | [] -> () | eq::eqs -> match eq with - | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs + | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -576,10 +576,11 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = function - | PatVar(_,Anonymous) -> ids - | PatVar(_,Name id) -> Id.Set.add id ids - | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl + let rec ids_of_pat ids = Loc.with_unloc (function + | PatVar Anonymous -> ids + | PatVar(Name id) -> Id.Set.add id ids + | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl + ) in ids_of_pat Id.Set.empty @@ -679,12 +680,12 @@ let zeta_normalize = let expand_as = - let rec add_as map pat = + let rec add_as map (loc, pat) = match pat with | PatVar _ -> map - | PatCstr(_,_,patl,Name id) -> - Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl) - | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl + | PatCstr(_,patl,Name id) -> + Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl) + | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map rt = match rt with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1e405d2c90..ee7b33227c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -193,10 +193,10 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = (d0,RegularStyle,None, [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), (Anonymous,None)], - [d0, [v_id], [PatCstr(d0,(destIndRef + [d0, [v_id], [d0,PatCstr((destIndRef (delayed_force coq_sig_ref),1), - [PatVar(d0, Name v_id); - PatVar(d0, Anonymous)], + [d0, PatVar(Name v_id); + d0, PatVar(Anonymous)], Anonymous)], GVar(d0,v_id)]) in -- cgit v1.2.3 From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 14:23:53 +0100 Subject: [location] Switch glob_constr to Loc.located --- plugins/funind/glob_term_to_relation.ml | 102 +++++----- plugins/funind/glob_termops.ml | 328 +++++++++++++++----------------- plugins/funind/glob_termops.mli | 7 +- plugins/funind/indfun.ml | 20 +- plugins/funind/indfun_common.ml | 10 +- plugins/funind/merge.ml | 52 ++--- plugins/funind/recdef.ml | 18 +- 7 files changed, 259 insertions(+), 278 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 85d465a4bb..07a0d5a505 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -274,10 +274,10 @@ let make_discr_match_el = *) let make_discr_match_brl i = List.map_i - (fun j (_,idl,patl,_) -> + (fun j (_,(idl,patl,_)) -> Loc.tag @@ if Int.equal j i - then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) - else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref)) + then (idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -464,13 +464,13 @@ let rec pattern_to_term_and_type env typ = Loc.with_unloc (function *) -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = +let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + | _, GRef _ | _, GVar _ | _, GEvar _ | _, GPatVar _ | _, GSort _ | _, GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | GApp(_,_,_) -> + | _, GApp(_,_) -> let f,args = glob_decompose_app rt in let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) @@ -482,20 +482,20 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f with + match Loc.obj f with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> + | u::l -> Loc.tag @@ match t with - | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,None,aux b l) + | loc, GLambda(na,_,nat,b) -> + GLetIn(na,u,None,aux b l) | _ -> - GApp(Loc.ghost,t,l) + GApp(t,l) in build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Id.Set.mem id funnames -> + | 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], add [res] and its "value" (i.e. [res v1 ... vn]) to each @@ -536,7 +536,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,v,t,b) -> + | GLetIn(n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -550,7 +550,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (GVar(Loc.ghost,id)) + (Loc.tag @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -568,7 +568,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res - | GCast(_,b,_) -> + | GCast(b,_) -> (* for an applied cast we just trash the cast part and restart the work. @@ -579,7 +579,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | GLambda(_,n,_,t,b) -> + | _, GLambda(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -594,7 +594,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | GProd(_,n,_,t,b) -> + | _, GProd(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -604,13 +604,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | GLetIn(loc,n,v,typ,b) -> + | loc, GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in + let v = match typ with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env 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) (EConstr.of_constr v_as_constr) in @@ -622,13 +622,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | GCases(_,_,_,el,brl) -> + | _, 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 - | GIf(_,b,(na,e_option),lhs,rhs) -> + | _, 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) (EConstr.of_constr b_as_constr) in let (ind,_) = @@ -642,7 +642,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Int.equal (Array.length case_pats) 2); let brl = List.map_i - (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) + (fun i x -> Loc.tag ([],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -651,7 +651,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | GLetTuple(_,nal,_,b,e) -> + | _, GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = List.map @@ -673,14 +673,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); let br = - (Loc.ghost,[],[case_pats.(0)],e) + (Loc.ghost,([],[case_pats.(0)],e)) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr end - | GRec _ -> error "Not handled GRec" - | GCast(_,b,_) -> + | _, GRec _ -> error "Not handled GRec" + | _, GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) @@ -740,7 +740,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve | [] -> (* computed_branches *) {result = [];to_avoid = avoid} | br::brl' -> (* alpha conversion to prevent name clashes *) - let _,idl,patl,return = alpha_br avoid br in + let _,(idl,patl,return) = alpha_br avoid br in let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *) (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) @@ -862,9 +862,9 @@ let is_res id = -let same_raw_term rt1 rt2 = +let same_raw_term (_,rt1) (_,rt2) = match rt1,rt2 with - | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2 + | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -897,15 +897,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in match rt with - | GProd(_,n,k,t,b) -> + | _, GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin match t with - | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> + | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id -> begin match args' with - | (GVar(_,this_relname))::args' -> + | (_, (GVar this_relname))::args' -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious @@ -927,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt]) + | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt]) when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -964,9 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = - GApp(Loc.ghost, - GRef (Loc.ghost,Globnames.IndRef (fst ind),None), + let rt_typ = Loc.tag @@ + GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] env (Evd.from_env env) @@ -976,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) + Loc.tag ~loc:loc1 @@ GApp(Loc.tag ~loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ~loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1045,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2]) + | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2]) when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -1096,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Id.Set.filter not_free_in_t id_to_exclude) | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end - | GLambda(_,n,k,t,b) -> + | _, GLambda(n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -1115,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + Loc.tag @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(loc,n,v,t,b) -> + | loc, GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in + let t = match t with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1138,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> Loc.tag @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end - | GLetTuple(_,nal,(na,rto),t,b) -> + | _, GLetTuple(nal,(na,rto),t,b) -> assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in @@ -1164,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - GLetTuple(Loc.ghost,nal,(na,None),t,new_b), + Loc.tag @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1190,16 +1189,16 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params = function +let rec compute_cst_params relnames params gt = Loc.with_unloc (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames -> + | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) - | GApp(_,f,args) -> + | GApp(f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | GLetIn(_,_,v,t,b) -> + | GLetIn(_,v,t,b) -> let v_params = compute_cst_params relnames params v in let t_params = Option.fold_left (compute_cst_params relnames) v_params t in compute_cst_params relnames t_params b @@ -1210,10 +1209,11 @@ let rec compute_cst_params relnames params = function | GHole _ -> params | GIf _ | GRec _ | GCast _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) + ) gt and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + | ((Name id,_,None) as param)::params',(_, GVar id')::rtl' when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 51ca8c4717..01e607412a 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,16 +10,16 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = GRef(Loc.ghost,ref,None) -let mkGVar id = GVar(Loc.ghost,id) -let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) -let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) -let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) -let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) -let mkGSort s = GSort(Loc.ghost,s) -let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) +let mkGRef ref = Loc.tag @@ GRef(ref,None) +let mkGVar id = Loc.tag @@ GVar(id) +let mkGApp(rt,rtl) = Loc.tag @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = Loc.tag @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = Loc.tag @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = Loc.tag @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = Loc.tag @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = Loc.tag @@ GSort(s) +let mkGHole () = Loc.tag @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -27,7 +27,7 @@ let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) *) let glob_decompose_prod = let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> + | _, GProd(n,k,t,b) -> glob_decompose_prod ((n,t)::args) b | rt -> args,rt in @@ -35,9 +35,9 @@ let glob_decompose_prod = let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> + | _, GProd(n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,b,t,c) -> + | _, GLetIn(n,b,t,c) -> glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in @@ -59,7 +59,7 @@ let glob_decompose_prod_n n = if i<=0 then args,c else match c with - | GProd(_,n,_,t,b) -> + | _, GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in @@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n = if i<=0 then args,c else match c with - | GProd(_,n,_,t,b) -> + | _, GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,b,t,c) -> + | _, GLetIn(n,b,t,c) -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in @@ -84,7 +84,7 @@ let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | GApp(_,rt,rtl) -> + | _, GApp(rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -120,75 +120,70 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - match rt with - | GRef _ -> rt - | GVar(loc,id) -> + Loc.map (function + | GRef _ as x -> x + | GVar id -> let new_id = try Id.Map.find id mapping with Not_found -> id in - GVar(loc,new_id) - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - change_vars mapping rt', + GVar(new_id) + | GEvar _ as x -> x + | GPatVar _ as x -> x + | GApp(rt',rtl) -> + GApp(change_vars mapping rt', List.map (change_vars mapping) rtl ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(name,k,t,b) -> + GLambda(name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(name,k,t,b) -> + GProd( name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,typ,b) -> - GLetIn(loc, - name, + | GLetIn(name,def,typ,b) -> + GLetIn(name, change_vars mapping def, Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) - | GLetTuple(loc,nal,(na,rto),b,e) -> + | GLetTuple(nal,(na,rto),b,e) -> let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - GLetTuple(loc, - nal, + GLetTuple(nal, (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, - change_vars mapping b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(change_vars mapping b, (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) | GRec _ -> error "Local (co)fixes are not supported" - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,change_vars mapping b, + | GSort _ as x -> x + | GHole _ as x -> x + | GCast(b,c) -> + GCast(change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) - and change_vars_br mapping ((loc,idl,patl,res) as br) = + ) rt + and change_vars_br mapping ((loc,(idl,patl,res)) as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in if Id.Map.is_empty new_mapping then br - else (loc,idl,patl,change_vars new_mapping res) + else (loc,(idl,patl,change_vars new_mapping res)) in change_vars @@ -259,30 +254,30 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] -let rec alpha_rt excluded rt = - let new_rt = +let rec alpha_rt excluded (loc, rt) = + let new_rt = Loc.tag ~loc @@ match rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt - | GLambda(loc,Anonymous,k,t,b) -> + | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Anonymous,k,t,b) -> + GLambda(Name new_id,k,new_t,new_b) + | GProd(Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,b,t,c) -> + GProd(Anonymous,k,new_t,new_b) + | GLetIn(Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in let new_t = Option.map (alpha_rt excluded) t in let new_c = alpha_rt excluded c in - GLetIn(loc,Anonymous,new_b,new_t,new_c) - | GLambda(loc,Name id,k,t,b) -> + GLetIn(Anonymous,new_b,new_t,new_c) + | GLambda(Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if Id.equal new_id id - then t,b + then t, b else let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in (t,replace b) @@ -290,8 +285,8 @@ let rec alpha_rt excluded rt = let new_excluded = new_id::excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Name id,k,t,b) -> + GLambda(Name new_id,k,new_t,new_b) + | GProd(Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -303,8 +298,8 @@ let rec alpha_rt excluded rt = in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,b,t,c) -> + GProd(Name new_id,k,new_t,new_b) + | GLetIn(Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in let c = if Id.equal new_id id then c @@ -314,10 +309,9 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in let new_t = Option.map (alpha_rt new_excluded) t in let new_c = alpha_rt new_excluded c in - GLetIn(loc,Name new_id,new_b,new_t,new_c) - + GLetIn(Name new_id,new_b,new_t,new_c) - | GLetTuple(loc,nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> let rev_new_nal,new_excluded,mapping = List.fold_left (fun (nal,excluded,mapping) na -> @@ -344,14 +338,14 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded new_t in let new_b = alpha_rt new_excluded new_b in let new_rto = Option.map (alpha_rt new_excluded) new_rto in - GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | GCases(loc,sty,infos,el,brl) -> + GLetTuple(new_nal,(na,new_rto),new_t,new_b) + | GCases(sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | GIf(loc,b,(na,e_o),lhs,rhs) -> - GIf(loc,alpha_rt excluded b, + GCases(sty,infos,new_el,List.map (alpha_br excluded) brl) + | GIf(b,(na,e_o),lhs,rhs) -> + GIf(alpha_rt excluded b, (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs @@ -359,66 +353,65 @@ let rec alpha_rt excluded rt = | GRec _ -> error "Not handled GRec" | GSort _ -> rt | GHole _ -> rt - | GCast (loc,b,c) -> - GCast(loc,alpha_rt excluded b, + | GCast (b,c) -> + GCast(alpha_rt excluded b, Miscops.map_cast_type (alpha_rt excluded) c) - | GApp(loc,f,args) -> - GApp(loc, - alpha_rt excluded f, + | GApp(f,args) -> + GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) in new_rt -and alpha_br excluded (loc,ids,patl,res) = +and alpha_br excluded (loc,(ids,patl,res)) = let new_patl,new_excluded,mapping = alpha_patl excluded patl in let new_ids = List.fold_right raw_get_pattern_id new_patl [] in let new_excluded = new_ids@excluded in let renamed_res = change_vars mapping res in let new_res = alpha_rt new_excluded renamed_res in - (loc,new_ids,new_patl,new_res) + (loc,(new_ids,new_patl,new_res)) (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in = function + let rec is_free_in (loc, gt) = match gt with | GRef _ -> false - | GVar(_,id') -> Id.compare id' id == 0 + | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false | GPatVar _ -> false - | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> + | GApp(rt,rtl) -> List.exists is_free_in (rt::rtl) + | GLambda(n,_,t,b) | GProd(n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | GLetIn(_,n,b,t,c) -> + | GLetIn(n,b,t,c) -> let check_in_c = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) - | GCases(_,_,_,el,brl) -> + | GCases(_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | GLetTuple(_,nal,_,b,t) -> + | GLetTuple(nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal) in is_free_in t || (check_in_nal && is_free_in b) - | GIf(_,cond,_,br1,br2) -> + | GIf(cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t - | GCast (_,b,CastCoerce) -> is_free_in b - and is_free_in_br (_,ids,_,rt) = + | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t + | GCast (b,CastCoerce) -> is_free_in b + and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt in is_free_in @@ -452,60 +445,55 @@ let rec pattern_to_term pt = Loc.with_unloc (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern rt = + let rec replace_var_by_pattern (loc, rt) = Loc.tag ~loc @@ match rt with | GRef _ -> rt - | GVar(_,id) when Id.compare id x_id == 0 -> term + | GVar id when Id.compare id x_id == 0 -> Loc.obj term | GVar _ -> rt | GEvar _ -> rt | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - replace_var_by_pattern rt', + | GApp(rt',rtl) -> + GApp(replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | GLambda(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLambda(name,k,t,b) -> + GLambda(name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GProd(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GProd(name,k,t,b) -> + GProd( name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,typ,b) -> - GLetIn(loc, - name, + | GLetIn(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(name,def,typ,b) -> + GLetIn(name, replace_var_by_pattern def, Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) - | GLetTuple(_,nal,_,_,_) + | GLetTuple(nal,_,_,_) when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal -> rt - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, + | GLetTuple(nal,(na,rto),def,b) -> + GLetTuple(nal, (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, replace_var_by_pattern b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs @@ -513,13 +501,13 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,replace_var_by_pattern b, + | GCast(b,c) -> + GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) - and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = + and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl then br - else (loc,idl,patl,replace_var_by_pattern res) + else (loc,(idl,patl,replace_var_by_pattern res)) in replace_var_by_pattern @@ -590,22 +578,22 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc c = + let rec ids_of_glob_constr acc (loc, c) = let idof = id_of_name in match c with - | GVar (_,id) -> id::acc - | GApp (loc,g,args) -> + | GVar id -> id::acc + | GApp (g,args) -> ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc - | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc - | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc - | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc - | GLetTuple (_,nal,(na,po),b,c) -> + | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc + | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc + | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc + | GLetTuple (nal,(na,po),b,c) -> List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCases (loc,sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) + | GCases (sty,rtntypopt,tml,brchl) -> + List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl) | GRec _ -> failwith "Fix inside a constructor branch" | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in @@ -617,49 +605,46 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term rt = + let rec zeta_normalize_term (loc, rt) = Loc.tag ~loc @@ match rt with | GRef _ -> rt | GVar _ -> rt | GEvar _ -> rt | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - zeta_normalize_term rt', + | GApp(rt',rtl) -> + GApp(zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(name,k,t,b) -> + GLambda(name, k, zeta_normalize_term t, zeta_normalize_term b ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(name,k,t,b) -> + GProd(name, k, zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,typ,b) -> - zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, + | GLetIn(Name id,def,typ,b) -> + Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b) + | GLetIn(Anonymous,def,typ,b) -> + Loc.obj @@ zeta_normalize_term b + | GLetTuple(nal,(na,rto),def,b) -> + GLetTuple(nal, (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, zeta_normalize_term b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(zeta_normalize_term b, (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs @@ -667,11 +652,11 @@ let zeta_normalize = | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,zeta_normalize_term b, + | GCast(b,c) -> + GCast(zeta_normalize_term b, Miscops.map_cast_type zeta_normalize_term c) - and zeta_normalize_br (loc,idl,patl,res) = - (loc,idl,patl,zeta_normalize_term res) + and zeta_normalize_br (loc,(idl,patl,res)) = + (loc,(idl,patl,zeta_normalize_term res)) in zeta_normalize_term @@ -687,33 +672,34 @@ let expand_as = Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map rt = + let rec expand_as map (loc, rt) = + Loc.tag ~loc @@ match rt with | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt - | GVar(_,id) -> + | GVar id -> begin try - Id.Map.find id map + Loc.obj @@ Id.Map.find id map with Not_found -> rt end - | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) - | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) - | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) - | GLetTuple(loc,nal,(na,po),v,b) -> - GLetTuple(loc,nal,(na,Option.map (expand_as map) po), + | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) + | GLambda(na,k,t,b) -> GLambda(na,k,expand_as map t, expand_as map b) + | GProd(na,k,t,b) -> GProd(na,k,expand_as map t, expand_as map b) + | GLetIn(na,v,typ,b) -> GLetIn(na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) + | GLetTuple(nal,(na,po),v,b) -> + GLetTuple(nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) - | GIf(loc,e,(na,po),br1,br2) -> - GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + | GIf(e,(na,po),br1,br2) -> + GIf(expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" - | GCast(loc,b,c) -> - GCast(loc,expand_as map b, + | GCast(b,c) -> + GCast(expand_as map b, Miscops.map_cast_type (expand_as map) c) - | GCases(loc,sty,po,el,brl) -> - GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + | GCases(sty,po,el,brl) -> + GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - and expand_as_br map (loc,idl,cpl,rt) = - (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) + and expand_as_br map (loc,(idl,cpl,rt)) = + (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) in expand_as Id.Map.empty diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 84359a36b7..25d79582f3 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -82,11 +82,8 @@ val alpha_rt : Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Id.t list -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr - + Glob_term.cases_clause -> + Glob_term.cases_clause (* Reduction function *) val replace_var_by_term : diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6ee7553231..cad96946ca 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -190,18 +190,18 @@ let build_newrecursive l = let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names = function - | GVar(_,id) -> check_id id names + let rec lookup names (loc, gt) = match gt with + | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false - | GCast(_,b,_) -> lookup names b + | GCast(b,_) -> lookup names b | GRec _ -> error "GRec not handled" - | GIf(_,b,_,lhs,rhs) -> + | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> + | GProd(na,_,t,b) | GLambda(na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b - | GLetIn(_,na,b,t,c) -> + | GLetIn(na,b,t,c) -> lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c - | GLetTuple(_,nal,_,t,b) -> lookup names t || + | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left (fun acc na -> Nameops.name_fold Id.Set.remove na acc) @@ -209,11 +209,11 @@ let is_rec names = nal ) b - | GApp(_,f,args) -> List.exists (lookup names) (f::args) - | GCases(_,_,_,el,brl) -> + | GApp(f,args) -> List.exists (lookup names) (f::args) + | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl - and lookup_br names (_,idl,_,rt) = + and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7b0d7d27d7..8f0c986242 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -69,9 +69,9 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b + match Loc.obj rt with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -83,8 +83,8 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + match Loc.obj rt with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 29de56478b..9dc1d48df3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -66,7 +66,7 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | GVar (_,x) -> Id.equal x f + | _, GVar x -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -504,40 +504,40 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array exception NoMerge -let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = +let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1 , c2 with - | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + match c1, c2 with + | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) - | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge - | GLetIn(_,nme,bdy,typ,trm) , _ -> + Loc.tag @@ GApp ((Loc.tag @@ GVar shift.ident) , args) + | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge + | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in - let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) - | _, GLetIn(_,nme,bdy,typ,trm) -> + let newtrm = merge_app trm (loc2, c2) id1 id2 shift filter_shift_stable in + Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in - let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in + Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge -let rec merge_app_unsafe c1 c2 shift filter_shift_stable = +let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with - | GApp(_,f1, arr1), GApp(_,f2,arr2) -> + | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) + Loc.tag @@ GApp (Loc.tag @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,typ,trm) , _ -> + | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in - let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) - | _, GLetIn(_,nme,bdy,typ,trm) -> + let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in + Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in - let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in + Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -550,14 +550,14 @@ let rec merge_rec_hyps shift accrec filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (GApp(_,i,args) as ind)) + | (nme,x,Some (_, GApp(i,args) as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some (_, GApp(f, largs) as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -573,7 +573,7 @@ let find_app (nme:Id.t) ltyp = (List.map (fun x -> match x with - | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some (_, GApp(f,_)) when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -633,7 +633,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> (match t1 with - | GApp(_,f,carr) when isVarf ind1name f -> + | _, GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = @@ -864,7 +864,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = | LocalAssum (nme,t) -> let t = EConstr.of_constr t in let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - GProd (Loc.ghost,nme,Explicit,traw,t2) + Loc.tag @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ee7b33227c..c796fe7a2d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -172,7 +172,6 @@ let simpl_iter clause = let (value_f:Constr.constr list -> global_reference -> Constr.constr) = let open Term in fun al fterm -> - let d0 = Loc.ghost in let rev_x_id_l = ( List.fold_left @@ -189,16 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - GCases - (d0,RegularStyle,None, - [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), + Loc.tag @@ + GCases + (RegularStyle,None, + [Loc.tag @@ GApp(Loc.tag @@ GRef(fterm,None), List.rev_map (fun x_id -> Loc.tag @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [d0, [v_id], [d0,PatCstr((destIndRef - (delayed_force coq_sig_ref),1), - [d0, PatVar(Name v_id); - d0, PatVar(Anonymous)], - Anonymous)], - GVar(d0,v_id)]) + [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous], + Anonymous)], + Loc.tag @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context -- cgit v1.2.3 From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 15:06:26 +0100 Subject: [location] Use located in misctypes. --- plugins/funind/g_indfun.ml4 | 4 ++-- plugins/funind/invfun.ml | 4 ++-- plugins/funind/recdef.ml | 10 ++++------ 3 files changed, 8 insertions(+), 10 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0dccd25d75..129c8dc165 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -24,8 +24,8 @@ open Pltac DECLARE PLUGIN "recdef_plugin" let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 94ec0a898a..8da4f9233e 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -31,8 +31,8 @@ module RelDecl = Context.Rel.Declaration let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c796fe7a2d..25daedd0e4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -882,9 +882,8 @@ let rec make_rewrite_list expr_info max = function Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - f_S max]) false) g) ) + ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); + Loc.tag @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -910,9 +909,8 @@ let make_rewrite expr_info l hp max = (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - f_S (f_S max)]) false)) g) + ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); + Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ -- cgit v1.2.3 From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- plugins/funind/glob_term_to_relation.ml | 22 ++++++++++------------ plugins/funind/indfun.ml | 22 +++++++++++----------- plugins/funind/indfun_common.ml | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/merge.ml | 12 ++++++------ plugins/funind/recdef.ml | 4 ++-- 6 files changed, 31 insertions(+), 33 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 07a0d5a505..946ee55d46 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -672,9 +672,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); - let br = - (Loc.ghost,([],[case_pats.(0)],e)) - in + let br = Loc.tag ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr @@ -1254,7 +1252,7 @@ let rec rebuild_return_type (loc, rt) = Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.ghost,Anonymous], + | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt], Loc.tag @@ Constrexpr.CSort(GType [])) @@ -1307,12 +1305,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> Loc.tag @@ Constrexpr.CProdN - ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1374,12 +1372,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> Loc.tag @@ Constrexpr.CProdN - ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1406,18 +1404,18 @@ let do_build_inductive (fun (n,t,typ) -> match typ with | Some typ -> - Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) | None -> Constrexpr.CLocalAssum - ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((Loc.ghost,id), + false,((Loc.tag id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1425,7 +1423,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.ghost,relnames.(i)), None), + (((Loc.tag @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index cad96946ca..1da85c467a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -156,7 +156,7 @@ let build_newrecursive let (rec_sign,rec_impls) = List.fold_left (fun (env,impls) (((_,recname),_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in + let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in @@ -355,7 +355,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = Ident (Loc.ghost,mk_rel_id (List.nth names 0)) in + let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg (pr_reference f_R_mut++str ": Not an inductive type!") @@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = - let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in + let type_of_f = Constrexpr_ops.mkCProdN args ret_type in let rec_arg_num = let names = List.map @@ -470,7 +470,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = Loc.tag @@ Constrexpr.CAppExpl( - (None,(Ident (Loc.ghost,fname)),None) , + (None,(Ident (Loc.tag fname)),None) , (List.map (function | _,Anonymous -> assert false @@ -480,10 +480,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), + Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in - let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in + let eq = Constrexpr_ops.mkCProdN args unbounded_eq in let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try @@ -537,13 +537,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path + Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -554,7 +554,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let a = Names.Id.of_string "___a" in let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( - [Loc.ghost,Name a;Loc.ghost,Name b], + [Loc.tag @@ Name a;Loc.tag @@ Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -891,14 +891,14 @@ let make_graph (f_ref:global_reference) = ) in let b' = add_args (snd id) new_args b in - ((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (con_label c) in - [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = repr_con c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8f0c986242..de8dc53f11 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -106,7 +106,7 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.ghost,id)) + qualid_of_reference (Libnames.Ident (Loc.tag id)) in try Constrintern.locate_reference princ_ref with Not_found -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8da4f9233e..e4536278c0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -274,7 +274,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.map (fun decl -> List.map - (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) + (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9dc1d48df3..f2654b5de8 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -73,7 +73,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.ghost,id), None) in + let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when CErrors.noncritical e -> false @@ -825,7 +825,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = @@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - Loc.tag @@ CProdN ([[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in @@ -849,12 +849,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(Id.t * glob_constr) list) = - let lident = (Loc.ghost, shift.ident), None in + let lident = (Loc.tag shift.ident), None in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((Loc.ghost,id),glob_constr_to_constr_expr t)) + (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t)) rawlist in lident , bindlist , Some cstr_expr , lcstor_expr @@ -902,7 +902,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Find infos on identifier id. *) let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = let kn_of_id x = - let f_ref = Libnames.Ident (Loc.ghost,x) in + let f_ref = Libnames.Ident (Loc.tag x) in locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) locate_constant f_ref in try find_Function_infos (kn_of_id id) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 25daedd0e4..9e469c7564 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1306,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.ghost,na) in + let na_ref = Libnames.Ident (Loc.tag na) in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); -- cgit v1.2.3 From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 14 +++++++------- plugins/funind/glob_termops.ml | 16 ++++++++-------- plugins/funind/indfun.ml | 4 ++-- 4 files changed, 18 insertions(+), 18 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 129c8dc165..ee82d95d09 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -159,7 +159,7 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> !@loc, g ]] + [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] ; END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 946ee55d46..48ab3dd57c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -610,7 +610,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env 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) (EConstr.of_constr v_as_constr) in @@ -973,7 +973,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - Loc.tag ~loc:loc1 @@ GApp(Loc.tag ~loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ~loc:loc3 @@ GVar id;rt_typ;rt]) + Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1119,7 +1119,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = end | loc, GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1249,11 +1249,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_ let rec rebuild_return_type (loc, rt) = match rt with | Constrexpr.CProdN(n,t') -> - Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t') + Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> - Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt], + Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt], Loc.tag @@ Constrexpr.CSort(GType [])) let do_build_inductive diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 01e607412a..66b9897d04 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -193,14 +193,14 @@ let rec alpha_pat excluded (loc, pat) = match pat with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded), + (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else (Loc.tag ~loc pat),excluded,Id.Map.empty + else (Loc.tag ?loc pat),excluded,Id.Map.empty | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with @@ -218,7 +218,7 @@ let rec alpha_pat excluded (loc, pat) = ([],new_excluded,map) patl in - (Loc.tag ~loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -255,7 +255,7 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded (loc, rt) = - let new_rt = Loc.tag ~loc @@ + let new_rt = Loc.tag ?loc @@ match rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt | GLambda(Anonymous,k,t,b) -> @@ -445,7 +445,7 @@ let rec pattern_to_term pt = Loc.with_unloc (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern (loc, rt) = Loc.tag ~loc @@ + let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@ match rt with | GRef _ -> rt | GVar id when Id.compare id x_id == 0 -> Loc.obj term @@ -605,7 +605,7 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term (loc, rt) = Loc.tag ~loc @@ + let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@ match rt with | GRef _ -> rt | GVar _ -> rt @@ -673,7 +673,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map (loc, rt) = - Loc.tag ~loc @@ + Loc.tag ?loc @@ match rt with | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt | GVar id -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1da85c467a..3dc16626ce 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -756,7 +756,7 @@ let rec add_args id new_args = Loc.map (function List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc @@ (cpl,add_args id new_args e)) cal + List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), @@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> Loc.tag ~loc @@ + (fun (loc,n) -> Loc.tag ?loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false -- cgit v1.2.3 From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 23:19:35 +0200 Subject: [location] [ast] Switch Constrexpr AST to an extensible node type. Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. --- plugins/funind/glob_term_to_relation.ml | 23 ++++++++++++----------- plugins/funind/indfun.ml | 24 ++++++++++++------------ plugins/funind/merge.ml | 4 ++-- 3 files changed, 26 insertions(+), 25 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 48ab3dd57c..938fe52373 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1246,15 +1246,16 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_ in List.rev !l -let rec rebuild_return_type (loc, rt) = - match rt with +let rec rebuild_return_type rt = + let loc = rt.CAst.loc in + match rt.CAst.v with | Constrexpr.CProdN(n,t') -> - Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') + CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> - Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt], - Loc.tag @@ Constrexpr.CSort(GType [])) + CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt], + CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) @@ -1305,11 +1306,11 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Loc.tag @@ Constrexpr.CProdN + CAst.make @@ Constrexpr.CProdN ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) @@ -1372,11 +1373,11 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Loc.tag @@ Constrexpr.CProdN + CAst.make @@ Constrexpr.CProdN ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc16626ce..f4e9aa3720 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -469,7 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in let unbounded_eq = let f_app_args = - Loc.tag @@ Constrexpr.CAppExpl( + CAst.make @@ Constrexpr.CAppExpl( (None,(Ident (Loc.tag fname)),None) , (List.map (function @@ -480,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -588,12 +588,12 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) -> + | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal, snd typ with + match nal, typ.CAst.v with | [], _ -> rebuild_bl (aux,assoc) bl' typ | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ | _,CProdN((nal',bk',nal't)::rest,typ') -> @@ -606,7 +606,7 @@ let rec rebuild_bl (aux,assoc) bl typ = rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' - else Loc.tag @@ if List.is_empty new_nal' + else CAst.make @@ if List.is_empty new_nal' then CProdN(rest,typ') else CProdN(((new_nal',bk',nal't)::rest),typ')) else @@ -614,7 +614,7 @@ let rec rebuild_bl (aux,assoc) bl typ = let nassoc = make_assoc assoc nal' captured_nal in let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ')) + bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) | _ -> assert false let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ @@ -725,7 +725,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof in () -let rec add_args id new_args = Loc.map (function +let rec add_args id new_args = CAst.map (function | CRef (r,_) as b -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> @@ -794,7 +794,7 @@ let rec chop_n_arrow n t = if n <= 0 then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) - match snd t with + match t.CAst.v with | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on @@ -813,7 +813,7 @@ let rec chop_n_arrow n t = then aux (n - nal_l) nal_ta' else - let new_t' = Loc.tag @@ + let new_t' = CAst.make @@ Constrexpr.CProdN( ((snd (List.chop n nal)),k,t'')::nal_ta',t') in @@ -829,7 +829,7 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = - match snd b with + match b.CAst.v with | Constrexpr.CLambdaN ((nal_ta), b') -> begin let n = @@ -869,7 +869,7 @@ let make_graph (f_ref:global_reference) = in let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = - match snd b with + match b.CAst.v with | Constrexpr.CFix(l_id,fixexprl) -> let l = List.map @@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> Loc.tag ?loc @@ + (fun (loc,n) -> CAst.make ?loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f2654b5de8..5b51a213a1 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -73,7 +73,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in + let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when CErrors.noncritical e -> false @@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in -- cgit v1.2.3 From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:35:20 +0200 Subject: [location] [ast] Port module AST to CAst --- plugins/funind/glob_term_to_relation.ml | 84 +++++++++--------- plugins/funind/glob_termops.ml | 146 ++++++++++++++++---------------- plugins/funind/indfun.ml | 2 +- plugins/funind/indfun_common.ml | 4 +- plugins/funind/merge.ml | 42 ++++----- plugins/funind/recdef.ml | 10 +-- 6 files changed, 147 insertions(+), 141 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 938fe52373..7f2b21e79d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -345,10 +345,10 @@ let raw_push_named (na,raw_value,raw_typ) env = let add_pat_variables pat typ env : Environ.env = - let rec add_pat_variables env (loc, pat) typ : 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 pat with + match pat.CAst.v with | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = @@ -398,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = Loc.with_unloc (function +let rec pattern_to_term_and_type env typ = CAst.with_val (function | PatVar Anonymous -> assert false | PatVar (Name id) -> mkGVar id @@ -466,11 +466,12 @@ let rec pattern_to_term_and_type env typ = Loc.with_unloc (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); - match rt with - | _, GRef _ | _, GVar _ | _, GEvar _ | _, GPatVar _ | _, GSort _ | _, GHole _ -> + let open CAst in + match rt.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | _, GApp(_,_) -> + | GApp(_,_) -> let f,args = glob_decompose_app rt in let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) @@ -482,14 +483,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match Loc.obj f with + match f.v with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> Loc.tag @@ - match t with - | loc, GLambda(na,_,nat,b) -> + | u::l -> CAst.make @@ + match t.v with + | GLambda(na,_,nat,b) -> GLetIn(na,u,None,aux b l) | _ -> GApp(t,l) @@ -550,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (Loc.tag @@ GVar id) + (CAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -579,7 +580,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | _, GLambda(n,_,t,b) -> + | GLambda(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | _, GProd(n,_,t,b) -> + | GProd(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -604,13 +605,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | loc, GLetIn(n,v,typ,b) -> + | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env 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) (EConstr.of_constr v_as_constr) in @@ -622,13 +623,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | _, GCases(_,_,el,brl) -> + | 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 - | _, GIf(b,(na,e_option),lhs,rhs) -> + | 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) (EConstr.of_constr b_as_constr) in let (ind,_) = @@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | _, GLetTuple(nal,_,b,e) -> + | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = List.map @@ -677,8 +678,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid match_expr end - | _, GRec _ -> error "Not handled GRec" - | _, GCast(b,_) -> + | GRec _ -> error "Not handled GRec" + | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) @@ -860,8 +861,8 @@ let is_res id = -let same_raw_term (_,rt1) (_,rt2) = - match rt1,rt2 with +let same_raw_term rt1 rt2 = + match CAst.(rt1.v, rt2.v) with | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false @@ -894,16 +895,17 @@ exception Continue let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in - match rt with - | _, GProd(n,k,t,b) -> + let open CAst in + match rt.v with + | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin match t with - | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id -> + | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> begin match args' with - | (_, (GVar this_relname))::args' -> + | { v = GVar this_relname }::args' -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious @@ -925,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -962,8 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = Loc.tag @@ - GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None), + let rt_typ = CAst.make @@ + GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] env (Evd.from_env env) @@ -973,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt]) + CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1042,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -1093,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Id.Set.filter not_free_in_t id_to_exclude) | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end - | _, GLambda(n,k,t,b) -> + | GLambda(n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -1112,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - Loc.tag @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | loc, GLetIn(n,v,t,b) -> + | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1135,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> Loc.tag @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end - | _, GLetTuple(nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in @@ -1161,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - Loc.tag @@ GLetTuple(nal,(na,None),t,new_b), + CAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1187,9 +1189,9 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params gt = Loc.with_unloc (function +let rec compute_cst_params relnames params gt = CAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames -> + | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) | GApp(f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) @@ -1211,7 +1213,7 @@ let rec compute_cst_params relnames params gt = Loc.with_unloc (function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params',(_, GVar id')::rtl' + | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 66b9897d04..5abcb100f7 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,16 +10,16 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = Loc.tag @@ GRef(ref,None) -let mkGVar id = Loc.tag @@ GVar(id) -let mkGApp(rt,rtl) = Loc.tag @@ GApp(rt,rtl) -let mkGLambda(n,t,b) = Loc.tag @@ GLambda(n,Explicit,t,b) -let mkGProd(n,t,b) = Loc.tag @@ GProd(n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = Loc.tag @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = Loc.tag @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = Loc.tag @@ GSort(s) -let mkGHole () = Loc.tag @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t) +let mkGRef ref = CAst.make @@ GRef(ref,None) +let mkGVar id = CAst.make @@ GVar(id) +let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = CAst.make @@ GSort(s) +let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -27,7 +27,7 @@ let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t) *) let glob_decompose_prod = let rec glob_decompose_prod args = function - | _, GProd(n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,t)::args) b | rt -> args,rt in @@ -35,9 +35,9 @@ let glob_decompose_prod = let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function - | _, GProd(n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,None,Some t)::args) b - | _, GLetIn(n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in @@ -59,7 +59,7 @@ let glob_decompose_prod_n n = if i<=0 then args,c else match c with - | _, GProd(n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in @@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n = if i<=0 then args,c else match c with - | _, GProd(n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | _, GLetIn(n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in @@ -84,7 +84,7 @@ let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | _, GApp(rt,rtl) -> + | { CAst.v = GApp(rt,rtl) } -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - Loc.map (function + CAst.map (function | GRef _ as x -> x | GVar id -> let new_id = @@ -189,18 +189,19 @@ let change_vars = -let rec alpha_pat excluded (loc, pat) = - match pat with +let rec alpha_pat excluded pat = + let loc = pat.CAst.loc in + match pat.CAst.v with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded), + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else (Loc.tag ?loc pat),excluded,Id.Map.empty + else pat, excluded,Id.Map.empty | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with @@ -218,7 +219,7 @@ let rec alpha_pat excluded (loc, pat) = ([],new_excluded,map) patl in - (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -236,8 +237,8 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = - let rec get_pattern_id (loc, pat) = - match pat with + let rec get_pattern_id pat = + match pat.CAst.v with | PatVar(Anonymous) -> assert false | PatVar(Name id) -> [id] @@ -254,10 +255,11 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] -let rec alpha_rt excluded (loc, rt) = - let new_rt = Loc.tag ?loc @@ - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt +let rec alpha_rt excluded rt = + let loc = rt.CAst.loc in + let new_rt = CAst.make ?loc @@ + match rt.CAst.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in let new_excluded = new_id :: excluded in @@ -351,8 +353,8 @@ let rec alpha_rt excluded (loc, rt) = alpha_rt excluded rhs ) | GRec _ -> error "Not handled GRec" - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, Miscops.map_cast_type (alpha_rt excluded) c) @@ -375,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) = [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in (loc, gt) = match gt with + let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function | GRef _ -> false | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false @@ -411,6 +413,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + ) x and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt in @@ -418,7 +421,7 @@ let is_free_in id = -let rec pattern_to_term pt = Loc.with_unloc (function +let rec pattern_to_term pt = CAst.with_val (function | PatVar Anonymous -> assert false | PatVar(Name id) -> mkGVar id @@ -445,39 +448,38 @@ let rec pattern_to_term pt = Loc.with_unloc (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@ - match rt with - | GRef _ -> rt - | GVar id when Id.compare id x_id == 0 -> Loc.obj term - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt + let rec replace_var_by_pattern x = CAst.map (function + | GVar id when Id.compare id x_id == 0 -> term.CAst.v + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt | GApp(rt',rtl) -> GApp(replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | GLambda(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GLambda(name,k,t,b) -> GLambda(name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GProd(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GProd(name,k,t,b) -> GProd( name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GLetIn(name,def,typ,b) -> GLetIn(name, replace_var_by_pattern def, Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) - | GLetTuple(nal,_,_,_) + | GLetTuple(nal,_,_,_) as rt when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal -> rt | GLetTuple(nal,(na,rto),def,b) -> @@ -499,11 +501,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) + ) x and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl then br @@ -520,9 +523,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs - | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> + | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -542,9 +546,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs - | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> + | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -564,7 +569,7 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = Loc.with_unloc (function + let rec ids_of_pat ids = CAst.with_val (function | PatVar Anonymous -> ids | PatVar(Name id) -> Id.Set.add id ids | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl @@ -578,7 +583,7 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc (loc, c) = + let rec ids_of_glob_constr acc {loc; CAst.v = c} = let idof = id_of_name in match c with | GVar id -> id::acc @@ -605,12 +610,11 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@ - match rt with - | GRef _ -> rt - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt + let rec zeta_normalize_term x = CAst.map (function + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt | GApp(rt',rtl) -> GApp(zeta_normalize_term rt', List.map zeta_normalize_term rtl @@ -628,9 +632,9 @@ let zeta_normalize = zeta_normalize_term b ) | GLetIn(Name id,def,typ,b) -> - Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b) + (zeta_normalize_term (replace_var_by_term id def b)).CAst.v | GLetIn(Anonymous,def,typ,b) -> - Loc.obj @@ zeta_normalize_term b + (zeta_normalize_term b).CAst.v | GLetTuple(nal,(na,rto),def,b) -> GLetTuple(nal, (na,Option.map zeta_normalize_term rto), @@ -650,11 +654,12 @@ let zeta_normalize = zeta_normalize_term rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast(b,c) -> GCast(zeta_normalize_term b, Miscops.map_cast_type zeta_normalize_term c) + ) x and zeta_normalize_br (loc,(idl,patl,res)) = (loc,(idl,patl,zeta_normalize_term res)) in @@ -665,21 +670,19 @@ let zeta_normalize = let expand_as = - let rec add_as map (loc, pat) = + let rec add_as map ({loc; CAst.v = pat } as rt) = match pat with | PatVar _ -> map | PatCstr(_,patl,Name id) -> - Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl) + Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map (loc, rt) = - Loc.tag ?loc @@ - match rt with - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt - | GVar id -> + let rec expand_as map = CAst.map (function + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GVar id as rt -> begin try - Loc.obj @@ Id.Map.find id map + (Id.Map.find id map).CAst.v with Not_found -> rt end | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) @@ -699,6 +702,7 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) + ) and expand_as_br map (loc,(idl,cpl,rt)) = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f4e9aa3720..ab83cb15a6 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -190,7 +190,7 @@ let build_newrecursive l = let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names (loc, gt) = match gt with + let rec lookup names gt = match gt.CAst.v with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index de8dc53f11..394b252aac 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -69,7 +69,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -83,7 +83,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 5b51a213a1..d4865bf5ea 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -66,7 +66,7 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | _, GVar x -> Id.equal x f + | { CAst.v = GVar x } -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -504,40 +504,40 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array exception NoMerge -let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable = +let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1, c2 with + match CAst.(c1.v, c2.v) with | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - Loc.tag @@ GApp ((Loc.tag @@ GVar shift.ident) , args) + CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in - let newtrm = merge_app trm (loc2, c2) id1 id2 shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in - let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge -let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable = +let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1 , c2 with + match CAst.(c1.v, c2.v) with | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - Loc.tag @@ GApp (Loc.tag @@ GVar shift.ident, args) + CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in - let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in - let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -550,14 +550,14 @@ let rec merge_rec_hyps shift accrec filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (_, GApp(i,args) as ind)) + | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (_, GApp(f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -573,7 +573,7 @@ let find_app (nme:Id.t) ltyp = (List.map (fun x -> match x with - | _,None,Some (_, GApp(f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -632,8 +632,8 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1 with - | _, GApp(f,carr) when isVarf ind1name f -> + (match t1.CAst.v with + | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = @@ -864,7 +864,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = | LocalAssum (nme,t) -> let t = EConstr.of_constr t in let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - Loc.tag @@ GProd (nme,Explicit,traw,t2) + CAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9e469c7564..8c88399448 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -188,15 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - Loc.tag @@ + CAst.make @@ GCases (RegularStyle,None, - [Loc.tag @@ GApp(Loc.tag @@ GRef(fterm,None), List.rev_map (fun x_id -> Loc.tag @@ GVar x_id) rev_x_id_l), + [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous], + [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], Anonymous)], - Loc.tag @@ GVar v_id)]) + CAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context -- cgit v1.2.3