From: Enrico Tassi Date: Mon, 18 May 2009 15:25:52 +0000 (+0000) Subject: in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as X-Git-Tag: make_still_working~3963 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as Type[0]. The same holds for CProp. tests/ng_pts.ma defines some sorts, you may want to include it --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 45fa23a0d..a835e074f 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -154,6 +154,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Sort (`Type _) -> "Type" | Ast.Sort (`CProp _)-> "CProp" | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" + | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" | Ast.Symbol (name, _) -> "'" ^ name | Ast.UserInput -> "" diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 3ffa95258..46381e4bc 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -29,7 +29,8 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of +CicUniv.universe | `NType of string |`NCProp of string] type fold_kind = [ `Left | `Right ] type location = Stdpp.location diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index fb8909152..c02c5892d 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -126,7 +126,7 @@ let ast_of_acic0 ~output_type term_info acic k = let binder_kind = match sort_of_id id with | `Set | `Type _ | `NType _ -> `Pi - | `Prop | `CProp _ -> `Forall + | `Prop | `CProp _ | `NCProp _ -> `Forall in idref id (Ast.Binder (binder_kind, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend index 0c39328ae..e69de29bb 100644 --- a/helm/software/components/binaries/extractor/.depend +++ b/helm/software/components/binaries/extractor/.depend @@ -1,4 +0,0 @@ -extractor.cmo: -extractor.cmx: -extractor_manager.cmo: -extractor_manager.cmx: diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt index 0c39328ae..e69de29bb 100644 --- a/helm/software/components/binaries/extractor/.depend.opt +++ b/helm/software/components/binaries/extractor/.depend.opt @@ -1,4 +0,0 @@ -extractor.cmo: -extractor.cmx: -extractor_manager.cmo: -extractor_manager.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend index 33147b949..e69de29bb 100644 --- a/helm/software/components/binaries/table_creator/.depend +++ b/helm/software/components/binaries/table_creator/.depend @@ -1,2 +0,0 @@ -table_creator.cmo: -table_creator.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt index 33147b949..e69de29bb 100644 --- a/helm/software/components/binaries/table_creator/.depend.opt +++ b/helm/software/components/binaries/table_creator/.depend.opt @@ -1,2 +0,0 @@ -table_creator.cmo: -table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index 9ad05dc92..3285dcc15 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -25,13 +25,14 @@ (* $Id$ *) -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string] let string_of_sort = function | `Prop -> "Prop" | `Set -> "Set" | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) | `NType s -> "Type[" ^ s ^ "]" + | `NCProp s -> "CProp[" ^ s ^ "]" | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli index 9182ad618..0bf874e86 100644 --- a/helm/software/components/cic_acic/cic2acic.mli +++ b/helm/software/components/cic_acic/cic2acic.mli @@ -31,7 +31,7 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string] val string_of_sort: sort_kind -> string (*val sort_of_string: string -> sort_kind*) diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 3e9124e69..b869536bf 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -496,6 +496,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) + | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ())) | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~mk_choice ~env diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 8ddb78781..14032d451 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -581,8 +581,9 @@ EXTEND sort: [ [ "Prop" -> `Prop | "Set" -> `Set - | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n + | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n | "Type" -> `Type (CicUniv.fresh ()) + | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n | "CProp" -> `CProp (CicUniv.fresh ()) ] ]; diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 85f4a3187..00f6c9789 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -94,6 +94,7 @@ let string_of_sort_kind = function | `CProp _ -> "CProp" | `Type _ -> "Type" | `NType s -> "Type[" ^ s ^ "]" + | `NCProp s -> "CProp[" ^ s ^ "]" let map_space f l = HExtlib.list_concat diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index a2d1ef655..c61319233 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -171,7 +171,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 19 +let magic = 20 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -192,6 +192,7 @@ type ('term,'obj) command = | Print of loc * string | Qed of loc | NObj of loc * CicNotationPt.term CicNotationPt.obj + | NUnivConstraint of loc * bool * NUri.uri * NUri.uri | NQed of loc type punctuation_tactical = diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 6806713a4..70acd56d8 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -358,6 +358,9 @@ let pp_command ~term_pp ~obj_pp = function | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value | NObj (_,o) -> "not supported" + | NUnivConstraint (_) -> "not supported" + | NQed (_) -> "not supported" + | Pump (_) -> "not supported" let pp_punctuation_tactical = function diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ccd02981f..037a36f38 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -789,6 +789,9 @@ prerr_endline "CSC: here we should fix the height!!!"; status, `Old [] (*CSC: TO BE FIXED *) | GrafiteAst.Set (loc, name, value) -> status, `Old [] (* GrafiteTypes.set_option status name value,[] *) + | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> + NCicEnvironment.add_constraint strict [false,u1] [false,u2]; + status, `New [u1;u2] | GrafiteAst.NObj (loc,obj) -> let lexicon_status = match status.GrafiteTypes.ng_status with diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 8830a600d..e94507a86 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -836,6 +836,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= | GrafiteAst.Print _ | GrafiteAst.Qed _ | GrafiteAst.NQed _ + | GrafiteAst.NUnivConstraint _ | GrafiteAst.Set _ as cmd -> lexicon_status,metasenv,cmd | GrafiteAst.Obj (loc,obj) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 742e538fe..396567a2e 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -664,7 +664,7 @@ EXTEND in L.Number_alias (instance, dsc) ] - ]; + ]; argument: [ [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; id = IDENT -> @@ -785,6 +785,27 @@ EXTEND ind_types in G.NObj (loc, N.Inductive (params, ind_types)) + | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; + strict = [ SYMBOL <:unicode> -> true + | SYMBOL <:unicode> -> false ]; + u2 = tactic_term -> + let u1 = + match u1 with + | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) -> + NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ") + | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) -> + NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ") + | _ -> raise (Failure "only a sort can be constrained") + in + let u2 = + match u2 with + | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) -> + NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ") + | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) -> + NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ") + | _ -> raise (Failure "only a sort can be constrained") + in + G.NUnivConstraint (loc, strict,u1,u2) | IDENT "coercion" ; t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; arity = OPT int ; saturations = OPT int; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index f0a3fa0eb..5ded5b886 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -316,7 +316,7 @@ let interpretate_term_and_interpretate_term_option | CicNotationPt.Ident (name, subst) -> assert (subst = None); (try - NCic.Rel (find_in_context name context) + NCic.Rel (find_in_context name context) with Not_found -> try NCic.Const (List.assoc name obj_context) with Not_found -> @@ -342,11 +342,13 @@ let interpretate_term_and_interpretate_term_option | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) + [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"]) | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) + | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type + [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")]) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) + [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"]) | CicNotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) @@ -647,6 +649,7 @@ let disambiguate_obj in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; +(* let _ = let mk_type n = if n = 0 then @@ -685,4 +688,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index f31c4e9b1..4d60e5d42 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -29,6 +29,16 @@ let max l1 l2 = let le_constraints = ref [] (* strict,a,b *) +let resolve_universe u = + HExtlib.list_findopt + (fun (_,a,b) _ -> + prerr_endline (NUri.name_of_uri a); + if NUri.name_of_uri a = u then Some a + else if NUri.name_of_uri b = u then Some b + else None) + !le_constraints +;; + let rec le_path_uri avoid strict a b = (not strict && NUri.eq a b) || List.exists diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 4604bd2fd..c4fa396cc 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -33,6 +33,8 @@ val add_constraint: bool -> NCic.universe -> NCic.universe -> unit val sup : NCic.universe -> NCic.universe option val pp_constraints: unit -> string +val resolve_universe: string -> NUri.uri option + val get_checked_def: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 2e34a62a9..3ce24c446 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,6 +1,6 @@ -nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi -nCicElim.cmi: +nCicTacReduction.cmo: nCicTacReduction.cmi +nCicTacReduction.cmx: nCicTacReduction.cmi nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 2e34a62a9..3ce24c446 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,6 +1,6 @@ -nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi -nCicElim.cmi: +nCicTacReduction.cmo: nCicTacReduction.cmi +nCicTacReduction.cmx: nCicTacReduction.cmi nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index cbb73844d..2241043a9 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "nat/plus.ma". +include "ng_pts.ma". ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A. @@ -30,6 +30,8 @@ naxiom NP: Prop. ndefinition Q: Prop ≝ NP. +include "nat/nat.ma". + nlet rec nzero (n:nat) : nat ≝ match n with [ O ⇒ O @@ -57,4 +59,4 @@ and nmzero (m:mat 0 (dt ?)) : nnat 0 (dt ?) ≝ [ mS n ⇒ nnzero n ]. nrecord pair (n: nat) (x: DT n) (label: Type): Type ≝ - { lbl:label; l: pair n x label; r: pair n x label}. \ No newline at end of file + { lbl:label; l: pair n x label; r: pair n x label}. diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma index dfded53ee..c8998a227 100644 --- a/helm/software/matita/tests/ng_elim.ma +++ b/helm/software/matita/tests/ng_elim.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "ng_pts.ma". + ninductive nat: Type ≝ O: nat | S: nat → nat. diff --git a/helm/software/matita/tests/ng_pts.ma b/helm/software/matita/tests/ng_pts.ma new file mode 100644 index 000000000..24606b802 --- /dev/null +++ b/helm/software/matita/tests/ng_pts.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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 constraint Type[0] < Type[1]. +universe constraint Type[1] < Type[2]. +universe constraint CProp[0] < CProp[1]. +universe constraint CProp[1] < CProp[2]. +universe constraint Type[0] ≤ CProp[0]. +universe constraint CProp[0] ≤ Type[0]. +universe constraint Type[1] ≤ CProp[1]. +universe constraint CProp[1] ≤ Type[1]. +universe constraint Type[2] ≤ CProp[2]. +universe constraint CProp[2] ≤ Type[2]. \ No newline at end of file diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma index 6c7e161f6..3bb4a6fa4 100644 --- a/helm/software/matita/tests/ng_tactics.ma +++ b/helm/software/matita/tests/ng_tactics.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ng_pts.ma". include "nat/plus.ma". ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).