diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 120 | ||||
| -rw-r--r-- | interp/constrextern.mli | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 158 | ||||
| -rw-r--r-- | interp/constrintern.mli | 18 | ||||
| -rw-r--r-- | interp/doc.tex | 2 | ||||
| -rw-r--r-- | interp/genarg.ml | 6 | ||||
| -rw-r--r-- | interp/genarg.mli | 32 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 26 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 56 | ||||
| -rw-r--r-- | interp/notation.mli | 18 | ||||
| -rw-r--r-- | interp/reserve.ml | 46 | ||||
| -rw-r--r-- | interp/reserve.mli | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 244 | ||||
| -rw-r--r-- | interp/topconstr.mli | 32 |
15 files changed, 385 insertions, 385 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index eb779200c3..4029f61507 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -29,7 +29,7 @@ open Reserve open Detyping (*i*) -(* Translation from rawconstr to front constr *) +(* Translation from glob_constr to front constr *) (**********************************************************************) (* Parametrization *) @@ -272,7 +272,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) = (fun (loc,p) -> CPatPrim (loc,p)) destPatPrim terms - (* Better to use extern_rawconstr composed with injection/retraction ?? *) + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.raw_print or !print_no_symbol then raise No_match; @@ -458,7 +458,7 @@ let rec extern_args extern scopes env args subscopes = extern argscopes env a :: extern_args extern scopes env args subscopes let rec remove_coercions inctx = function - | RApp (loc,RRef (_,r),args) as c + | GApp (loc,GRef (_,r),args) as c when not (!Flags.raw_print or !print_coercions) -> let nargs = List.length args in @@ -477,13 +477,13 @@ let rec remove_coercions inctx = function been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if l = [] then a' else RApp (loc,a',l) + if l = [] then a' else GApp (loc,a',l) | _ -> c with Not_found -> c) | c -> c let rec flatten_application = function - | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l)) + | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l)) | a -> a (**********************************************************************) @@ -495,7 +495,7 @@ let extern_possible_prim_token scopes r = let (sc,n) = uninterp_prim_token r in match availability_of_prim_token n sc scopes with | None -> None - | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key) + | Some key -> Some (insert_delimiters (CPrim (loc_of_glob_constr r,n)) key) with No_match -> None @@ -525,23 +525,23 @@ let rec extern inctx scopes vars r = if !Flags.raw_print or !print_no_symbol then raise No_match; extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with - | RRef (loc,ref) -> + | GRef (loc,ref) -> extern_global loc (select_stronger_impargs (implicits_of_global ref)) (extern_reference loc vars ref) - | RVar (loc,id) -> CRef (Ident (loc,id)) + | GVar (loc,id) -> CRef (Ident (loc,id)) - | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) + | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) - | REvar (loc,n,l) -> + | GEvar (loc,n,l) -> extern_evar loc n (Option.map (List.map (extern false scopes vars)) l) - | RPatVar (loc,n) -> + | GPatVar (loc,n) -> if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n) - | RApp (loc,f,args) -> + | GApp (loc,f,args) -> (match f with - | RRef (rloc,ref) -> + | GRef (rloc,ref) -> let subscopes = find_arguments_scope ref in let args = extern_args (extern true) (snd scopes) vars args subscopes in @@ -587,63 +587,63 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) - | RProd (loc,Anonymous,_,t,c) -> + | GProd (loc,Anonymous,_,t,c) -> (* Anonymous product are never factorized *) CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c) - | RLetIn (loc,na,t,c) -> + | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) - | RProd (loc,na,bk,t,c) -> + | GProd (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RLambda (loc,na,bk,t,c) -> + | GLambda (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RCases (loc,sty,rtntypopt,tml,eqns) -> + | GCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with - Anonymous, RVar (_,id) when - rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt) + Anonymous, GVar (_,id) when + rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt) -> Some (dummy_loc,Anonymous) | Anonymous, _ -> None - | Name id, RVar (_,id') when id=id' -> None + | Name id, GVar (_,id') when id=id' -> None | Name _, _ -> Some (dummy_loc,na) in (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,n,nal) -> let params = list_tabulate - (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in + (fun _ -> GHole (dummy_loc,Evd.InternalHole)) n in let args = List.map (function - | Anonymous -> RHole (dummy_loc,Evd.InternalHole) - | Name id -> RVar (dummy_loc,id)) nal in - let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in + | Anonymous -> GHole (dummy_loc,Evd.InternalHole) + | Name id -> GVar (dummy_loc,id)) nal in + let t = GApp (dummy_loc,GRef (dummy_loc,IndRef ind),params@args) in (extern_typ scopes vars t)) x))) tml in let eqns = List.map (extern_eqn inctx scopes vars) eqns in CCases (loc,sty,rtntypopt',tml,eqns) - | RLetTuple (loc,nal,(na,typopt),tm,b) -> + | GLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal, (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) - | RIf (loc,c,(na,typopt),b1,b2) -> + | GIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) - | RRec (loc,fk,idv,blv,tyv,bv) -> + | GRec (loc,fk,idv,blv,tyv,bv) -> let vars' = Array.fold_right Idset.add idv vars in (match fk with | RFix (nv,n) -> @@ -674,16 +674,16 @@ let rec extern inctx scopes vars r = in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) - | RSort (loc,s) -> CSort (loc,extern_rawsort s) + | GSort (loc,s) -> CSort (loc,extern_rawsort s) - | RHole (loc,e) -> CHole (loc, Some e) + | GHole (loc,e) -> CHole (loc, Some e) - | RCast (loc,c, CastConv (k,t)) -> + | GCast (loc,c, CastConv (k,t)) -> CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) - | RCast (loc,c, CastCoerce) -> + | GCast (loc,c, CastCoerce) -> CCast (loc,sub_extern true scopes vars c, CastCoerce) - | RDynamic (loc,d) -> CDynamic (loc,d) + | GDynamic (loc,d) -> CDynamic (loc,d) and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes) @@ -695,7 +695,7 @@ and factorize_prod scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RProd (loc,(Name id as na),bk,ty,c) + | GProd (loc,(Name id as na),bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in @@ -707,7 +707,7 @@ and factorize_lambda inctx scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RLambda (loc,na,bk,ty,c) + | GLambda (loc,na,bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) -> let (nal,c) = @@ -743,11 +743,11 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> - let loc = Rawterm.loc_of_rawconstr t in + let loc = Rawterm.loc_of_glob_constr t in try (* Adjusts to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match t,n with - | RApp (_,(RRef (_,ref) as f),args), Some n + | GApp (_,(GRef (_,ref) as f),args), Some n when List.length args >= n -> let args1, args2 = list_chop n args in let subscopes = @@ -757,15 +757,15 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function select_impargs_size (List.length args) (implicits_of_global ref) in try list_skipn n impls with _ -> [] in - (if n = 0 then f else RApp (dummy_loc,f,args1)), + (if n = 0 then f else GApp (dummy_loc,f,args1)), args2, subscopes, impls - | RApp (_,(RRef (_,ref) as f),args), None -> + | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], [] + | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -815,10 +815,10 @@ and extern_recursion_order scopes vars = function Option.map (extern true scopes vars) r) -let extern_rawconstr vars c = +let extern_glob_constr vars c = extern false (None,[]) vars c -let extern_rawtype vars c = +let extern_glob_type vars c = extern_typ (None,[]) vars c (******************************************************************) @@ -841,7 +841,7 @@ let extern_constr at_top env t = let extern_type at_top env t = let avoid = if at_top then ids_of_context env else [] in let r = Detyping.detype at_top avoid (names_of_rel_context env) t in - extern_rawtype (vars_of_env env) r + extern_glob_type (vars_of_env env) r let extern_sort s = extern_rawsort (detype_sort s) @@ -849,37 +849,37 @@ let extern_sort s = extern_rawsort (detype_sort s) (* Main translation function from pattern -> constr_expr *) let rec raw_of_pat env = function - | PRef ref -> RRef (loc,ref) - | PVar id -> RVar (loc,id) - | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) + | PRef ref -> GRef (loc,ref) + | PVar id -> GVar (loc,id) + | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly "rawconstr_of_pattern: index to an anonymous variable" + anomaly "glob_constr_of_pattern: index to an anonymous variable" with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in - RVar (loc,id) - | PMeta None -> RHole (loc,Evd.InternalHole) - | PMeta (Some n) -> RPatVar (loc,(false,n)) + GVar (loc,id) + | PMeta None -> GHole (loc,Evd.InternalHole) + | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> - RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) + GApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) | PSoApp (n,args) -> - RApp (loc,RPatVar (loc,(true,n)), + GApp (loc,GPatVar (loc,(true,n)), List.map (raw_of_pat env) args) | PProd (na,t,c) -> - RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c) + GProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c) | PLetIn (na,t,c) -> - RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) + GLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | PLambda (na,t,c) -> - RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c) + GLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c) | PIf (c,b1,b2) -> - RIf (loc, raw_of_pat env c, (Anonymous,None), + GIf (loc, raw_of_pat env c, (Anonymous,None), raw_of_pat env b1, raw_of_pat env b2) | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in - RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) + GLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) | PCase (_,PMeta None,tm,[||]) -> - RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[]) + GCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[]) | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> let brs = Array.to_list (Array.map (raw_of_pat env) bv) in let brns = Array.to_list cstr_nargs in @@ -891,10 +891,10 @@ let rec raw_of_pat env = function else let nparams,n = Option.get ind_nargs in return_type_of_predicate ind nparams n (raw_of_pat env p) in - RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat) + GCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) | PCoFix c -> Detyping.detype false [] env (mkCoFix c) - | PSort s -> RSort (loc,s) + | PSort s -> GSort (loc,s) let extern_constr_pattern env pat = extern true (None,[]) Idset.empty (raw_of_pat env pat) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 08f089d4e9..979c974acd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -25,8 +25,8 @@ val check_same_type : constr_expr -> constr_expr -> unit trees for printing *) val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr -val extern_rawconstr : Idset.t -> rawconstr -> constr_expr -val extern_rawtype : Idset.t -> rawconstr -> constr_expr +val extern_glob_constr : Idset.t -> glob_constr -> constr_expr +val extern_glob_type : Idset.t -> glob_constr -> constr_expr val extern_constr_pattern : names_context -> constr_pattern -> constr_expr (** If [b=true] in [extern_constr b env c] then the variables in the first diff --git a/interp/constrintern.ml b/interp/constrintern.ml index fad3c49105..c097ce43d9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -46,7 +46,7 @@ type var_internalization_data = type internalization_env = (identifier * var_internalization_data) list -type raw_binder = (name * binding_kind * rawconstr option * rawconstr) +type glob_binder = (name * binding_kind * glob_constr option * glob_constr) let interning_grammar = ref false @@ -295,12 +295,12 @@ let reset_tmp_scope (ids,unb,tmp_scope,scopes) = let rec it_mkRProd env body = match env with - (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + (na, bk, _, t) :: tl -> it_mkRProd tl (GProd (dummy_loc, na, bk, t, body)) | [] -> body let rec it_mkRLambda env body = match env with - (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + (na, bk, _, t) :: tl -> it_mkRLambda tl (GLambda (dummy_loc, na, bk, t, body)) | [] -> body (**********************************************************************) @@ -313,11 +313,11 @@ let check_capture loc ty = function () 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 check_hidden_implicit_parameters id (_,_,_,impls) = @@ -350,9 +350,9 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar Implicit_quantifiers.combine_params_freevar ty in let ty' = intern_type (ids,true,tmpsc,sc) ty in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in + let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in + let bl = List.map (fun (id, loc) -> (Name id, b, None, GHole (loc, Evd.BinderType (Name id)))) fvs in let na = match na with | Anonymous -> if global_level then na @@ -383,11 +383,11 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b env, b @ bl) | LocalRawDef((loc,na as locna),def) -> (push_name_env lvar env locna, - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + (na,Explicit,Some(intern env def),GHole(loc,Evd.BinderType na))::bl) let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = let c = intern (ids,true,tmp_scope,scopes) c in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in + let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids c in let env', c' = let abs = let pi = @@ -399,10 +399,10 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a in if pi then (fun (id, loc') acc -> - RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) else (fun (id, loc') acc -> - RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> let env' = push_name_env lvar env (loc, Name id) in @@ -426,7 +426,7 @@ let iterate_binder intern lvar (env,bl) = function env, b @ bl) | LocalRawDef((loc,na as locna),def) -> (push_name_env lvar env locna, - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + (na,Explicit,Some(intern env def),GHole(loc,Evd.BinderType na))::bl) (**********************************************************************) (* Syntax extensions *) @@ -460,10 +460,10 @@ let traverse_binder (terms,_,_ as subst) (renaming',env), Name id' let rec subst_iterator y t = function - | RVar (_,id) as x -> if id = y then t else x - | x -> map_rawconstr (subst_iterator y t) x + | GVar (_,id) as x -> if id = y then t else x + | x -> map_glob_constr (subst_iterator y t) x -let subst_aconstr_in_rawconstr loc intern lvar subst infos c = +let subst_aconstr_in_glob_constr loc intern lvar subst infos c = let (terms,termlists,binders) = subst in let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c = let subinfos = renaming,(ids,unb,None,scopes) in @@ -477,10 +477,10 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = intern (ids,unb,scopt,subscopes@scopes) a with Not_found -> try - RVar (loc,List.assoc id renaming) + GVar (loc,List.assoc id renaming) with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) - RVar (loc,id) + GVar (loc,id) end | AList (x,_,iter,terminator,lassoc) -> (try @@ -497,7 +497,7 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = let na = try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in - RHole (loc,Evd.BinderType na) + GHole (loc,Evd.BinderType na) | ABinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -512,12 +512,12 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = anomaly "Inconsistent substitution of recursive notation") | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> let (na,bk,_,t) = snd (Option.get binderopt) in - RProd (loc,na,bk,t,aux subst' infos c') + GProd (loc,na,bk,t,aux subst' infos c') | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> let (na,bk,_,t) = snd (Option.get binderopt) in - RLambda (loc,na,bk,t,aux subst' infos c') + GLambda (loc,na,bk,t,aux subst' infos c') | t -> - rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + glob_constr_of_aconstr_with_binders loc (traverse_binder subst) (aux subst') subinfos t in aux (terms,None) infos c @@ -538,7 +538,7 @@ let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs = let terms = make_subst ids args in let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in - subst_aconstr_in_rawconstr loc intern lvar + subst_aconstr_in_glob_constr loc intern lvar (terms,termlists,binders) ([],env) c (**********************************************************************) @@ -558,20 +558,20 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), make_implicits_list impls, argsc, expl_impls + GVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Idset.mem id ids or List.mem id ltacvars then - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] (* Is [id] a notation variable *) else if List.mem_assoc id ntnvars then - (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], []) + (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) (* Is [id] the special variable for recursive notations *) else if ntnvars <> [] && id = ldots_var then - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] else (* Is [id] bound to a free name in ltac (this is an ltac error message) *) try @@ -589,14 +589,14 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - RRef (loc, ref), impls, scopes, [] + GRef (loc, ref), impls, scopes, [] with _ -> (* [id] a goal variable *) - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] let find_appl_head_data = function - | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] - | RApp (_,RRef (_,ref),l) as x + | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] + | GApp (_,GRef (_,ref),l) as x when l <> [] & Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in x,List.map (drop_first_implicits n) (implicits_of_global ref), @@ -629,7 +629,7 @@ let intern_reference ref = let intern_qualid loc qid intern env lvar args = match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> - RRef (loc, ref), args + GRef (loc, ref), args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -637,12 +637,12 @@ let intern_qualid loc qid intern env lvar args = let args1,args2 = list_chop nids args in check_no_explicitation args1; let subst = make_subst ids (List.map fst args1) in - subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2 + subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2 (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar args = match intern_qualid loc qid intern env lvar args with - | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid + | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function @@ -659,7 +659,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function with e -> (* Extra allowance for non globalizing functions *) if !interning_grammar || unb then - (RVar (loc,id), [], [], []),args + (GVar (loc,id), [], [], []),args else raise e let interp_reference vars r = @@ -1046,7 +1046,7 @@ let merge_impargs l args = let check_projection isproj nargs r = match (r,isproj) with - | RRef (loc, ref), Some _ -> + | GRef (loc, ref), Some _ -> (try let n = Recordops.find_projection_nparams ref + 1 in if nargs <> n then @@ -1054,15 +1054,15 @@ let check_projection isproj nargs r = with Not_found -> user_err_loc (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) - | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.") + | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.") | _, None -> () let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) - | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) + | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) + | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) | _ -> anomaly "Only refs have implicits" let exists_implicit_name id = @@ -1112,7 +1112,7 @@ let internalize sigma globalenv env allow_patvar lvar c = intern_applied_reference intern env lvar [] ref in (match intern_impargs c env imp subscopes l with | [] -> c - | l -> RApp (constr_loc x, c, l)) + | l -> GApp (constr_loc x, c, l)) | CFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in @@ -1144,7 +1144,7 @@ let internalize sigma globalenv env allow_patvar lvar c = ((n, ro), List.rev rbl, intern_type (ids',unb,tmp_scope,scopes) ty, intern (ids'',unb,None,scopes) bd)) dl in - RRec (loc,RFix + GRec (loc,RFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, @@ -1166,13 +1166,13 @@ let internalize sigma globalenv env allow_patvar lvar c = (List.rev rbl, intern_type (ids',unb,tmp_scope,scopes) ty, intern (ids'',unb,None,scopes) bd)) dl in - RRec (loc,RCoFix n, + GRec (loc,RCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CArrow (loc,c1,c2) -> - RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) + GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> intern_type env c2 | CProdN (loc,(nal,bk,ty)::bll,c2) -> @@ -1182,7 +1182,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal | CLetIn (loc,na,c1,c2) -> - RLetIn (loc, snd na, intern (reset_tmp_scope env) c1, + GLetIn (loc, snd na, intern (reset_tmp_scope env) c1, intern (push_name_env lvar env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> @@ -1201,8 +1201,8 @@ let internalize sigma globalenv env allow_patvar lvar c = let args = List.map (fun a -> (a,None)) args in intern_applied_reference intern env lvar args ref in check_projection isproj (List.length args) f; - (* Rem: RApp(_,f,[]) stands for @f *) - RApp (loc, f, intern_args env args_scopes (List.map fst args)) + (* Rem: GApp(_,f,[]) stands for @f *) + GApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with (* Compact notations like "t.(f args') args" *) @@ -1221,8 +1221,8 @@ let internalize sigma globalenv env allow_patvar lvar c = check_projection isproj (List.length args) c; (match c with (* Now compact "(f args') args" *) - | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) - | _ -> RApp (loc, c, args)) + | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args) + | _ -> GApp (loc, c, args)) | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs @@ -1244,14 +1244,14 @@ let internalize sigma globalenv env allow_patvar lvar c = tms ([],env) in let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, sty, rtnpo, tms, List.flatten eqns') + GCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let p' = Option.map (fun p -> let env'' = List.fold_left (push_name_env lvar) env ids in intern_type env'' p) po in - RLetTuple (loc, List.map snd nal, (na', p'), b', + GLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in @@ -1259,23 +1259,23 @@ let internalize sigma globalenv env allow_patvar lvar c = let p' = Option.map (fun p -> let env'' = List.fold_left (push_name_env lvar) env ids in intern_type env'' p) po in - RIf (loc, c', (na', p'), intern env b1, intern env b2) + GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> - RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) + GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) | CPatVar (loc, n) when allow_patvar -> - RPatVar (loc, n) + GPatVar (loc, n) | CPatVar (loc, _) -> raise (InternalizationError (loc,IllegalMetavariable)) | CEvar (loc, n, l) -> - REvar (loc, n, Option.map (List.map (intern env)) l) + GEvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> - RSort(loc,s) + GSort(loc,s) | CCast (loc, c1, CastConv (k, c2)) -> - RCast (loc,intern env c1, CastConv (k, intern_type env c2)) + GCast (loc,intern env c1, CastConv (k, intern_type env c2)) | CCast (loc, c1, CastCoerce) -> - RCast (loc,intern env c1, CastCoerce) + GCast (loc,intern env c1, CastCoerce) - | CDynamic (loc,d) -> RDynamic (loc,d) + | CDynamic (loc,d) -> GDynamic (loc,d) and intern_type env = intern (set_type_scope env) @@ -1318,17 +1318,17 @@ let internalize sigma globalenv env allow_patvar lvar c = let tids = List.fold_right Idset.add tids Idset.empty in let t = intern_type (tids,unb,None,scopes) t in let loc,ind,l = match t with - | RRef (loc,IndRef ind) -> (loc,ind,[]) - | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) in + | GRef (loc,IndRef ind) -> (loc,ind,[]) + | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l) + | _ -> error_bad_inductive_type (loc_of_glob_constr t) in let nparams, nrealargs = inductive_nargs globalenv ind in let nindargs = nparams + nrealargs in if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole (loc,_) -> loc,Anonymous - | RVar (loc,id) -> loc,Name id - | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in + | GHole (loc,_) -> loc,Anonymous + | GVar (loc,id) -> loc,Name id + | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in if List.exists (fun (_,na) -> na <> Anonymous) parnal then error_inductive_parameter_not_implicit loc; @@ -1336,8 +1336,8 @@ let internalize sigma globalenv env allow_patvar lvar c = | None -> [], None in let na = match tm', na with - | RVar (loc,id), None when Idset.mem id vars -> loc,Name id - | RRef (loc, VarRef id), None -> loc,Name id + | GVar (loc,id), None when Idset.mem id vars -> loc,Name id + | GRef (loc, VarRef id), None -> loc,Name id | _, None -> dummy_loc,Anonymous | _, Some (loc,na) -> loc,na in (tm',(snd na,typ)), na::ids @@ -1348,7 +1348,7 @@ let internalize sigma globalenv env allow_patvar lvar c = if nal <> [] then check_capture loc1 ty na; let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RProd (join_loc loc1 loc2, na, bk, ty, body) + GProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body in match bk with @@ -1364,7 +1364,7 @@ let internalize sigma globalenv env allow_patvar lvar c = if nal <> [] then check_capture loc1 ty na; let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RLambda (join_loc loc1 loc2, na, bk, ty, body) + GLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body in match bk with | Default b -> default env b nal @@ -1391,7 +1391,7 @@ let internalize sigma globalenv env allow_patvar lvar c = (* with implicit arguments if maximal insertion is set *) [] else - RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: + GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: aux (n+1) impl' subscopes' eargs rargs end | (imp::impl', a::rargs') -> @@ -1423,7 +1423,7 @@ let internalize sigma globalenv env allow_patvar lvar c = explain_internalization_error e) (**************************************************************************) -(* Functions to translate constr_expr into rawconstr *) +(* Functions to translate constr_expr into glob_constr *) (**************************************************************************) let extract_ids env = @@ -1477,18 +1477,18 @@ let interp_open_constr sigma env c = let interp_open_constr_patvar sigma env c = let raw = intern_gen false sigma env c ~allow_patvar:true in let sigma = ref (Evd.create_evar_defs sigma) in - let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in + let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in let rec patvar_to_evar r = match r with - | RPatVar (loc,(_,id)) -> + | GPatVar (loc,(_,id)) -> ( try Gmap.find id !evars with Not_found -> let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in let ev = Evarutil.e_new_evar sigma env ev in - let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in + let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in evars := Gmap.add id rev !evars; rev ) - | _ -> map_rawconstr patvar_to_evar r in + | _ -> map_glob_constr patvar_to_evar r in let raw = patvar_to_evar raw in Default.understand_tcc !sigma env raw @@ -1531,7 +1531,7 @@ type ltac_sign = identifier list * unbound_ltac_var_map let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in - pattern_of_rawconstr c + pattern_of_glob_constr c let interp_aconstr ?(impls=[]) vars recvars a = let env = Global.env () in @@ -1540,7 +1540,7 @@ let interp_aconstr ?(impls=[]) vars recvars a = let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, []) false (([],[]),Environ.named_context env,vl,impls) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_rawconstr vars recvars c in + let a = aconstr_of_glob_constr vars recvars c in (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in @@ -1552,12 +1552,12 @@ let interp_aconstr ?(impls=[]) vars recvars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in - 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 Default.understand_type sigma env t' let interp_binder_evars evdref env na t = let t = intern_gen true !evdref env t in - 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 Default.understand_tcc_evars evdref env IsType t' open Environ @@ -1580,7 +1580,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (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 = understand_type env t' in let d = (na,None,t) in let impls = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 6e977056cc..cf9e899a6f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,7 +18,7 @@ open Topconstr open Termops open Pretyping -(** Translation from front abstract syntax of term to untyped terms (rawconstr) *) +(** Translation from front abstract syntax of term to untyped terms (glob_constr) *) (** The translation performs: @@ -68,23 +68,23 @@ type manual_implicits = (explicitation * (bool * bool * bool)) list type ltac_sign = identifier list * unbound_ltac_var_map -type raw_binder = (name * binding_kind * rawconstr option * rawconstr) +type glob_binder = (name * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> rawconstr +val intern_constr : evar_map -> env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> rawconstr +val intern_type : evar_map -> env -> constr_expr -> glob_constr val intern_gen : bool -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> - constr_expr -> rawconstr + constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list -val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list +val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list (** {6 Composing internalization with pretyping } *) @@ -142,7 +142,7 @@ val intern_constr_pattern : val intern_reference : reference -> global_reference (** Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> rawconstr +val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) @@ -152,8 +152,8 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types (** Interpret contexts: returns extended env and context *) -val interp_context_gen : (env -> rawconstr -> types) -> - (env -> rawconstr -> unsafe_judgment) -> +val interp_context_gen : (env -> glob_constr -> types) -> + (env -> glob_constr -> unsafe_judgment) -> ?global_level:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits diff --git a/interp/doc.tex b/interp/doc.tex index ddf40d6c87..4ce5811da3 100644 --- a/interp/doc.tex +++ b/interp/doc.tex @@ -5,7 +5,7 @@ \ocwsection \label{interp} This chapter describes the translation from \Coq\ context-dependent front abstract syntax of terms (\verb=front=) to and from the -context-free, untyped, globalized form of constructions (\verb=rawconstr=). +context-free, untyped, globalized form of constructions (\verb=glob_constr=). The modules translating back and forth the front abstract syntax are organized as follows. diff --git a/interp/genarg.ml b/interp/genarg.ml index 5b221d4c0b..23e17a2d49 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -51,11 +51,11 @@ let loc_of_or_by_notation f = function | AN c -> f c | ByNotation (loc,s,_) -> loc -type rawconstr_and_expr = rawconstr * constr_expr option +type glob_constr_and_expr = glob_constr * constr_expr option type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr +type open_glob_constr = unit * glob_constr_and_expr -type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern +type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern type 'a with_ebindings = 'a * open_constr bindings diff --git a/interp/genarg.mli b/interp/genarg.mli index 963c2742e3..231126d449 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -27,12 +27,12 @@ val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc (** In globalize tactics, we need to keep the initial [constr_expr] to recompute in the environment by the effective calls to Intro, Inversion, etc The [constr_expr] field is [None] in TacDef though *) -type rawconstr_and_expr = rawconstr * constr_expr option +type glob_constr_and_expr = glob_constr * constr_expr option type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr +type open_glob_constr = unit * glob_constr_and_expr -type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern +type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern type 'a with_ebindings = 'a * open_constr bindings @@ -53,11 +53,11 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds {% \begin{%}verbatim{% }%} parsing in_raw out_raw - char stream ----> rawtype ----> constr_expr generic_argument --------| + char stream ----> glob_type ----> constr_expr generic_argument --------| encapsulation decaps | | V - rawtype + glob_type | globalization | V @@ -66,10 +66,10 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds encaps | in_glob | V - rawconstr generic_argument + glob_constr generic_argument | out in out_glob | - type <--- constr generic_argument <---- type <------ rawtype <--------| + type <--- constr generic_argument <---- type <------ glob_type <--------| | decaps encaps interp decaps | V @@ -78,7 +78,7 @@ effective use To distinguish between the uninterpreted (raw), globalized and interpreted worlds, we annotate the type [generic_argument] by a -phantom argument which is either [constr_expr], [rawconstr] or +phantom argument which is either [constr_expr], [glob_constr] or [constr]. Transformation for each type : @@ -175,35 +175,35 @@ val globwit_sort : (rawsort,glevel) abstract_argument_type val wit_sort : (sorts,tlevel) abstract_argument_type val rawwit_constr : (constr_expr,rlevel) abstract_argument_type -val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type +val globwit_constr : (glob_constr_and_expr,glevel) abstract_argument_type val wit_constr : (constr,tlevel) abstract_argument_type val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type -val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) may_eval,glevel) abstract_argument_type +val globwit_constr_may_eval : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,glevel) abstract_argument_type val wit_constr_may_eval : (constr,tlevel) abstract_argument_type val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type +val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type +val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type +val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type -val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type +val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type -val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type +val globwit_bindings : (glob_constr_and_expr bindings,glevel) abstract_argument_type val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type -val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type +val globwit_red_expr : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type val wit_list0 : diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 1e97c5178a..864e521bf7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -136,33 +136,33 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Idset.add id set -let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) = +let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty) = let rec vars bound vs = function - | RVar (loc,id) -> + | GVar (loc,id) -> if is_freevar bound (Global.env ()) id then if List.mem_assoc id vs then vs else (id, loc) :: vs else vs - | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> + | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c - | RCases (loc,sty,rtntypopt,tml,pl) -> + | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in List.fold_left (vars_pattern bound) vs2 pl - | RLetTuple (loc,nal,rtntyp,b,c) -> + | GLetTuple (loc,nal,rtntyp,b,c) -> let vs1 = vars_return_type bound vs rtntyp in let vs2 = vars bound vs1 b in let bound' = List.fold_left add_name_to_ids bound nal in vars bound' vs2 c - | RIf (loc,c,rtntyp,b1,b2) -> + | GIf (loc,c,rtntyp,b1,b2) -> let vs1 = vars_return_type bound vs rtntyp in let vs2 = vars bound vs1 c in let vs3 = vars bound vs2 b1 in vars bound vs3 b2 - | RRec (loc,fk,idl,bl,tyl,bv) -> + | GRec (loc,fk,idl,bl,tyl,bv) -> let bound' = Array.fold_right Idset.add idl bound in let vars_fix i vs fid = let vs1,bound1 = @@ -180,9 +180,9 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) vars bound1 vs2 bv.(i) in array_fold_left_i vars_fix vs idl - | RCast (loc,c,k) -> let v = vars bound vs c in + | GCast (loc,c,k) -> let v = vars bound vs c in (match k with CastConv (_,t) -> vars bound v t | _ -> v) - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs and vars_pattern bound vs (loc,idl,p,c) = let bound' = List.fold_right Idset.add idl bound in @@ -307,14 +307,14 @@ let implicits_of_rawterm ?(with_products=true) l = else rest in match c with - | RProd (loc, na, bk, t, b) -> + | GProd (loc, na, bk, t, b) -> if with_products then abs loc na bk t b else (if bk = Implicit then msg_warning (str "Ignoring implicit status of product binder " ++ pr_name na ++ str " and following binders"); []) - | RLambda (loc, na, bk, t, b) -> abs loc na bk t b - | RLetIn (loc, na, t, b) -> aux i b + | GLambda (loc, na, bk, t, b) -> abs loc na bk t b + | GLetIn (loc, na, t, b) -> aux i b | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index fee7babe95..4c73edbf7a 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -37,12 +37,12 @@ val free_vars_of_binders : (** Returns the generalizable free ids in left-to-right order with the location of their first occurence *) -val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t -> - rawconstr -> (Names.identifier * loc) list +val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> + glob_constr -> (Names.identifier * loc) list val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_rawterm : ?with_products:bool -> Rawterm.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> diff --git a/interp/notation.ml b/interp/notation.ml index 09edd7b30a..eea8afeefc 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -197,9 +197,9 @@ let make_gr = function ConstructRef((mind_of_kn(canonical_mind kn),i),j) | VarRef id -> VarRef id -let rawconstr_key = function - | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref) - | RRef (_,ref) -> RefKey (make_gr ref) +let glob_constr_key = function + | GApp (_,GRef (_,ref),_) -> RefKey (make_gr ref) + | GRef (_,ref) -> RefKey (make_gr ref) | _ -> Oth let cases_pattern_key = function @@ -219,15 +219,15 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) type required_module = full_path * string list type 'a prim_token_interpreter = - loc -> 'a -> rawconstr + loc -> 'a -> glob_constr type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_uninterpreter = - rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + glob_constr list * (glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - loc -> prim_token -> required_module * (unit -> rawconstr) + loc -> prim_token -> required_module * (unit -> glob_constr) let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) @@ -244,7 +244,7 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; add_prim_token_interpreter sc interp; List.iter (fun pat -> - Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b)) + Hashtbl.add prim_token_key_table (glob_constr_key pat) (sc,uninterp,b)) patl let mkNumeral n = Numeral n @@ -350,7 +350,7 @@ let find_prim_token g loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (rawconstr_of_aconstr loc c),df + g (glob_constr_of_aconstr loc c),df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in @@ -370,7 +370,7 @@ let interp_prim_token = interp_prim_token_gen (fun x -> x) let interp_prim_token_cases_pattern loc p name = - interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p + interp_prim_token_gen (cases_pattern_of_glob_constr name) loc p let rec interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in @@ -380,7 +380,7 @@ let rec interp_notation loc ntn local_scopes = (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) let uninterp_notations c = - Gmapl.find (rawconstr_key c) !notations_key_table + Gmapl.find (glob_constr_key c) !notations_key_table let uninterp_cases_pattern_notations c = Gmapl.find (cases_pattern_key c) !notations_key_table @@ -392,7 +392,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = let uninterp_prim_token c = try - let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in + let (sc,numpr,_) = Hashtbl.find prim_token_key_table (glob_constr_key c) in match numpr c with | None -> raise No_match | Some n -> (sc,n) @@ -403,7 +403,7 @@ let uninterp_prim_token_cases_pattern c = let k = cases_pattern_key c in let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in if not b then raise No_match; - let na,c = rawconstr_of_closed_cases_pattern c in + let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with | None -> raise No_match | Some n -> (na,sc,n) @@ -581,11 +581,11 @@ let pr_scope_classes sc = hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++ spc() ++ prlist_with_sep spc pr_class l) ++ fnl() -let pr_notation_info prraw ntn c = +let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prraw (rawconstr_of_aconstr dummy_loc c) + prglob (glob_constr_of_aconstr dummy_loc c) -let pr_named_scope prraw scope sc = +let pr_named_scope prglob scope sc = (if scope = default_scope then match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with | 0 -> str "No lonely notation" @@ -596,14 +596,14 @@ let pr_named_scope prraw scope sc = ++ pr_scope_classes scope ++ Gmap.fold (fun ntn ((_,r),(_,df)) strm -> - pr_notation_info prraw df r ++ fnl () ++ strm) + pr_notation_info prglob df r ++ fnl () ++ strm) sc.notations (mt ()) -let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope) +let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope) -let pr_scopes prraw = +let pr_scopes prglob = Gmap.fold - (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm) + (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm) !scope_map (mt ()) let rec find_default ntn = function @@ -670,7 +670,7 @@ let interp_notation_as_global_reference loc test ntn sc = | [] -> error_notation_not_reference loc ntn | _ -> error_ambiguous_notation loc ntn -let locate_notation prraw ntn scope = +let locate_notation prglob ntn scope = let ntns = factorize_entries (browse_notation false ntn !scope_map) in let scopes = Option.fold_right push_scope scope !scope_stack in if ntns = [] then @@ -683,7 +683,7 @@ let locate_notation prraw ntn scope = prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prraw df r ++ tbrk (1,2) ++ + pr_notation_info prglob df r ++ tbrk (1,2) ++ (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ tbrk (1,2) ++ (if Some sc = scope then str "(default interpretation)" else mt ()) @@ -719,10 +719,10 @@ let collect_notations stack = (all',ntn::knownntn)) ([],[]) stack) -let pr_visible_in_scope prraw (scope,ntns) = +let pr_visible_in_scope prglob (scope,ntns) = let strm = List.fold_right - (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) + (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm) ntns (mt ()) in (if scope = default_scope then str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt()) @@ -730,14 +730,14 @@ let pr_visible_in_scope prraw (scope,ntns) = str "Visible in scope " ++ str scope) ++ fnl () ++ strm -let pr_scope_stack prraw stack = +let pr_scope_stack prglob stack = List.fold_left - (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ()) + (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ()) (mt ()) (collect_notations stack) -let pr_visibility prraw = function - | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack) - | None -> pr_scope_stack prraw !scope_stack +let pr_visibility prglob = function + | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack) + | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) (* Mapping notations to concrete syntax *) diff --git a/interp/notation.mli b/interp/notation.mli index 84f92f8742..290d5f3df0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -65,10 +65,10 @@ type required_module = full_path * string list type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - loc -> 'a -> rawconstr + loc -> 'a -> glob_constr type 'a prim_token_uninterpreter = - rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + glob_constr list * (glob_constr -> 'a option) * cases_pattern_status val declare_numeral_interpreter : scope_name -> required_module -> bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit @@ -80,7 +80,7 @@ val declare_string_interpreter : scope_name -> required_module -> given scope context*) val interp_prim_token : loc -> prim_token -> local_scopes -> - rawconstr * (notation_location * scope_name option) + glob_constr * (notation_location * scope_name option) val interp_prim_token_cases_pattern : loc -> prim_token -> name -> local_scopes -> cases_pattern * (notation_location * scope_name option) @@ -88,7 +88,7 @@ val interp_prim_token_cases_pattern : loc -> prim_token -> name -> raise [No_match] if no such token *) val uninterp_prim_token : - rawconstr -> scope_name * prim_token + glob_constr -> scope_name * prim_token val uninterp_prim_token_cases_pattern : cases_pattern -> name * scope_name * prim_token @@ -112,7 +112,7 @@ val interp_notation : loc -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) (** Return the possible notations for a given term *) -val uninterp_notations : rawconstr -> +val uninterp_notations : glob_constr -> (interp_rule * interpretation * int option) list val uninterp_cases_pattern_notations : cases_pattern -> (interp_rule * interpretation * int option) list @@ -160,12 +160,12 @@ val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list (** Prints scopes (expects a pure aconstr printer) *) -val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds -val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> +val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds +val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds +val locate_notation : (glob_constr -> std_ppcmds) -> notation -> scope_name option -> std_ppcmds -val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds +val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds (** {6 Printing rules for notations} *) diff --git a/interp/reserve.ml b/interp/reserve.ml index 2d36f24099..9d20236b8b 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -49,42 +49,42 @@ let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table open Rawterm let rec unloc = function - | RVar (_,id) -> RVar (dummy_loc,id) - | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args) - | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) - | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) - | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,sty,rtntypopt,tml,pl) -> - RCases (dummy_loc,sty, + | GVar (_,id) -> GVar (dummy_loc,id) + | GApp (_,g,args) -> GApp (dummy_loc,unloc g, List.map unloc args) + | GLambda (_,na,bk,ty,c) -> GLambda (dummy_loc,na,bk,unloc ty,unloc c) + | GProd (_,na,bk,ty,c) -> GProd (dummy_loc,na,bk,unloc ty,unloc c) + | GLetIn (_,na,b,c) -> GLetIn (dummy_loc,na,unloc b,unloc c) + | GCases (_,sty,rtntypopt,tml,pl) -> + GCases (dummy_loc,sty, (Option.map unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | RLetTuple (_,nal,(na,po),b,c) -> - RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) - | RIf (_,c,(na,po),b1,b2) -> - RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) - | RRec (_,fk,idl,bl,tyl,bv) -> - RRec (dummy_loc,fk,idl, + | GLetTuple (_,nal,(na,po),b,c) -> + GLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) + | GIf (_,c,(na,po),b1,b2) -> + GIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) + | GRec (_,fk,idl,bl,tyl,bv) -> + GRec (dummy_loc,fk,idl, Array.map (List.map (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) bl, Array.map unloc tyl, Array.map unloc bv) - | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t)) - | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce) - | RSort (_,x) -> RSort (dummy_loc,x) - | RHole (_,x) -> RHole (dummy_loc,x) - | RRef (_,x) -> RRef (dummy_loc,x) - | REvar (_,x,l) -> REvar (dummy_loc,x,l) - | RPatVar (_,x) -> RPatVar (dummy_loc,x) - | RDynamic (_,x) -> RDynamic (dummy_loc,x) + | GCast (_,c, CastConv (k,t)) -> GCast (dummy_loc,unloc c, CastConv (k,unloc t)) + | GCast (_,c, CastCoerce) -> GCast (dummy_loc,unloc c, CastCoerce) + | GSort (_,x) -> GSort (dummy_loc,x) + | GHole (_,x) -> GHole (dummy_loc,x) + | GRef (_,x) -> GRef (dummy_loc,x) + | GEvar (_,x,l) -> GEvar (dummy_loc,x,l) + | GPatVar (_,x) -> GPatVar (dummy_loc,x) + | GDynamic (_,x) -> GDynamic (dummy_loc,x) let anonymize_if_reserved na t = match na with | Name id as na -> (try if not !Flags.raw_print & - aconstr_of_rawconstr [] [] t = find_reserved_type id - then RHole (dummy_loc,Evd.BinderType na) + aconstr_of_glob_constr [] [] t = find_reserved_type id + then GHole (dummy_loc,Evd.BinderType na) else t with Not_found -> t) | Anonymous -> t diff --git a/interp/reserve.mli b/interp/reserve.mli index 3bcba719ca..1766f77b9d 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -13,4 +13,4 @@ open Topconstr val declare_reserved_type : identifier located -> aconstr -> unit val find_reserved_type : identifier -> aconstr -val anonymize_if_reserved : name -> rawconstr -> rawconstr +val anonymize_if_reserved : name -> glob_constr -> glob_constr diff --git a/interp/topconstr.ml b/interp/topconstr.ml index e27bf67212..61549cb1f7 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -18,7 +18,7 @@ open Mod_subst (*i*) (**********************************************************************) -(* This is the subtype of rawconstr allowed in syntactic extensions *) +(* This is the subtype of glob_constr allowed in syntactic extensions *) (* For AList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted @@ -26,12 +26,12 @@ open Mod_subst boolean is associativity *) type aconstr = - (* Part common to rawconstr and cases_pattern *) + (* Part common to glob_constr and cases_pattern *) | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list | AList of identifier * identifier * aconstr * aconstr * bool - (* Part only in rawconstr *) + (* Part only in glob_constr *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ABinderList of identifier * identifier * aconstr * aconstr @@ -65,7 +65,7 @@ type interpretation = (identifier * (subscopes * notation_var_instance_type)) list * aconstr (**********************************************************************) -(* Re-interpret a notation as a rawconstr, taking care of binders *) +(* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function | Anonymous -> error "This expression should be a simple identifier." @@ -81,43 +81,43 @@ let rec cases_pattern_fold_map loc g e = function let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') -let rec subst_rawvars l = function - | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) - | RProd (loc,Name id,bk,t,c) -> +let rec subst_glob_vars l = function + | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | GProd (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with RVar(_,id') -> id' | _ -> id + try match List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in - RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) - | RLambda (loc,Name id,bk,t,c) -> + GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GLambda (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with RVar(_,id') -> id' | _ -> id + try match List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in - RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) - | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *) + GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) let ldots_var = id_of_string ".." -let rawconstr_of_aconstr_with_binders loc g f e = function - | AVar id -> RVar (loc,id) - | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args) +let glob_constr_of_aconstr_with_binders loc g f e = function + | AVar id -> GVar (loc,id) + | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args) | AList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x,RVar(loc,y)]) in - let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in - subst_rawvars outerl it + let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in + let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in + subst_glob_vars outerl it | ABinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in - let innerl = [(ldots_var,t);(x,RVar(loc,y))] in - let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in + let innerl = [(ldots_var,t);(x,GVar(loc,y))] in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in - subst_rawvars outerl it + subst_glob_vars outerl it | ALambda (na,ty,c) -> - let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c) + let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | AProd (na,ty,c) -> - let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c) + let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) | ALetIn (na,b,c) -> - let e',na = g e na in RLetIn (loc,na,f e b,f e' c) + let e',na = g e na in GLetIn (loc,na,f e b,f e' c) | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -133,36 +133,36 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let ((idl,e),patl) = list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in - RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') + GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> let e',nal = list_fold_map g e nal in let e'',na = g e na in - RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) + GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) | AIf (c,(na,po),b1,b2) -> let e',na = g e na in - RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) + GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) | ARec (fk,idl,dll,tl,bl) -> let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = array_fold_map (to_id g) e idl in - RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | ACast (c,k) -> RCast (loc,f e c, + GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) + | ACast (c,k) -> GCast (loc,f e c, match k with | CastConv (k,t) -> CastConv (k,f e t) | CastCoerce -> CastCoerce) - | ASort x -> RSort (loc,x) - | AHole x -> RHole (loc,x) - | APatVar n -> RPatVar (loc,(false,n)) - | ARef x -> RRef (loc,x) + | ASort x -> GSort (loc,x) + | AHole x -> GHole (loc,x) + | APatVar n -> GPatVar (loc,(false,n)) + | ARef x -> GRef (loc,x) -let rec rawconstr_of_aconstr loc x = +let rec glob_constr_of_aconstr loc x = let rec aux () x = - rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x + glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x (****************************************************************************) -(* Translating a rawconstr into a notation, interpreting recursive patterns *) +(* Translating a glob_constr into a notation, interpreting recursive patterns *) let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) let add_name r = function Anonymous -> () | Name id -> add_id r id @@ -170,51 +170,51 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id let split_at_recursive_part c = let sub = ref None in let rec aux = function - | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var -> + | GApp (loc0,GVar(loc,v),c::l) when v = ldots_var -> if !sub <> None then (* Not narrowed enough to find only one recursive part *) raise Not_found else (sub := Some c; - if l = [] then RVar (loc,ldots_var) - else RApp (loc0,RVar (loc,ldots_var),l)) - | c -> map_rawconstr aux c in + if l = [] then GVar (loc,ldots_var) + else GApp (loc0,GVar (loc,ldots_var),l)) + | c -> map_glob_constr aux c in let outer_iterator = aux c in match !sub with | None -> (* No recursive pattern found *) raise Not_found | Some c -> match outer_iterator with - | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found + | GVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, c let on_true_do b f c = if b then (f c; b) else b -let compare_rawconstr f add t1 t2 = match t1,t2 with - | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 - | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) - | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 - | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 - | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> +let compare_glob_constr f add t1 t2 = match t1,t2 with + | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 + | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) + | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 + | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 + | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 - | RHole _, RHole _ -> true - | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 -> + | GHole _, GHole _ -> true + | GSort (_,s1), GSort (_,s2) -> s1 = s2 + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 -> on_true_do (f b1 b2 & f c1 c2) add na1 - | (RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ - | _,(RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) + | (GCases _ | GRec _ | GDynamic _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ + | _,(GCases _ | GRec _ | GDynamic _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) -> error "Unsupported construction in recursive notations." - | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ - | RHole _ | RSort _ | RLetIn _), _ + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | GHole _ | GSort _ | GLetIn _), _ -> false -let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2 +let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) -let check_is_hole id = function RHole _ -> () | t -> - user_err_loc (loc_of_rawconstr t,"", +let check_is_hole id = function GHole _ -> () | t -> + user_err_loc (loc_of_glob_constr t,"", strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") @@ -222,40 +222,40 @@ let compare_recursive_parts found f (iterator,subc) = let diff = ref None in let terminator = ref None in let rec aux c1 c2 = match c1,c2 with - | RVar(_,v), term when v = ldots_var -> + | GVar(_,v), term when v = ldots_var -> (* We found the pattern *) assert (!terminator = None); terminator := Some term; true - | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var -> + | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var -> (* We found the pattern, but there are extra arguments *) (* (this allows e.g. alternative (recursive) notation of application) *) assert (!terminator = None); terminator := Some term; list_for_all2eq aux l1 l2 - | RVar (_,x), RVar (_,y) when x<>y -> + | GVar (_,x), GVar (_,y) when x<>y -> (* We found the position where it differs *) let lassoc = (!terminator <> None) in let x,y = if lassoc then y,x else x,y in !diff = None && (diff := Some (x,y,Some lassoc); true) - | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term) - | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) -> + | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) + | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) check_is_hole y t_x; check_is_hole y t_y; !diff = None && (diff := Some (x,y,None); aux c term) | _ -> - compare_rawconstr aux (add_name found) c1 c2 in + compare_glob_constr aux (add_name found) c1 c2 in if aux iterator subc then match !diff with | None -> - let loc1 = loc_of_rawconstr iterator in - let loc2 = loc_of_rawconstr (Option.get !terminator) in + let loc1 = loc_of_glob_constr iterator in + let loc2 = loc_of_glob_constr (Option.get !terminator) in (* Here, we would need a loc made of several parts ... *) user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in let iterator = - f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator + f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator else iterator) in (* found have been collected by compare_constr *) found := newfound; @@ -269,7 +269,7 @@ let compare_recursive_parts found f (iterator,subc) = else raise Not_found -let aconstr_and_vars_of_rawconstr a = +let aconstr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in let rec aux c = let keepfound = !found in @@ -278,7 +278,7 @@ let aconstr_and_vars_of_rawconstr a = with Not_found -> found := keepfound; match c with - | RApp (_,RVar (loc,f),[c]) when f = ldots_var -> + | GApp (_,GVar (loc,f),[c]) when f = ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) user_err_loc (loc,"", @@ -286,12 +286,12 @@ let aconstr_and_vars_of_rawconstr a = | c -> aux' c and aux' = function - | RVar (_,id) -> add_id found id; AVar id - | RApp (_,g,args) -> AApp (aux g, List.map aux args) - | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) - | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) - | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) - | RCases (_,sty,rtntypopt,tml,eqnl) -> + | GVar (_,id) -> add_id found id; AVar id + | GApp (_,g,args) -> AApp (aux g, List.map aux args) + | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) + | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) + | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in ACases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> @@ -300,28 +300,28 @@ let aconstr_and_vars_of_rawconstr a = (fun (_,_,_,nl) -> List.iter (add_name found) nl) x; (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml, List.map f eqnl) - | RLetTuple (loc,nal,(na,po),b,c) -> + | GLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; ALetTuple (nal,(na,Option.map aux po),aux b,aux c) - | RIf (loc,c,(na,po),b1,b2) -> + | GIf (loc,c,(na,po),b1,b2) -> add_name found na; AIf (aux c,(na,Option.map aux po),aux b1,aux b2) - | RRec (_,fk,idl,dll,tl,bl) -> + | GRec (_,fk,idl,dll,tl,bl) -> Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk <> Explicit then error "Binders marked as implicit not allowed in notations."; add_name found na; (na,Option.map aux oc,aux b))) dll in ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | RCast (_,c,k) -> ACast (aux c, + | GCast (_,c,k) -> ACast (aux c, match k with CastConv (k,t) -> CastConv (k,aux t) | CastCoerce -> CastCoerce) - | RSort (_,s) -> ASort s - | RHole (_,w) -> AHole w - | RRef (_,r) -> ARef r - | RPatVar (_,(_,n)) -> APatVar n - | RDynamic _ | REvar _ -> + | GSort (_,s) -> ASort s + | GHole (_,w) -> AHole w + | GRef (_,r) -> ARef r + | GPatVar (_,(_,n)) -> APatVar n + | GDynamic _ | GEvar _ -> error "Existential variables not allowed in notations." in @@ -370,15 +370,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = | NtnInternTypeIdent -> check_bound x in List.iter check_type vars -let aconstr_of_rawconstr vars recvars a = - let a,found = aconstr_and_vars_of_rawconstr a in +let aconstr_of_glob_constr vars recvars a = + let a,found = aconstr_and_vars_of_glob_constr a in check_variables vars recvars found; a (* Substitution of kernel names, avoiding a list of bound identifiers *) let aconstr_of_constr avoiding t = - aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t) + aconstr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with @@ -508,7 +508,7 @@ let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in (metas,subst_aconstr subst bound pat) -(* Pattern-matching rawconstr and aconstr *) +(* Pattern-matching glob_constr and aconstr *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> @@ -518,9 +518,9 @@ let abstract_return_type_context pi mklam tml rtno = List.fold_right mklam nal rtn) rtno -let abstract_return_type_context_rawconstr = +let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,_,nal) -> nal) - (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c)) + (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c)) let abstract_return_type_context_aconstr = abstract_return_type_context pi3 @@ -543,7 +543,7 @@ let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = else raise No_match with Not_found -> (* Check that no capture of binding variables occur *) - if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match; + if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::sigma,sigmalist,sigmabinders) @@ -565,7 +565,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Name id1,Name id2) when List.mem id2 (fst metas) -> - alp, bind_env alp sigma id2 (RVar (dummy_loc,id1)) + alp, bind_env alp sigma id2 (GVar (dummy_loc,id1)) | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -582,13 +582,13 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function - | RLambda (_,na,bk,t,b) when islambda -> + | GLambda (_,na,bk,t,b) when islambda -> match_iterated_binders islambda ((na,bk,None,t)::decls) b - | RProd (_,(Name _ as na),bk,t,b) when not islambda -> + | GProd (_,(Name _ as na),bk,t,b) when not islambda -> match_iterated_binders islambda ((na,bk,None,t)::decls) b - | RLetIn (loc,na,c,b) when glue_letin_with_decls -> + | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b + ((na,Explicit (*?*), Some c,GHole(loc,Evd.BinderType na))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = @@ -630,11 +630,11 @@ let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with match_alist (match_ alp) metas sigma r1 x iter termin lassoc (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> + | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) match_ alp metas (bind_binder sigma x decls) b termin - | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) + | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) when na1 <> Anonymous -> let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) @@ -644,36 +644,36 @@ let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with match_abinderlist_with_app (match_ alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> + | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - | RProd (_,na,bk,t,b1), AProd (Name id,_,b2) + | GProd (_,na,bk,t,b1), AProd (Name id,_,b2) when List.mem id blmetas & na <> Anonymous -> match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) - | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma - | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma - | RApp (loc,f1,l1), AApp (f2,l2) -> + | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma + | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma + | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma + | GApp (loc,f1,l1), AApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = if n1 < n2 then let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22 else if n1 > n2 then - let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2 + let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2 - | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> + | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> + | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> + | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) + | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) when sty1 = sty2 & List.length tml1 = List.length tml2 & List.length eqnl1 = List.length eqnl2 -> - let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in + let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in let sigma = try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' @@ -682,17 +682,17 @@ let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2 - | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) + | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) when List.length nal1 = List.length nal2 -> let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in let sigma = match_ alp metas sigma b1 b2 in let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_ alp metas sigma c1 c2 - | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> + | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2] - | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) + | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 -> @@ -705,14 +705,14 @@ let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in array_fold_left2 (match_ alp metas) sigma bl1 bl2 - | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> + | GCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 - | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> + | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> match_ alp metas sigma c1 c2 - | RSort (_,s1), ASort s2 when s1 = s2 -> sigma - | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | GSort (_,s1), ASort s2 when s1 = s2 -> sigma + | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, AHole _ -> sigma - | (RDynamic _ | RRec _ | REvar _), _ + | (GDynamic _ | GRec _ | GEvar _), _ | _,_ -> raise No_match and match_binders alp metas na1 na2 sigma b1 b2 = @@ -737,7 +737,7 @@ let match_aconstr c (metas,pat) = with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) - RVar (dummy_loc,x) in + GVar (dummy_loc,x) in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> diff --git a/interp/topconstr.mli b/interp/topconstr.mli index cb4ac5e84f..6e8769b858 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -17,18 +17,18 @@ open Mod_subst (** Topconstr: definitions of [aconstr] et [constr_expr] *) (** {6 aconstr } *) -(** This is the subtype of rawconstr allowed in syntactic extensions +(** This is the subtype of glob_constr allowed in syntactic extensions No location since intended to be substituted at any place of a text Complex expressions such as fixpoints and cofixpoints are excluded, non global expressions such as existential variables also *) type aconstr = - (** Part common to [rawconstr] and [cases_pattern] *) + (** Part common to [glob_constr] and [cases_pattern] *) | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list | AList of identifier * identifier * aconstr * aconstr * bool - (** Part only in [rawconstr] *) + (** Part only in [glob_constr] *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ABinderList of identifier * identifier * aconstr * aconstr @@ -67,35 +67,35 @@ type notation_var_internalization_type = type interpretation = (identifier * (subscopes * notation_var_instance_type)) list * aconstr -(** Translate a rawconstr into a notation given the list of variables +(** Translate a glob_constr into a notation given the list of variables bound by the notation; also interpret recursive patterns *) -val aconstr_of_rawconstr : +val aconstr_of_glob_constr : (identifier * notation_var_internalization_type) list -> - (identifier * identifier) list -> rawconstr -> aconstr + (identifier * identifier) list -> glob_constr -> aconstr (** Name of the special identifier used to encode recursive notations *) val ldots_var : identifier -(** Equality of rawconstr (warning: only partially implemented) *) -val eq_rawconstr : rawconstr -> rawconstr -> bool +(** Equality of glob_constr (warning: only partially implemented) *) +val eq_glob_constr : glob_constr -> glob_constr -> bool -(** Re-interpret a notation as a rawconstr, taking care of binders *) +(** Re-interpret a notation as a glob_constr, taking care of binders *) -val rawconstr_of_aconstr_with_binders : loc -> +val glob_constr_of_aconstr_with_binders : loc -> ('a -> name -> 'a * name) -> - ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr + ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr -val rawconstr_of_aconstr : loc -> aconstr -> rawconstr +val glob_constr_of_aconstr : loc -> aconstr -> glob_constr -(** [match_aconstr] matches a rawconstr against a notation interpretation; +(** [match_aconstr] matches a glob_constr against a notation interpretation; raise [No_match] if the matching fails *) exception No_match -val match_aconstr : rawconstr -> interpretation -> - (rawconstr * subscopes) list * (rawconstr list * subscopes) list * - (rawdecl list * subscopes) list +val match_aconstr : glob_constr -> interpretation -> + (glob_constr * subscopes) list * (glob_constr list * subscopes) list * + (glob_decl list * subscopes) list val match_aconstr_cases_pattern : cases_pattern -> interpretation -> (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list |