aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:50:45 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:50:45 +0000
commit8f9461509338a3ebba46faaad3116c4e44135423 (patch)
tree23da64d38f2194a1f9e42b789b16b82402d6908f /interp
parentfafba6b545c7d0d774bcd79bdbddb8869517aabb (diff)
Change of nomenclature: rawconstr -> glob_constr
There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml120
-rw-r--r--interp/constrextern.mli4
-rw-r--r--interp/constrintern.ml158
-rw-r--r--interp/constrintern.mli18
-rw-r--r--interp/doc.tex2
-rw-r--r--interp/genarg.ml6
-rw-r--r--interp/genarg.mli32
-rw-r--r--interp/implicit_quantifiers.ml26
-rw-r--r--interp/implicit_quantifiers.mli6
-rw-r--r--interp/notation.ml56
-rw-r--r--interp/notation.mli18
-rw-r--r--interp/reserve.ml46
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/topconstr.ml244
-rw-r--r--interp/topconstr.mli32
15 files changed, 385 insertions, 385 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index eb779200c..4029f6150 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 08f089d4e..979c974ac 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 fad3c4910..c097ce43d 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 6e977056c..cf9e899a6 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 ddf40d6c8..4ce5811da 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 5b221d4c0..23e17a2d4 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 963c2742e..231126d44 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 1e97c5178..864e521bf 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 fee7babe9..4c73edbf7 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 09edd7b30..eea8afeef 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 84f92f874..290d5f3df 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 2d36f2409..9d20236b8 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 3bcba719c..1766f77b9 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 e27bf6721..61549cb1f 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 cb4ac5e84..6e8769b85 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 01:05:25 +0000