aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml16
-rw-r--r--interp/constrintern.ml26
-rw-r--r--interp/constrintern.mli6
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation_ops.ml31
-rw-r--r--interp/topconstr.ml28
6 files changed, 42 insertions, 67 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4c29fc8097..f6da10c961 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -740,7 +740,7 @@ let rec extern inctx scopes vars r =
| GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
- List.fold_right (name_fold Id.Set.add)
+ List.fold_right (Name.fold_right Id.Set.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)) ->
@@ -790,12 +790,12 @@ let rec extern inctx scopes vars r =
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
- let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
- let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+ let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+ let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
let n =
match fst nv.(i) with
| None -> None
- | Some x -> Some (Loc.tag @@ out_name (List.nth assums x))
+ | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x))
in
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
@@ -807,8 +807,8 @@ let rec extern inctx scopes vars r =
Array.mapi (fun i fi ->
let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
let (_,ids,bl) = extern_local_binder scopes vars bl in
- let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
- let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+ let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+ let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern false scopes vars1 bv.(i))) idv
in
@@ -852,14 +852,14 @@ and extern_local_binder scopes vars = function
[] -> ([],[],[])
| { v = GLocalDef (na,bk,bd,ty)}::l ->
let (assums,ids,l) =
- extern_local_binder scopes (name_fold Id.Set.add na vars) l in
+ extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
(assums,na::ids,
CLocalDef((Loc.tag na), extern false scopes vars bd,
Option.map (extern false scopes vars) ty) :: l)
| { v = GLocalAssum (na,bk,ty)}::l ->
let ty = extern_typ scopes vars ty in
- (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
+ (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
when constr_expr_eq ty ty' &&
match na with Name id -> not (occur_var_constr_expr id ty')
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..190369e8fa 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -98,16 +98,16 @@ let global_reference_of_reference ref =
locate_reference (snd (qualid_of_reference ref))
let global_reference id =
- Universes.constr_of_global (locate_reference (qualid_of_ident id))
+ locate_reference (qualid_of_ident id)
let construct_reference ctx id =
try
- Term.mkVar (let _ = Context.Named.lookup id ctx in id)
+ VarRef (let _ = Context.Named.lookup id ctx in id)
with Not_found ->
global_reference id
let global_reference_in_absolute_module dir id =
- Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+ Nametab.global_of_path (Libnames.make_path dir id)
(**********************************************************************)
(* Internalization errors *)
@@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
try
(* Binders bound in the notation are considered first-order objects *)
let _,na = coerce_to_name (fst (Id.Map.find id terms)) in
- (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na
+ (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer =
let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
match projs with
| [] -> (idx, acc_first_idx, acc)
- | (Some name) :: projs ->
- let field_glob_ref = ConstRef name in
+ | (Some field_glob_id) :: projs ->
+ let field_glob_ref = ConstRef field_glob_id in
let first_field = eq_gr field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch")
@@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer =
build_proj_list projs proj_kinds idx ~acc_first_idx acc
else
build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
- ((idx, field_glob_ref) :: acc)
+ ((idx, field_glob_id) :: acc)
end
| None :: projs ->
if complete then
@@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer =
user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+ let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
@@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
sort_fields ~complete:true loc fs
- (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+ (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
Misctypes.IntroAnonymous, None))
in
begin
@@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
| CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
- (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
+ (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
inb) Id.Set.empty tms in
(* as, in & return vars *)
let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
@@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
(match naming with
| Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
- | _ -> Evar_kinds.QuestionMark st)
+ | _ -> Evar_kinds.QuestionMark (st,Anonymous))
| Some k -> k
in
let solve = match solve with
@@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders =
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-let interp_rawcontext_evars env evdref k bl =
+let interp_glob_context_evars env evdref k bl =
let open EConstr in
let (env, par, _, impls) =
List.fold_left
@@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl =
let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
let int_env,bl = intern_context global_level env impl_env params in
- let x = interp_rawcontext_evars env evdref shift bl in
+ let x = interp_glob_context_evars env evdref shift bl in
int_env, x
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644cafe575..644f60d850 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -176,9 +176,9 @@ val interp_context_evars :
val locate_reference : Libnames.qualid -> Globnames.global_reference
val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
-val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
+val global_reference : Id.t -> Globnames.global_reference
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cfc6e6c2a6..ade524141a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
let () = match bk with
| Implicit ->
Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++
- pr_name na ++ strbrk " and following binders")
+ Name.print na ++ strbrk " and following binders")
| _ -> ()
in []
| GLambda (na, bk, t, b) -> abs na bk b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6f91009111..8e876ec16d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -22,31 +22,6 @@ open Notation_term
(**********************************************************************)
(* Utilities *)
-let on_true_do b f c = if b then (f c; b) else b
-
-let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with
- | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2
- | GVar v1, GVar v2 -> on_true_do (Id.equal 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 Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
- on_true_do (f ty1 ty2 && f c1 c2) add na1
- | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2)
- when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
- on_true_do (f ty1 ty2 && f c1 c2) add na1
- | GHole _, GHole _ -> true
- | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
- | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 ->
- on_true_do (f b1 b2 && f c1 c2) add na1
- | (GCases _ | GRec _
- | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
- | _,(GCases _ | GRec _
- | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
- -> user_err Pp.(str "Unsupported construction in recursive notations.")
- | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
- | GHole _ | GSort _ | GLetIn _), _
- -> false
-
let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
@@ -184,7 +159,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
e',Some (Loc.tag ?loc (ind,nal')) in
let e',na' = g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
- let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
+ let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
@@ -287,7 +262,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
| Some _ -> false
end
| GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
- | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) ->
+ | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
(* We found a binding position where it differs *)
begin match !diff with
| None ->
@@ -296,7 +271,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
| Some _ -> false
end
| _ ->
- compare_glob_constr aux (add_name found) c1 c2 in
+ mk_glob_constr_eq aux c1 c2 in
if aux iterator subc then
match !diff with
| None ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a79f10df6b..94bbc60eaf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms =
(fun (_, ona, indnal) l ->
Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
indnal
- (Option.fold_right (down_located (name_fold Id.Set.add)) ona l))
+ (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
tms Id.Set.empty
let rec fold_constr_expr_binders g f n acc b = function
| (nal,bk,t)::l ->
let nal = snd (List.split nal) in
- let n' = List.fold_right (name_fold g) nal n in
+ let n' = List.fold_right (Name.fold_right g) nal n in
f n (fold_constr_expr_binders g f n' acc b l) t
| [] ->
f n acc b
@@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function
let rec fold_local_binders g f n acc b = function
| CLocalAssum (nal,bk,t)::l ->
let nal = snd (List.split nal) in
- let n' = List.fold_right (name_fold g) nal n in
+ let n' = List.fold_right (Name.fold_right g) nal n in
f n (fold_local_binders g f n' acc b l) t
| CLocalDef ((_,na),c,t)::l ->
- Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
+ Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
| CLocalPattern (_,(pat,t))::l ->
let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
Option.fold_left (f n) acc t
@@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
| CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
| CLetIn (na,a,t,b) ->
- f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+ f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
| CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
| CCast (a,CastCoerce) -> f n acc a
| CNotation (_,(l,ll,bll)) ->
@@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
let ids = ids_of_pattern_list patl in
f (Id.Set.fold g ids n) acc rhs) bl acc
| CLetTuple (nal,(ona,po),b,c) ->
- let n' = List.fold_right (down_located (name_fold g)) nal n in
- f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+ let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
+ f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
| CIf (c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
Option.fold_left
- (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+ (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
| CFix (_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -198,7 +198,7 @@ let split_at_annot bl na =
(* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -212,7 +212,7 @@ let map_local_binders f g e bl =
CLocalAssum(nal,k,ty) ->
(map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
| CLocalDef((loc,na),c,ty) ->
- (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
+ (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
| CLocalPattern (loc,(pat,t)) ->
let ids = ids_of_pattern pat in
(Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
@@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CLambdaN (bl,b) ->
let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
| CLetIn (na,a,t,b) ->
- CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+ CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
| CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
| CNotation (n,(l,ll,bll)) ->
(* This is an approximation because we don't know what binds what *)
@@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
| CLetTuple (nal,(ona,po),b,c) ->
- let e' = List.fold_right (down_located (name_fold g)) nal e in
- let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+ let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
+ let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (c,(ona,po),b1,b2) ->
- let e' = Option.fold_right (down_located (name_fold g)) ona e in
+ let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (id,dl) ->
CFix (id,List.map (fun (id,n,bl,t,d) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:51:33 +0000