As required by M. Maietti,

cyclic sort hierarchies are now allowed through the "cyclic" keyword
so we can write:
universe cyclic constraint Type[U] < Type[U].
definition inconsistent: Type[U] ≝ Type[U].
matitaclean all is required after this commit

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 02e16178077eb412b751b3f7bd63903d8702309e..5d138bbe06624ed27896cfb0511767ee045448a6 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -84,7 +84,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 36
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
@@ -102,7 +102,7 @@ type command =
   | NObj of loc * nterm NotationPt.obj * bool
   | NDiscriminator of loc * nterm
   | NInverter of loc * string * nterm * bool list option * nterm option
-  | NUnivConstraint of loc * NUri.uri * NUri.uri
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string * bool * 
       (nterm * nterm * (string * nterm) * nterm) option

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 5086eb845c6424574c565f8471ecc96b216bac14..387a09fe78b86ea4542736f7e499726a5ead5454 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -380,7 +380,7 @@ let index_eq_for_auto status uri =
 ;; 
 
 let inject_constraint =
- let basic_eval_add_constraint (u1,u2) 
+ let basic_eval_add_constraint (acyclic,u1,u2) 
      ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
      ~alias_only status
  =
@@ -390,7 +390,7 @@ let inject_constraint =
     (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
      * and also to the storage (for undo/redo). During inclusion of compiled
      * files the storage must not be touched. *)
-    NCicEnvironment.add_lt_constraint u1 u2;
+    NCicEnvironment.add_lt_constraint acyclic u1 u2;
     status
   else
    status
@@ -398,9 +398,9 @@ let inject_constraint =
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
 
-let eval_add_constraint status u1 u2 = 
- let status = NCicLibrary.add_constraint status u1 u2 in
-  NCicLibrary.dump_obj status (inject_constraint (u1,u2))
+let eval_add_constraint status acyclic u1 u2 = 
+ let status = NCicLibrary.add_constraint status acyclic u1 u2 in
+  NCicLibrary.dump_obj status (inject_constraint (acyclic,u1,u2))
 ;;
 
 let eval_ng_tac tac =
@@ -939,8 +939,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             eval_ncommand ~include_paths opts status
              ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
         | _ -> assert false)
-  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
-      eval_add_constraint status [`Type,u1] [`Type,u2]
+  | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) ->
+      eval_add_constraint status acyclic [`Type,u1] [`Type,u2]
   (* ex lexicon commands *)
   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
      let cic_appl_pattern =

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 24cade68afae5be4544d3ade1df050e5cff2bab2..e84cd708495bf436cd79853ee5f8fa242b059c9d 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -556,8 +556,9 @@ EXTEND
       paramspec = OPT inverter_param_list ; 
       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
         G.NInverter (loc,name,indty,paramspec,outsort)
-    | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
+    | IDENT "universe"; cyclic = OPT [ IDENT "cyclic" -> () ] ; IDENT "constraint"; u1 = tactic_term; 
         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+        let acyclic = match cyclic with None -> true | Some () -> false in
         let urify = function 
           | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
@@ -565,7 +566,7 @@ EXTEND
         in
         let u1 = urify u1 in
         let u2 = urify u2 in
-         G.NUnivConstraint (loc,u1,u2)
+         G.NUnivConstraint (loc,acyclic,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
     | IDENT "coercion"; name = IDENT;

diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index 74e28ff9c7925c81bcb0ed0cdf7e5f01601e5209..991a88f6406a120b9066d9c28e062ce7ff1aa13b 100644 (file)
--- a/matita/components/ng_kernel/nCicEnvironment.ml
+++ b/matita/components/ng_kernel/nCicEnvironment.ml
@@ -155,11 +155,11 @@ let typeof_sort = function
   | C.Prop -> (C.Type [])
 ;;
 
-let add_lt_constraint a b = 
+let add_lt_constraint ~acyclic a b = 
   match a,b with
   | [`Type,a2],[`Type,b2] -> 
       if not (lt_path_uri [] a2 b2) then (
-        if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+        if acyclic && (lt_path_uri [] b2 a2 || NUri.eq a2 b2) then
          (raise(BadConstraint(lazy("universe inconsistency adding "^
                     pp_constraint a2 b2
            ^ " to:\n" ^ pp_constraints ()))));

diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli
index a557ef563b0b922b6bb6424adf8d26382b61992a..650d126207d9704f2e47c18b60d95d747f217a93 100644 (file)
--- a/matita/components/ng_kernel/nCicEnvironment.mli
+++ b/matita/components/ng_kernel/nCicEnvironment.mli
@@ -62,7 +62,7 @@ val max: NCic.universe -> NCic.universe -> NCic.universe
 (* raise BadConstraints if the second arg. is an inferred universe or
  * if the added constraint gives circularity *)
 exception BadConstraint of string Lazy.t;;
-val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val add_lt_constraint: acyclic:bool -> NCic.universe -> NCic.universe -> unit
 val universe_eq: NCic.universe -> NCic.universe -> bool
 val universe_leq: NCic.universe -> NCic.universe -> bool
 val universe_lt: NCic.universe -> NCic.universe -> bool

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 3117a12ad387d8458711ab9c50cf9b32271fac4c..0620a6233dcdff5279e11b31e5b3762ad873ce68 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -372,7 +372,7 @@ let add_obj status ((u,_,_,_,_) as orig_obj) =
   status#set_timestamp (!storage,!local_aliases)
 ;;
 
-let add_constraint status u1 u2 = 
+let add_constraint status ~acyclic u1 u2 = 
   if
    List.exists
     (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false)
@@ -380,7 +380,7 @@ let add_constraint status u1 u2 =
   then
    (*CSC: raise an exception here! *)
    (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false);
-  NCicEnvironment.add_lt_constraint u1 u2;
+  NCicEnvironment.add_lt_constraint ~acyclic u1 u2;
   storage := (`Constr (u1,u2)) :: !storage;
   status#set_timestamp (!storage,!local_aliases)
 ;;

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index 451beaa70fc51883f1cddb09c68b4c188ea2654d..165b70ce19156e6d55c0f62030be3b7e0f2ea9bf 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -27,7 +27,8 @@ class virtual status :
 (* it also checks it and add it to the environment *)
 val add_obj: #status as 'status -> NCic.obj -> 'status
 val add_constraint: 
-  #status as 'status -> NCic.universe -> NCic.universe -> 'status
+  #status as 'status -> acyclic:bool ->
+  NCic.universe -> NCic.universe -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (*

diff --git a/matita/matita/lib/self_typing.ma b/matita/matita/lib/self_typing.ma
new file mode 100644 (file)
index 0000000..ef3abed
--- /dev/null
+++ b/matita/matita/lib/self_typing.ma
@@ -0,0 +1,17 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+universe cyclic constraint Type[U] < Type[U].
+
+definition inconsistent: Type[U] ≝ Type[U].

diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 136efe5736aa0bc99fccaac2e18ec54f081a34c8..399d5631b60b7250c337c0665fc7d22905054c87 100644 (file)
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -118,6 +118,7 @@
           <keyword>coinductive</keyword>
           <keyword>constraint</keyword>          
           <keyword>corec</keyword>
+          <keyword>cyclic</keyword>
           <keyword>default</keyword>
           <keyword>discriminator</keyword>
           <keyword>for</keyword>