diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:45 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:45 +0000 |
| commit | 8f9461509338a3ebba46faaad3116c4e44135423 (patch) | |
| tree | 23da64d38f2194a1f9e42b789b16b82402d6908f /plugins | |
| parent | fafba6b545c7d0d774bcd79bdbddb8869517aabb (diff) | |
Change of nomenclature: rawconstr -> glob_constr
There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.
In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.
The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.
This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):
perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
28 files changed, 608 insertions, 608 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 3b98a1dca..6c6dbf0f6 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -83,8 +83,8 @@ type raw_proof_instr = raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((identifier*(Genarg.rawconstr_and_expr option)) located, - Genarg.rawconstr_and_expr, + ((identifier*(Genarg.glob_constr_and_expr option)) located, + Genarg.glob_constr_and_expr, Topconstr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index f5bc47109..d16a26550 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -21,7 +21,7 @@ open Compat (* INTERN *) -let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) +let raw_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args) let intern_justification_items globs = Option.map (List.map (intern_constr globs)) @@ -184,16 +184,16 @@ let interp_constr_or_thesis check_sort sigma env = function let abstract_one_hyp inject h raw = match h with Hvar (loc,(id,None)) -> - RProd (dummy_loc,Name id, Explicit, RHole (loc,Evd.BinderType (Name id)), raw) + GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), raw) | Hvar (loc,(id,Some typ)) -> - RProd (dummy_loc,Name id, Explicit, fst typ, raw) + GProd (dummy_loc,Name id, Explicit, fst typ, raw) | Hprop st -> - RProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw) + GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw) -let rawconstr_of_hyps inject hyps head = +let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let raw_prop = RSort (dummy_loc,RProp Null) +let raw_prop = GSort (dummy_loc,RProp Null) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -211,7 +211,7 @@ let rec match_hyps blend names constr = function qhyp::rhyps,head let interp_hyps_gen inject blend sigma env hyps head = - let constr=understand sigma env (rawconstr_of_hyps inject hyps head) in + let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in match_hyps blend [] constr hyps let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop) @@ -236,32 +236,32 @@ let rec raw_of_pat = function PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" | PatVar (loc,Name id) -> - RVar (loc,id) + GVar (loc,id) | PatCstr(loc,((ind,_) as cstr),lpat,_) -> let mind= fst (Global.lookup_inductive ind) in let rec add_params n q = if n<=0 then q else - add_params (pred n) (RHole(dummy_loc, + add_params (pred n) (GHole(dummy_loc, Evd.TomatchTypeParameter(ind,n))::q) in let args = List.map raw_of_pat lpat in - raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr), + raw_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function (loc,(id,None)) -> (fun raw -> - RProd (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw)) + GProd (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), raw)) | (loc,(id,Some typ)) -> (fun raw -> - RProd (dummy_loc,Name id, Explicit, fst typ, raw)) + GProd (dummy_loc,Name id, Explicit, fst typ, raw)) let prod_one_id (loc,id) raw = - RProd (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw) + GProd (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), raw) let let_in_one_alias (id,pat) raw = - RLetIn (dummy_loc,Name id, raw_of_pat pat, raw) + GLetIn (dummy_loc,Name id, raw_of_pat pat, raw) let rec bind_primary_aliases map pat = match pat with @@ -331,34 +331,34 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in let rparams = List.map detype_ground pinfo.per_params in let rparams_rec = List.map (fun (loc,(id,_)) -> - RVar (loc,id)) params in + GVar (loc,id)) params in let dum_args= - list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) + list_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) oib.Declarations.mind_nrealargs in raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) + Thesis (Plain) -> Rawterm.GSort(dummy_loc,RProp Null) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Rawterm.RSort(dummy_loc,RProp Null) + Rawterm.GSort(dummy_loc,RProp Null) | This (c,_) -> c in - let term1 = rawconstr_of_hyps inject hyps raw_prop in + let term1 = glob_constr_of_hyps inject hyps raw_prop in let loc_ids,npatt = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in let term2 = - RLetIn(dummy_loc,Anonymous, - RCast(dummy_loc,raw_of_pat npatt, + GLetIn(dummy_loc,Anonymous, + GCast(dummy_loc,raw_of_pat npatt, CastConv (DEFAULTcast,app_ind)),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in @@ -413,17 +413,17 @@ let interp_casee sigma env = function let abstract_one_arg = function (loc,(id,None)) -> (fun raw -> - RLambda (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw)) + GLambda (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), raw)) | (loc,(id,Some typ)) -> (fun raw -> - RLambda (dummy_loc,Name id, Explicit, fst typ, raw)) + GLambda (dummy_loc,Name id, Explicit, fst typ, raw)) -let rawconstr_of_fun args body = +let glob_constr_of_fun args body = List.fold_right abstract_one_arg args (fst body) let interp_fun sigma env args body = - let constr=understand sigma env (rawconstr_of_fun args body) in + let constr=understand sigma env (glob_constr_of_fun args body) in match_args destLambda [] constr args let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 0236c3095..97277ad58 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1291,7 +1291,7 @@ let understand_my_constr c gls = let env = pf_env gls in let nc = names_of_rel_context env in let rawc = Detyping.detype false [] nc c in - let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in + let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) let set_refine,my_refine = diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c79a8b818..24ec23484 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -123,9 +123,9 @@ let mk_open_instance id gl m t= let rec raux n t= if n=0 then t else match t with - RLambda(loc,name,k,_,t0)-> + GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) + GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try Pretyping.Default.understand evmap env (raux m rawt) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9c3982cb5..b2b4145d7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -125,12 +125,12 @@ let functional_induction with_clean c princl pat = Dumpglob.continue (); res -let rec abstract_rawconstr c = function +let rec abstract_glob_constr c = function | [] -> c - | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl) + | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl) | Topconstr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl - (abstract_rawconstr c bl) + (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = Constrintern.intern_gen false sigma env ~impls @@ -161,7 +161,7 @@ let build_newrecursive try List.map (fun (_,bl,_,def) -> - let def = abstract_rawconstr def bl in + let def = abstract_glob_constr def bl in interp_casted_constr_with_implicits sigma rec_sign rec_impls def ) @@ -188,15 +188,15 @@ let rec is_rec names = let names = List.fold_right Idset.add names Idset.empty in let check_id id names = Idset.mem id names in let rec lookup names = function - | RVar(_,id) -> check_id id names - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_) -> lookup names b - | RRec _ -> error "RRec not handled" - | RIf(_,b,_,lhs,rhs) -> + | GVar(_,id) -> check_id id names + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GDynamic _ -> false + | GCast(_,b,_) -> lookup names b + | GRec _ -> error "GRec not handled" + | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> + | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b - | RLetTuple(_,nal,_,t,b) -> lookup names t || + | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left (fun acc na -> Nameops.name_fold Idset.remove na acc) @@ -204,8 +204,8 @@ let rec is_rec names = nal ) b - | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,_,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) = @@ -222,7 +222,7 @@ let rec local_binders_length = function let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in -(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) +(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 002fb7098..9db361cf5 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -76,8 +76,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Rawterm.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Rawterm.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -90,7 +90,7 @@ let chop_rprod_n = then List.rev acc,rt else match rt with - | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | Rawterm.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index c48dff0c6..d802ecf2b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -35,11 +35,11 @@ val list_union_eq : val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list -val chop_rlambda_n : int -> Rawterm.rawconstr -> - (name*Rawterm.rawconstr*bool) list * Rawterm.rawconstr +val chop_rlambda_n : int -> Rawterm.glob_constr -> + (name*Rawterm.glob_constr*bool) list * Rawterm.glob_constr -val chop_rprod_n : int -> Rawterm.rawconstr -> - (name*Rawterm.rawconstr) list * Rawterm.rawconstr +val chop_rprod_n : int -> Rawterm.glob_constr -> + (name*Rawterm.glob_constr) list * Rawterm.glob_constr val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 7c460f7d3..ed8cb9cb6 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -25,7 +25,7 @@ open Rawtermops (** {1 Utilities} *) -(** {2 Useful operations on constr and rawconstr} *) +(** {2 Useful operations on constr and glob_constr} *) let rec popn i c = if i<=0 then c else pop (popn (i-1) c) @@ -60,7 +60,7 @@ let string_of_name nme = string_of_id (id_of_name nme) (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | RVar (_,x) -> Pervasives.compare x f = 0 + | GVar (_,x) -> Pervasives.compare x f = 0 | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -97,7 +97,7 @@ let prNamedConstr s c = let prNamedRConstr s c = begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc @@ -377,11 +377,11 @@ let verify_inds mib1 mib2 = let build_raw_params prms_decl avoid = let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in let _ = prNamedConstr "DUMMY" dummy_constr in - let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in - let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in - let res,_ = raw_decompose_prod dummy_rawconstr in + let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in + let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in + let res,_ = glob_decompose_prod dummy_glob_constr in let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr))) + comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_glob_constr))) *) let ids_of_rawlist avoid rawl = @@ -511,37 +511,37 @@ exception NoMerge 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 - | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n";Pp.flush_all() in let args = filter_shift_stable lnk (arr1 @ arr2) in - RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args) - | RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge - | RLetIn(_,nme,bdy,trm) , _ -> + GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args) + | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge + | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2!\n";Pp.flush_all() in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> + GLetIn(dummy_loc,nme,bdy,newtrm) + | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3!\n";Pp.flush_all() in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with - | RApp(_,f1, arr1), RApp(_,f2,arr2) -> + | GApp(_,f1, arr1), GApp(_,f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args) + GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | RLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> + GLetIn(dummy_loc,nme,bdy,newtrm) + | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge @@ -550,24 +550,24 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = calls of branch 1 with all rec calls of branch 2. *) (* TODO: reecrire cette heuristique (jusqu'a merge_types) *) let rec merge_rec_hyps shift accrec - (ltyp:(Names.name * rawconstr option * rawconstr option) list) - filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list = + (ltyp:(Names.name * glob_constr option * glob_constr option) list) + filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (RApp(_,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 (RApp(_,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 -let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = +let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec @@ -577,7 +577,7 @@ let find_app (nme:identifier) ltyp = (List.map (fun x -> match x with - | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -591,9 +591,9 @@ let prnt_prod_or_letin nm letbdy typ = let rec merge_types shift accrec1 - (ltyp1:(name * rawconstr option * rawconstr option) list) - (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2 - : (name * rawconstr option * rawconstr option) list * rawconstr = + (ltyp1:(name * glob_constr option * glob_constr option) list) + (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2 + : (name * glob_constr option * glob_constr option) list * glob_constr = let _ = prstr "MERGE_TYPES\n" in let _ = prstr "ltyp 1 : " in let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in @@ -637,7 +637,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> (match t1 with - | RApp(_,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 = @@ -704,8 +704,8 @@ let build_link_map allargs1 allargs2 lnk = Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint. TODO: return nothing if equalities (after linking) are contradictory. *) -let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) - (typcstr2:rawconstr) : rawconstr = +let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr) + (typcstr2:glob_constr) : glob_constr = (* FIXME: les noms des parametres corerspondent en principe au parametres du niveau mib, mais il faudrait s'en assurer *) (* shift.nfunresprmsx last args are functional result *) @@ -713,17 +713,17 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in let nargs2 = shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in - let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in - let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in + let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in + let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in let rest2 = change_vars linked_map rest2 in - let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in - let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in + let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in + let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in let ltyp,concl2 = merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in let _ = prNamedRLDecl "ltyp result:" ltyp in - let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in + let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in let revargs1 = list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in let _ = prNamedRLDecl "ltyp allargs1" allargs1 in @@ -733,7 +733,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) let _ = prNamedRLDecl "ltyp allargs2" allargs2 in let _ = prNamedRLDecl "ltyp revargs2" revargs2 in let typwithprms = - raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in + glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in typwithprms @@ -759,8 +759,8 @@ let merge_constructor_id id1 id2 shift:identifier = constructor [(name*type)]. These are translated to rawterms first, each of them having distinct var names. *) let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) - (typcstr1:(identifier * rawconstr) list) - (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list = + (typcstr1:(identifier * glob_constr) list) + (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list = List.flatten (List.map (fun (id1,rawtyp1) -> @@ -778,12 +778,12 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) info in [shift], avoiding identifiers in [avoid]. *) let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (oib2:one_inductive_body) = - (* building rawconstr type of constructors *) + (* building glob_constr type of constructors *) let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in Detyping.detype false (Idset.elements avoid) [] substindtyp in - let lcstr1: rawconstr list = + let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in @@ -792,10 +792,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in let params1 = - try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) + try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) with _ -> [] in let params2 = - try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) + try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) with _ -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in @@ -816,8 +816,8 @@ let rec merge_mutual_inductive_body merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) -let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) - Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x +let rawterm_to_constr_expr x = (* build a constr_expr from a glob_constr *) + Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let params = prms2 @ prms1 in @@ -849,7 +849,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = [rawlist], named ident. FIXME: params et cstr_expr (arity) *) let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * rawconstr) list) = + (rawlist:(identifier * glob_constr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in @@ -861,21 +861,21 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift -let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = +let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,Explicit,traw,t2) + GProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false -let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = +let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,Explicit,traw,t2) + GProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index f8da96bdf..7b67e20f3 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/rawterm_to_relation.ml @@ -23,14 +23,14 @@ type binder_type = | Prod of name | LetIn of name -type raw_context = (binder_type*rawconstr) list +type glob_context = (binder_type*glob_constr) list (* - compose_raw_context [(bt_1,n_1,t_1);......] rt returns + compose_glob_context [(bt_1,n_1,t_1);......] rt returns b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the binders corresponding to the bt_i's *) -let compose_raw_context = +let compose_glob_context = let compose_binder (bt,t) acc = match bt with | Lambda n -> mkRLambda(n,t,acc) @@ -47,7 +47,7 @@ let compose_raw_context = type 'a build_entry_pre_return = { - context : raw_context; (* the binding context of the result *) + context : glob_context; (* the binding context of the result *) value : 'a; (* The value *) } @@ -159,7 +159,7 @@ let apply_args ctxt body args = | _,[] -> (* No more args *) (ctxt,body) | [],_ -> (* no more fun *) - let f,args' = raw_decompose_app body in + let f,args' = glob_decompose_app body in (ctxt,mkRApp(f,args'@args)) | (Lambda Anonymous,t)::ctxt',arg::args' -> do_apply avoid ctxt' body args' @@ -215,8 +215,8 @@ let combine_app f args = let combine_lam n t b = { context = []; - value = mkRLambda(n, compose_raw_context t.context t.value, - compose_raw_context b.context b.value ) + value = mkRLambda(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) } @@ -319,15 +319,15 @@ let build_constructors_of_type ind' argl = let pat_as_term = mkRApp(mkRRef (ConstructRef(ind',i+1)),argl) in - cases_pattern_of_rawconstr Anonymous pat_as_term + cases_pattern_of_glob_constr Anonymous pat_as_term ) ind.Declarations.mind_consnames (* [find_type_of] very naive attempts to discover the type of an if or a letin *) let rec find_type_of nb b = - let f,_ = raw_decompose_app b in + let f,_ = glob_decompose_app b in match f with - | RRef(_,ref) -> + | GRef(_,ref) -> begin let ind_type = match ref with @@ -350,8 +350,8 @@ let rec find_type_of nb b = then raise (Invalid_argument "find_type_of : not a valid inductive"); ind_type end - | RCast(_,b,_) -> find_type_of nb b - | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) + | GCast(_,b,_) -> find_type_of nb b + | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) | _ -> raise (Invalid_argument "not a ref") @@ -472,7 +472,7 @@ let rec pattern_to_term_and_type env typ = function and concatenate them (informally, each branch of a match produces a new constructor) \end{itemize} - WARNING: The terms constructed here are only USING the rawconstr syntax but are highly bad formed. + WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed. We must wait to have complete all the current calculi to set the recursive calls. At this point, each term [f t1 ... tn] (where f appears in [funnames]) is replaced by a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later. @@ -481,15 +481,15 @@ let rec pattern_to_term_and_type env typ = function *) -let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = - observe (str " Entering : " ++ Printer.pr_rawconstr rt); +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 - | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | RApp(_,_,_) -> - let f,args = raw_decompose_app rt in - let args_res : (rawconstr list) build_entry_return = + | 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 *) (fun arg ctxt_argsl -> let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in @@ -500,19 +500,19 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = in begin match f with - | RLambda _ -> + | GLambda _ -> let rec aux t l = match l with | [] -> t | u::l -> match t with - | RLambda(loc,na,_,nat,b) -> - RLetIn(dummy_loc,na,u,aux b l) + | GLambda(loc,na,_,nat,b) -> + GLetIn(dummy_loc,na,u,aux b l) | _ -> - RApp(dummy_loc,t,l) + GApp(dummy_loc,t,l) in build_entry_lc env funnames avoid (aux f args) - | RVar(_,id) when Idset.mem id funnames -> + | GVar(_,id) when Idset.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 @@ -538,7 +538,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = args_res.result in { result = new_result; to_avoid = new_avoid } - | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ -> + | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ -> (* if have [g t1 ... tn] with [g] not appearing in [funnames] then foreach [ctxt,v1 ... vn] in [args_res] we return @@ -552,8 +552,8 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = {args_res with value = mkRApp(f,args_res.value)}) args_res.result } - | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *) - | RLetIn(_,n,t,b) -> + | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) + | GLetIn(_,n,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 @@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let new_b = replace_var_by_term id - (RVar(dummy_loc,id)) + (GVar(dummy_loc,id)) b in (Name new_id,new_b,new_avoid) @@ -578,26 +578,26 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = funnames avoid (mkRLetIn(new_n,t,mkRApp(new_b,args))) - | RCases _ | RIf _ | RLetTuple _ -> + | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and then combine each of them with each of args one *) let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res - | RDynamic _ ->error "Not handled RDynamic" - | RCast(_,b,_) -> + | GDynamic _ ->error "Not handled GDynamic" + | GCast(_,b,_) -> (* for an applied cast we just trash the cast part and restart the work. WARNING: We need to restart since [b] itself should be an application term *) build_entry_lc env funnames avoid (mkRApp(b,args)) - | RRec _ -> error "Not handled RRec" - | RProd _ -> error "Cannot apply a type" + | GRec _ -> error "Not handled GRec" + | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | RLambda(_,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 @@ -612,7 +612,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr 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 - | RProd(_,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 @@ -622,7 +622,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr 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 - | RLetIn(_,n,v,b) -> + | GLetIn(_,n,v,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] @@ -638,21 +638,21 @@ let rec build_entry_lc env funnames avoid rt : rawconstr 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 - | RCases(_,_,_,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 - | RIf(_,b,(na,e_option),lhs,rhs) -> + | GIf(_,b,(na,e_option),lhs,rhs) -> let b_as_constr = Pretyping.Default.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_rawconstr b ++ str " in " ++ - Printer.pr_rawconstr rt ++ str ". try again with a cast") + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type ind [] in assert (Array.length case_pats = 2); @@ -665,11 +665,11 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let match_expr = mkRCases(None,[(b,(Anonymous,None))],brl) in - (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *) + (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | RLetTuple(_,nal,_,b,e) -> + | GLetTuple(_,nal,_,b,e) -> begin - let nal_as_rawconstr = + let nal_as_glob_constr = List.map (function Name id -> mkRVar id @@ -683,10 +683,10 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_rawconstr b ++ str " in " ++ - Printer.pr_rawconstr rt ++ str ". try again with a cast") + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind nal_as_rawconstr in + let case_pats = build_constructors_of_type ind nal_as_glob_constr in assert (Array.length case_pats = 1); let br = (dummy_loc,[],[case_pats.(0)],e) @@ -695,14 +695,14 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = build_entry_lc env funnames avoid match_expr end - | RRec _ -> error "Not handled RRec" - | RCast(_,b,_) -> + | GRec _ -> error "Not handled GRec" + | GCast(_,b,_) -> build_entry_lc env funnames avoid b - | RDynamic _ -> error "Not handled RDynamic" + | GDynamic _ -> error "Not handled GDynamic" and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) (brl:Rawterm.cases_clauses) avoid : - rawconstr build_entry_return = + glob_constr build_entry_return = match el with | [] -> assert false (* this case correspond to match <nothing> with .... !*) | el -> @@ -762,7 +762,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (will be used in the following recursive calls) *) let new_env = List.fold_right2 add_pat_variables patl types env in - let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = + let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> @@ -780,7 +780,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve in mkRProd (Name id,raw_typ_of_id,acc)) pat_ids - (raw_make_neq pat'_as_term (pattern_to_term renamed_pat)) + (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)) ) patl types @@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve else acc ) idl - [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)] + [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)] ) patl matched_expr.value @@ -883,18 +883,18 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_rawconstr rt); + observe (str "rebuilding : " ++ pr_glob_constr rt); match rt with - | RProd(_,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 - | RApp(_,(RVar(_,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 - | (RVar(_,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 @@ -916,12 +916,12 @@ 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 - | RApp(loc1,RRef(loc2,eq_as_ref),[ty;RVar(loc3,id);rt]) + | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous -> begin try - observe (str "computing new type for eq : " ++ pr_rawconstr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue in @@ -953,8 +953,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.list_chop nparam args')) in let rt_typ = - RApp(Util.dummy_loc, - RRef (Util.dummy_loc,Libnames.IndRef ind), + GApp(Util.dummy_loc, + GRef (Util.dummy_loc,Libnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) @@ -964,9 +964,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkRHole ())))) in let eq' = - RApp(loc1,RRef(loc2,jmeq),[ty;RVar(loc3,id);rt_typ;rt]) + GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_rawconstr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1033,7 +1033,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else new_b, Idset.add id id_to_exclude *) | _ -> - observe (str "computing new type for prod : " ++ pr_rawconstr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t' = Pretyping.Default.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1048,11 +1048,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Idset.filter not_free_in_t id_to_exclude) | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude end - | RLambda(_,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 - observe (str "computing new type for lambda : " ++ pr_rawconstr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr rt); let t' = Pretyping.Default.understand Evd.empty env t in match n with | Name id -> @@ -1067,12 +1067,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) else - RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude + GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude | _ -> anomaly "Should not have an anonymous function here" (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | RLetIn(_,n,t,b) -> + | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let t' = Pretyping.Default.understand Evd.empty env t in @@ -1086,10 +1086,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> RLetIn(dummy_loc,n,t,new_b), + | _ -> GLetIn(dummy_loc,n,t,new_b), Idset.filter not_free_in_t id_to_exclude end - | RLetTuple(_,nal,(na,rto),t,b) -> + | GLetTuple(_,nal,(na,rto),t,b) -> assert (rto=None); begin let not_free_in_t id = not (is_free_in id t) in @@ -1112,7 +1112,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Idset.mem id id_to_exclude -> *) (* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - RLetTuple(dummy_loc,nal,(na,None),t,new_b), + GLetTuple(dummy_loc,nal,(na,None),t,new_b), Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') end @@ -1122,12 +1122,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* debuging wrapper *) let rebuild_cons env nb_args relname args crossed_types rt = -(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *) +(* observennl (str "rebuild_cons : rt := "++ pr_glob_constr rt ++ *) (* str "nb_args := " ++ str (string_of_int nb_args)); *) let res = rebuild_cons env nb_args relname args crossed_types 0 rt in -(* observe (str " leads to "++ pr_rawconstr (fst res)); *) +(* observe (str " leads to "++ pr_glob_constr (fst res)); *) res @@ -1139,30 +1139,30 @@ 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 - | RRef _ | RVar _ | REvar _ | RPatVar _ -> params - | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) - | RApp(_,f,args) -> + | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | RCases _ -> + | GCases _ -> params (* If there is still cases at this point they can only be discriminitation ones *) - | RSort _ -> params - | RHole _ -> params - | RIf _ | RRec _ | RCast _ | RDynamic _ -> + | GSort _ -> params + | GHole _ -> params + | GIf _ | GRec _ | GCast _ | GDynamic _ -> raise (UserError("compute_cst_params", str "Not handled case")) 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,_,is_defined) as param)::params',(RVar(_,id'))::rtl' + | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' when id_ord id id' == 0 && not is_defined -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts = +let compute_params_name relnames (args : (Names.name * Rawterm.glob_constr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1181,7 +1181,7 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) if array_for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined') + n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') rels_params then l := param::!l @@ -1204,11 +1204,11 @@ let rec rebuild_return_type rt = let do_build_inductive - funnames (funsargs: (Names.name * rawconstr * bool) list list) + funnames (funsargs: (Names.name * glob_constr * bool) list list) returned_types - (rtl:rawconstr list) = + (rtl:glob_constr list) = let _time1 = System.get_time () in -(* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *) +(* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in let funnames = Array.of_list funnames in let funsargs = Array.of_list funsargs in @@ -1233,19 +1233,19 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = + let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list = funargs in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t, + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1264,9 +1264,9 @@ let do_build_inductive let constr i res = List.map (function result (* (args',concl') *) -> - let rt = compose_raw_context result.context result.value in + let rt = compose_glob_context result.context result.value in let nb_args = List.length funsargs.(i) in - (* with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_rawconstr rt)) rt; *) + (* with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *) fst ( rebuild_cons env_with_graphs nb_args relnames.(i) [] @@ -1285,7 +1285,7 @@ let do_build_inductive i*) id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) in - let rel_constructors i rt : (identifier*rawconstr) list = + let rel_constructors i rt : (identifier*glob_constr) list = next_constructor_id := (-1); List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) in @@ -1299,19 +1299,19 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = + let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list = (snd (list_chop nrel_params funargs)) in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t, + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1328,10 +1328,10 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t) + Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) else Topconstr.LocalRawAssum - ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t) + ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) ) rels_params in @@ -1341,7 +1341,7 @@ let do_build_inductive false,((dummy_loc,id), Flags.with_option Flags.raw_print - (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t) + (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) ) )) (rel_constructors) diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli index a314050f7..772e422f8 100644 --- a/plugins/funind/rawterm_to_relation.mli +++ b/plugins/funind/rawterm_to_relation.mli @@ -9,8 +9,8 @@ val build_inductive : Names.identifier list -> (* The list of function name *) - (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *) + (Names.name*Rawterm.glob_constr*bool) list list -> (* The list of function args *) Topconstr.constr_expr list -> (* The list of function returned type *) - Rawterm.rawconstr list -> (* the list of body *) + Rawterm.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml index e31f1452d..f372fb017 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/rawtermops.ml @@ -6,46 +6,46 @@ open Names let idmap_is_empty m = m = Idmap.empty (* - Some basic functions to rebuild rawconstr + Some basic functions to rebuild glob_constr In each of them the location is Util.dummy_loc *) -let mkRRef ref = RRef(dummy_loc,ref) -let mkRVar id = RVar(dummy_loc,id) -let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) -let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) -let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl) -let mkRSort s = RSort(dummy_loc,s) -let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) +let mkRRef ref = GRef(dummy_loc,ref) +let mkRVar id = GVar(dummy_loc,id) +let mkRApp(rt,rtl) = GApp(dummy_loc,rt,rtl) +let mkRLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) +let mkRProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) +let mkRLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) +let mkRCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) +let mkRSort s = GSort(dummy_loc,s) +let mkRHole () = GHole(dummy_loc,Evd.BinderType Anonymous) +let mkRCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* - Some basic functions to decompose rawconstrs + Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -let raw_decompose_prod = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,t)::args) b +let glob_decompose_prod = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,t)::args) b | rt -> args,rt in - raw_decompose_prod [] - -let raw_decompose_prod_or_letin = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod ((n,Some t,None)::args) b + glob_decompose_prod [] + +let glob_decompose_prod_or_letin = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod [] + glob_decompose_prod [] -let raw_compose_prod = +let glob_compose_prod = List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) -let raw_compose_prod_or_letin = +let glob_compose_prod_or_letin = List.fold_left ( fun concl decl -> match decl with @@ -53,37 +53,37 @@ let raw_compose_prod_or_letin = | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) | _ -> assert false) -let raw_decompose_prod_n n = - let rec raw_decompose_prod i args c = +let glob_decompose_prod_n n = + let rec glob_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,t)::args) b + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_prod_or_letin_n n = - let rec raw_decompose_prod i args c = +let glob_decompose_prod_or_letin_n n = + let rec glob_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod (i-1) ((n,Some t,None)::args) b + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod (i-1) ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_app = +let glob_decompose_app = let rec decompose_rapp acc rt = -(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *) +(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | RApp(_,rt,rtl) -> + | GApp(_,rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -92,24 +92,24 @@ let raw_decompose_app = -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -let raw_make_eq ?(typ= mkRHole ()) t1 t2 = +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +let glob_make_eq ?(typ= mkRHole ()) t1 t2 = mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) -(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) -let raw_make_neq t1 t2 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2]) +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +let glob_make_neq t1 t2 = + mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) -(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) -let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +let glob_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding to [P1 \/ ( .... \/ Pn)] *) -let rec raw_make_or_list = function +let rec glob_make_or_list = function | [] -> raise (Invalid_argument "mk_or") | [e] -> e - | e::l -> raw_make_or e (raw_make_or_list l) + | e::l -> glob_make_or e (glob_make_or_list l) let remove_name_from_mapping mapping na = @@ -120,70 +120,70 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = match rt with - | RRef _ -> rt - | RVar(loc,id) -> + | GRef _ -> rt + | GVar(loc,id) -> let new_id = try Idmap.find id mapping with Not_found -> id in - RVar(loc,new_id) - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> - RApp(loc, + GVar(loc,new_id) + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, change_vars mapping def, change_vars (remove_name_from_mapping mapping name) b ) - | RLetTuple(loc,nal,(na,rto),b,e) -> + | GLetTuple(loc,nal,(na,rto),b,e) -> let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - RLetTuple(loc, + GLetTuple(loc, nal, (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> - RIf(loc, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, change_vars mapping b, (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) - | RRec _ -> error "Local (co)fixes are not supported" - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv (k,t)) -> - RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,change_vars mapping b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" + | GRec _ -> error "Local (co)fixes are not supported" + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv (k,t)) -> + GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,change_vars mapping b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in if idmap_is_empty new_mapping @@ -262,22 +262,22 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let new_rt = match rt with - | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,k,t,b) -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt + | GLambda(loc,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 - RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Anonymous,k,t,b) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RProd(loc,Anonymous,k,new_t,new_b) - | RLetIn(loc,Anonymous,t,b) -> + GProd(loc,Anonymous,k,new_t,new_b) + | GLetIn(loc,Anonymous,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RLetIn(loc,Anonymous,new_t,new_b) - | RLambda(loc,Name id,k,t,b) -> + GLetIn(loc,Anonymous,new_t,new_b) + | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -289,8 +289,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 - RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Name id,k,t,b) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,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 = @@ -302,8 +302,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 - RProd(loc,Name new_id,k,new_t,new_b) - | RLetIn(loc,Name id,t,b) -> + GProd(loc,Name new_id,k,new_t,new_b) + | GLetIn(loc,Name id,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -315,10 +315,10 @@ 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 - RLetIn(loc,Name new_id,new_t,new_b) + GLetIn(loc,Name new_id,new_t,new_b) - | RLetTuple(loc,nal,(na,rto),t,b) -> + | GLetTuple(loc,nal,(na,rto),t,b) -> let rev_new_nal,new_excluded,mapping = List.fold_left (fun (nal,excluded,mapping) na -> @@ -345,28 +345,28 @@ 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 - RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | RCases(loc,sty,infos,el,brl) -> + GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) + | GCases(loc,sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | RIf(loc,b,(na,e_o),lhs,rhs) -> - RIf(loc,alpha_rt excluded b, + 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, (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) - | RRec _ -> error "Not handled RRec" - | RSort _ -> rt - | RHole _ -> rt - | RCast (loc,b,CastConv (k,t)) -> - RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | RCast (loc,b,CastCoerce) -> - RCast(loc,alpha_rt excluded b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" - | RApp(loc,f,args) -> - RApp(loc, + | GRec _ -> error "Not handled GRec" + | GSort _ -> rt + | GHole _ -> rt + | GCast (loc,b,CastConv (k,t)) -> + GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | GCast (loc,b,CastCoerce) -> + GCast(loc,alpha_rt excluded b,CastCoerce) + | GDynamic _ -> error "Not handled GDynamic" + | GApp(loc,f,args) -> + GApp(loc, alpha_rt excluded f, List.map (alpha_rt excluded) args ) @@ -386,35 +386,35 @@ and alpha_br excluded (loc,ids,patl,res) = *) let is_free_in id = let rec is_free_in = function - | RRef _ -> false - | RVar(_,id') -> id_ord id' id == 0 - | REvar _ -> false - | RPatVar _ -> false - | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) -> + | GRef _ -> false + | GVar(_,id') -> id_ord 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) | GLetIn(_,n,t,b) -> let check_in_b = match n with | Name id' -> id_ord id' id <> 0 | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | RCases(_,_,_,el,brl) -> + | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetTuple(_,nal,_,b,t) -> + | GLetTuple(_,nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> id'= id | _ -> false) nal) in is_free_in t || (check_in_nal && is_free_in b) - | RIf(_,cond,_,br1,br2) -> + | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> false - | RHole _ -> false - | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t - | RCast (_,b,CastCoerce) -> is_free_in b - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> false + | GHole _ -> false + | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,CastCoerce) -> is_free_in b + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt in @@ -451,69 +451,69 @@ let rec pattern_to_term = function let replace_var_by_term x_id term = let rec replace_var_by_pattern rt = match rt with - | RRef _ -> rt - | RVar(_,id) when id_ord id x_id == 0 -> term - | RVar _ -> rt - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> - RApp(loc, + | GRef _ -> rt + | GVar(_,id) when id_ord id x_id == 0 -> term + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, replace_var_by_pattern def, replace_var_by_pattern b ) - | RLetTuple(_,nal,_,_,_) + | GLetTuple(_,nal,_,_,_) when List.exists (function Name id -> id = x_id | _ -> false) nal -> rt - | RLetTuple(loc,nal,(na,rto),def,b) -> - RLetTuple(loc, + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, nal, (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> - RIf(loc, replace_var_by_pattern b, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv(k,t)) -> - RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,replace_var_by_pattern b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,replace_var_by_pattern b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl then br @@ -590,21 +590,21 @@ let ids_of_rawterm c = let rec ids_of_rawterm acc c = let idof = id_of_name in match c with - | RVar (_,id) -> id::acc - | RApp (loc,g,args) -> + | GVar (_,id) -> id::acc + | GApp (loc,g,args) -> ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc - | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc - | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc - | RLetTuple (_,nal,(na,po),b,c) -> + | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc + | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc + | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc + | GLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCases (loc,sty,rtntypopt,tml,brchl) -> + | GCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) - | RRec _ -> failwith "Fix inside a constructor branch" - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] + | GRec _ -> failwith "Fix inside a constructor branch" + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] in (* build the set *) List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) @@ -616,59 +616,59 @@ let ids_of_rawterm c = let zeta_normalize = let rec zeta_normalize_term rt = match rt with - | RRef _ -> rt - | RVar _ -> rt - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> - RApp(loc, + | GRef _ -> rt + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RLetIn(_,Name id,def,b) -> + | GLetIn(_,Name id,def,b) -> zeta_normalize_term (replace_var_by_term id def b) - | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b - | RLetTuple(loc,nal,(na,rto),def,b) -> - RLetTuple(loc, + | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, nal, (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> - RIf(loc, zeta_normalize_term b, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, zeta_normalize_term b, (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs ) - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv(k,t)) -> - RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,zeta_normalize_term b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,zeta_normalize_term b,CastCoerce) + | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -688,29 +688,29 @@ let expand_as = in let rec expand_as map rt = match rt with - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt - | RVar(_,id) -> + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt + | GVar(_,id) -> begin try Idmap.find id map with Not_found -> rt end - | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args) - | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b) - | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b) - | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) - | RLetTuple(loc,nal,(na,po),v,b) -> - RLetTuple(loc,nal,(na,Option.map (expand_as map) po), + | 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,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetTuple(loc,nal,(na,po),v,b) -> + GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) - | RIf(loc,e,(na,po),br1,br2) -> - RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + | GIf(loc,e,(na,po),br1,br2) -> + GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | RRec _ -> error "Not handled RRec" - | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) - | RCases(loc,sty,po,el,brl) -> - RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + | GRec _ -> error "Not handled GRec" + | GDynamic _ -> error "Not handled GDynamic" + | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | 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, 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) diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli index 465703386..9e872c236 100644 --- a/plugins/funind/rawtermops.mli +++ b/plugins/funind/rawtermops.mli @@ -7,60 +7,60 @@ val idmap_is_empty : 'a Names.Idmap.t -> bool (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) val get_pattern_id : cases_pattern -> Names.identifier list -(* [pattern_to_term pat] returns a rawconstr corresponding to [pat]. +(* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. [pat] must not contain occurences of anonymous pattern *) -val pattern_to_term : cases_pattern -> rawconstr +val pattern_to_term : cases_pattern -> glob_constr (* - Some basic functions to rebuild rawconstr + Some basic functions to rebuild glob_constr In each of them the location is Util.dummy_loc *) -val mkRRef : Libnames.global_reference -> rawconstr -val mkRVar : Names.identifier -> rawconstr -val mkRApp : rawconstr*(rawconstr list) -> rawconstr -val mkRLambda : Names.name * rawconstr * rawconstr -> rawconstr -val mkRProd : Names.name * rawconstr * rawconstr -> rawconstr -val mkRLetIn : Names.name * rawconstr * rawconstr -> rawconstr -val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr -val mkRSort : rawsort -> rawconstr -val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *) -val mkRCast : rawconstr* rawconstr -> rawconstr +val mkRRef : Libnames.global_reference -> glob_constr +val mkRVar : Names.identifier -> glob_constr +val mkRApp : glob_constr*(glob_constr list) -> glob_constr +val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr +val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr +val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr +val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr +val mkRSort : rawsort -> glob_constr +val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) +val mkRCast : glob_constr* glob_constr -> glob_constr (* - Some basic functions to decompose rawconstrs + Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr -val raw_decompose_prod_or_letin : - rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr -val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr -val raw_decompose_prod_or_letin_n : int -> rawconstr -> - (Names.name*rawconstr option*rawconstr option) list * rawconstr -val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr -val raw_compose_prod_or_letin: rawconstr -> - (Names.name*rawconstr option*rawconstr option) list -> rawconstr -val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) - - -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -val raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr -(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) -val raw_make_neq : rawconstr -> rawconstr -> rawconstr -(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) -val raw_make_or : rawconstr -> rawconstr -> rawconstr - -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding +val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin : + glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin_n : int -> glob_constr -> + (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr +val glob_compose_prod_or_letin: glob_constr -> + (Names.name*glob_constr option*glob_constr option) list -> glob_constr +val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) + + +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +val glob_make_neq : glob_constr -> glob_constr -> glob_constr +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +val glob_make_or : glob_constr -> glob_constr -> glob_constr + +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding to [P1 \/ ( .... \/ Pn)] *) -val raw_make_or_list : rawconstr list -> rawconstr +val glob_make_or_list : glob_constr list -> glob_constr (* alpha_conversion functions *) -(* Replace the var mapped in the rawconstr/context *) -val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr +(* Replace the var mapped in the glob_constr/context *) +val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr @@ -80,27 +80,27 @@ val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt conventions and does not share bound variables with avoid *) -val alpha_rt : Names.identifier list -> rawconstr -> rawconstr +val alpha_rt : Names.identifier list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Names.identifier list -> Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.rawconstr -> + Rawterm.glob_constr -> Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.rawconstr + Rawterm.glob_constr (* Reduction function *) val replace_var_by_term : Names.identifier -> - Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr + Rawterm.glob_constr -> Rawterm.glob_constr -> Rawterm.glob_constr (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) -val is_free_in : Names.identifier -> rawconstr -> bool +val is_free_in : Names.identifier -> glob_constr -> bool val are_unifiable : cases_pattern -> cases_pattern -> bool @@ -115,12 +115,12 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool val ids_of_pat : cases_pattern -> Names.Idset.t (* TODO: finish this function (Fix not treated) *) -val ids_of_rawterm: rawconstr -> Names.Idset.t +val ids_of_rawterm: glob_constr -> Names.Idset.t (* removing let_in construction in a rawterm *) -val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr +val zeta_normalize : Rawterm.glob_constr -> Rawterm.glob_constr -val expand_as : rawconstr -> rawconstr +val expand_as : glob_constr -> glob_constr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f066e39d0..1b43d4045 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1107,22 +1107,22 @@ let (value_f:constr list -> global_reference -> constr) = ) in let fun_body = - RCases + GCases (d0,RegularStyle,None, - [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), + [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), (Anonymous,None)], [d0, [v_id], [PatCstr(d0,(ind_of_ref (delayed_force coq_sig_ref),1), [PatVar(d0, Name v_id); PatVar(d0, Anonymous)], Anonymous)], - RVar(d0,v_id)]) + GVar(d0,v_id)]) in let value = List.fold_left2 (fun acc x_id a -> - RLambda - (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), + GLambda + (d0, Name x_id, Explicit, GDynamic(d0, constr_in a), acc ) ) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 64cfa0d01..112a13e53 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -141,7 +141,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in TacFun([Some(id_of_string"t")], TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None); + [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None); Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) (* let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 62fa0b2c9..0ea2290db 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -88,7 +88,7 @@ let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; print_subgoals () -let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) +let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index b6a42b6b4..5ef6f0f88 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -86,7 +86,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) = type rhs = { rhs_env : env; avoid_ids : identifier list; - it : rawconstr; + it : glob_constr; } type equation = @@ -234,7 +234,7 @@ type pattern_matching_problem = mat : matrix; caseloc : loc; casestyle: case_style; - typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment } + typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment } (*--------------------------------------------------------------------------* * A few functions to infer the inductive type from the patterns instead of * @@ -366,10 +366,10 @@ let find_tomatch_tycon isevars env loc = function | None -> empty_tycon let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_rawconstr tomatch) in + let loc = Some (loc_of_glob_constr tomatch) in let tycon = find_tomatch_tycon isevars env loc indopt in let j = typing_fun tycon env tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in + let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in isevars := evd; let typ = nf_evar ( !isevars) j.uj_type in let t = @@ -527,7 +527,7 @@ let extract_rhs pb = let occur_in_rhs na rhs = match na with | Anonymous -> false - | Name id -> occur_rawconstr id rhs.it + | Name id -> occur_glob_constr id rhs.it let is_dep_patt eqn = function | PatVar (_,name) -> occur_in_rhs name eqn.rhs @@ -1515,7 +1515,7 @@ let mk_JMeq typ x typ' y = mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |]) -let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) +let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) let constr_of_pat env isevars arsign pat avoid = let rec typ env (ty, realargs) pat avoid = @@ -1604,12 +1604,12 @@ let vars_of_ctx ctx = match b with | Some t' when kind_of_term t' = Rel 0 -> prev, - (RApp (dummy_loc, - (RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars + (GApp (dummy_loc, + (GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars | _ -> match na with Anonymous -> raise (Invalid_argument "vars_of_ctx") - | Name n -> n, RVar (dummy_loc, n) :: vars) + | Name n -> n, GVar (dummy_loc, n) :: vars) ctx (id_of_string "vars_of_ctx_error", []) in List.rev y @@ -1741,13 +1741,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = - let bref = RVar (dummy_loc, branch_name) in + let bref = GVar (dummy_loc, branch_name) in match vars_of_ctx rhs_rels with [] -> bref - | l -> RApp (dummy_loc, bref, l) + | l -> GApp (dummy_loc, bref, l) in let branch = match ineqs with - Some _ -> RApp (dummy_loc, branch, [ hole ]) + Some _ -> GApp (dummy_loc, branch, [ hole ]) | None -> branch in incr i; diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 852776630..24fdd679b 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -84,16 +84,16 @@ let interp_constr_judgment isevars env c = { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } let locate_if_isevar loc na = function - | RHole _ -> + | GHole _ -> (try match na with - | Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id) + | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> RHole (loc, Evd.BinderType na)) + with Not_found -> GHole (loc, Evd.BinderType na)) | x -> x let interp_binder sigma env na t = let t = Constrintern.intern_gen true ( !sigma) env t in - SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t) + SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t) let interp_context_evars evdref env params = let bl = Constrintern.intern_context false !evdref env params in @@ -102,7 +102,7 @@ let interp_context_evars evdref env params = (fun (env,params,n,impls) (na, k, b, t) -> match b with None -> - let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t' = locate_if_isevar (loc_of_glob_constr t) na t in let t = SPretyping.understand_tcc_evars evdref env IsType t' in let d = (na,None,t) in let impls = diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 2eb7408aa..09cc17328 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -58,7 +58,7 @@ let my_print_rec_info env t = str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ str "Full type: " ++ my_print_constr env t.f_fulltype -(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *) +(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *) (* str " and tycon "++ my_print_tycon env tycon ++ *) (* str " in environment: " ++ my_print_env env); *) @@ -81,9 +81,9 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.glob_constr = Constrintern.intern_constr evd env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.glob_constr = Constrintern.intern_type evd env let env_with_binders env isevars l = diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli index 48906b23c..2b0c8fda2 100644 --- a/plugins/subtac/subtac_pretyping.mli +++ b/plugins/subtac/subtac_pretyping.mli @@ -13,7 +13,7 @@ module Pretyping : Pretyping.S val interp : Environ.env -> Evd.evar_map ref -> - Rawterm.rawconstr -> + Rawterm.glob_constr -> Evarutil.type_constraint -> Term.constr * Term.constr val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list -> diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 3d79508c3..debd4f053 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -189,22 +189,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env evdref lvar c = -(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *) +(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) (* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) (* with _ -> () *) (* in *) match c with - | RRef (loc,ref) -> + | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref evdref env ref) tycon - | RVar (loc, id) -> + | GVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref (pretype_id loc env !evdref lvar id) tycon - | REvar (loc, ev, instopt) -> + | GEvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let hyps = evar_context (Evd.find !evdref ev) in @@ -215,10 +215,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon - | RPatVar (loc,(someta,n)) -> + | GPatVar (loc,(someta,n)) -> anomaly "Found a pattern variable in a rawterm to type" - | RHole (loc,k) -> + | GHole (loc,k) -> let ty = match tycon with | Some (None, ty) -> ty @@ -226,7 +226,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | RRec (loc,fixkind,names,bl,lar,vdef) -> + | GRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,k,None,ty)::bl -> @@ -306,10 +306,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon - | RSort (loc,s) -> + | GSort (loc,s) -> inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon - | RApp (loc,f,args) -> + | GApp (loc,f,args) -> let length = List.length args in let ftycon = let ty = @@ -326,11 +326,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | _ -> None in let fj = pretype ftycon env evdref lvar f in - let floc = loc_of_rawconstr f in + let floc = loc_of_glob_constr f in let rec apply_rec env n resj tycon = function | [] -> resj | c::rest -> - let argloc = loc_of_rawconstr c in + let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with @@ -364,7 +364,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLambda(loc,name,k,c1,c2) -> + | GLambda(loc,name,k,c1,c2) -> let tycon' = evd_comb1 (fun evd tycon -> match tycon with @@ -382,7 +382,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let resj = judge_of_abstraction env name j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RProd(loc,name,k,c1,c2) -> + | GProd(loc,name,k,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in let var = (name,j.utj_val) in let env' = Termops.push_rel_assum var env in @@ -392,7 +392,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLetIn(loc,name,c1,c2) -> + | GLetIn(loc,name,c1,c2) -> let j = pretype empty_tycon env evdref lvar c1 in let t = Termops.refresh_universes j.uj_type in let var = (name,Some j.uj_val,t) in @@ -401,12 +401,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } - | RLetTuple (loc,nal,(na,po),c,d) -> + | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in @@ -466,12 +466,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = ccl }) - | RIf (loc,c,(na,po),b1,b2) -> + | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then @@ -536,12 +536,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = p } - | RCases (loc,sty,po,tml,eqns) -> + | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) - | RCast (loc,c,k) -> + | GCast (loc,c,k) -> let cj = match k with CastCoerce -> @@ -557,7 +557,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in inh_conv_coerce_to_tycon loc env evdref cj tycon - | RDynamic (loc,d) -> + | GDynamic (loc,d) -> if (Dyn.tag d) = "constr" then let c = constr_out d in let j = (Retyping.get_judgment_of env !evdref c) in @@ -568,7 +568,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type valcon env evdref lvar = function - | RHole loc -> + | GHole loc -> (match valcon with | Some v -> let s = @@ -588,7 +588,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct utj_type = s}) | c -> let j = pretype empty_tycon env evdref lvar c in - let loc = loc_of_rawconstr c in + let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with | None -> tj @@ -596,7 +596,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct if e_cumul env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env !evdref tj.utj_val v let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 106ac4d09..43b55ca95 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -116,7 +116,7 @@ let my_print_rel_context env ctx = Printer.pr_rel_context env ctx let my_print_context = Termops.print_rel_context let my_print_named_context = Termops.print_named_context let my_print_env = Termops.print_env -let my_print_rawconstr = Printer.pr_rawconstr_env +let my_print_glob_constr = Printer.pr_glob_constr_env let my_print_evardefs = Evd.pr_evar_map let my_print_tycon_type = Evarutil.pr_tycon_type diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index f56c2932e..659a67781 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -74,7 +74,7 @@ val my_print_context : env -> std_ppcmds val my_print_rel_context : env -> rel_context -> std_ppcmds val my_print_named_context : env -> std_ppcmds val my_print_env : env -> std_ppcmds -val my_print_rawconstr : env -> rawconstr -> std_ppcmds +val my_print_glob_constr : env -> glob_constr -> std_ppcmds val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 79e1a6eb2..50498f0f4 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -39,9 +39,9 @@ let interp_ascii dloc p = let rec aux n p = if n = 0 then [] else let mp = p mod 2 in - RRef (dloc,if mp = 0 then glob_false else glob_true) + GRef (dloc,if mp = 0 then glob_false else glob_true) :: (aux (n-1) (p/2)) in - RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p) + GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p) let interp_ascii_string dloc s = let p = @@ -57,12 +57,12 @@ let interp_ascii_string dloc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when n = 0 -> 0 - | RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) + | GRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let rec aux = function - | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l + | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -78,4 +78,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true) + ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index b673fdb9d..3d8860be4 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -36,11 +36,11 @@ let nat_of_int dloc n = strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed)."); - let ref_O = RRef (dloc, glob_O) in - let ref_S = RRef (dloc, glob_S) in + let ref_O = GRef (dloc, glob_O) in + let ref_S = GRef (dloc, glob_S) in let rec mk_nat acc n = if n <> zero then - mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) else acc in @@ -56,8 +56,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) - | RRef (_,z) when z = glob_O -> zero + | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) + | GRef (_,z) when z = glob_O -> zero | _ -> raise Non_closed_number let uninterp_nat p = @@ -73,4 +73,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,["Coq";"Init";"Datatypes"]) nat_of_int - ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true) + ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 2a0425dca..892a5595a 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -98,9 +98,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint dloc n = - let ref_construct = RRef (dloc, int31_construct) in - let ref_0 = RRef (dloc, int31_0) in - let ref_1 = RRef (dloc, int31_1) in + let ref_construct = GRef (dloc, int31_construct) in + let ref_0 = GRef (dloc, int31_0) in + let ref_1 = GRef (dloc, int31_1) in let rec args counter n = if counter <= 0 then [] @@ -108,7 +108,7 @@ let int31_of_pos_bigint dloc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - RApp (dloc, ref_construct, List.rev (args 31 n)) + GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") @@ -125,12 +125,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur) - | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur) + | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in function - | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero + | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero | _ -> raise Non_closed let uninterp_int31 i = @@ -143,7 +143,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([RRef (Util.dummy_loc, int31_construct)], + ([GRef (Util.dummy_loc, int31_construct)], uninterp_int31, true) @@ -174,24 +174,24 @@ let height bi = (* n must be a non-negative integer (from bigint.ml) *) let word_of_pos_bigint dloc hght n = - let ref_W0 = RRef (dloc, zn2z_W0) in - let ref_WW = RRef (dloc, zn2z_WW) in + let ref_W0 = GRef (dloc, zn2z_W0) in + let ref_WW = GRef (dloc, zn2z_WW) in let rec decomp hgt n = if is_neg_or_zero hgt then int31_of_pos_bigint dloc n else if equal n zero then - RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)]) + GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)]) else let (h,l) = split_at hgt n in - RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole); + GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole); decomp (sub_1 hgt) h; decomp (sub_1 hgt) l]) in decomp hght n let bigN_of_pos_bigint dloc n = - let ref_constructor i = RRef (dloc, bigN_constructor i) in - let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then + let ref_constructor i = GRef (dloc, bigN_constructor i) in + let result h word = GApp (dloc, ref_constructor h, if less_than h n_inlined then [word] else [Nat_syntax.nat_of_int dloc (sub h n_inlined); @@ -215,7 +215,7 @@ let interp_bigN dloc n = let bigint_of_word = let rec get_height rc = match rc with - | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW -> + | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW -> let hleft = get_height lft in let hright = get_height rght in add_1 @@ -227,8 +227,8 @@ let bigint_of_word = in let rec transform hght rc = match rc with - | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero - | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in + | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero + | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in add (mult (rank new_hght) (transform (new_hght) lft)) (transform (new_hght) rght) @@ -240,8 +240,8 @@ let bigint_of_word = let bigint_of_bigN rc = match rc with - | RApp (_,_,[one_arg]) -> bigint_of_word one_arg - | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg + | GApp (_,_,[one_arg]) -> bigint_of_word one_arg + | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg | _ -> raise Non_closed let uninterp_bigN rc = @@ -257,7 +257,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if less_than i (add_1 n_inlined) then - RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) + GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) else [] in @@ -274,17 +274,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope (*** Parsing for bigZ in digital notation ***) let interp_bigZ dloc n = - let ref_pos = RRef (dloc, bigZ_pos) in - let ref_neg = RRef (dloc, bigZ_neg) in + let ref_pos = GRef (dloc, bigZ_pos) in + let ref_neg = GRef (dloc, bigZ_neg) in if is_pos_or_zero n then - RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) + GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) else - RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) + GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg - | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg -> + | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg + | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg -> let opp_val = bigint_of_bigN one_arg in if equal opp_val zero then raise Non_closed @@ -303,19 +303,19 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([RRef (Util.dummy_loc, bigZ_pos); - RRef (Util.dummy_loc, bigZ_neg)], + ([GRef (Util.dummy_loc, bigZ_pos); + GRef (Util.dummy_loc, bigZ_neg)], uninterp_bigZ, true) (*** Parsing for bigQ in digital notation ***) let interp_bigQ dloc n = - let ref_z = RRef (dloc, bigQ_z) in - RApp (dloc, ref_z, [interp_bigZ dloc n]) + let ref_z = GRef (dloc, bigQ_z) in + GApp (dloc, ref_z, [interp_bigZ dloc n]) let uninterp_bigQ rc = try match rc with - | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z -> + | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z -> Some (bigint_of_bigZ one_arg) | _ -> None (* we don't pretty-print yet fractions *) with Non_closed -> None @@ -324,5 +324,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, + ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 7f093ae95..fc953e5e5 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -46,24 +46,24 @@ let four = mult_2 two (* Unary representation of strictly positive numbers *) let rec small_r dloc n = - if equal one n then RRef (dloc, glob_R1) - else RApp(dloc,RRef (dloc,glob_Rplus), - [RRef (dloc, glob_R1);small_r dloc (sub_1 n)]) + if equal one n then GRef (dloc, glob_R1) + else GApp(dloc,GRef (dloc,glob_Rplus), + [GRef (dloc, glob_R1);small_r dloc (sub_1 n)]) let r_of_posint dloc n = - let r1 = RRef (dloc, glob_R1) in + let r1 = GRef (dloc, glob_R1) in let r2 = small_r dloc two in let rec r_of_pos n = if less_than n four then small_r dloc n else let (q,r) = div2_with_rest n in - let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in - if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in - if n <> zero then r_of_pos n else RRef(dloc,glob_R0) + let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in + if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in + if n <> zero then r_of_pos n else GRef(dloc,glob_R0) let r_of_int dloc z = if is_strictly_neg z then - RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) + GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) else r_of_posint dloc z @@ -75,33 +75,33 @@ let bignat_of_r = (* for numbers > 1 *) let rec bignat_of_pos = function (* 1+1 *) - | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) + | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two (* 1+(1+1) *) - | RApp (_,RRef (_,p1), [RRef (_,o1); - RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])]) + | GApp (_,GRef (_,p1), [GRef (_,o1); + GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) when p1 = glob_Rplus & p2 = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three (* (1+1)*b *) - | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult -> + | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult -> if bignat_of_pos a <> two then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) - | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])]) + | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> if bignat_of_pos a <> two then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number in let bignat_of_r = function - | RRef (_,a) when a = glob_R0 -> zero - | RRef (_,a) when a = glob_R1 -> one + | GRef (_,a) when a = glob_R0 -> zero + | GRef (_,a) when a = glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> + | GApp (_,GRef (_,o), [a]) when o = glob_Ropp -> let n = bignat_of_r a in if n = zero then raise Non_closed_number; neg n @@ -116,8 +116,8 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0); - RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult); - RRef(dummy_loc,glob_R1)], + ([GRef(dummy_loc,glob_Ropp);GRef(dummy_loc,glob_R0); + GRef(dummy_loc,glob_Rplus);GRef(dummy_loc,glob_Rmult); + GRef(dummy_loc,glob_R1)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index cb2b16858..61643881e 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -37,8 +37,8 @@ open Lazy let interp_string dloc s = let le = String.length s in let rec aux n = - if n = le then RRef (dloc, force glob_EmptyString) else - RApp (dloc,RRef (dloc, force glob_String), + if n = le then GRef (dloc, force glob_EmptyString) else + GApp (dloc,GRef (dloc, force glob_String), [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) in aux 0 @@ -46,11 +46,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | RApp (_,RRef (_,k),[a;s]) when k = force glob_String -> + | GApp (_,GRef (_,k),[a;s]) when k = force glob_String -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | RRef (_,z) when z = force glob_EmptyString -> + | GRef (_,z) when z = force glob_EmptyString -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -62,6 +62,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([RRef (dummy_loc,static_glob_String); - RRef (dummy_loc,static_glob_EmptyString)], + ([GRef (dummy_loc,static_glob_String); + GRef (dummy_loc,static_glob_EmptyString)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index fb8de1f92..81588bced 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -42,13 +42,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat dloc x = - let ref_xI = RRef (dloc, glob_xI) in - let ref_xH = RRef (dloc, glob_xH) in - let ref_xO = RRef (dloc, glob_xO) in + let ref_xI = GRef (dloc, glob_xI) in + let ref_xH = GRef (dloc, glob_xH) in + let ref_xO = GRef (dloc, glob_xO) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> RApp (dloc, ref_xO,[pos_of q]) - | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q]) + | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) + | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -66,9 +66,9 @@ let interp_positive dloc n = (**********************************************************************) let rec bignat_of_pos = function - | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) - | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) - | RRef (_, a) when a = glob_xH -> Bigint.one + | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a) when a = glob_xH -> Bigint.one | _ -> raise Non_closed_number let uninterp_positive p = @@ -84,9 +84,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,positive_module) interp_positive - ([RRef (dummy_loc, glob_xI); - RRef (dummy_loc, glob_xO); - RRef (dummy_loc, glob_xH)], + ([GRef (dummy_loc, glob_xI); + GRef (dummy_loc, glob_xO); + GRef (dummy_loc, glob_xH)], uninterp_positive, true) @@ -106,9 +106,9 @@ let n_path = make_path binnat_module "N" let n_of_binnat dloc pos_or_neg n = if n <> zero then - RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n]) else - RRef (dloc, glob_N0) + GRef (dloc, glob_N0) let error_negative dloc = user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") @@ -122,8 +122,8 @@ let n_of_int dloc n = (**********************************************************************) let bignat_of_n = function - | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a - | RRef (_, a) when a = glob_N0 -> Bigint.zero + | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a + | GRef (_, a) when a = glob_N0 -> Bigint.zero | _ -> raise Non_closed_number let uninterp_n p = @@ -136,8 +136,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnat_module) n_of_int - ([RRef (dummy_loc, glob_N0); - RRef (dummy_loc, glob_Npos)], + ([GRef (dummy_loc, glob_N0); + GRef (dummy_loc, glob_Npos)], uninterp_n, true) @@ -160,18 +160,18 @@ let z_of_int dloc n = if n <> zero then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n]) else - RRef (dloc, glob_ZERO) + GRef (dloc, glob_ZERO) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function - | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a - | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) - | RRef (_, a) when a = glob_ZERO -> Bigint.zero + | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a) when a = glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number let uninterp_z p = @@ -185,8 +185,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binint_module) z_of_int - ([RRef (dummy_loc, glob_ZERO); - RRef (dummy_loc, glob_POS); - RRef (dummy_loc, glob_NEG)], + ([GRef (dummy_loc, glob_ZERO); + GRef (dummy_loc, glob_POS); + GRef (dummy_loc, glob_NEG)], uninterp_z, true) |