Added new syntax Type[n] where n is a number.

The old kernel interpretes it simply as Type.
The new kernel as Typen.

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 29898eb13ace83196d7340d8f10ff653dc170cc6..b92b38656dd3704e58ee97342b6f1f94fbe150dc 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -153,6 +153,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
+    | Ast.Sort (`NType s)-> "Type[" ^ 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 c7659018127aed95d660f9a23d9a5dd19674336a..3c96a5a512ac7d1bd49b94ff9ab79cf373b9d0b9 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -29,7 +29,7 @@
 
 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]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType 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 61e77c6fe12047b9efbe5939a362df8b088333fb..508411d2847b1b84083141efa5bbe14aed16a8fa 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -109,7 +109,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type _ -> `Pi
+          | `Set | `Type _ | `NType _ -> `Pi
           | `Prop | `CProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 563beaa1c11dd678680e828b02220b78d26f2f70..9ad05dc926725e75b9ca287ebc4b8e3324ae4a9e 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,12 +25,13 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe  ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType 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 ^ "]"
   | `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 4526521fbd0e6d00f6e57d0b0eb6f05ab8636c09..9182ad618794b21c5fa6b6c86d3ca5d74ab21dba 100644 (file)
--- 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]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType 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 2b469ce9d7d4b24585421f5007ff1cc80602c1f4..ed28894a7f6320c0f326c5b3fbf3ce07c911c2e6 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -484,11 +484,15 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | 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 (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env
          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index e3e54f112a5730608644d65f28b6135df444f250..cd02c9d36070a011c46911210917e84246b0beb3 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -563,6 +563,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
     | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]

diff --git a/helm/software/components/content_pres/content2pres.mli b/helm/software/components/content_pres/content2pres.mli
index 8d3753d8662e59c16c21a6862ec3889505b6bfc0..c5d32e9fdd5e27ef0a86ad6bdcffae1dc916ca83 100644 (file)
--- a/helm/software/components/content_pres/content2pres.mli
+++ b/helm/software/components/content_pres/content2pres.mli
@@ -34,7 +34,7 @@
 
 val content2pres:
   ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool ->
-  ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+  ids_to_inner_sorts:(Cic.id, CicNotationPt.sort_kind) Hashtbl.t ->
   Cic.annterm Content.cobj ->
     CicNotationPres.boxml_markup
 

diff --git a/helm/software/components/content_pres/sequent2pres.mli b/helm/software/components/content_pres/sequent2pres.mli
index d6d9daa4005918fbe6892eb920679190e940492d..a9384eb182601ac516cd96e4ca9b652cf0280fa3 100644 (file)
--- a/helm/software/components/content_pres/sequent2pres.mli
+++ b/helm/software/components/content_pres/sequent2pres.mli
@@ -33,6 +33,6 @@
 (***************************************************************************)
 
 val sequent2pres :
-  ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+  ids_to_inner_sorts:(Cic.id, CicNotationPt.sort_kind) Hashtbl.t ->
   Cic.annterm Content.conjecture ->
     CicNotationPres.boxml_markup

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index e15442970a0ac3a139d54cf2cf0b1d85d2c1ee95..d6694cbb66419be45f3c88609c12f6434e4eef62 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -93,6 +93,7 @@ let string_of_sort_kind = function
   | `Set -> "Set"
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
+  | `NType s -> "Type[" ^ s ^ "]"
 
 let pp_ast0 t k =
   let rec aux =

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 9e9130857145c2bb84d74eb718c33625f78d0e3b..a09c085995108286f62dea5db8c6c36706e3140d 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -76,9 +76,6 @@ let interpretate_term
   assert (uri = None);
 
   let rec aux ~localize loc context = function
-    t ->
-            let res = 
-    match t with
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
         if localize then 
@@ -399,16 +396,17 @@ patterns not implemented *)
        [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"])
+    | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
-
-            in
-(*             prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] res); *)
-            res
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> NCic.Implicit annotation
     | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) ->