From e91e815449698c6f2595958f94cd06c10ba10398 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 27 Sep 2009 21:22:09 +0000 Subject: [PATCH] Type printed as such, CProp printed as such --- .../content_pres/termContentPres.ml | 26 ++++++++++++------- .../ng_cic_content/nTermCicContent.ml | 24 +++++++++-------- 2 files changed, 29 insertions(+), 21 deletions(-) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 3fae0f52b..68cc4ccbb 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -88,13 +88,21 @@ let binder_symbol s = add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) (builtin_symbol s) -let string_of_sort_kind = function - | `Prop -> "Prop" - | `Set -> "Set" - | `CProp _ -> "CProp" - | `Type _ -> "Type" - | `NType s -> "Type[" ^ s ^ "]" - | `NCProp s -> "CProp[" ^ s ^ "]" +let xml_of_sort x = + let to_string x = Ast.Ident (x, None) in + let identify x = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x) + in + let lvl t = Ast.AttributedTerm (`Level 90,t) in + match x with + | `Prop -> identify "Prop" + | `Set -> identify "Set" + | `CProp _ -> identify "CProp" + | `Type _ -> identify "Type" + | `NType s -> lvl(Ast.Layout (Ast.Sub (identify "Type",to_string s))) + | `NCProp s -> lvl(Ast.Layout (Ast.Sub (identify "CProp",to_string s))) +;; + let map_space f l = HExtlib.list_concat @@ -268,9 +276,7 @@ let pp_ast0 t k = | Ast.Literal _ | Ast.UserInput as leaf -> leaf | t -> CicNotationUtil.visit_ast ~special_k k t - and aux_sort sort_kind = - add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) - (Ast.Ident (string_of_sort_kind sort_kind, None)) + and aux_sort sort_kind = xml_of_sort sort_kind and aux_ty = function | None -> builtin_symbol "?" | Some ty -> k ty diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 3c17823b6..e36a1290c 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -58,6 +58,12 @@ let idref register_ref = Ast.AttributedTerm (`IdRef id, t) ;; +let level_of_uri u = + let name = NUri.name_of_uri u in + assert(String.length name > String.length "Type"); + String.sub name 4 (String.length name - 4) +;; + (* CODICE c&p da NCicPp *) let nast_of_cic0 status ~(idref: @@ -81,17 +87,13 @@ let nast_of_cic0 status idref (Ast.Meta (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l)) | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) - | NCic.Sort NCic.Type _ -> idref (Ast.Sort `Set) - (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0" - | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) - | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) - | C.Sort (C.Type l) -> - F.fprintf f "Max("; - aux ctx (C.Sort (C.Type [List.hd l])); - List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) - (List.tl l); - F.fprintf f ")"*) - (* CSC: qua siamo grezzi *) + | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) + | NCic.Sort NCic.Type ((`Type,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u))) + | NCic.Sort NCic.Type ((`CProp,u)::_) -> + idref(Ast.Sort (`NCProp (level_of_uri u))) + | NCic.Sort NCic.Type ((`Succ,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u ^ "+1"))) | NCic.Implicit `Hole -> idref (Ast.UserInput) | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector) | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) -- 2.39.2