Splitting Term into five unrelated interfaces:

1. sorts.ml: A small file utility for sorts;

2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;

3. vars.ml: Everything related to term variables, that is, occurences
and substitution;

4. context.ml: Rel/Named context and all that;

5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 64 insertions, 0 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
new file mode 100644
index 000000000..7ab6b553a
--- /dev/null
+++ b/kernel/sorts.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Univ
+
+type contents = Pos | Null
+
+type family = InProp | InSet | InType
+
+type t =
+  | Prop of contents                      (* proposition types *)
+  | Type of universe
+
+let prop = Prop Null
+let set = Prop Pos
+let type1 = Type type1_univ
+
+let compare s1 s2 =
+  if s1 == s2 then 0 else
+  match s1, s2 with
+  | Prop c1, Prop c2 ->
+    begin match c1, c2 with
+    | Pos, Pos | Null, Null -> 0
+    | Pos, Null -> -1
+    | Null, Pos -> 1
+    end
+  | Type u1, Type u2 -> Universe.compare u1 u2
+  | Prop _, Type _ -> -1
+  | Type _, Prop _ -> 1
+
+let equal s1 s2 = Int.equal (compare s1 s2) 0
+
+let is_prop = function
+| Prop Null -> true
+| _ -> false
+
+let family = function
+  | Prop Null -> InProp
+  | Prop Pos -> InSet
+  | Type _ -> InType
+
+module Hsorts =
+  Hashcons.Make(
+    struct
+      type _t = t
+      type t = _t
+      type u = universe -> universe
+      let hashcons huniv = function
+          Prop c -> Prop c
+        | Type u -> Type (huniv u)
+      let equal s1 s2 =
+        match (s1,s2) with
+            (Prop c1, Prop c2) -> c1 == c2
+          | (Type u1, Type u2) -> u1 == u2
+          |_ -> false
+      let hash = Hashtbl.hash
+    end)
+
+let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ