summaryrefslogtreecommitdiff
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml97
1 files changed, 48 insertions, 49 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index de4e7c18..9bf74315 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term
type constr = t
type existential = existential_key * constr array
-type rec_declaration = Name.t array * constr array * constr array
-type fixpoint = (int array * int) * rec_declaration
- (* The array of [int]'s tells for each component of the array of
- mutual fixpoints the number of lambdas to skip before finding the
- recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
- (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
- the recursive argument);
- The second component [int] tells which component of the block is
- returned *)
-type cofixpoint = int * rec_declaration
- (* The component [int] tells which component of the block of
- cofixpoint is returned *)
type types = constr
+type rec_declaration = (constr, types) prec_declaration
+type fixpoint = (constr, types) pfixpoint
+type cofixpoint = (constr, types) pcofixpoint
+
(*********************)
(* Term constructors *)
(*********************)
@@ -138,8 +130,8 @@ let mkProp = Sort Sorts.prop
let mkSet = Sort Sorts.set
let mkType u = Sort (Sorts.Type u)
let mkSort = function
- | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *)
- | Sorts.Prop Sorts.Pos -> mkSet
+ | Sorts.Prop -> mkProp (* Easy sharing *)
+ | Sorts.Set -> mkSet
| s -> Sort s
(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
@@ -268,17 +260,17 @@ let isSort c = match kind c with
| _ -> false
let rec isprop c = match kind c with
- | Sort (Sorts.Prop _) -> true
+ | Sort (Sorts.Prop | Sorts.Set) -> true
| Cast (c,_,_) -> isprop c
| _ -> false
let rec is_Prop c = match kind c with
- | Sort (Sorts.Prop Sorts.Null) -> true
+ | Sort Sorts.Prop -> true
| Cast (c,_,_) -> is_Prop c
| _ -> false
let rec is_Set c = match kind c with
- | Sort (Sorts.Prop Sorts.Pos) -> true
+ | Sort Sorts.Set -> true
| Cast (c,_,_) -> is_Set c
| _ -> false
@@ -468,16 +460,16 @@ let iter_with_binders g f n c = match kind c with
| Prod (_,t,c) -> f n t; f (g n) c
| Lambda (_,t,c) -> f n t; f (g n) c
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
- | App (c,l) -> f n c; CArray.Fun1.iter f n l
- | Evar (_,l) -> CArray.Fun1.iter f n l
- | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+ | App (c,l) -> f n c; Array.Fun1.iter f n l
+ | Evar (_,l) -> Array.Fun1.iter f n l
+ | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
- CArray.Fun1.iter f n tl;
- CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+ Array.Fun1.iter f n tl;
+ Array.Fun1.iter f (iterate g (Array.length tl) n) bl
| CoFix (_,(_,tl,bl)) ->
- CArray.Fun1.iter f n tl;
- CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+ Array.Fun1.iter f n tl;
+ Array.Fun1.iter f (iterate g (Array.length tl) n) bl
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
@@ -537,7 +529,7 @@ let map f c = match kind c with
else mkLetIn (na, b', t', k')
| App (b,l) ->
let b' = f b in
- let l' = Array.smartmap f l in
+ let l' = Array.Smart.map f l in
if b'==b && l'==l then c
else mkApp (b', l')
| Proj (p,t) ->
@@ -545,23 +537,23 @@ let map f c = match kind c with
if t' == t then c
else mkProj (p, t')
| Evar (e,l) ->
- let l' = Array.smartmap f l in
+ let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
- let bl' = Array.smartmap f bl in
+ let bl' = Array.Smart.map f bl in
if b'==b && p'==p && bl'==bl then c
else mkCase (ci, p', b', bl')
| Fix (ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap f tl in
- let bl' = Array.smartmap f bl in
+ let tl' = Array.Smart.map f tl in
+ let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap f tl in
- let bl' = Array.smartmap f bl in
+ let tl' = Array.Smart.map f tl in
+ let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
@@ -593,7 +585,7 @@ let fold_map f accu c = match kind c with
else accu, mkLetIn (na, b', t', k')
| App (b,l) ->
let accu, b' = f accu b in
- let accu, l' = Array.smartfoldmap f accu l in
+ let accu, l' = Array.Smart.fold_left_map f accu l in
if b'==b && l'==l then accu, c
else accu, mkApp (b', l')
| Proj (p,t) ->
@@ -601,23 +593,23 @@ let fold_map f accu c = match kind c with
if t' == t then accu, c
else accu, mkProj (p, t')
| Evar (e,l) ->
- let accu, l' = Array.smartfoldmap f accu l in
+ let accu, l' = Array.Smart.fold_left_map f accu l in
if l'==l then accu, c
else accu, mkEvar (e, l')
| Case (ci,p,b,bl) ->
let accu, b' = f accu b in
let accu, p' = f accu p in
- let accu, bl' = Array.smartfoldmap f accu bl in
+ let accu, bl' = Array.Smart.fold_left_map f accu bl in
if b'==b && p'==p && bl'==bl then accu, c
else accu, mkCase (ci, p', b', bl')
| Fix (ln,(lna,tl,bl)) ->
- let accu, tl' = Array.smartfoldmap f accu tl in
- let accu, bl' = Array.smartfoldmap f accu bl in
+ let accu, tl' = Array.Smart.fold_left_map f accu tl in
+ let accu, bl' = Array.Smart.fold_left_map f accu bl in
if tl'==tl && bl'==bl then accu, c
else accu, mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let accu, tl' = Array.smartfoldmap f accu tl in
- let accu, bl' = Array.smartfoldmap f accu bl in
+ let accu, tl' = Array.Smart.fold_left_map f accu tl in
+ let accu, bl' = Array.Smart.fold_left_map f accu bl in
if tl'==tl && bl'==bl then accu, c
else accu, mkCoFix (ln,(lna,tl',bl'))
@@ -653,7 +645,7 @@ let map_with_binders g f l c0 = match kind c0 with
else mkLetIn (na, b', t', c')
| App (c, al) ->
let c' = f l c in
- let al' = CArray.Fun1.smartmap f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if c' == c && al' == al then c0
else mkApp (c', al')
| Proj (p, t) ->
@@ -661,28 +653,28 @@ let map_with_binders g f l c0 = match kind c0 with
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
- let al' = CArray.Fun1.smartmap f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
let p' = f l p in
let c' = f l c in
- let bl' = CArray.Fun1.smartmap f l bl in
+ let bl' = Array.Fun1.Smart.map f l bl in
if p' == p && c' == c && bl' == bl then c0
else mkCase (ci, p', c', bl')
| Fix (ln, (lna, tl, bl)) ->
- let tl' = CArray.Fun1.smartmap f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.smartmap f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
if tl' == tl && bl' == bl then c0
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = CArray.Fun1.smartmap f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.smartmap f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
Univ.Instance.t -> Univ.Instance.t -> bool
type constr_compare_fn = int -> constr -> constr -> bool
@@ -720,10 +712,10 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
| Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
| Const (c1,u1), Const (c2,u2) ->
(* The args length currently isn't used but may as well pass it. *)
- Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2
- | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2
+ Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
+ | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2
| Construct (c1,u1), Construct (c2,u2) ->
- eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2
+ eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
@@ -1217,3 +1209,10 @@ let hcons =
Id.hcons)
(* let hcons_types = hcons_constr *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 16:54:30 +0000