diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 25 |
1 files changed, 15 insertions, 10 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 |