X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fkernel.ml;h=818ad07d9e9319c013e990f576f3f60ca1d5bb60;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=f9ed0c4666e297f2ec8d2142bc2b9f874f078e28;hpb=ea6b4322051d3eb1794bfca3928f6e1773f971ba;p=helm.git

diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml
index f9ed0c466..818ad07d9 100644
--- a/matita/components/binaries/matex/kernel.ml
+++ b/matita/components/binaries/matex/kernel.ml
@@ -44,11 +44,17 @@ let init () =
    H.set_log_callback no_log;
    let u0 = mk_type_universe "0" in
    let u1 = mk_type_universe "1" in
-   E.add_lt_constraint u0 u1
+   E.add_lt_constraint ~acyclic:true u0 u1
 
-let fst_var = 1
+let fst_var = 1 (* first variable *)
 
-let snd_var = 2
+let snd_var = 2 (* second variable *)
+
+let fst_con = 1 (* first constructor *)
+
+let appl ts = C.Appl ts
+
+let prod s w t = C.Prod (s, w, t)
 
 let lambda s w t = C.Lambda (s, w, t)
 
@@ -93,6 +99,17 @@ let whd c t =
 let typeof c t =
    K.typeof G.status [] [] c t
 
+let whd_typeof c t = whd c (typeof c t)
+
+let not_prop1 c u = match whd_typeof c u with
+   | C.Sort (C.Prop) -> false
+   | _               -> true
+
+let not_prop2 c t = not_prop1 c (typeof c t)
+
+let does_not_occur i c t =
+   K.does_not_occur G.status ~subst:[] c 0 i t
+
 let segments_of_uri u =
    let s = U.string_of_uri u in
    let s = F.chop_extension s in
@@ -101,7 +118,7 @@ let segments_of_uri u =
    let s = S.sub s (i+2) (l-i-2) in
    X.segments_of_string [] (l-i-2) s
 
-let name_of_reference ss = function
+let names_of_reference ss = function
    | C.Constant (_, name, _, _, _), R.Decl      ->
       ss, name
    | C.Constant (_, name, _, _, _), R.Def _     ->
@@ -121,3 +138,10 @@ let name_of_reference ss = function
       (name :: ss), name
    | _                                          ->
       failwith "name_of_reference"
+
+let resolve_reference = function
+   | R.Ref (u, r) ->
+      let ss = segments_of_uri u in
+      let _, _, _, _, obj = E.get_checked_obj G.status u in  
+      let ss, name = names_of_reference ss (obj, r) in
+      X.rev_map_concat X.id "." "type" ss, name