aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/proofview.ml3
-rw-r--r--engine/termops.ml47
-rw-r--r--engine/uState.ml30
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univGen.ml5
-rw-r--r--engine/univGen.mli2
-rw-r--r--engine/univNames.ml2
9 files changed, 59 insertions, 37 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 59eea97ce9..706e51d4b3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -983,6 +983,9 @@ let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
+let fresh_array_instance ?loc ?(rigid=univ_flexible) env evd =
+ with_context_set ?loc rigid evd (UnivGen.fresh_array_instance env)
+
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
diff --git a/engine/evd.mli b/engine/evd.mli
index 911e00c23a..a6d55c2615 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -698,6 +698,8 @@ val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
-> env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
-> env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_array_instance : ?loc:Loc.t -> ?rigid:rigid
+ -> env -> evar_map -> evar_map * Univ.Instance.t
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
evar_map -> GlobRef.t -> evar_map * econstr
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 22863f451d..b3061eaa81 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -909,10 +909,11 @@ let tclPROGRESS t =
in
let test =
quick_test ||
+ (CList.same_length initial.comb final.comb &&
Util.List.for_all2eq begin fun i f ->
Progress.goal_equal ~evd:initial.solution
~extended_evd:final.solution (drop_state i) (drop_state f)
- end initial.comb final.comb
+ end initial.comb final.comb)
in
if not test then
tclUNIT res
diff --git a/engine/termops.ml b/engine/termops.ml
index ccd49ca495..66131e1a8f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -677,12 +677,21 @@ let map_constr_with_binders_left_to_right sigma g f l c =
if def' == def && t' == t && ty' == ty then c
else mkArray(u,t',def',ty')
-let map_under_context_with_full_binders sigma g f l n d =
- let open EConstr in
- let f l c = Unsafe.to_constr (f l (of_constr c)) in
- let g d l = g (of_rel_decl d) l in
- let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in
- EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d)
+let rec map_under_context_with_full_binders sigma g f l n d =
+ if n = 0 then f l d else
+ match EConstr.kind sigma d with
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
+ if b' == b && t' == t && c' == c then d
+ else EConstr.mkLetIn (na,b',t',c')
+ | Lambda (na,t,b) ->
+ let t' = f l t in
+ let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
+ if t' == t && b' == b then d
+ else EConstr.mkLambda (na,t',b')
+ | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
let map_branches_with_full_binders sigma g f l ci bl =
let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
@@ -775,11 +784,27 @@ let map_constr_with_full_binders_user_view sigma g f =
each binder traversal; it is not recursive *)
let fold_constr_with_full_binders sigma g f n acc c =
- let open EConstr in
- let f l acc c = f l acc (of_constr c) in
- let g d l = g (of_rel_decl d) l in
- let c = Unsafe.to_constr (whd_evar sigma c) in
- Constr.fold_with_full_binders g f n acc c
+ let open EConstr.Vars in
+ let open Context.Rel.Declaration in
+ match EConstr.kind sigma c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (_,c) -> f n acc c
+ | Evar (_,l) -> List.fold_left (f n) acc l
+ | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
let fold_constr_with_binders sigma g f n acc c =
let open EConstr in
diff --git a/engine/uState.ml b/engine/uState.ml
index 0c994dfea0..20ea24dd87 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -113,19 +113,18 @@ let constraints uctx = snd uctx.local
let context uctx = ContextSet.to_context uctx.local
let compute_instance_binders inst ubinders =
- let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
let map lvl =
- try Name (LMap.find lvl revmap)
- with Not_found -> Anonymous
+ try Name (Option.get (LMap.find lvl ubinders).uname)
+ with Option.IsNone | Not_found -> Anonymous
in
Array.map map (Instance.to_array inst)
let univ_entry ~poly uctx =
let open Entries in
if poly then
- let (binders, _) = uctx.names in
+ let (_, rbinders) = uctx.names in
let uctx = context uctx in
- let nas = compute_instance_binders (UContext.instance uctx) binders in
+ let nas = compute_instance_binders (UContext.instance uctx) rbinders in
Polymorphic_entry (nas, uctx)
else Monomorphic_entry (context_set uctx)
@@ -158,23 +157,8 @@ let of_binders names =
in
{ empty with names = (names, rev_map) }
-let invent_name (named,cnt) u =
- let rec aux i =
- let na = Id.of_string ("u"^(string_of_int i)) in
- if Id.Map.mem na named then aux (i+1)
- else Id.Map.add na u named, i+1
- in
- aux cnt
-
let universe_binders uctx =
- let named, rev = uctx.names in
- let named, _ = LSet.fold (fun u named ->
- match LMap.find u rev with
- | exception Not_found -> (* not sure if possible *) invent_name named u
- | { uname = None } -> invent_name named u
- | { uname = Some _ } -> named)
- (ContextSet.levels uctx.local) (named, 0)
- in
+ let named, _ = uctx.names in
named
let instantiate_variable l b v =
@@ -447,9 +431,9 @@ let check_univ_decl ~poly uctx decl =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
if poly then
- let (binders, _) = uctx.names in
+ let (_, rbinders) = uctx.names in
let uctx = universe_context ~names ~extensible uctx in
- let nas = compute_instance_binders (UContext.instance uctx) binders in
+ let nas = compute_instance_binders (UContext.instance uctx) rbinders in
Entries.Polymorphic_entry (nas, uctx)
else
let () = check_universe_context_set ~names ~extensible uctx in
diff --git a/engine/uState.mli b/engine/uState.mli
index 442c29180c..9cff988c99 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -79,7 +79,7 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
val universe_binders : t -> UnivNames.universe_binders
-(** Return names of universes, inventing names if needed *)
+(** Return local names of universes. *)
(** {5 Constraints handling} *)
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 6f27ccb7dc..278ca6bf34 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -65,6 +65,11 @@ let fresh_constructor_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
(c, u), ctx
+let fresh_array_instance env =
+ let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
+ let u, ctx = fresh_instance_from auctx None in
+ u, ctx
+
let fresh_global_instance ?loc ?names env gr =
let u, ctx = fresh_global_instance ?loc ?names env gr in
mkRef (gr, u), ctx
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 81bdac17ce..05737411f5 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -42,6 +42,8 @@ val fresh_inductive_instance : env -> inductive ->
pinductive in_universe_context_set
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
+val fresh_array_instance : env ->
+ Instance.t in_universe_context_set
val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
diff --git a/engine/univNames.ml b/engine/univNames.ml
index f5542cc0f7..215f27f535 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,7 +15,7 @@ open Univ
let qualid_of_level ctx l =
match Level.name l with
| Some qid ->
- (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
+ (try Some (Nametab.shortest_qualid_of_universe ctx qid)
with Not_found -> None)
| None -> None
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:25:48 +0000