diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 386 |
1 files changed, 313 insertions, 73 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index ba7fecadf8..8e5d15dd2d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -100,28 +100,20 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) 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 *) @@ -235,6 +227,12 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id +let mkRef (gr,u) = let open GlobRef in match gr with + | ConstRef c -> mkConstU (c,u) + | IndRef ind -> mkIndU (ind,u) + | ConstructRef c -> mkConstructU (c,u) + | VarRef x -> mkVar x + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -245,6 +243,17 @@ let mkVar id = Var id let kind c = c +let rec kind_nocast_gen kind c = + match kind c with + | Cast (c, _, _) -> kind_nocast_gen kind c + | App (h, outer) as k -> + (match kind_nocast_gen kind h with + | App (h, inner) -> App (h, Array.append inner outer) + | _ -> k) + | k -> k + +let kind_nocast c = kind_nocast_gen kind c + (* The other way around. We treat specifically smart constructors *) let of_kind = function | App (f, a) -> mkApp (f, a) @@ -268,17 +277,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 @@ -368,17 +377,17 @@ let destConst c = match kind c with (* Destructs an existential variable *) let destEvar c = match kind c with - | Evar (kn, a as r) -> r + | Evar (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a (co)inductive type named kn *) let destInd c = match kind c with - | Ind (kn, a as r) -> r + | Ind (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a constructor *) let destConstruct c = match kind c with - | Construct (kn, a as r) -> r + | Construct (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) @@ -398,6 +407,12 @@ let destCoFix c = match kind c with | CoFix cofix -> cofix | _ -> raise DestKO +let destRef c = let open GlobRef in match kind c with + | Var x -> VarRef x, Univ.Instance.empty + | Const (c,u) -> ConstRef c, u + | Ind (ind,u) -> IndRef ind, u + | Construct (c,u) -> ConstructRef c, u + | _ -> raise DestKO (******************************************************************) (* Flattening and unflattening of embedded applications and casts *) @@ -429,12 +444,12 @@ let fold f acc c = match kind c with | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c + | Proj (_p,c) -> f acc c | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> + | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> + | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl (* [iter f c] iters [f] on the immediate subterms of [c]; it is @@ -449,7 +464,7 @@ let iter f c = match kind c with | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c + | Proj (_p,c) -> f c | Evar (_,l) -> Array.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -468,22 +483,122 @@ 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 - | Proj (p,c) -> f n c + | 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 + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (_na,t,c) -> f (g n) (f n acc t) c + | Lambda (_na,t,c) -> f (g n) (f n acc t) c + | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(_,tl,bl)) -> + let n' = iterate g (Array.length tl) n 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 (_,(_,tl,bl)) -> + let n' = iterate g (Array.length tl) n 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 (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) -let map f c = match kind c with +let rec map_under_context f n d = + if n = 0 then f d else + match kind d with + | LetIn (na,b,t,c) -> + let b' = f b in + let t' = f t in + let c' = map_under_context f (n-1) c in + if b' == b && t' == t && c' == c then d + else mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f t in + let b' = map_under_context f (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches f ci bl = + let nl = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context f) nl bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate f ci p = + map_under_context f (List.length ci.ci_pp_info.ind_tags) p + +let rec map_under_context_with_binders g f l n d = + if n = 0 then f l d else + match kind 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_binders g f (g l) (n-1) c in + if b' == b && t' == t && c' == c then d + else mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f l t in + let b' = map_under_context_with_binders g f (g l) (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches_with_binders g f l ci bl = + let tags = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate_with_binders g f l ci p = + map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p + +let rec map_under_context_with_full_binders g f l n d = + if n = 0 then f l d else + match kind 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 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 mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f l t in + let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in + if t' == t && b' == b then d + else mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") + +let map_branches_with_full_binders g f l ci bl = + let tags = Array.map List.length ci.ci_pp_info.cstr_tags in + let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in + if Array.for_all2 (==) bl' bl then bl else bl' + +let map_return_predicate_with_full_binders g f l ci p = + map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p + +let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c | Cast (b,k,t) -> @@ -509,7 +624,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) -> @@ -517,26 +632,35 @@ 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) when userview -> + let b' = f b in + let p' = map_return_predicate f ci p in + let bl' = map_branches f ci bl in + if b'==b && p'==p && bl'==bl then c + else mkCase (ci, p', b', bl') | 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')) +let map_user_view = map_gen true +let map = map_gen false + (* Like {!map} but with an accumulator. *) let fold_map f accu c = match kind c with @@ -565,7 +689,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) -> @@ -573,23 +697,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')) @@ -625,7 +749,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) -> @@ -633,31 +757,74 @@ 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 -> - Univ.Instance.t -> Univ.Instance.t -> bool +(*********************) +(* Lifting *) +(*********************) + +(* The generic lifting function *) +let rec exliftn el c = + let open Esubst in + match kind c with + | Rel i -> mkRel(reloc_rel i el) + | _ -> map_with_binders el_lift exliftn el c + +(* Lifting the binding depth across k bindings *) -type constr_compare_fn = int -> constr -> constr -> bool +let liftn n k c = + let open Esubst in + match el_liftn (pred k) (el_shft n el_id) with + | ELID -> c + | el -> exliftn el c + +let lift n = liftn n 1 + +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> 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) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) 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 + + +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool + +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose @@ -671,19 +838,16 @@ type constr_compare_fn = int -> constr -> constr -> bool calls to {!Array.equal_norefl}). *) let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = - match kind1 t1, kind2 t2 with + match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with + | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1, _, _), _ -> leq nargs c1 t2 - | _, Cast (c2, _, _) -> leq nargs t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 - | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && @@ -692,10 +856,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)) -> @@ -808,8 +972,10 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if UGraph.check_leq univs u1 u2 then true else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in + cstrs := Univ.Constraint.union c !cstrs; + true + with Univ.UniverseInconsistency _ -> false) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -860,11 +1026,11 @@ let constr_ord_int f t1 t2 = | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | App _, _ -> -1 | _, App _ -> 1 - | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -1123,9 +1289,9 @@ let rec hash t = combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) - | Fix (ln ,(_, tl, bl)) -> + | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) - | CoFix(ln, (_, tl, bl)) -> + | CoFix(_ln, (_, tl, bl)) -> combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n @@ -1187,3 +1353,77 @@ 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 + +(* Sorts and sort family *) + +let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) = + let open Pp in + let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in + hov 1 + (str"fix " ++ int i ++ spc() ++ str"{" ++ + v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ + str"}") + +let pr_puniverses p u = + if Univ.Instance.is_empty u then p + else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)") + +(* Minimalistic constr printer, typically for debugging *) + +let rec debug_print c = + let open Pp in + match kind c with + | Rel n -> str "#"++int n + | Meta n -> str "Meta(" ++ int n ++ str ")" + | Var id -> Id.print id + | Sort s -> Sorts.debug_print s + | Cast (c,_, t) -> hov 1 + (str"(" ++ debug_print c ++ cut() ++ + str":" ++ debug_print t ++ str")") + | Prod (Name(id),t,c) -> hov 1 + (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++ + spc() ++ debug_print c) + | Prod (Anonymous,t,c) -> hov 0 + (str"(" ++ debug_print t ++ str " ->" ++ spc() ++ + debug_print c ++ str")") + | Lambda (na,t,c) -> hov 1 + (str"fun " ++ Name.print na ++ str":" ++ + debug_print t ++ str" =>" ++ spc() ++ debug_print c) + | LetIn (na,b,t,c) -> hov 0 + (str"let " ++ Name.print na ++ str":=" ++ debug_print b ++ + str":" ++ brk(1,2) ++ debug_print t ++ cut() ++ + debug_print c) + | App (c,l) -> hov 1 + (str"(" ++ debug_print c ++ spc() ++ + prlist_with_sep spc debug_print (Array.to_list l) ++ str")") + | Evar (e,l) -> hov 1 + (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ + prlist_with_sep spc debug_print (Array.to_list l) ++str"}") + | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")" + | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" + | Construct (((sp,i),j),u) -> + str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" + | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")" + | Case (_ci,p,c,bl) -> v 0 + (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++ + debug_print c ++ str"of") ++ cut() ++ + prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++ + cut() ++ str"end") + | Fix f -> debug_print_fix debug_print f + | CoFix(i,(lna,tl,bl)) -> + let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in + hov 1 + (str"cofix " ++ int i ++ spc() ++ str"{" ++ + v 0 (prlist_with_sep spc (fun (na,ty,bd) -> + Name.print na ++ str":" ++ debug_print ty ++ + cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ + str"}") |