From: Claudio Sacerdoti Coen Date: Fri, 5 Dec 2008 23:12:39 +0000 (+0000) Subject: Added new syntax Type[n] where n is a number. X-Git-Tag: make_still_working~4444 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git 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 29898eb13..b92b38656 100644 --- 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 c76590181..3c96a5a51 100644 --- 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 61e77c6fe..508411d28 100644 --- 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 563beaa1c..9ad05dc92 100644 --- 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 4526521fb..9182ad618 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] +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 2b469ce9d..ed28894a7 100644 --- 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 e3e54f112..cd02c9d36 100644 --- 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 8d3753d86..c5d32e9fd 100644 --- 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 d6d9daa40..a9384eb18 100644 --- 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 e15442970..d6694cbb6 100644 --- 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 9e9130857..a09c08599 100644 --- 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)) ->