From: Ferruccio Guidi Date: Mon, 18 Apr 2016 15:29:33 +0000 (+0000) Subject: As required by M. Maietti, X-Git-Tag: make_still_working~600 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=e9f96fa56226dfd74de214c89d827de0c5018ac7;p=helm.git 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 02e161780..5d138bbe0 100644 --- 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 5086eb845..387a09fe7 100644 --- 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 24cade68a..e84cd7084 100644 --- 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> ; 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 74e28ff9c..991a88f64 100644 --- 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 a557ef563..650d12620 100644 --- 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 3117a12ad..0620a6233 100644 --- 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 451beaa70..165b70ce1 100644 --- 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 index 000000000..ef3abed3e --- /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 136efe573..399d5631b 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -118,6 +118,7 @@ coinductive constraint corec + cyclic default discriminator for