aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml25
-rw-r--r--engine/eConstr.mli1
-rw-r--r--engine/evarutil.ml32
-rw-r--r--engine/evarutil.mli25
-rw-r--r--engine/namegen.ml3
-rw-r--r--engine/termops.ml11
-rw-r--r--engine/univMinim.ml43
-rw-r--r--engine/univSubst.ml7
8 files changed, 73 insertions, 74 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 32eb63a818..334c23c963 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -77,6 +77,7 @@ let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
let mkInt i = of_kind (Int i)
let mkFloat f = of_kind (Float f)
+let mkArray (u,t,def,ty) = of_kind (Array (u,t,def,ty))
let mkRef (gr,u) = let open GlobRef in match gr with
| ConstRef c -> mkConstU (c,u)
@@ -366,6 +367,7 @@ let iter_with_full_binders sigma g f n c =
Array.iter (f n) tl;
let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
Array.iter (f n') bl
+ | Array (_u,t,def,ty) -> Array.Fun1.iter f n t; f n def; f n ty
let iter_with_binders sigma g f n c =
let f l c = f l (of_constr c) in
@@ -546,18 +548,21 @@ let universes_of_constr sigma c =
let rec aux s c =
match kind sigma c with
| Const (c, u) ->
- LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
| Sort u ->
- let sort = ESorts.kind sigma u in
- if Sorts.is_small sort then s
- else
- let u = Sorts.univ_of_sort sort in
- LSet.fold LSet.add (Universe.levels u) s
+ let sort = ESorts.kind sigma u in
+ if Sorts.is_small sort then s
+ else
+ let u = Sorts.univ_of_sort sort in
+ LSet.fold LSet.add (Universe.levels u) s
| Evar (k, args) ->
- let concl = Evd.evar_concl (Evd.find sigma k) in
- fold sigma aux (aux s concl) c
+ let concl = Evd.evar_concl (Evd.find sigma k) in
+ fold sigma aux (aux s concl) c
+ | Array (u,_,_,_) ->
+ let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+ fold sigma aux s c
| _ -> fold sigma aux s c
in aux LSet.empty c
@@ -762,7 +767,7 @@ let kind_of_type sigma t = match kind sigma t with
| (Rel _ | Meta _ | Var _ | Evar _ | Const _
| Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
-> AtomicType (t,[||])
- | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
+ | (Lambda _ | Construct _ | Int _ | Float _ | Array _) -> failwith "Not a type"
module Unsafe =
struct
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2bf8f69af7..d0f675319d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -135,6 +135,7 @@ val mkArrow : t -> Sorts.relevance -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkFloat : Float64.t -> t
+val mkArray : EInstance.t * t array * t * t -> t
val mkRef : GlobRef.t * EInstance.t -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 423af1d4ec..b4b2032dd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -409,15 +409,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar_full evd ?typeclass_candidate evi =
- let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
- let evd = Evd.declare_future_goal evk evd in
- (evd, evk)
-
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
- ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ =
- let default_naming = IntroAnonymous in
- let naming = Option.default default_naming naming in
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
+ ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
let name = match naming with
| IntroAnonymous -> None
| IntroIdentifier id -> Some id
@@ -443,22 +436,6 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_ar
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
- ?principal sign evd typ instance =
- let open EConstr in
- assert (not !Flags.debug ||
- List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
- evd, mkEvar (newevk, instance)
-
-let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
- let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
- let instance =
- match filter with
- | None -> instance
- | Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance
-
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
@@ -470,8 +447,9 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
- ?typeclass_candidate ?principal instance
+ let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+ ?typeclass_candidate ?principal in
+ (evd, EConstr.mkEvar (evk, instance))
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b3c94e6b3b..41b58d38b0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -25,14 +25,6 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
-val new_evar_from_context :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?candidates:constr list ->
- ?naming:intro_pattern_naming_expr ->
- ?typeclass_candidate:bool ->
- ?principal:bool ->
- named_context_val -> evar_map -> types -> evar_map * EConstr.t
-
type naming_mode =
| KeepUserNameAndRenameExistingButSectionNames
| KeepUserNameAndRenameExistingEvenSectionNames
@@ -56,8 +48,6 @@ val new_pure_evar :
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
-val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
-
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
@@ -73,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
val new_global : evar_map -> GlobRef.t -> evar_map * constr
-(** Create a fresh evar in a context different from its definition context:
- [new_evar_instance sign evd ty inst] creates a new evar of context
- [sign] and type [ty], [inst] is a mapping of the evar context to
- the context where the evar should occur. This means that the terms
- of [inst] are typed in the occurrence context and their type (seen
- as a telescope) is [sign] *)
-val new_evar_instance :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
- ?naming:intro_pattern_naming_expr ->
- ?typeclass_candidate:bool ->
- ?principal:bool ->
- named_context_val -> evar_map -> types ->
- constr list -> evar_map * constr
-
val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 1cf5be10ae..fb9f6db0ea 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
- | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None
+ | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ | Array _ -> None
in
hdrec c
@@ -166,6 +166,7 @@ let hdchar env sigma c =
| Meta _ | Case _ -> "y"
| Int _ -> "i"
| Float _ -> "f"
+ | Array _ -> "a"
in
hdrec 0 c
diff --git a/engine/termops.ml b/engine/termops.ml
index f6d0807823..e5231ef9cd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -659,6 +659,12 @@ let map_constr_with_binders_left_to_right sigma g f l c =
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then c
else mkCoFix (ln,(lna,tl',bl'))
+ | Array(u,t,def,ty) ->
+ let t' = Array.map_left (f l) t in
+ let def' = f l def in
+ let ty' = f l ty in
+ 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
@@ -738,6 +744,11 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
else mkCoFix (ln,(lna,tl',bl'))
+ | Array(u,t,def,ty) ->
+ let t' = Array.Smart.map (f l) t in
+ let def' = f l def in
+ let ty' = f l ty in
+ if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty')
let map_constr_with_full_binders sigma g f =
map_constr_with_full_binders_gen false sigma g f
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 4dd7fe7e70..1c7e716fc2 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -85,12 +85,33 @@ let lower_of_list l =
type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
-exception Found of Level.t * lowermap
-let find_inst insts v =
- try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
- if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
- insts; raise Not_found
- with Found (f,l) -> (f,l)
+module LBMap :
+sig
+ type t = private { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t }
+ val empty : t
+ val add : Level.t -> lbound -> t -> t
+end =
+struct
+ type t = { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t }
+ (* lbrev is uniquely given from lbmap as a partial reverse mapping *)
+ let empty = { lbmap = LMap.empty; lbrev = Universe.Map.empty }
+ let add u bnd m =
+ let lbmap = LMap.add u bnd m.lbmap in
+ let lbrev =
+ if not bnd.alg && bnd.enforce then
+ match Universe.Map.find bnd.lbound m.lbrev with
+ | (v, _) ->
+ if Level.compare u v <= 0 then
+ Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev
+ else m.lbrev
+ | exception Not_found ->
+ Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev
+ else m.lbrev
+ in
+ { lbmap; lbrev }
+end
+
+let find_inst insts v = Universe.Map.find v insts.LBMap.lbrev
let compute_lbound left =
(* The universe variable was not fixed yet.
@@ -114,11 +135,11 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts,
let inst = Universe.make u in
let cstrs' = enforce_leq lbound inst cstrs in
(ctx, us, LSet.remove u algs,
- LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+ LBMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
{enforce; alg; lbound=inst; lower}
else (* Actually instantiate *)
(Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
- LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+ LBMap.add u {enforce;alg;lbound;lower} insts, cstrs),
{enforce; alg; lbound; lower}
type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
@@ -180,10 +201,10 @@ let minimize_univ_variables ctx us algs left right cstrs =
let lbounds =
match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
| None -> lbounds
- | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
+ | Some lbound -> LBMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
lbounds
in (Univ.LMap.remove r left, lbounds))
- left (left, Univ.LMap.empty)
+ left (left, LBMap.empty)
in
let rec instance (ctx, us, algs, insts, cstrs as acc) u =
let acc, left, lower =
@@ -256,7 +277,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
with UpperBoundedAlg ->
enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
and aux (ctx, us, algs, seen, cstrs as acc) u =
- try acc, LMap.find u seen
+ try acc, LMap.find u seen.LBMap.lbmap
with Not_found -> instance acc u
in
LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index f06aeaf54e..335c2e5e68 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -151,6 +151,13 @@ let nf_evars_and_universes_opt_subst f subst =
let univs' = Instance.subst_fn lsubst univs in
if univs' == univs then Constr.map aux c
else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+ | Array (u,elems,def,ty) ->
+ let u' = Univ.Instance.subst_fn lsubst u in
+ let elems' = CArray.Smart.map aux elems in
+ let def' = aux def in
+ let ty' = aux ty in
+ if u == u' && elems == elems' && def == def' && ty == ty' then c
+ else mkArray (u',elems',def',ty')
| _ -> Constr.map aux c
in aux
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:51:10 +0000