diff options
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) |