From 08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 25 Jul 2005 10:14:34 +0000 Subject: [PATCH] implemented transformations on top of notation code --- .../METAS/meta.helm-cic_transformations.src | 2 +- helm/ocaml/Makefile.in | 2 +- helm/ocaml/cic_notation/.depend | 28 +- helm/ocaml/cic_notation/Makefile | 4 +- helm/ocaml/cic_notation/TODO | 14 +- .../box.ml | 4 +- .../box.mli | 2 + helm/ocaml/cic_notation/cicNotation.ml | 18 +- helm/ocaml/cic_notation/cicNotationFwd.ml | 3 +- helm/ocaml/cic_notation/cicNotationLexer.ml | 2 - helm/ocaml/cic_notation/cicNotationMatcher.ml | 7 +- helm/ocaml/cic_notation/cicNotationParser.mli | 2 +- helm/ocaml/cic_notation/cicNotationPp.ml | 24 +- helm/ocaml/cic_notation/cicNotationPres.ml | 183 +++-- helm/ocaml/cic_notation/cicNotationPres.mli | 7 + helm/ocaml/cic_notation/cicNotationRew.ml | 247 ++++-- helm/ocaml/cic_notation/cicNotationTag.ml | 11 - helm/ocaml/cic_notation/cicNotationUtil.ml | 11 +- helm/ocaml/cic_notation/cicNotationUtil.mli | 3 +- helm/ocaml/cic_notation/doc/samples.ma | 6 +- helm/ocaml/cic_notation/grafiteAst.ml | 6 +- helm/ocaml/cic_notation/grafiteAstPp.ml | 10 +- helm/ocaml/cic_notation/grafiteParser.ml | 16 +- .../mpresentation.ml | 6 +- .../mpresentation.mli | 0 .../renderingAttrs.ml} | 21 +- .../renderingAttrs.mli} | 39 +- helm/ocaml/cic_notation/test_parser.conf.xml | 4 + helm/ocaml/cic_notation/test_parser.ml | 48 +- helm/ocaml/cic_omdoc/Makefile | 11 +- helm/ocaml/cic_transformations/.depend | 50 +- helm/ocaml/cic_transformations/Makefile | 34 +- helm/ocaml/cic_transformations/acic2Ast.ml | 285 ------- helm/ocaml/cic_transformations/acic2Ast.mli | 37 - .../applyTransformation.ml | 12 +- helm/ocaml/cic_transformations/ast2pres.ml | 700 ------------------ helm/ocaml/cic_transformations/ast2pres.mli | 54 -- helm/ocaml/cic_transformations/boxPp.ml | 55 -- helm/ocaml/cic_transformations/cicAst.ml | 96 --- helm/ocaml/cic_transformations/cicAst.mli | 84 --- helm/ocaml/cic_transformations/cicAstPp.ml | 102 --- helm/ocaml/cic_transformations/cicAstPp.mli | 27 - .../ocaml/cic_transformations/content2pres.ml | 367 +++------ .../cic_transformations/content2pres.mli | 2 +- .../ocaml/cic_transformations/contentTable.ml | 109 --- .../cic_transformations/contentTable.mli | 6 - .../ocaml/cic_transformations/sequent2pres.ml | 32 +- .../cic_transformations/sequent2pres.mli | 2 +- helm/ocaml/cic_transformations/tacticAst.ml | 167 ----- helm/ocaml/cic_transformations/tacticAstPp.ml | 290 -------- 50 files changed, 691 insertions(+), 2561 deletions(-) rename helm/ocaml/{cic_transformations => cic_notation}/box.ml (97%) rename helm/ocaml/{cic_transformations => cic_notation}/box.mli (93%) rename helm/ocaml/{cic_transformations => cic_notation}/mpresentation.ml (97%) rename helm/ocaml/{cic_transformations => cic_notation}/mpresentation.mli (100%) rename helm/ocaml/{cic_transformations/boxPp.mli => cic_notation/renderingAttrs.ml} (62%) rename helm/ocaml/{cic_transformations/tacticAstPp.mli => cic_notation/renderingAttrs.mli} (54%) delete mode 100644 helm/ocaml/cic_transformations/acic2Ast.ml delete mode 100644 helm/ocaml/cic_transformations/acic2Ast.mli delete mode 100644 helm/ocaml/cic_transformations/ast2pres.ml delete mode 100644 helm/ocaml/cic_transformations/ast2pres.mli delete mode 100644 helm/ocaml/cic_transformations/boxPp.ml delete mode 100644 helm/ocaml/cic_transformations/cicAst.ml delete mode 100644 helm/ocaml/cic_transformations/cicAst.mli delete mode 100644 helm/ocaml/cic_transformations/cicAstPp.ml delete mode 100644 helm/ocaml/cic_transformations/cicAstPp.mli delete mode 100644 helm/ocaml/cic_transformations/contentTable.ml delete mode 100644 helm/ocaml/cic_transformations/contentTable.mli delete mode 100644 helm/ocaml/cic_transformations/tacticAst.ml delete mode 100644 helm/ocaml/cic_transformations/tacticAstPp.ml diff --git a/helm/ocaml/METAS/meta.helm-cic_transformations.src b/helm/ocaml/METAS/meta.helm-cic_transformations.src index 375ce4237..0543f4220 100644 --- a/helm/ocaml/METAS/meta.helm-cic_transformations.src +++ b/helm/ocaml/METAS/meta.helm-cic_transformations.src @@ -1,4 +1,4 @@ -requires="helm-utf8_macros helm-xml helm-cic_proof_checking helm-cic_omdoc helm-registry gdome2" +requires="helm-utf8_macros helm-xml helm-cic_proof_checking helm-cic_omdoc helm-registry helm-cic_notation gdome2" version="0.0.1" archive(byte)="cic_transformations.cma" archive(native)="cic_transformations.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index f74927b6e..cc4d94f10 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -15,8 +15,8 @@ MODULES = \ cic_omdoc \ metadata \ tactics \ - cic_transformations \ cic_notation \ + cic_transformations \ cic_textual_parser2 \ paramodulation \ $(NULL) diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 27f186e2f..da57d442c 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -8,10 +8,12 @@ cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi grafiteParser.cmi: grafiteAst.cmo cicNotationPt.cmo -cicNotationPres.cmi: cicNotationPt.cmo +cicNotationPres.cmi: mpresentation.cmi cicNotationPt.cmo box.cmi cicNotation.cmi: grafiteAst.cmo grafiteAst.cmo: cicNotationPt.cmo grafiteAst.cmx: cicNotationPt.cmx +renderingAttrs.cmo: renderingAttrs.cmi +renderingAttrs.cmx: renderingAttrs.cmi cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi @@ -36,10 +38,12 @@ cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ cicNotationFwd.cmi cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ cicNotationFwd.cmi -cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ - cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi -cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ - cicNotationMatcher.cmx cicNotationEnv.cmx cicNotationRew.cmi +cicNotationRew.cmo: renderingAttrs.cmi cicNotationUtil.cmi cicNotationPt.cmo \ + cicNotationPp.cmi cicNotationMatcher.cmi cicNotationEnv.cmi \ + cicNotationRew.cmi +cicNotationRew.cmx: renderingAttrs.cmx cicNotationUtil.cmx cicNotationPt.cmx \ + cicNotationPp.cmx cicNotationMatcher.cmx cicNotationEnv.cmx \ + cicNotationRew.cmi cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationPp.cmi cicNotationLexer.cmi cicNotationEnv.cmi \ cicNotationParser.cmi @@ -50,10 +54,16 @@ grafiteParser.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationParser.cmi \ grafiteParser.cmi grafiteParser.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationParser.cmx \ grafiteParser.cmi -cicNotationPres.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ - cicNotationPres.cmi cicNotationPp.cmi cicNotationPres.cmi -cicNotationPres.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ - cicNotationPres.cmx cicNotationPp.cmx cicNotationPres.cmi +mpresentation.cmo: mpresentation.cmi +mpresentation.cmx: mpresentation.cmi +box.cmo: renderingAttrs.cmi box.cmi +box.cmx: renderingAttrs.cmx box.cmi +cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationUtil.cmi \ + cicNotationPt.cmo cicNotationPres.cmi cicNotationPp.cmi box.cmi \ + cicNotationPres.cmi +cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationUtil.cmx \ + cicNotationPt.cmx cicNotationPres.cmx cicNotationPp.cmx box.cmx \ + cicNotationPres.cmi cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotationRew.cmi \ cicNotationParser.cmi cicNotationFwd.cmi cicNotation.cmi cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotationRew.cmx \ diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index d54e0a5f3..898efa32a 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -5,11 +5,11 @@ REQUIRES = \ helm-cic \ helm-utf8_macros \ camlp4.gramlib \ - helm-cic_transformations\ helm-cic_proof_checking \ ulex \ $(NULL) INTERFACE_FILES = \ + renderingAttrs.mli \ cicNotationUtil.mli \ cicNotationTag.mli \ cicNotationLexer.mli \ @@ -21,6 +21,8 @@ INTERFACE_FILES = \ cicNotationRew.mli \ cicNotationParser.mli \ grafiteParser.mli \ + mpresentation.mli \ + box.mli \ cicNotationPres.mli \ cicNotation.mli \ $(NULL) diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 21cfffd5e..9b74c2cfa 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -8,9 +8,13 @@ TODO * sintassi concreta - studiare/implementare sintassi con ... per i magic fold * integrazione - - portare le trasformazioni al nuovo ast - togliere file non piu' utilizzati (caterva di cvs remove) - - gestire i problemi di ridefinizione della stessa notazione? +* trasformazioni + - parentesi cagose + - spacing delle keyword + - hyperlink su head dei case pattern e sul tipo induttivo su cui si fa match +* bug di rimozione della notazione: pare che camlp4 distrugga un livello + grammaticale quando toglie l'ultima produzione ivi definita DONE @@ -31,4 +35,10 @@ DONE - refactoring: unico punto di accesso allo stato imperativo della notazione - gestire cast - salvare la notazione nei file .moo + - portare le trasformazioni al nuovo ast + - gestire i problemi di ridefinizione della stessa notazione? +* gtkmathview + - aggiungere metodo per caricare un file di configurazione dell'utente (idem + nel binding) + - algoritmo di layout delle scatole diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_notation/box.ml similarity index 97% rename from helm/ocaml/cic_transformations/box.ml rename to helm/ocaml/cic_notation/box.ml index 96c55b18a..3c079d316 100644 --- a/helm/ocaml/cic_transformations/box.ml +++ b/helm/ocaml/cic_notation/box.ml @@ -111,9 +111,11 @@ let document_of_box ~obj2xml pres = let b_h a b = H(a,b) let b_v a b = V(a,b) +let b_hv a b = H(a,b) +let b_hov a b = V(a,b) let b_text a b = Text(a,b) let b_object b = Object ([],b) let b_indent = indent let b_space = Space [None, "width", "0.5em"] -let b_kw = b_text [None, "color", "red"] +let b_kw = b_text (RenderingAttrs.object_keyword_attributes `BoxML) diff --git a/helm/ocaml/cic_transformations/box.mli b/helm/ocaml/cic_notation/box.mli similarity index 93% rename from helm/ocaml/cic_transformations/box.mli rename to helm/ocaml/cic_notation/box.mli index 296b14c15..296695780 100644 --- a/helm/ocaml/cic_transformations/box.mli +++ b/helm/ocaml/cic_notation/box.mli @@ -63,6 +63,8 @@ val document_of_box : val b_h: attr -> 'expr box list -> 'expr box val b_v: attr -> 'expr box list -> 'expr box +val b_hv: attr -> 'expr box list -> 'expr box (** default indent and spacing *) +val b_hov: attr -> 'expr box list -> 'expr box (** default indent and spacing *) val b_text: attr -> string -> 'expr box val b_object: 'expr -> 'expr box val b_indent: 'expr box -> 'expr box diff --git a/helm/ocaml/cic_notation/cicNotation.ml b/helm/ocaml/cic_notation/cicNotation.ml index 87eb9980e..f6ea55a48 100644 --- a/helm/ocaml/cic_notation/cicNotation.ml +++ b/helm/ocaml/cic_notation/cicNotation.ml @@ -32,15 +32,23 @@ type notation_id = let process_notation st = match st with - | Notation (loc, l1, associativity, precedence, l2) -> + | Notation (loc, dir, l1, associativity, precedence, l2) -> let rule_id = - CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2) + if dir <> Some `RightToLeft then + [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)) ] + else + [] in let pp_id = - CicNotationRew.add_pretty_printer ?precedence ?associativity l2 l1 + if dir <> Some `LeftToRight then + [ PrettyPrinterId + (CicNotationRew.add_pretty_printer ?precedence ?associativity + l2 l1) ] + else + [] in - st, [ RuleId rule_id; PrettyPrinterId pp_id ] + st, rule_id @ pp_id | Interpretation (loc, dsc, l2, l3) -> let interp_id = CicNotationRew.add_interpretation dsc l2 l3 in st, [ InterpretationId interp_id ] diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 93a4c684d..4f17e8049 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -242,7 +242,8 @@ let instantiate_level2 env term = | _ -> assert false in instantiate_fold_right env) - | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t)) + | If (_, p_true, p_false) as t -> + aux env (CicNotationUtil.find_branch (Magic t)) | Fail -> assert false | _ -> assert false in diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 3dc82ae42..9c0efc8bb 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -91,8 +91,6 @@ let level2_meta_keywords = (* (string, unit) Hashtbl.t, to exploit multiple bindings *) let level2_ast_keywords = Hashtbl.create 23 let _ = - (* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to - * be reviewed *) List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; "with"; "in"; "and"; "to"; "as"; "on"; "names" ] diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 91937ed34..b9809335c 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -195,7 +195,8 @@ struct struct type pattern_t = Pt.term type term_t = Pt.term - let classify = function + let rec classify = function + | Pt.AttributedTerm (_, t) -> classify t | Pt.Variable _ -> Variable | Pt.Magic _ | Pt.Layout _ @@ -386,8 +387,10 @@ struct type term_t = Cic.annterm let classify = function + | Pt.ImplicitPattern | Pt.VarPattern _ -> Variable - | _ -> Constructor + | Pt.UriPattern _ + | Pt.ApplPattern _ -> Constructor end module M = Matcher (Pattern32) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 048551915..80d79ef44 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -40,7 +40,7 @@ val parse_level2_meta: char Stream.t -> CicNotationPt.term type rule_id val extend: - CicNotationPt.term -> + CicNotationPt.term -> (* level 1 pattern *) precedence:int -> associativity:Gramext.g_assoc -> (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) -> diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 639ae48e0..b126a3def 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -28,7 +28,11 @@ open Printf open CicNotationEnv open CicNotationPt -let print_attributes = true + (* when set to true debugging information, not in sync with input syntax, will + * be added to the output of pp_term. + * set to false if you need, for example, cut and paste from matitac output to + * matitatop *) +let debug_printing = true let pp_binder = function | `Lambda -> "lambda" @@ -36,23 +40,23 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -(* let pp_literal = function (* debugging version *) +let pp_literal = function (* debugging version *) | `Symbol s -> sprintf "symbol(%s)" s | `Keyword s -> sprintf "keyword(%s)" s - | `Number s -> sprintf "number(%s)" s *) + | `Number s -> sprintf "number(%s)" s -let pp_literal = function +(* let pp_literal = function | `Symbol s | `Keyword s - | `Number s -> s + | `Number s -> s *) let rec pp_term ?(pp_parens = true) t = let t_pp = match t with -(* | AttributedTerm (`Href _, term) when print_attributes -> - sprintf "#[%s]" (pp_term term) - | AttributedTerm (_, term) when print_attributes -> - sprintf "@[%s]" (pp_term term) *) + | AttributedTerm (`Href _, term) when debug_printing -> + sprintf "#[%s]" (pp_term ~pp_parens:false term) + | AttributedTerm (_, term) when debug_printing -> + sprintf "@[%s]" (pp_term ~pp_parens:false term) | AttributedTerm (`Raw text, _) -> text | AttributedTerm (_, term) -> pp_term ~pp_parens:false term @@ -99,7 +103,7 @@ let rec pp_term ?(pp_parens = true) t = | Sort `Prop -> "Prop" | Sort `Type -> "Type" | Sort `CProp -> "CProp" - | Symbol (name, _) -> name + | Symbol (name, _) -> "'" ^ name | UserInput -> "" diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 395cab6c2..e7afad578 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -29,16 +29,8 @@ and boxml_markup = mathml_markup Box.box type markup = mathml_markup let atop_attributes = [None, "linethickness", "0pt"] -let binder_attributes = [None, "mathcolor", "blue"] -let indent_attributes = [None, "indent", "1em"] -let keyword_attributes = [None, "mathcolor", "blue"] -let to_unicode s = - try - if s.[0] = '\\' then - Utf8Macro.expand (String.sub s 1 (String.length s - 1)) - else s - with Utf8Macro.Macro_not_found _ -> s +let to_unicode = Utf8Macro.unicode_of_tex let rec make_attributes l1 = function | [] -> [] @@ -57,10 +49,27 @@ let mpres_of_box = Box.Object (_, mpres) -> mpres | box -> Mpresentation.Mobject ([], box) -let genuine_math = +let rec genuine_math = function - | Mpresentation.Mobject _ -> false + | Mpresentation.Mobject ([], obj) -> not (genuine_box obj) | _ -> true +and genuine_box = + function + | Box.Object ([], mpres) -> not (genuine_math mpres) + | _ -> true + +let rec eligible_math = + function + | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> eligible_math mpres + | Mpresentation.Mobject ([], _) -> false + | _ -> true + +let rec promote_to_math = + function + | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> promote_to_math mpres + | math -> math + +let small_skip = Mpresentation.Mspace [None, "width", "0.5em"] let box_of mathonly spec attrs children = match children with @@ -69,7 +78,7 @@ let box_of mathonly spec attrs children = let kind, spacing, indent = spec in let dress children = if spacing then - CicNotationUtil.dress (Mpresentation.Mtext ([], " ")) children + CicNotationUtil.dress small_skip children else children in @@ -77,25 +86,39 @@ let box_of mathonly spec attrs children = else let attrs' = (if spacing then [None, "spacing", "0.5em"] else []) - @ (if indent then [None, "indent", "0em 0.5em"] else []) - @ attrs + @ (if indent then [None, "indent", "0.5em"] else []) + @ attrs in match kind with - | CicNotationPt.H when List.for_all genuine_math children -> - Mpresentation.Mrow (attrs', dress children) - | CicNotationPt.H -> - mpres_of_box (Box.H (attrs', List.map box_of_mpres children)) + | CicNotationPt.H -> + if List.for_all eligible_math children then + Mpresentation.Mrow (attrs', + dress (List.map promote_to_math children)) + else + mpres_of_box (Box.H (attrs', + List.map box_of_mpres children)) +(* | CicNotationPt.H when List.for_all genuine_math children -> + Mpresentation.Mrow (attrs', dress children) *) | CicNotationPt.V -> - mpres_of_box (Box.V (attrs', List.map box_of_mpres children)) + mpres_of_box (Box.V (attrs', + List.map box_of_mpres children)) | CicNotationPt.HV -> - mpres_of_box (Box.HV (attrs', List.map box_of_mpres children)) + mpres_of_box (Box.HV (attrs', + List.map box_of_mpres children)) | CicNotationPt.HOV -> - mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children)) + mpres_of_box (Box.HOV (attrs', + List.map box_of_mpres children)) -let open_paren = Mpresentation.Mo ([], "(") -let closed_paren = Mpresentation.Mo ([], ")") -let open_box_paren = Box.Text ([], "(") -let closed_box_paren = Box.Text ([], ")") +let open_paren = Mpresentation.Mo ([], "(") +let closed_paren = Mpresentation.Mo ([], ")") +let open_brace = Mpresentation.Mo ([], "{") +let closed_brace = Mpresentation.Mo ([], "}") +let hidden_substs = Mpresentation.Mtext ([], "{...}") +let open_box_paren = Box.Text ([], "(") +let closed_box_paren = Box.Text ([], ")") +let semicolon = Mpresentation.Mo ([], ";") +let toggle_action children = + Mpresentation.Maction ([None, "actiontype", "toggle"], children) type child_pos = [ `None | `Left | `Right | `Inner ] @@ -140,8 +163,6 @@ let is_atomic t = aux_mpres t let add_parens child_prec child_assoc child_pos curr_prec t = -(* prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec - (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); *) if is_atomic t then t else if child_prec < curr_prec || (child_prec = curr_prec && @@ -180,31 +201,67 @@ let render ids_to_uris = @ make_attributes [Some "helm", "xref"; Some "xlink", "href"] [xref; uri] in let make_xref xref = make_attributes [Some "helm","xref"] [xref] in - let make_box = function - | P.Mobject (attrs, box) -> - assert (attrs = []); - box - | m -> Box.Object ([], m) - in (* when mathonly is true no boxes should be generated, only mrows *) let rec aux xmlattrs mathonly xref pos prec uris t = match t with | A.AttributedTerm (attr, t) -> aux_attribute xmlattrs mathonly xref pos prec uris t attr - | A.Ident (literal, _) -> - P.Mi (make_href xmlattrs xref [], to_unicode literal) | A.Num (literal, _) -> - P.Mn (make_href xmlattrs xref [], to_unicode literal) + let attrs = + (RenderingAttrs.number_attributes `MathML) + @ make_href xmlattrs xref uris + in + P.Mn (attrs, literal) | A.Symbol (literal, _) -> - P.Mo (make_href xmlattrs xref uris, to_unicode literal) - | A.Uri (literal, _) -> - P.Mi (make_href xmlattrs xref [], to_unicode literal) + let attrs = + (RenderingAttrs.symbol_attributes `MathML) + @ make_href xmlattrs xref uris + in + P.Mo (attrs, to_unicode literal) + | A.Ident (literal, subst) + | A.Uri (literal, subst) -> + let attrs = + (RenderingAttrs.ident_attributes `MathML) + @ make_href xmlattrs xref [] + in + let name = P.Mi (attrs, to_unicode literal) in + (match subst with + | Some [] + | None -> name + | Some substs -> + let substs' = + box_of mathonly (A.H, false, false) [] + (open_brace + :: (CicNotationUtil.dress semicolon + (List.map + (fun (name, t) -> + box_of mathonly (A.H, false, false) [] [ + P.Mi ([], name); + P.Mo ([], to_unicode "\\def"); + aux [] mathonly xref pos prec uris t ]) + substs)) + @ [ closed_brace ]) +(* (CicNotationUtil.dress semicolon + (List.map + (fun (var, t) -> + let var_uri = UriManager.uri_of_string var in + let var_name = UriManager.name_of_uri var_uri in + let href_attr = Some "xlink", "href", var in + box_of mathonly (A.H, false, false) [] [ + P.Mi ([href_attr], var_name); + P.Mo ([], to_unicode "\\def"); + aux [] mathonly xref pos prec uris t ]) + substs)) *) + in + let substs_maction = toggle_action [ hidden_substs; substs' ] in + box_of mathonly (A.H, false, false) [] [ name; substs_maction ]) | A.Literal l -> aux_literal xmlattrs xref prec uris l + | A.UserInput -> P.Mtext ([], "%") | A.Layout l -> aux_layout mathonly xref pos prec uris l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> - prerr_endline (CicNotationPp.pp_term t); + prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); assert false and aux_attribute xmlattrs mathonly xref pos prec uris t = function @@ -218,10 +275,10 @@ let render ids_to_uris = | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t and aux_literal xmlattrs xref prec uris l = let attrs = make_href xmlattrs xref uris in - match l with - | `Symbol s -> P.Mo (attrs, to_unicode s) - | `Keyword s -> P.Mo (attrs, to_unicode s) - | `Number s -> P.Mn (attrs, to_unicode s) + (match l with + | `Symbol s -> P.Mo (attrs, to_unicode s) + | `Keyword s -> P.Mo (attrs, to_unicode s) + | `Number s -> P.Mn (attrs, to_unicode s)) and aux_layout mathonly xref pos prec uris l = let attrs = make_xref xref in let invoke' t = aux [] true None pos prec uris t in @@ -237,11 +294,17 @@ let render ids_to_uris = | A.Sqrt t -> P.Msqrt (attrs, invoke' t) | A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2) | A.Box ((_, spacing, _) as kind, terms) -> - let children = aux_children mathonly spacing xref pos prec uris (CicNotationUtil.ungroup terms) in - box_of mathonly kind attrs children + let children = + aux_children mathonly spacing xref pos prec uris + (CicNotationUtil.ungroup terms) + in + box_of mathonly kind attrs children | A.Group terms -> - let children = aux_children false mathonly xref pos prec uris (CicNotationUtil.ungroup terms) in - box_of mathonly (A.H, false, false) attrs children + let children = + aux_children mathonly false xref pos prec uris + (CicNotationUtil.ungroup terms) + in + box_of mathonly (A.H, false, false) attrs children | A.Break -> assert false (* TODO? *) and aux_children mathonly spacing xref pos prec uris terms = let find_clusters = @@ -249,8 +312,10 @@ let render ids_to_uris = function [] when acc = [] -> List.rev clusters | [] -> aux_list first (List.rev acc :: clusters) [] [] - | (A.Layout A.Break) :: tl when acc = [] -> aux_list first clusters [] tl - | (A.Layout A.Break) :: tl -> aux_list first (List.rev acc :: clusters) [] tl + | (A.Layout A.Break) :: tl when acc = [] -> + aux_list first clusters [] tl + | (A.Layout A.Break) :: tl -> + aux_list first (List.rev acc :: clusters) [] tl | [hd] -> let pos' = if first then @@ -262,7 +327,8 @@ let render ids_to_uris = | `Right -> `Right | `Left -> `Inner in - aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) [] + aux_list false clusters + (aux [] mathonly xref pos' prec uris hd :: acc) [] | hd :: tl -> let pos' = match pos, first with @@ -273,7 +339,8 @@ let render ids_to_uris = | `Right, _ -> `Inner | `Inner, _ -> `Inner in - aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) tl + aux_list false clusters + (aux [] mathonly xref pos' prec uris hd :: acc) tl in aux_list true [] [] in @@ -286,12 +353,12 @@ let render ids_to_uris = in aux [] false None `None 0 [] +let rec print_box (t: CicNotationPres.boxml_markup) = + Box.box2xml print_mpres t +and print_mpres (t: CicNotationPres.mathml_markup) = + Mpresentation.print_mpres print_box t + let render_to_boxml id_to_uri t = - let rec print_box (t: CicNotationPres.boxml_markup) = - Box.box2xml print_mpres t - and print_mpres (t: CicNotationPres.mathml_markup) = - Mpresentation.print_mpres print_box t - in let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in - Ast2pres.add_xml_declaration xml_stream + Xml.add_xml_declaration xml_stream diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli index 68da94458..f507dc6bf 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.mli +++ b/helm/ocaml/cic_notation/cicNotationPres.mli @@ -32,9 +32,16 @@ type markup = mathml_markup * @param ids_to_uris mapping id -> uri for hyperlinking *) val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup +(** @param ids_to_uris *) val render_to_boxml: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t (* val render_to_mathml: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> mathml_markup *) +val mpres_of_box: boxml_markup -> mathml_markup +val box_of_mpres: mathml_markup -> boxml_markup + +val print_mpres: mathml_markup -> Xml.token Stream.t +val print_box: boxml_markup -> Xml.token Stream.t + diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index b7322afd4..8c73f8407 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -69,50 +69,187 @@ let resolve_binder = function | `Forall -> "\\forall" | `Exists -> "\\exists" -let binder_attributes = [None, "mathcolor", "blue"] -let atop_attributes = [None, "linethickness", "0pt"] -let indent_attributes = [None, "indent", "1em"] -let keyword_attributes = [None, "mathcolor", "blue"] +let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) + +let rec remove_level_info = + function + | Ast.AttributedTerm (`Level _, t) -> remove_level_info t + | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) + | t -> t + +let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t) +let add_keyword_attrs = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) +let box kind spacing indent content = + Ast.Layout (Ast.Box ((kind, spacing, indent), content)) +let hbox = box Ast.H +let vbox = box Ast.V +let hvbox = box Ast.HV +let hovbox = box Ast.HOV +let break = Ast.Layout Ast.Break +let reset_href t = Ast.AttributedTerm (`Href [], t) +let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) +let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k))) +let number s = + reset_href + (add_xml_attrs (RenderingAttrs.number_attributes `MathML) + (Ast.Literal (`Number s))) +let ident i = + add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None)) +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" let pp_ast0 t k = - let reset_href t = Ast.AttributedTerm (`Href [], t) in - let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in - let binder_symbol s = - Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s) - in let rec aux = function | Ast.Appl ts -> - Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc), - Ast.Layout - (Ast.Box ((Ast.HOV, true, true), - (CicNotationUtil.dress - (Ast.Layout Ast.Break) - (List.map k ts))))) - | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) - | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> - Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), - Ast.Layout (Ast.Box ((Ast.HV, false, true), [ - aux_ty ty; - Ast.Layout Ast.Break; - binder_symbol "\\to"; - k body]))) + add_level_info Ast.apply_prec Ast.apply_assoc + (hovbox true true (CicNotationUtil.dress break (List.map k ts))) | Ast.Binder (binder_kind, (id, ty), body) -> - Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), - Ast.Layout (Ast.Box ((Ast.HV, false, true), [ - binder_symbol (resolve_binder binder_kind); - k id; - builtin_symbol ":"; - aux_ty ty; - Ast.Layout Ast.Break; - builtin_symbol "."; - k body ]))) + add_level_info Ast.binder_prec Ast.binder_assoc + (hvbox false true + [ binder_symbol (resolve_binder binder_kind); + k id; builtin_symbol ":"; aux_ty ty; break; + builtin_symbol "."; k body ]) + | Ast.Case (what, indty_opt, outty_opt, patterns) -> + let outty_box = + match outty_opt with + | None -> [] + | Some outty -> + [ builtin_symbol "["; remove_level_info (k outty); + builtin_symbol "]"; break ] + in + let indty_box = + match indty_opt with + | None -> [] + | Some indty -> [ keyword "in"; ident indty ] + in + let match_box = + hvbox false true [ + keyword "match"; break; + hvbox false false ([ k what ] @ indty_box); break; + keyword "with" ] + in + let mk_case_pattern (head, vars) = + hbox true false (ident head :: List.map aux_var vars) + in + let patterns' = + List.map + (fun (lhs, rhs) -> + remove_level_info + (hvbox false true [ + hbox false true [ + mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; + break; k rhs ])) + patterns + in + let patterns'' = + let rec aux_patterns = function + | [] -> assert false + | [ last ] -> + [ break; + hbox false false [ + builtin_symbol "|"; + last; builtin_symbol "]" ] ] + | hd :: tl -> + [ break; hbox false false [ builtin_symbol "|"; hd ] ] + @ aux_patterns tl + in + match patterns' with + | [] -> + [ hbox false false [ builtin_symbol "["; builtin_symbol "]" ] ] + | [ one ] -> + [ hbox false false [ + builtin_symbol "["; one; builtin_symbol "]" ] ] + | hd :: tl -> + hbox false false [ builtin_symbol "["; hd ] + :: aux_patterns tl + in + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false false [ + hvbox false false (outty_box @ [ match_box ]); break; + hbox false false [ hvbox false false patterns'' ] ]) + | Ast.Cast (bo, ty) -> + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false true [ + builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty; + builtin_symbol ")"]) + | Ast.LetIn (var, s, t) -> + add_level_info Ast.let_in_prec Ast.let_in_assoc + (hvbox false true [ + hvbox false true [ + keyword "let"; + hvbox false true [ + aux_var var; builtin_symbol "\\def"; break; k s ]; + break; keyword "in" ]; + k t ]) + | Ast.LetRec (rec_kind, funs, where) -> + let rec_op = + match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" + in + let mk_fun (var, body, _) = aux_var var, k body in + let mk_funs = List.map mk_fun in + let fst_fun, tl_funs = + match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false + in + let fst_row = + let (name, body) = fst_fun in + hvbox false true [ + keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; + body ] + in + let tl_rows = + List.map + (fun (name, body) -> + [ break; + hvbox false true [ + keyword "and"; name; builtin_symbol "\\def"; break; body ] ]) + tl_funs + in + add_level_info Ast.let_in_prec Ast.let_in_assoc + ((hvbox false false + (fst_row :: List.flatten tl_rows + @ [ break; keyword "in"; break; k where ]))) + | Ast.Implicit -> builtin_symbol "?" + | Ast.Meta (n, l) -> + let local_context l = + CicNotationUtil.dress (builtin_symbol ";") + (List.map (function None -> builtin_symbol "_" | Some t -> k t) l) + in + hbox false false + ([ builtin_symbol "?"; number (string_of_int n) ] + @ (if l <> [] then local_context l else [])) + | Ast.Sort sort -> aux_sort sort + | Ast.Num _ + | Ast.Symbol _ + | Ast.Ident (_, None) | Ast.Ident (_, Some []) + | Ast.Uri (_, None) | Ast.Uri (_, Some []) + | 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_ty = function | None -> builtin_symbol "?" | Some ty -> k ty + and aux_var = function + | name, Some ty -> + hvbox false true [ + builtin_symbol "("; name; builtin_symbol ":"; break; k ty; + builtin_symbol ")" ] + | name, None -> name and special_k = function | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) - | _ -> assert false + | t -> + prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t); + assert false in aux t @@ -217,7 +354,8 @@ let ast_of_acic0 term_info acic k = | Cic.ACoFix (id, no, funs) -> let defs = List.map - (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + (fun (_, n, ty, bo) -> + ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) funs in let name = @@ -273,9 +411,8 @@ let instantiate21 env (* precedence associativity *) l1 = assert (CicNotationEnv.well_typed expected_ty value); [ CicNotationEnv.term_of_value value ] | Ast.Magic m -> subst_magic env m - | Ast.Literal (`Keyword k) as t -> - [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ] - | Ast.Literal _ as t -> [ t ] + | Ast.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ] + | Ast.Literal _ as t -> [ (*reset_href*) t ] | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] and subst_magic env = function @@ -295,10 +432,11 @@ let instantiate21 env (* precedence associativity *) l1 = | [] -> List.rev acc | value_set :: [] -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] + instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl + instantiate_list + (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl in instantiate_list [] values | Ast.Opt p -> @@ -345,18 +483,15 @@ let rec pp_ast1 term = match term with | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) | _ -> - begin - match (get_compiled21 ()) term with - | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> - let precedence, associativity, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false - in - Ast.AttributedTerm (`Level (precedence, associativity), - (instantiate21 (ast_env_of_env env) l1)) - end + (match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> + let prec, assoc, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1)) let instantiate32 term_info env symbol args = let rec instantiate_arg = function @@ -376,8 +511,10 @@ let instantiate32 term_info env symbol args = in add_lambda t (n - count_lambda t) in - let args' = List.map instantiate_arg args in - Ast.Appl (Ast.Symbol (symbol, 0) :: args') + let head = Ast.Symbol (symbol, 0) in + match args with + | [] -> head + | _ -> Ast.Appl (head :: List.map instantiate_arg args) let rec ast_of_acic1 term_info annterm = match (get_compiled32 ()) annterm with @@ -407,7 +544,9 @@ let ast_of_acic id_to_sort annterm = let ast = ast_of_acic1 term_info annterm in ast, term_info.uri -let pp_ast term = pp_ast1 term +let pp_ast term = +(* prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *) + pp_ast1 term let fresh_id = let counter = ref ~-1 in diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml index b454cf24d..37579c827 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.ml +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -43,14 +43,3 @@ let get_tag term0 = let tag = Hashtbl.hash term_mask in tag, !subterms -let compatible t1 t2 = - match t1, t2 with - | Variable _, Variable _ -> true - | Variable _, _ - | _, Variable _ - | Magic _, _ - | _, Magic _ -> false - | Layout _, _ - | _, Layout _ -> assert false - | _ -> true - diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index f2c2539cd..44b83fd1d 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -336,7 +336,7 @@ let ungroup = in aux [] -let dress sauce = +let dress ~sep:sauce = let rec aux = function | [] -> [] @@ -345,6 +345,15 @@ let dress sauce = in aux +let dressn ~sep:sauces = + let rec aux = + function + | [] -> [] + | [hd] -> [hd] + | hd :: tl -> hd :: sauces @ aux tl + in + aux + let find_appl_pattern_uris ap = let rec aux acc = function diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index d11f1917e..a7dbc2aca 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -49,7 +49,8 @@ val ncombine: 'a list list -> 'a list list val string_of_literal: CicNotationPt.literal -> string -val dress: 'a -> 'a list -> 'a list +val dress: sep:'a -> 'a list -> 'a list +val dressn: sep:'a list -> 'a list -> 'a list val boxify: CicNotationPt.term list -> CicNotationPt.term val group: CicNotationPt.term list -> CicNotationPt.term diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index 803d624c0..ff6380151 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -114,7 +114,11 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y). render cic:/Coq/Arith/Mult/mult_plus_distr_r.con. notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d. -interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)). +interpretation "megacoso" 'megacoso x y z w = + (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) + cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) + (cic:/Coq/Init/Peano/plus.con x y) + (cic:/Coq/Init/Peano/plus.con z w)). render cic:/Coq/Arith/Plus/plus_comm.con. # full samples diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index 11fef69a1..c2e44a5df 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -137,9 +137,9 @@ type ('term,'obj) command = | Alias of loc * alias_spec (** parameters, name, type, fields *) | Obj of loc * 'obj - | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int * - CicNotationPt.term - (* level 1 pattern, associativity, precedence, level 2 pattern *) + | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * + int * CicNotationPt.term + (* direction, l1 pattern, associativity, precedence, l2 pattern *) | Interpretation of loc * string * (string * CicNotationPt.argument_pattern list) * CicNotationPt.cic_appl_pattern diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index 6af1efd71..c15b6fe71 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -261,6 +261,11 @@ let pp_associativity = function let pp_precedence i = sprintf "with precedence %d" i +let pp_dir_opt = function + | None -> "" + | Some `LeftToRight -> "> " + | Some `RightToLeft -> "< " + let pp_command = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" @@ -277,8 +282,9 @@ let pp_command = function dsc symbol (String.concat " " (List.map pp_argument_pattern arg_patterns)) (pp_cic_appl_pattern cic_appl_pattern) - | Notation (_, l1_pattern, assoc, prec, l2_pattern) -> - sprintf "notation \"%s\" %s %s for %s" + | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> + sprintf "notation %s\"%s\" %s %s for %s" + (pp_dir_opt dir_opt) (pp_l1_pattern l1_pattern) (pp_associativity assoc) (pp_precedence prec) diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 056e595e7..fae3df93d 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -364,7 +364,7 @@ EXTEND [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ - [ s = QSTRING; + [ dir = OPT direction; s = QSTRING; assoc = OPT associativity; prec = OPT precedence; IDENT "for"; p2 = @@ -385,9 +385,11 @@ EXTEND | None -> default_precedence | Some prec -> prec in - (add_raw_attribute ~text:s - (CicNotationParser.parse_level1_pattern (Stream.of_string s)), - assoc, prec, p2) + let p1 = + add_raw_attribute ~text:s + (CicNotationParser.parse_level1_pattern (Stream.of_string s)) + in + (dir, p1, assoc, prec, p2) ] ]; level3_term: [ @@ -402,7 +404,7 @@ EXTEND ] ]; interpretation: [ - [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> + [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> (s, args, t) ] ]; @@ -458,8 +460,8 @@ EXTEND | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in GrafiteAst.Default (loc,what,uris) - | IDENT "notation"; (l1, assoc, prec, l2) = notation -> - GrafiteAst.Notation (loc, l1, assoc, prec, l2) + | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation -> + GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2) | IDENT "interpretation"; id = QSTRING; (symbol, args, l3) = interpretation -> GrafiteAst.Interpretation (loc, id, (symbol, args), l3) diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_notation/mpresentation.ml similarity index 97% rename from helm/ocaml/cic_transformations/mpresentation.ml rename to helm/ocaml/cic_notation/mpresentation.ml index 6943d9caf..69d4fd9a0 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_notation/mpresentation.ml @@ -156,7 +156,11 @@ let print_mpres obj_printer mpres = X.xml_nempty ~prefix "maction" attr [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >] | Mobject (attr, obj) -> - X.xml_nempty ~prefix "semantics" attr (obj_printer obj) + let box_stream = obj_printer obj in + X.xml_nempty ~prefix "semantics" attr + [< X.xml_nempty ~prefix "annotation-xml" [None, "encoding", "BoxML"] + box_stream >] + and aux_mrow = let module X = Xml in function diff --git a/helm/ocaml/cic_transformations/mpresentation.mli b/helm/ocaml/cic_notation/mpresentation.mli similarity index 100% rename from helm/ocaml/cic_transformations/mpresentation.mli rename to helm/ocaml/cic_notation/mpresentation.mli diff --git a/helm/ocaml/cic_transformations/boxPp.mli b/helm/ocaml/cic_notation/renderingAttrs.ml similarity index 62% rename from helm/ocaml/cic_transformations/boxPp.mli rename to helm/ocaml/cic_notation/renderingAttrs.ml index de984d26e..fd2ddd24a 100644 --- a/helm/ocaml/cic_transformations/boxPp.mli +++ b/helm/ocaml/cic_notation/renderingAttrs.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,7 +23,22 @@ * http://helm.cs.unibo.it/ *) -val to_string : ('expr -> string) -> 'expr Box.box -> string list +type xml_attribute = string option * string * string +type markup = [ `MathML | `BoxML ] -val pp_term : ?ids_to_uris: (Cic.id, string) Hashtbl.t -> CicAst.term -> string +let keyword_attributes = function + | `MathML -> [ None, "mathcolor", "blue" ] + | `BoxML -> [ None, "color", "blue" ] + +let builtin_symbol_attributes = function + | `MathML -> [ None, "mathcolor", "blue" ] + | `BoxML -> [ None, "color", "blue" ] + +let object_keyword_attributes = function + | `MathML -> [ None, "mathcolor", "red" ] + | `BoxML -> [ None, "color", "red" ] + +let symbol_attributes _ = [] +let ident_attributes _ = [] +let number_attributes _ = [] diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_notation/renderingAttrs.mli similarity index 54% rename from helm/ocaml/cic_transformations/tacticAstPp.mli rename to helm/ocaml/cic_notation/renderingAttrs.mli index fb9b45084..a9fc0badb 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.mli +++ b/helm/ocaml/cic_notation/renderingAttrs.mli @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,16 +23,27 @@ * http://helm.cs.unibo.it/ *) -val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string -val pp_obj: TacticAst.obj -> string -val pp_command: (CicAst.term,TacticAst.obj) TacticAst.command -> string -val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string -val pp_comment: (CicAst.term,TacticAst.obj,string) TacticAst.comment -> string -val pp_executable: (CicAst.term,TacticAst.obj,string) TacticAst.code -> string -val pp_statement: (CicAst.term,TacticAst.obj,string) TacticAst.statement -> string -val pp_macro_ast: CicAst.term TacticAst.macro -> string -val pp_macro_cic: Cic.term TacticAst.macro -> string -val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string -val pp_alias: TacticAst.alias_spec -> string - -val pp_cic_command: (Cic.term,Cic.obj) TacticAst.command -> string +(** XML attributes for MathML/BoxML rendering of terms and objects + * markup defaults to MathML in all functions below *) + +type xml_attribute = string option * string * string +type markup = [ `MathML | `BoxML ] + +val keyword_attributes: (* let, match, in, ... *) + markup -> xml_attribute list + +val builtin_symbol_attributes: (* \\Pi, \\to, ... *) + markup -> xml_attribute list + +val symbol_attributes: (* +, *, ... *) + markup -> xml_attribute list + +val ident_attributes: (* nat, plus, ... *) + markup -> xml_attribute list + +val number_attributes: (* 1, 2, ... *) + markup -> xml_attribute list + +val object_keyword_attributes: (* Body, Definition, ... *) + markup -> xml_attribute list + diff --git a/helm/ocaml/cic_notation/test_parser.conf.xml b/helm/ocaml/cic_notation/test_parser.conf.xml index 9864ac1dc..05a838fea 100644 --- a/helm/ocaml/cic_notation/test_parser.conf.xml +++ b/helm/ocaml/cic_notation/test_parser.conf.xml @@ -4,6 +4,10 @@ cic:/ file:///projects/helm/library/coq_contribs/ + + cic:/matita/ + file:///home/zacchiro/helm/matita/.matita/xml/matita/ +
../../matita/core_notation.ma diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 960af9d5f..dc76884ac 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -47,12 +47,6 @@ let extract_loc = | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc -let errquit ignore_exn = - if not ignore_exn then begin - prerr_endline "Error, exiting!"; - exit 2 - end - let pp_associativity = function | Gramext.LeftA -> "left" | Gramext.RightA -> "right" @@ -60,18 +54,28 @@ let pp_associativity = function let pp_precedence = string_of_int -let process_stream ?(ignore_exn = false) istream = +(* let last_rule_id = ref None *) + +let process_stream istream = let char_count = ref 0 in let module P = CicNotationPt in let module G = GrafiteAst in try - while Stream.peek istream <> None do + while true do try let statement = GrafiteParser.parse_statement istream in let floc = extract_loc statement in let (_, y) = P.loc_of_floc floc in char_count := y + !char_count; match statement with +(* | G.Executable (_, G.Macro (_, G.Check (_, + P.AttributedTerm (_, P.Ident _)))) -> + prerr_endline "mega hack"; + (match !last_rule_id with + | None -> () + | Some id -> + prerr_endline "removing last notation rule ..."; + CicNotationParser.delete id) *) | G.Executable (_, G.Macro (_, G.Check (_, t))) -> prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); let t' = CicNotationRew.pp_ast t in @@ -80,7 +84,7 @@ let process_stream ?(ignore_exn = false) istream = let tbl = Hashtbl.create 0 in dump_xml t' tbl "out.xml" | G.Executable (_, G.Command (_, - G.Notation (_, l1, associativity, precedence, l2))) -> + G.Notation (_, dir, l1, associativity, precedence, l2))) -> prerr_endline "notation"; prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); @@ -90,10 +94,14 @@ let process_stream ?(ignore_exn = false) istream = if keywords <> [] then prerr_endline (sprintf "keywords: %s" (String.concat " " keywords)); - ignore (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); - ignore (CicNotationRew.add_pretty_printer - ?precedence ?associativity l2 l1) + if dir <> Some `RightToLeft then + ignore + (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); +(* last_rule_id := Some rule_id; *) + if dir <> Some `LeftToRight then + ignore (CicNotationRew.add_pretty_printer + ?precedence ?associativity l2 l1) | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> prerr_endline "interpretation"; prerr_endline (sprintf "dsc: %s" id); @@ -115,9 +123,10 @@ let process_stream ?(ignore_exn = false) istream = let t, id_to_uri = CicNotationRew.ast_of_acic id_to_sort annterm in - prerr_endline "AST"; + prerr_endline "Raw AST"; prerr_endline (CicNotationPp.pp_term t); let t' = CicNotationRew.pp_ast t in + prerr_endline "Rendered AST"; prerr_endline (CicNotationPp.pp_term t'); dump_xml t' id_to_uri "out.xml" | _ -> prerr_endline "Unsupported statement" @@ -131,15 +140,12 @@ let process_stream ?(ignore_exn = false) istream = eprintf "%s%s%s\n" before error after; prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) prerr_endline (sprintf "Parse error at character %d-%d: %s" - (!char_count + x) (!char_count + y) msg); - errquit ignore_exn + (!char_count + x) (!char_count + y) msg) | exn -> prerr_endline - (sprintf "Uncaught exception: %s" (Printexc.to_string exn)); - errquit ignore_exn + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) done - with End_of_file -> - () + with End_of_file -> () let _ = let arg_spec = [ ] in @@ -149,5 +155,5 @@ let _ = CicNotation.load_notation (Helm_registry.get "notation.core_file"); print_endline "done."; flush stdout; - process_stream ~ignore_exn:false (Stream.of_channel stdin) + process_stream (Stream.of_channel stdin) diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile index 33f1b3f07..80d1d351a 100644 --- a/helm/ocaml/cic_omdoc/Makefile +++ b/helm/ocaml/cic_omdoc/Makefile @@ -2,8 +2,15 @@ PACKAGE = cic_omdoc REQUIRES = helm-cic_proof_checking PREDICATES = -INTERFACE_FILES = eta_fixing.mli doubleTypeInference.mli cic2acic.mli \ - content.mli contentPp.mli cic2content.mli content2cic.mli +INTERFACE_FILES = \ + eta_fixing.mli \ + doubleTypeInference.mli \ + cic2acic.mli \ + content.mli \ + contentPp.mli \ + cic2content.mli \ + content2cic.mli \ + $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = \ diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 2aff8f942..2ab1d50be 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,50 +1,16 @@ -cicAst.cmo: cicAst.cmi -cicAst.cmx: cicAst.cmi -contentTable.cmi: cicAst.cmi -acic2Ast.cmi: cicAst.cmi -cicAstPp.cmi: cicAst.cmi -ast2pres.cmi: mpresentation.cmi cicAst.cmi box.cmi -content2pres.cmi: mpresentation.cmi box.cmi -sequent2pres.cmi: mpresentation.cmi box.cmi -tacticAstPp.cmi: tacticAst.cmo cicAst.cmi -boxPp.cmi: cicAst.cmi box.cmi -tacticAst.cmo: cicAst.cmi -tacticAst.cmx: cicAst.cmx -cicAst.cmo: cicAst.cmi -cicAst.cmx: cicAst.cmi -contentTable.cmo: cicAst.cmi contentTable.cmi -contentTable.cmx: cicAst.cmx contentTable.cmi cic2Xml.cmo: cic2Xml.cmi cic2Xml.cmx: cic2Xml.cmi -mpresentation.cmo: mpresentation.cmi -mpresentation.cmx: mpresentation.cmi -box.cmo: box.cmi -box.cmx: box.cmi -acic2Ast.cmo: cicAst.cmi acic2Ast.cmi -acic2Ast.cmx: cicAst.cmx acic2Ast.cmi -cicAstPp.cmo: cicAst.cmi cicAstPp.cmi -cicAstPp.cmx: cicAst.cmx cicAstPp.cmi -ast2pres.cmo: mpresentation.cmi cicAst.cmi box.cmi ast2pres.cmi -ast2pres.cmx: mpresentation.cmx cicAst.cmx box.cmx ast2pres.cmi -content2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \ - content2pres.cmi -content2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \ - content2pres.cmi -sequent2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \ - sequent2pres.cmi -sequent2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \ - sequent2pres.cmi +content2pres.cmo: content2pres.cmi +content2pres.cmx: content2pres.cmi +sequent2pres.cmo: sequent2pres.cmi +sequent2pres.cmx: sequent2pres.cmi domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi sequentPp.cmo: cic2Xml.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx sequentPp.cmi -applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \ - domMisc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi -applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \ - domMisc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi -tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi -tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi -boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi -boxPp.cmx: cicAstPp.cmx box.cmx ast2pres.cmx boxPp.cmi +applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi domMisc.cmi \ + content2pres.cmi applyTransformation.cmi +applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx domMisc.cmx \ + content2pres.cmx applyTransformation.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 0dda80d4e..3669f5d7e 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -1,24 +1,26 @@ PACKAGE = cic_transformations -REQUIRES = \ - gdome2 \ - helm-xml helm-cic_proof_checking helm-cic_omdoc helm-registry \ - helm-utf8_macros +REQUIRES = \ + gdome2 \ + helm-xml \ + helm-cic_proof_checking \ + helm-cic_omdoc \ + helm-registry \ + helm-utf8_macros \ + helm-cic_notation \ + $(NULL) PREDICATES = # modules which have both a .ml and a .mli -INTERFACE_FILES = \ - cicAst.ml \ - contentTable.mli \ - cic2Xml.mli \ - mpresentation.mli box.mli \ - acic2Ast.mli \ - cicAstPp.mli ast2pres.mli content2pres.mli \ - sequent2pres.mli \ - domMisc.mli xml2Gdome.mli sequentPp.mli \ - applyTransformation.mli \ - tacticAstPp.mli boxPp.mli +INTERFACE_FILES = \ + cic2Xml.mli \ + content2pres.mli \ + sequent2pres.mli \ + domMisc.mli \ + xml2Gdome.mli \ + sequentPp.mli \ + applyTransformation.mli \ + $(NULL) IMPLEMENTATION_FILES = \ - tacticAst.ml \ $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml deleted file mode 100644 index 76be244ad..000000000 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ /dev/null @@ -1,285 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -module Ast = CicAst - -let symbol_table = Hashtbl.create 1024 - -let get_types uri = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - | Cic.InductiveDefinition (l,_,_,_) -> l - | _ -> assert false - -let name_of_inductive_type uri i = - let types = get_types uri in - let (name, _, _, _) = try List.nth types i with Not_found -> assert false in - name - - (* returns pairs *) -let constructors_of_inductive_type uri i = - let types = get_types uri in - let (_, _, _, constructors) = - try List.nth types i with Not_found -> assert false - in - constructors - - (* returns name only *) -let constructor_of_inductive_type uri i j = - (try - fst (List.nth (constructors_of_inductive_type uri i) (j-1)) - with Not_found -> assert false) - -let ast_of_acic ids_to_inner_sorts acic = - let ids_to_uris = Hashtbl.create 503 in - let register_uri id uri = Hashtbl.add ids_to_uris id uri in - let sort_of_id id = - try - Hashtbl.find ids_to_inner_sorts id - with Not_found -> assert false - in - let idref id t = Ast.AttributedTerm (`IdRef id, t) in - let rec aux = - function - | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) - | Cic.AVar (id,uri,subst) -> - register_uri id (UriManager.string_of_uri uri); - idref id - (Ast.Ident (UriManager.name_of_uri uri, astsubst_of_cicsubst subst)) - | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l)) - | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) - | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) - | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *) - | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) - | Cic.AImplicit _ -> assert false - | Cic.AProd (id,n,s,t) -> - let binder_kind = - match sort_of_id id with - | `Set | `Type | `Meta -> `Pi - | `Prop | `CProp -> `Forall - in - idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t)) - | Cic.ACast (id,v,t) -> idref id (Ast.Cast (aux v, aux t)) - | Cic.ALambda (id,n,s,t) -> - idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t)) - | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t)) - | Cic.AAppl (aid,Cic.AConst (sid,uri,subst)::tl) -> - let uri_str = UriManager.string_of_uri uri in - register_uri sid uri_str; - (try - let f = Hashtbl.find symbol_table uri_str in - f aid sid tl aux - with Not_found -> - idref aid - (Ast.Appl (idref sid - (Ast.Ident (UriManager.name_of_uri uri, - astsubst_of_cicsubst subst)) :: (List.map aux tl)))) - | Cic.AAppl (aid,Cic.AMutInd (sid,uri,i,subst)::tl) -> - let name = name_of_inductive_type uri i in - let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in - register_uri sid puri_str; - (try - (let f = Hashtbl.find symbol_table puri_str in - f aid sid tl aux) - with Not_found -> - idref aid - (Ast.Appl (idref sid - (Ast.Ident (name, - astsubst_of_cicsubst subst)) :: (List.map aux tl)))) - | Cic.AAppl (id,li) -> idref id (Ast.Appl (List.map aux li)) - | Cic.AConst (id,uri,subst) -> - let uri_str = UriManager.string_of_uri uri in - register_uri id uri_str; - (try - let f = Hashtbl.find symbol_table uri_str in - f "dummy" id [] aux - with Not_found -> - idref id - (Ast.Ident - (UriManager.name_of_uri uri, astsubst_of_cicsubst subst))) - | Cic.AMutInd (id,uri,i,subst) -> - let name = name_of_inductive_type uri i in - let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in - register_uri id puri_str; - (try - let f = Hashtbl.find symbol_table puri_str in - f "dummy" id [] aux - with Not_found -> - idref id (Ast.Ident (name, astsubst_of_cicsubst subst))) - | Cic.AMutConstruct (id,uri,i,j,subst) -> - let name = constructor_of_inductive_type uri i j in - let uri_str = UriManager.string_of_uri uri in - let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in - register_uri id puri_str; - (try - let f = Hashtbl.find symbol_table puri_str in - f "dummy" id [] aux - with Not_found -> - idref id (Ast.Ident (name, astsubst_of_cicsubst subst))) - | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> - let name = name_of_inductive_type uri typeno in - let constructors = constructors_of_inductive_type uri typeno in - let rec eat_branch ty pat = - match (ty, pat) with - | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> - let (cv, rhs) = eat_branch t t' in - (name, Some (aux s)) :: cv, rhs - | _, _ -> [], aux pat - in - let patterns = - List.map2 - (fun (name, ty) pat -> - let (capture_variables, rhs) = eat_branch ty pat in - ((name, capture_variables), rhs)) - constructors patterns - in - idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns)) - | Cic.AFix (id, no, funs) -> - let defs = - List.map - (fun (_, n, decr_idx, ty, bo) -> - ((Cic.Name n, Some (aux ty)), aux bo, decr_idx)) - funs - in - let name = - try - (match List.nth defs no with - | (Cic.Name n, _), _, _ -> n - | _ -> assert false) - with Not_found -> assert false - in - idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) - | Cic.ACoFix (id, no, funs) -> - let defs = - List.map - (fun (_, n, ty, bo) -> ((Cic.Name n, Some (aux ty)), aux bo, 0)) - funs - in - let name = - try - (match List.nth defs no with - | (Cic.Name n, _), _, _ -> n - | _ -> assert false) - with Not_found -> assert false - in - idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None))) - - and astsubst_of_cicsubst subst = - Some - (List.map (fun (uri, annterm) -> - (UriManager.name_of_uri uri, aux annterm)) - subst) - - and astcontext_of_ciccontext context = - List.map - (function - | None -> None - | Some annterm -> Some (aux annterm)) - context - - in - aux acic, ids_to_uris - -let _ = (** fill symbol_table *) - let add_symbol name uri = - Hashtbl.add symbol_table uri - (fun aid sid args acic2ast -> - Ast.AttributedTerm (`IdRef aid, - Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) :: - List.map acic2ast args))) - in - (* eq *) - Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI - (fun aid sid args acic2ast -> - Ast.AttributedTerm (`IdRef aid, - Ast.Appl ( - Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) :: - List.map acic2ast (List.tl args)))); - (* exists *) - Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI - (fun aid sid args acic2ast -> - match (List.tl args) with - [Cic.ALambda (_,Cic.Name n,s,t)] -> - Ast.AttributedTerm (`IdRef aid, - Ast.Binder (`Exists, (Cic.Name n, Some (acic2ast s)), acic2ast t)) - | _ -> raise Not_found); - add_symbol "and" HelmLibraryObjects.Logic.and_XURI; - add_symbol "or" HelmLibraryObjects.Logic.or_XURI; - add_symbol "iff" HelmLibraryObjects.Logic.iff_SURI; - add_symbol "not" HelmLibraryObjects.Logic.not_SURI; - add_symbol "inv" HelmLibraryObjects.Reals.rinv_SURI; - add_symbol "opp" HelmLibraryObjects.Reals.ropp_SURI; - add_symbol "leq" HelmLibraryObjects.Peano.le_XURI; - add_symbol "leq" HelmLibraryObjects.Reals.rle_SURI; - add_symbol "lt" HelmLibraryObjects.Peano.lt_SURI; - add_symbol "lt" HelmLibraryObjects.Reals.rlt_SURI; - add_symbol "geq" HelmLibraryObjects.Peano.ge_SURI; - add_symbol "geq" HelmLibraryObjects.Reals.rge_SURI; - add_symbol "gt" HelmLibraryObjects.Peano.gt_SURI; - add_symbol "gt" HelmLibraryObjects.Reals.rgt_SURI; - add_symbol "plus" HelmLibraryObjects.Peano.plus_SURI; - add_symbol "plus" HelmLibraryObjects.BinInt.zplus_SURI; - add_symbol "times" HelmLibraryObjects.Peano.mult_SURI; - add_symbol "times" HelmLibraryObjects.Reals.rmult_SURI; - add_symbol "minus" HelmLibraryObjects.Peano.minus_SURI; - add_symbol "minus" HelmLibraryObjects.Reals.rminus_SURI; - add_symbol "div" HelmLibraryObjects.Reals.rdiv_SURI; - Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI - (fun aid sid args acic2ast -> - Ast.AttributedTerm (`IdRef sid, Ast.Num ("0", 0))); - Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI - (fun aid sid args acic2ast -> - Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", 0))); - (* plus *) - Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI - (fun aid sid args acic2ast -> - let appl () = - Ast.AttributedTerm (`IdRef aid, - Ast.Appl ( - Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) :: - List.map acic2ast args)) - in - let rec aux acc = function - | [ Cic.AConst (nid, uri, []); n] when - UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> - (match n with - | Cic.AConst (_, uri, []) when - UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> - Ast.AttributedTerm (`IdRef aid, - Ast.Num (string_of_int (acc + 2), 0)) - | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when - UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI -> - aux (acc + 1) args - | _ -> appl ()) - | _ -> appl () - in - aux 0 args) - diff --git a/helm/ocaml/cic_transformations/acic2Ast.mli b/helm/ocaml/cic_transformations/acic2Ast.mli deleted file mode 100644 index 411057cff..000000000 --- a/helm/ocaml/cic_transformations/acic2Ast.mli +++ /dev/null @@ -1,37 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val ast_of_acic : - (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> (* id -> sort *) -(* - (Cic.id, string) Hashtbl.t -> (* id -> uri *) - (string, - Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) -> - CicAst.term) - Hashtbl.t -> -*) - Cic.annterm -> - CicAst.term * (Cic.id, string) Hashtbl.t (* ast, id -> uri *) - diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 560f6a0d1..b6aa36987 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -34,16 +34,18 @@ (***************************************************************************) let mpres_document pres_box = - let obj2xml obj = Mpresentation.print_mpres (fun _ -> assert false) obj in - Ast2pres.add_xml_declaration (Box.box2xml ~obj2xml pres_box) + Xml.add_xml_declaration (CicNotationPres.print_box pres_box) let mml_of_cic_sequent metasenv sequent = let asequent,ids_to_terms, - ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses = - Cic2acic.asequent_of_sequent metasenv sequent in + ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses + = + Cic2acic.asequent_of_sequent metasenv sequent + in let content_sequent = Cic2content.map_sequent asequent in let pres_sequent = - (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in + (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) + in let xmlpres = mpres_document pres_sequent in Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, (asequent, diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml deleted file mode 100644 index 62a63c775..000000000 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ /dev/null @@ -1,700 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 28/6/2003 *) -(* *) -(**************************************************************************) - -module A = CicAst;; -module P = Mpresentation;; - -let symbol_table = Hashtbl.create 503;; -let symbol_table_charcount = Hashtbl.create 503;; - -let maxsize = 25;; - -let rec countvar current_size = function - (Cic.Anonymous, None) -> current_size + 1 (* underscore *) - | (Cic.Anonymous, Some ty) -> countterm current_size ty - | (Cic.Name s, None) -> current_size + String.length s - | (Cic.Name s, Some ty) -> current_size + countterm current_size ty - -and countterm current_size t = - if current_size > maxsize then current_size - else match t with - A.AttributedTerm (_,t) -> countterm current_size t - | A.Appl l -> - List.fold_left countterm current_size l - | A.Binder (_,var,body) -> - let varsize = countvar current_size var in - countterm (varsize + 1) body (* binder *) - | A.Case (arg, _, ty, pl) -> - let size1 = countterm (current_size+10) arg in (* match with *) - let size2 = - match ty with - None -> size1 - | Some ty -> countterm size1 ty in - List.fold_left - (fun c ((constr,vars),action) -> - let size3 = - List.fold_left countvar (c+String.length constr) vars in - countterm size3 action) size2 pl - | A.Cast (bo,ty) -> - countterm (countterm (current_size + 3) bo) ty - | A.LetIn (var,s,t) -> - let size1 = countvar current_size var in - let size2 = countterm size1 s in - countterm size2 t - | A.LetRec (_,l,t) -> - let size1 = - List.fold_left - (fun c (var,s,_) -> - let size1 = countvar c var in - countterm size1 s) current_size l in - countterm size1 t - | A.Ident (s,None) - | A.Uri (s, None) -> current_size + (String.length s) - | A.Ident (s,Some l) - | A.Uri (s,Some l) -> - List.fold_left - (fun c (v,t) -> countterm (c + (String.length v)) t) - (current_size + (String.length s)) l - | A.Implicit -> current_size + 1 (* underscore *) - | A.Meta (_,l) -> - List.fold_left - (fun c t -> - match t with - None -> c + 1 (* underscore *) - | Some t -> countterm c t) - (current_size + 1) l (* num *) - | A.Num (s, _) -> current_size + String.length s - | A.Sort _ -> current_size + 4 (* sort name *) - | A.Symbol (s,_) -> current_size + String.length s - - | A.UserInput -> current_size -;; - -let is_big t = - ((countterm 0 t) > maxsize) -;; - -let rec make_attributes l1 = - function - [] -> [] - | None::tl -> make_attributes (List.tl l1) tl - | (Some s)::tl -> - let p,n = List.hd l1 in - (p,n,s)::(make_attributes (List.tl l1) tl) -;; - -let map_tex unicode texcmd = - let default_map_tex = Printf.sprintf "\\%s " in - if unicode then - try - Utf8Macro.expand texcmd - with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd - else - default_map_tex texcmd - -let resolve_binder unicode = function - | `Lambda -> map_tex unicode "lambda" - | `Pi -> map_tex unicode "Pi" - | `Forall -> map_tex unicode "forall" - | `Exists -> map_tex unicode "exists" -;; - -let rec make_args f ~tail = function - | [] -> assert false - | [arg] -> [f ~tail arg] - | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl) - -let append_tail ~tail box = - match tail with - | [] -> box - | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail)) - -let rec find_symbol idref = function - | A.AttributedTerm (`Loc _, t) -> find_symbol None t - | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t - | A.Symbol (name, _) -> `Symbol (name, idref) - | _ -> `None - -let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) - (t, ids_to_uris) -= - let lookup_uri = function - | None -> None - | Some id -> - (try - Some (Hashtbl.find ids_to_uris id) - with Not_found -> None) - in - let make_std_attributes xref = - let uri = lookup_uri xref in - make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri] - in - let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t = - if is_big t then - bigast2box ~priority ~assoc ?xref ~tail t - else - let attrs = make_std_attributes xref in - append_tail ~tail (Box.Object (attrs, t)) - and - bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t = - match t with - | A.AttributedTerm (`Loc _, t) -> bigast2box ?xref ~tail t - | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t - | A.Appl [] -> assert false - | A.Appl ((hd::tl) as l) -> - let aattr = make_attributes [Some "helm","xref"] [xref] in - (match find_symbol None hd with - | `Symbol (name, sxref) -> - let sattr = make_std_attributes sxref in - (try - (let f = Hashtbl.find symbol_table_charcount name in - f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr) - with Not_found -> - Box.H - (make_attributes [Some "helm","xref"] [xref], - [Box.Text([],"("); - Box.V([], - make_args (fun ~tail t -> ast2box ~tail t) - ~tail:(")" :: tail) l); - Box.Text([],")")])) - | `None -> - Box.H - (make_attributes [Some "helm","xref"] [xref], - [Box.Text([],"("); - Box.V([], - make_args - (fun ~tail t -> ast2box ~tail t) - ~tail:(")" :: tail) l)] - )) - | A.Binder (`Forall, (Cic.Anonymous, typ), body) - | A.Binder (`Pi, (Cic.Anonymous, typ), body) -> - Box.V(make_attributes [Some "helm","xref"] [xref], - [(match typ with - | None -> Box.Text([], "?") - | Some typ -> ast2box ~tail:[] typ); - Box.H([], - [Box.skip; - Box.Text([], map_tex unicode "to"); - ast2box ~tail body])]) - | A.Binder(kind, var, body) -> - Box.V(make_attributes [Some "helm","xref"] [xref], - [Box.H([], - [Box.Text ([None,"color","blue"], resolve_binder unicode kind); - make_var ~tail:("." :: tail) var]); - Box.indent (ast2box ~tail body)]) - | A.Case(arg, _, ty, pl) -> - let make_rule ~tail sep ((constr,vars),rhs) = - if (is_big rhs) then - Box.V([],[Box.H([],[Box.Text([],sep); - Box.smallskip; - make_pattern constr vars; - Box.smallskip; - Box.Text([],map_tex unicode "Rightarrow")]); - Box.indent (bigast2box ~tail rhs)]) - else - Box.H([],[Box.Text([],sep); - Box.smallskip; - make_pattern constr vars; - Box.smallskip; - Box.Text([],map_tex unicode "Rightarrow"); - Box.smallskip; - append_tail ~tail (Box.Object([],rhs))]) in - let plbox = - match pl with - | [] -> append_tail ~tail (Box.Text([],"[]")) - | [r] -> (make_rule ~tail:("]" :: tail) "[" r) - | r::tl -> - Box.V([], - (make_rule ~tail:[] "[" r) :: - (make_args - (fun ~tail pat -> make_rule ~tail "|" pat) - ~tail:("]" :: tail) - tl)) - in - let ty_box = - match ty with - | Some ty -> - [ Box.H([],[Box.Text([],"["); - ast2box ~tail:[] ty; - Box.Text([],"]")]) ] - | None -> [] - in - if is_big arg then - Box.V(make_attributes [Some "helm","xref"] [xref], - ty_box @ - [Box.Text([],"match"); - Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg])); - Box.Text([],"with"); - Box.indent plbox]) - else - Box.V(make_attributes [Some "helm","xref"] [xref], - ty_box @ - [Box.H(make_attributes [Some "helm","xref"] [xref], - [Box.Text([],"match"); - Box.smallskip; - ast2box ~tail:[] arg; - Box.smallskip; - Box.Text([],"with")]); - Box.indent plbox]) - | A.Cast (bo,ty) -> - Box.V(make_attributes [Some "helm","xref"] [xref], - [Box.H([],[Box.Text([],"("); ast2box ~tail:[] bo]); - Box.H([],[Box.Text([],":"); ast2box ~tail ty;Box.Text([],")")])]) - | A.LetIn (var, s, t) -> - Box.V(make_attributes [Some "helm","xref"] [xref], - (make_def "let" var s "in")@[ast2box ~tail t]) - | A.LetRec (_, vars, body) -> - let definitions = - let rec make_defs let_txt = function - [] -> [] - | [(var,s,_)] -> make_def let_txt var s "in" - | (var,s,_)::tl -> - (make_def let_txt var s "")@(make_defs "and" tl) in - make_defs "let rec" vars in - Box.V(make_attributes [Some "helm","xref"] [xref], - definitions@[ast2box ~tail body]) - | A.Ident (s, subst) - | A.Uri (s, subst) -> - let subst = - let rec make_substs start_txt = - function - [] -> [] - | [(s,t)] -> - make_subst start_txt s t "" - | (s,t)::tl -> - (make_subst start_txt s t ";")@(make_substs "" tl) - in - match subst with - | Some subst -> - Box.H([], - [Box.Text(make_std_attributes xref,s); - Box.Action([], - [Box.Text([],"[...]"); - Box.H([], [Box.Text([], map_tex unicode "subst" ^ "["); - Box.V([], make_substs "" subst); - Box.Text([], "]")])])]) - | None -> Box.Text(make_std_attributes xref, s) - in - subst - (* - Box.H([], (* attr here or on Vbox? *) - [Box.Text(make_std_attributes xref,s); - Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])]) - (* Box.indent(Box.V([],subst))]) *) - *) - | A.Implicit -> - Box.Text([],"_") (* big? *) - | A.Meta (n, l) -> - let local_context = - List.map - (function t -> - Box.H([],[aux_option ~tail t; Box.Text([],";")])) - l in - Box.V(make_attributes [Some "helm","xref"] [xref], - [Box.Text([],"?"^(string_of_int n)); - Box.H([],[Box.Text([],"["); - Box.V([],local_context); - Box.Text([],"]")])]) - | A.Num (s, _) -> - Box.Text([],s) - | A.Sort kind -> - (match kind with - `Prop -> Box.Text([],"Prop") - | `Set -> Box.Text([],"Set") - | `Type -> Box.Text([],"Type") - | `CProp -> Box.Text([],"CProp")) - | A.Symbol (s, _) -> - Box.Text([],s) - - | A.UserInput -> Box.Text([],"") - - and aux_option ~tail = function - None -> Box.Text([],"_") - | Some ast -> ast2box ~tail ast - - and make_var ~tail = function - (Cic.Anonymous, None) -> Box.Text([],"_:_") - | (Cic.Anonymous, Some t) -> - Box.H([],[Box.Text([],"_:");ast2box ~tail t]) - | (Cic.Name s, None) -> Box.Text([],s) - | (Cic.Name s, Some t) -> - if is_big t then - Box.V([],[Box.Text([],s^":"); - Box.indent(bigast2box ~tail t)]) - else - Box.H([],[Box.Text([],s^":");Box.Object([],t)]) - - and make_pattern constr = - function - [] -> Box.Text([],constr) - | vars -> - let bvars = - List.fold_right - (fun var acc -> - let bv = - match var with - (* ignoring the type *) - (Cic.Anonymous, _) -> Box.Text([],"_") - | (Cic.Name s, _) -> Box.Text([],s) in - Box.smallskip::bv::acc) vars [Box.Text([],")")] in - Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars) - - - and make_def let_txt var def end_txt = - let name = - (match var with - (* ignoring the type *) - (Cic.Anonymous, _) -> Box.Text([],"_") - | (Cic.Name s, _) -> Box.Text([],s)) in - pretty_append ~tail:[end_txt] - [Box.Text([],let_txt); - Box.smallskip; - name; - Box.smallskip; - Box.Text([],"=") - ] - def - - and make_subst start_txt varname body end_txt = - pretty_append ~tail:[end_txt] - ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@ - [Box.Text([],varname); - Box.smallskip; - Box.Text([],map_tex unicode "Assign") - ]) - body - - and pretty_append ~tail l ast = - if is_big ast then - [Box.H([],l); - Box.H([],[Box.skip; bigast2box ~tail ast])] - else - [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])] - -in -ast2box ~priority ~assoc ~tail t -;; - -let m_row_with_fences = P.row_with_brackets -let m_row = P.row_without_brackets -let m_open_fence = P.Mo([None, "stretchy", "false"], "(") -let m_close_fence = P.Mo([None, "stretchy", "false"], ")") - -let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = - let lookup_uri = function - | None -> None - | Some id -> - (try - Some (Hashtbl.find ids_to_uris id) - with Not_found -> None) - in - let make_std_attributes xref = - let uri = lookup_uri xref in - make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri] - in - let rec aux ?xref = - function - | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast - | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast - | A.Symbol (name,_) -> - let attr = make_std_attributes xref in - P.Mi (attr,name) - | A.Ident (name,subst) - | A.Uri (name,subst) -> - let attr = make_std_attributes xref in - let rec make_subst = - (function - [] -> [] - | (n,a)::tl -> - (aux a):: - P.Mtext([],"/"):: - P.Mi([],n):: - P.Mtext([],"; "):: - P.smallskip:: - (make_subst tl)) in - let subst = - match subst with - | None -> [] - | Some subst -> make_subst subst - in - (match subst with - | [] -> P.Mi (attr, name) - | _ -> - P.Mrow ([], - P.Mi (attr,name):: - P.Mtext([],"["):: - subst @ - [(P.Mtext([],"]"))])) - | A.Meta (no,l) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let l' = - List.map - (function - None -> P.Mo([],"_") - | Some t -> aux t - ) l - in - P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") :: - l' @ [P.Mo ([],"]")]) - | A.Num (value, _) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - P.Mn (attr,value) - | A.Sort `Prop -> P.Mtext ([], "Prop") - | A.Sort `Set -> P.Mtext ([], "Set") - | A.Sort `Type -> P.Mtext ([], "Type") - | A.Sort `CProp -> P.Mtext ([], "CProp") - | A.Implicit -> P.Mtext([], "?") - | A.UserInput -> P.Mtext([], "") - | A.Appl [] -> assert false - | A.Appl ((hd::tl) as l) -> - let aattr = make_attributes [Some "helm","xref"] [xref] in - (match find_symbol None hd with - | `Symbol (name, sxref) -> - let sattr = make_std_attributes sxref in - (try - (let f = Hashtbl.find symbol_table name in - f tl ~priority ~assoc ~ids_to_uris aattr sattr) - with Not_found -> - P.Mrow(aattr, - m_open_fence :: P.Mi(sattr,name)::(make_args tl) @ - [m_close_fence])) - | `None -> - P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @ - [m_close_fence])) - | A.Cast (bo,ty) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - P.Mrow (attr, - [m_open_fence; aux bo; P.Mo ([],":"); aux ty; m_close_fence]) - | A.Binder (`Pi, (Cic.Anonymous, Some ty), body) - | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - P.Mrow (attr, [ - aux ty; - P.Mtext ([], map_tex true "to"); - aux body]) - | A.Binder (kind,var,body) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let binder = resolve_binder true kind in - let var = make_capture_variable var in - P.Mrow (attr, - P.Mtext([None,"mathcolor","blue"],binder) :: var @ - [P.Mo([],"."); aux body]) - | A.LetIn (var,s,body) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - P.Mrow (attr, - P.Mtext([],("let ")) :: - (make_capture_variable var @ - P.Mtext([],("=")):: - (aux s):: - P.Mtext([]," in "):: - [aux body])) - | A.LetRec (_, defs, body) -> - let attr = make_attributes [Some "helm","xref"] [xref] in - let rec make_defs = - (function - [] -> assert false - | [(var,body,_)] -> - make_capture_variable var @ [P.Mtext([],"=");(aux body)] - | (var,body,_)::tl -> - make_capture_variable var @ - (P.Mtext([],"="):: - (aux body)::P.Mtext([]," and")::(make_defs tl))) in - P.Mrow (attr, - P.Mtext([],("let rec ")):: - (make_defs defs)@ - (P.Mtext([]," in "):: - [aux body])) - | A.Case (arg,_,outtype,patterns) -> - (* TODO print outtype *) - let attr = make_attributes [Some "helm","xref"] [xref] in - let rec make_patterns = - (function - [] -> [] - | [(constr, vars),rhs] -> make_pattern constr vars rhs - | ((constr,vars), rhs)::tl -> - (make_pattern constr vars rhs)@(P.smallskip:: - P.Mtext([],"|")::P.smallskip::(make_patterns tl))) - and make_pattern constr vars rhs = - let lhs = - P.Mtext([], constr) :: - (List.concat - (List.map - (fun var -> P.smallskip :: make_capture_variable var) - vars)) - in - lhs @ - [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs] - in - P.Mrow (attr, - P.Mtext([],"match")::P.smallskip:: - (aux arg)::P.smallskip:: - P.Mtext([],"with")::P.smallskip:: - P.Mtext([],"[")::P.smallskip:: - (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))])) - - and make_capture_variable (name, ty) = - let name = - match name with - | Cic.Anonymous -> [P.Mtext([], "_")] - | Cic.Name s -> [P.Mtext([], s)] - in - let ty = - match ty with - | None -> [] - | Some ty -> [P.Mtext([],":"); aux ty] - in - name @ ty - - and make_args ?(priority = 0) ?(assoc = false) = - function - [] -> [] - | a::tl -> P.smallskip::(aux a)::(make_args tl) - - in - aux ast -;; - -let box_prefix = "b";; - -let add_xml_declaration stream = - [< - Xml.xml_cdata "\n" ; - Xml.xml_cdata "\n"; - Xml.xml_nempty ~prefix:box_prefix "box" - [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; - Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ; - Some "xmlns","helm","http://www.cs.unibo.it/helm" ; - Some "xmlns","xlink","http://www.w3.org/1999/xlink" - ] stream - >] - -let ast2mpresXml ((ast, ids_to_uris) as arg) = - let astBox = ast2astBox arg in - let smallAst2mpresXml ast = - P.print_mpres (fun _ -> assert false) (ast2mpres (ast, ids_to_uris)) - in - (Box.box2xml ~obj2xml:smallAst2mpresXml astBox) - -let b_open_fence = Box.b_text [] "(" -let b_close_fence = Box.b_text [] ")" -let b_v_with_fences attrs a b op = - Box.b_h attrs [ - b_open_fence; - Box.b_v [] [ - a; - Box.b_h [] [ op; b ] - ]; - b_close_fence - ] -let b_v_without_fences attrs a b op = - Box.b_v attrs [ - a; - Box.b_h [] [ op; b ] - ] - -let _ = (** fill symbol_table *) - let binary f = function [a;b] -> f a b | _ -> assert false in - let unary f = function [a] -> f a | _ -> assert false in - let add_binary_op name threshold ?(assoc=`Left) symbol = - let assoc = match assoc with `Left -> true | `Right -> false in - Hashtbl.add symbol_table name (binary - (fun a b ~priority ~assoc ~ids_to_uris aattr sattr -> - let symbol = - match symbol with - | `Symbol name -> map_tex true name - | `Ascii s -> s - in - if (priority > threshold) || (priority = threshold && assoc) then - m_row_with_fences aattr - (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris)) - (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris)) - (P.Mo(sattr,symbol)) - else - m_row aattr - (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris)) - (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris)) - (P.Mo(sattr,symbol)))); - Hashtbl.add symbol_table_charcount name (binary - (fun a b ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr -> - let symbol = - match symbol with - | `Symbol name -> map_tex unicode name - | `Ascii s -> s - in - - if (priority > threshold) || (priority = threshold && assoc) then - b_v_with_fences aattr - (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris)) - (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail - (b, ids_to_uris)) - (Box.Text(sattr,symbol)) - else - b_v_without_fences aattr - (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris)) - (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail - (b, ids_to_uris)) - (Box.Text(sattr,symbol)))) - in - Hashtbl.add symbol_table "not" (unary - (fun a ~priority ~assoc ~ids_to_uris attr sattr -> - (P.Mrow([], [ - m_open_fence; P.Mo([],map_tex true "lnot"); - ast2mpres (a, ids_to_uris); m_close_fence])))); - Hashtbl.add symbol_table "inv" (unary - (fun a ~priority ~assoc ~ids_to_uris attr sattr -> - P.Msup([], - P.Mrow([],[ m_open_fence; ast2mpres (a, ids_to_uris); m_close_fence]), - P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")])))); - Hashtbl.add symbol_table "opp" (unary - (fun a ~priority ~assoc ~ids_to_uris attr sattr -> - P.Mrow([],[ - P.Mo([],"-"); - m_open_fence; - ast2mpres (a, ids_to_uris); - m_close_fence]))); - add_binary_op "arrow" 5 ~assoc:`Right (`Symbol "to"); - add_binary_op "eq" 40 (`Ascii "="); - add_binary_op "and" 20 (`Symbol "land"); - add_binary_op "or" 10 (`Symbol "lor"); - add_binary_op "iff" 5 (`Symbol "iff"); - add_binary_op "leq" 40 (`Symbol "leq"); - add_binary_op "lt" 40 (`Symbol "lt"); - add_binary_op "geq" 40 (`Symbol "geq"); - add_binary_op "gt" 40 (`Symbol "gt"); - add_binary_op "plus" 60 (`Ascii "+"); - add_binary_op "times" 70 (`Ascii "*"); - add_binary_op "minus" 60 (`Ascii "-"); - add_binary_op "div" 60 (`Ascii "/"); - add_binary_op "cast" 80 (`Ascii ":"); - diff --git a/helm/ocaml/cic_transformations/ast2pres.mli b/helm/ocaml/cic_transformations/ast2pres.mli deleted file mode 100644 index 5b0e5a740..000000000 --- a/helm/ocaml/cic_transformations/ast2pres.mli +++ /dev/null @@ -1,54 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 28/6/2003 *) -(* *) -(**************************************************************************) - -val maxsize: int -val countterm: int -> CicAst.term -> int -val is_big: CicAst.term -> bool - -val ast2astBox: - ?unicode:bool -> ?priority:int -> ?assoc:bool -> ?tail:string list -> - CicAst.term * (Cic.id, string) Hashtbl.t -> - CicAst.term Box.box - -val ast2mpres: - ?priority:int -> ?assoc:bool -> - CicAst.term * (Cic.id, string) Hashtbl.t -> - unit Mpresentation.mpres - -val add_xml_declaration: Xml.token Stream.t -> Xml.token Stream.t - -val ast2mpresXml: - CicAst.term * (Cic.id, string) Hashtbl.t -> - Xml.token Stream.t - diff --git a/helm/ocaml/cic_transformations/boxPp.ml b/helm/ocaml/cic_transformations/boxPp.ml deleted file mode 100644 index fcc913421..000000000 --- a/helm/ocaml/cic_transformations/boxPp.ml +++ /dev/null @@ -1,55 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let to_string object_to_string b = - let layout = ref [] in - let rec aux_h current_s = - function - [] -> layout := current_s::!layout - | Box.Text (_,s)::tl -> aux_h (current_s ^ s) tl - | (Box.Space _)::tl -> aux_h (current_s ^ " ") tl - | Box.H (_,bl)::tl -> aux_h current_s (bl@tl) - | Box.V (_,[])::tl -> aux_h current_s tl - | Box.V (_,[b])::tl -> aux_h current_s (b::tl) - | Box.V (_,b::bl')::tl -> - aux_h current_s [b] ; - aux_h (String.make (String.length current_s) ' ') (Box.V([],bl')::tl) - | Box.HV _ :: _ | Box.HOV _ :: _ -> assert false (* not implemented *) - | Box.Object (_,obj)::tl -> aux_h (current_s ^ (object_to_string obj)) tl - | (Box.Action _)::tl -> assert false - | (Box.Ink _)::tl -> aux_h (current_s ^ "----------") tl - in - aux_h "" [b] ; - List.rev !layout - -let pp_term ?ids_to_uris t = - let ids_to_uris = - match ids_to_uris with - | None -> Hashtbl.create 0 - | Some tbl -> tbl - in - String.concat "\n" (to_string CicAstPp.pp_term - (Ast2pres.ast2astBox (t, ids_to_uris))) - diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml deleted file mode 100644 index 45fcc8820..000000000 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -type location = Lexing.position * Lexing.position - -let pp_location (loc_begin, loc_end) = - let c_begin = loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol in - let c_end = loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol in - if loc_begin.Lexing.pos_lnum = -1 || loc_end.Lexing.pos_lnum = -1 then - sprintf "%d-%d" c_begin c_end - else - sprintf "(%d,%d)-(%d,%d)" loc_begin.Lexing.pos_lnum c_begin - loc_end.Lexing.pos_lnum c_end - -let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) - -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) - -let dummy_floc = floc_of_loc (-1, -1) - -type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] -type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type | `CProp ] - -type term_attribute = - [ `Loc of location - | `IdRef of string - ] - -type term = - | AttributedTerm of term_attribute * term - - | Appl of term list - | Binder of binder_kind * capture_variable * term - | Case of term * string option * term option * (case_pattern * term) list - | Cast of term * term - | LetIn of capture_variable * term * term - | LetRec of induction_kind * (capture_variable * term * int) list * term - | Ident of string * subst list option - | Implicit - | Meta of int * meta_subst list - | Num of string * int - | Sort of sort_kind - | Symbol of string * int - - | UserInput - | Uri of string * subst list option - -and capture_variable = Cic.name * term option -and meta_subst = term option -and subst = string * term -and case_pattern = string * capture_variable list - -(* -let pack asts = - List.fold_right - (fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc)) - asts (Sort `Type) - -let rec unpack = function - | Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast] - | Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt - | _ -> assert false -*) diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli deleted file mode 100644 index 97cda2e47..000000000 --- a/helm/ocaml/cic_transformations/cicAst.mli +++ /dev/null @@ -1,84 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(** {2 Parsing related types} *) - -type location = Lexing.position * Lexing.position -val pp_location: location -> string - - (** maps old style (i.e. <= 3.07) lexer location to new style location, - * padding with dummy values where needed *) -val floc_of_loc: int * int -> location - - (* the other way round *) -val loc_of_floc: location -> int * int - - (* dummy location *) -val dummy_floc: location - -(** {2 Cic Ast} *) - -type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] -type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type | `CProp ] - -type term_attribute = - [ `Loc of location (* source file location *) - | `IdRef of string (* ACic pointer *) - ] - -type term = - | AttributedTerm of term_attribute * term - | Appl of term list - | Binder of binder_kind * capture_variable * term (* kind, name, body *) - | Case of term * string option * term option * (case_pattern * term) list - (* what to match, inductive type, out type, list *) - | Cast of term * term - | LetIn of capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (capture_variable * term * int) list * term - (* (name, body, decreasing argument) list, where *) - | Ident of string * subst list option - (* literal, substitutions. - * Some [] -> user has given an empty explicit substitution list - * None -> user has given no explicit substitution list *) - | Implicit - | Meta of int * meta_subst list - | Num of string * int (* literal, instance *) - | Sort of sort_kind - | Symbol of string * int (* canonical name, instance *) - - | UserInput (* place holder for user input, used by MatitaConsole, not to be - used elsewhere *) - | Uri of string * subst list option (* as Ident, for long names *) - -and capture_variable = Cic.name * term option (* name, type *) -and meta_subst = term option -and subst = string * term -and case_pattern = string * capture_variable list - -(* -val pack: term list -> term -val unpack: term -> term list -*) diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml deleted file mode 100644 index 2479fe24a..000000000 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ /dev/null @@ -1,102 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -let pp_binder = function - | `Lambda -> "lambda" - | `Pi -> "Pi" - | `Exists -> "exists" - | `Forall -> "forall" - -let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s - -let rec pp_term = function - | CicAst.AttributedTerm (_, term) -> pp_term term - | CicAst.Appl terms -> - sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body) - | CicAst.Binder (`Pi, (Cic.Anonymous, typ), body) -> - sprintf "(%s \\to %s)" - (match typ with None -> "?" | Some typ -> pp_term typ) - (pp_term body) - | CicAst.Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) - | CicAst.Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" - (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) - (pp_term term) (pp_patterns patterns) - | CicAst.Cast (t1,t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) - | CicAst.LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) - | CicAst.LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " - (List.map - (fun (var, body, _) -> - sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) - definitions)) - (pp_term term) - | CicAst.Ident (name, Some []) | CicAst.Ident (name, None) - | CicAst.Uri (name, Some []) | CicAst.Uri (name, None) -> - name - | CicAst.Ident (name, Some substs) - | CicAst.Uri (name, Some substs) -> - sprintf "%s \\subst [%s]" name (pp_substs substs) - | CicAst.Implicit -> "?" - | CicAst.Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | CicAst.Num (num, _) -> num - | CicAst.Sort `Set -> "Set" - | CicAst.Sort `Prop -> "Prop" - | CicAst.Sort `Type -> "Type" - | CicAst.Sort `CProp -> "CProp" - | CicAst.Symbol (name, _) -> name - | CicAst.UserInput -> "%" - -and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) -and pp_substs substs = String.concat "; " (List.map pp_subst substs) - -and pp_pattern ((head, vars), term) = - sprintf "%s \\Rightarrow %s" - (match vars with - | [] -> head - | _ -> - sprintf "(%s %s)" head - (String.concat " " (List.map pp_capture_variable vars))) - (pp_term term) - -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) - -and pp_capture_variable = function - | name, None -> pp_name name - | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")" - diff --git a/helm/ocaml/cic_transformations/cicAstPp.mli b/helm/ocaml/cic_transformations/cicAstPp.mli deleted file mode 100644 index bc6e4c96f..000000000 --- a/helm/ocaml/cic_transformations/cicAstPp.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val pp_term: CicAst.term -> string - diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 142982647..e73e4ec33 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2003-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -34,6 +34,7 @@ module P = Mpresentation module B = Box +module Con = Content let p_mtr a b = Mpresentation.Mtr(a,b) let p_mtd a b = Mpresentation.Mtd(a,b) @@ -49,95 +50,13 @@ let rec split n l = else let l1,l2 = split (n-1) (List.tl l) in (List.hd l)::l1,l2 -;; - -let is_big_general countterm p = - let maxsize = Ast2pres.maxsize in - let module Con = Content in - let rec countp current_size p = - if current_size > maxsize then current_size - else - let c1 = (countcontext current_size p.Con.proof_context) in - if c1 > maxsize then c1 - else - let c2 = (countapplycontext c1 p.Con.proof_apply_context) in - if c2 > maxsize then c2 - else - countconclude c2 p.Con.proof_conclude - - and - countcontext current_size c = - List.fold_left countcontextitem current_size c - and - countcontextitem current_size e = - if current_size > maxsize then maxsize - else - (match e with - `Declaration d -> - (match d.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Proof p -> countp current_size p - | `Definition d -> - (match d.Con.def_name with - Some s -> - let c1 = (current_size + 4 + (String.length s)) in - (countterm c1 d.Con.def_term) - | None -> - prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> maxsize + 1) (* we assume is big *) - and - countapplycontext current_size ac = - List.fold_left countp current_size ac - and - countconclude current_size co = - if current_size > maxsize then current_size - else - let c1 = countargs current_size co.Con.conclude_args in - if c1 > maxsize then c1 - else - (match co.Con.conclude_conclusion with - Some concl -> countterm c1 concl - | None -> c1) - and - countargs current_size args = - List.fold_left countarg current_size args - and - countarg current_size arg = - if current_size > maxsize then current_size - else - (match arg with - Con.Aux _ -> current_size - | Con.Premise prem -> - (match prem.Con.premise_binder with - Some s -> current_size + (String.length s) - | None -> current_size + 7) - | Con.Lemma lemma -> - current_size + (String.length lemma.Con.lemma_name) - | Con.Term t -> countterm current_size t - | Con.ArgProof p -> countp current_size p - | Con.ArgMethod s -> (maxsize + 1)) in - let size = (countp 0 p) in - (size > maxsize) -;; - -let is_big = is_big_general (Ast2pres.countterm) -;; - -let get_xref = - let module Con = Content in - function - `Declaration d - | `Hypothesis d -> d.Con.dec_id - | `Proof p -> p.Con.proof_id - | `Definition d -> d.Con.def_id - | `Joint jo -> jo.Con.joint_id -;; +let get_xref = function + | `Declaration d + | `Hypothesis d -> d.Con.dec_id + | `Proof p -> p.Con.proof_id + | `Definition d -> d.Con.def_id + | `Joint jo -> jo.Con.joint_id let make_row ?(attrs=[]) items concl = match concl with @@ -145,7 +64,6 @@ let make_row ?(attrs=[]) items concl = B.b_v attrs [B.b_h [] items; B.b_indent concl] | _ -> (* small *) B.b_h attrs (items@[B.b_space; concl]) -;; let make_concl ?(attrs=[]) verb concl = match concl with @@ -153,10 +71,8 @@ let make_concl ?(attrs=[]) verb concl = B.b_v attrs [ B.b_kw verb; B.b_indent concl] | _ -> (* small *) B.b_h attrs [ B.b_kw verb; B.b_space; concl ] -;; let make_args_for_apply term2pres args = - let module Con = Content in let make_arg_for_apply is_first arg row = let res = match arg with @@ -168,7 +84,11 @@ let make_args_for_apply term2pres args = | Some s -> s) in (B.b_object (P.Mi ([], name)))::row | Con.Lemma lemma -> - (B.b_object (P.Mi([],lemma.Con.lemma_name)))::row + let lemma_attrs = [ + Some "helm", "xref", lemma.Con.lemma_id; + Some "xlink", "href", lemma.Con.lemma_uri ] + in + (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row | Con.Term t -> if is_first then (term2pres t)::row @@ -184,15 +104,16 @@ let make_args_for_apply term2pres args = make_arg_for_apply true hd (List.fold_right (make_arg_for_apply false) tl []) | _ -> assert false -;; let get_name = function | Some s -> s | None -> "_" +let add_xref id = function + | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) + | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) + let rec justification term2pres p = - let module Con = Content in - let module P = Mpresentation in if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or ((p.Con.proof_context = []) & (p.Con.proof_apply_context = []) & @@ -206,40 +127,39 @@ let rec justification term2pres p = and proof2pres term2pres p = let rec proof2pres p = - let module Con = Content in - let indent = - let is_decl e = - (match e with - `Declaration _ - | `Hypothesis _ -> true - | _ -> false) in - ((List.filter is_decl p.Con.proof_context) != []) in - let omit_conclusion = (not indent) && (p.Con.proof_context != []) in - let concl = - (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> None - | Some t -> Some (term2pres t)) in - let body = - let presconclude = - conclude2pres p.Con.proof_conclude indent omit_conclusion in - let presacontext = - acontext2pres p.Con.proof_apply_context presconclude indent in - context2pres p.Con.proof_context presacontext in - match p.Con.proof_name with - None -> body - | Some name -> - let action = - match concl with - None -> body - | Some ac -> - B.Action - ([None,"type","toggle"], - [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] - "proof of" ac); body]) - in - B.V ([], - [B.Text ([],"(" ^ name ^ ")"); - B.indent action]) + let indent = + let is_decl e = + (match e with + `Declaration _ + | `Hypothesis _ -> true + | _ -> false) in + ((List.filter is_decl p.Con.proof_context) != []) in + let omit_conclusion = (not indent) && (p.Con.proof_context != []) in + let concl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> None + | Some t -> Some (term2pres t)) in + let body = + let presconclude = + conclude2pres p.Con.proof_conclude indent omit_conclusion in + let presacontext = + acontext2pres p.Con.proof_apply_context presconclude indent in + context2pres p.Con.proof_context presacontext in + match p.Con.proof_name with + None -> body + | Some name -> + let action = + match concl with + None -> body + | Some ac -> + B.Action + ([None,"type","toggle"], + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) + in + B.V ([], + [B.Text ([],"(" ^ name ^ ")"); + B.indent action]) and context2pres c continuation = (* we generate a subtable for each context element, for selection @@ -279,7 +199,6 @@ and proof2pres term2pres p = | (`Definition _) as x -> ce2pres x and ce2pres = - let module Con = Content in function `Declaration d -> (match d.Con.dec_name with @@ -314,15 +233,14 @@ and proof2pres term2pres p = Some s -> let term = term2pres d.Con.def_term in B.H ([], - [B.Text([],"Let "); - B.Object ([], P.Mi([],s)); - B.Text([]," = "); - term]) + [ B.b_kw "Let"; B.b_space; + B.Object ([], P.Mi([],s)); + B.Text([]," = "); + term]) | None -> prerr_endline "NO NAME!!"; assert false) and acontext2pres ac continuation indent = - let module Con = Content in List.fold_right (fun p continuation -> let hd = @@ -335,8 +253,6 @@ and proof2pres term2pres p = continuation])) ac continuation and conclude2pres conclude indent omit_conclusion = - let module Con = Content in - let module P = Mpresentation in let tconclude_body = match conclude.Con.conclude_conclusion with Some t when @@ -366,10 +282,7 @@ and proof2pres term2pres p = else B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - and conclude_aux conclude = - let module Con = Content in - let module P = Mpresentation in if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with @@ -404,7 +317,7 @@ and proof2pres term2pres p = B.b_h [] [B.b_kw "Consider"; B.b_space; arg] | Some c -> let conclusion = term2pres c in make_row - [arg; B.b_space; B.Text([],"proves")] + [arg; B.b_space; B.b_kw "proves"] conclusion ) else if conclude.Con.conclude_method = "Intros+LetTac" then @@ -464,37 +377,25 @@ and proof2pres term2pres p = B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")]) else - B.V - ([], - [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to"); - (B.indent - (B.V - ([], - args2pres conclude.Con.conclude_args)))]) + B.V ([], [ + B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to"); + (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))]) and args2pres l = List.map arg2pres l and arg2pres = - let module Con = Content in function - Con.Aux n -> - B.Text ([],"aux " ^ n) - | Con.Premise prem -> - B.Text ([],"premise") - | Con.Lemma lemma -> - B.Text ([],"lemma") - | Con.Term t -> - term2pres t - | Con.ArgProof p -> - proof2pres p - | Con.ArgMethod s -> - B.Text ([],"method") + Con.Aux n -> B.b_kw ("aux " ^ n) + | Con.Premise prem -> B.b_kw "premise" + | Con.Lemma lemma -> B.b_kw "lemma" + | Con.Term t -> term2pres t + | Con.ArgProof p -> proof2pres p + | Con.ArgMethod s -> B.b_kw "method" and case conclude = - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let arg,args_for_cases = (match conclude.Con.conclude_args with @@ -504,31 +405,26 @@ and proof2pres term2pres p = let case_on = let case_arg = (match arg with - Con.Aux n -> - B.Text ([],"an aux???") + Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.Text ([],"the previous result") + None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t - | Con.ArgProof p -> - B.Text ([],"a proof???") - | Con.ArgMethod s -> - B.Text ([],"a method???")) in + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") + in (make_concl "we proceed by cases on" case_arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V - ([], - case_on::to_prove::(make_cases args_for_cases)) + B.V ([], case_on::to_prove::(make_cases args_for_cases)) and byinduction conclude = - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with @@ -540,36 +436,29 @@ and proof2pres term2pres p = let induction_on = let arg = (match inductive_arg with - Con.Aux n -> - B.Text ([],"an aux???") + Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.Text ([],"the previous result") + None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t - | Con.ArgProof p -> - B.Text ([],"a proof???") - | Con.ArgMethod s -> - B.Text ([],"a method???")) in + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") in (make_concl "we proceed by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V - ([], - induction_on::to_prove:: - (make_cases args_for_cases)) + B.V ([], induction_on::to_prove:: (make_cases args_for_cases)) and make_cases l = List.map make_case l and make_case = - let module Con = Content in function Con.ArgProof p -> let name = (match p.Con.proof_name with - None -> B.Text([],"no name for case!!") + None -> B.b_kw "no name for case!!" | Some n -> B.Object ([], P.Mi([],n))) in let indhyps,args = List.partition @@ -595,20 +484,19 @@ and proof2pres term2pres p = dec@p) args [] in let pattern = B.H ([], - (B.Text([],"Case")::B.b_space::name::pattern_aux)@ + (B.b_kw "Case"::B.b_space::name::pattern_aux)@ [B.b_space; - B.Text([],"->")]) in + B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion!!!") + None -> B.b_kw "No conclusion!!!" | Some t -> term2pres t) in let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in let induction_hypothesis = (match indhyps with [] -> [] | _ -> - let text = - B.indent (B.Text([],"by induction hypothesis we know:")) in + let text = B.indent (B.b_kw "by induction hypothesis we know") in let make_hyp = function `Hypothesis h -> @@ -635,20 +523,15 @@ and proof2pres term2pres p = | {Con.proof_id = id}::_ -> id in B.Action([None,"type","toggle"], - [B.indent - (B.Text - ([None,"color","red" ; - Some "helm", "xref", acontext_id],"Proof")) ; - acontext2pres p.Con.proof_apply_context body true]) in + [ B.indent (add_xref acontext_id (B.b_kw "Proof")); + acontext2pres p.Con.proof_apply_context body true]) in B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) | _ -> assert false and falseind conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let case_arg = (match conclude.Con.conclude_args with @@ -662,21 +545,21 @@ and proof2pres term2pres p = Con.Aux n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with - None -> [B.Text([],"Contradiction, hence")] + None -> [B.b_kw "Contradiction, hence"] | Some n -> - [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")]) + [ B.Object ([],P.Mi([],n)); B.skip; + B.b_kw "is contradictory, hence"]) | Con.Lemma lemma -> - [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")] + [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; + B.b_kw "is contradictory, hence" ] | _ -> assert false) in (* let body = proof2pres {proof with Con.proof_context = tl} in *) make_row arg proof_conclusion and andind conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof,case_arg = (match conclude.Con.conclude_args with @@ -693,7 +576,8 @@ and proof2pres term2pres p = None -> [] | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) | Con.Lemma lemma -> - [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))] + [(B.b_kw "by");B.skip; + B.Object([], P.Mi([],lemma.Con.lemma_name))] | _ -> assert false) in match proof.Con.proof_context with `Hypothesis hyp1::`Hypothesis hyp2::tl -> @@ -721,19 +605,17 @@ and proof2pres term2pres p = acontext2pres proof.Con.proof_apply_context body false in B.V ([], - [B.H ([],arg@[B.skip; B.Text([],"we have")]); + [B.H ([],arg@[B.skip; B.b_kw "we have"]); preshyp1; - B.Text([],"and"); + B.b_kw "and"; preshyp2; presacontext]); | _ -> assert false and exists conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof = (match conclude.Con.conclude_args with @@ -773,12 +655,12 @@ and proof2pres term2pres p = [presdecl; suchthat; presacontext]); - | _ -> assert false in + | _ -> assert false -proof2pres p -;; + in + proof2pres p -exception ToDo;; +exception ToDo let counter = ref 0 @@ -814,7 +696,7 @@ let conjecture2pres term2pres (id, n, context, ty) = (match def_name with None -> "_" | Some n -> n)) ; - B.b_text [] ":=" ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); term2pres bo] | Some (`Proof p) -> let proof_name = p.Content.proof_name in @@ -823,10 +705,10 @@ let conjecture2pres term2pres (id, n, context, ty) = (match proof_name with None -> "_" | Some n -> n)) ; - B.b_text [] ":=" ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); proof2pres term2pres p]) (List.rev context)) @ - [ B.b_text [] "|-" ; + [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); B.b_object (p_mi [] (string_of_int n)) ; B.b_text [] ":" ; term2pres ty ]))) @@ -837,9 +719,8 @@ let metasenv2pres term2pres = function (* Conjectures are in their own table to make *) (* diffing the DOM trees easier. *) [B.b_v [] - ((B.b_text [] - ("Conjectures:" ^ - (let _ = incr counter; in (string_of_int !counter)))) :: + ((B.b_kw ("Conjectures:" ^ + (let _ = incr counter; in (string_of_int !counter)))) :: (List.map (conjecture2pres term2pres) metasenv'))] let params2pres params = @@ -867,7 +748,7 @@ let recursion_kind2pres params kind = | `Inductive _ -> "Inductive definition" | `CoInductive _ -> "CoInductive definition" in - B.b_h [] (B.b_text [] kind :: params2pres params) + B.b_h [] (B.b_kw kind :: params2pres params) let inductive2pres term2pres ind = let constructor2pres decl = @@ -879,7 +760,8 @@ let inductive2pres term2pres ind = in B.b_v [] (B.b_h [] [ - B.b_text [] (ind.Content.inductive_name ^ " of arity "); + B.b_kw (ind.Content.inductive_name ^ " of arity"); + B.smallskip; term2pres ind.Content.inductive_type ] :: List.map constructor2pres ind.Content.inductive_constructors) @@ -894,8 +776,8 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name p.Content.proof_name in B.b_v [Some "helm","xref","id"] - ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params); - B.b_text [] "Thesis:"; + ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params); + B.b_kw "Thesis:"; B.indent (term2pres thesis) ] @ metasenv2pres term2pres metasenv @ [proof2pres term2pres p]) @@ -903,18 +785,18 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name body.Content.def_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params); - B.b_text [] "Type:"; + ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); + B.b_kw "Type:"; B.indent (term2pres ty)] @ metasenv2pres term2pres metasenv @ - [term2pres body.Content.def_term]) + [B.b_kw "Body:"; term2pres body.Content.def_term]) | `Decl (_, `Declaration decl) | `Decl (_, `Hypothesis decl) -> let name = get_name decl.Content.dec_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params); - B.b_text [] "Type:"; + ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + B.b_kw "Type:"; B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) | `Joint joint -> @@ -922,23 +804,14 @@ let content2pres term2pres (id,params,metasenv,obj) = (recursion_kind2pres params joint.Content.joint_kind :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) | _ -> raise ToDo -;; - -(* -let content2pres ~ids_to_inner_sorts = - content2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) -;; -*) let content2pres ~ids_to_inner_sorts = content2pres (fun annterm -> - let (ast, ids_to_uris) as arg = - Acic2Ast.ast_of_acic ids_to_inner_sorts annterm + let ast, ids_to_uris = + CicNotationRew.ast_of_acic ids_to_inner_sorts annterm in - let astBox = Ast2pres.ast2astBox arg in - Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox) + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris + (CicNotationRew.pp_ast ast))) diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 7511a527e..793c31a4f 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -35,5 +35,5 @@ val content2pres: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.cobj -> - unit Mpresentation.mpres Box.box + CicNotationPres.boxml_markup diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml deleted file mode 100644 index c41a8386a..000000000 --- a/helm/ocaml/cic_transformations/contentTable.ml +++ /dev/null @@ -1,109 +0,0 @@ - -(* NOTATION *) - -let symbol_table = Hashtbl.create 503 ;; -let lookup_symbol = Hashtbl.find symbol_table ;; - -let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;; - -let add_symbol uri mnemonic = - Hashtbl.add symbol_table uri - (fun aid sid args ast_of_acic -> - idref aid (CicAst.Appl - (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args))) -;; - -(* eq *) -Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI - (fun aid sid args ast_of_acic -> - idref aid (CicAst.Appl - (idref sid (CicAst.Symbol ("eq", 0)) :: - List.map ast_of_acic (List.tl args)))) ;; - -(* and *) -add_symbol HelmLibraryObjects.Logic.and_XURI "and" ;; - -(* or *) -add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;; - -(* iff *) -add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;; - -(* not *) -add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;; - -(* Rinv *) -add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;; - -(* Ropp *) -add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;; - -(* exists *) -Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI - (fun aid sid args ast_of_acic -> - match (List.tl args) with - [Cic.ALambda (_,n,s,t)] -> - idref aid - (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t)) - | _ -> raise Not_found);; - -(* leq *) -add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;; -add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;; - -(* lt *) -add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;; -add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;; - -(* geq *) -add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;; -add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;; - -(* gt *) -add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;; -add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;; - -(* plus *) -add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;; -add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;; - -let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;; -let r1_uri = HelmLibraryObjects.Reals.r1_URI;; - -Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI - (fun aid sid args ast_of_acic -> - let appl () = - idref aid (CicAst.Appl - (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args)) - in - let rec aux acc = function - | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri -> - (match n with - | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri -> - idref aid (CicAst.Num (string_of_int (acc+2), 0)) - | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) - when UriManager.eq uri rplus_uri -> - aux (acc + 1) args - | _ -> appl ()) - | _ -> appl () - in - aux 0 args) -;; - -(* zero and one *) -Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI - (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;; -Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI - (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;; - -(* times *) -add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;; -add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;; - -(* minus *) -add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;; -add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;; - -(* div *) -add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;; - diff --git a/helm/ocaml/cic_transformations/contentTable.mli b/helm/ocaml/cic_transformations/contentTable.mli deleted file mode 100644 index bce877981..000000000 --- a/helm/ocaml/cic_transformations/contentTable.mli +++ /dev/null @@ -1,6 +0,0 @@ - -val lookup_symbol: - string -> - (Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) -> - CicAst.term) - diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml index ad2724134..bac0f1509 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.ml +++ b/helm/ocaml/cic_transformations/sequent2pres.ml @@ -42,9 +42,10 @@ let p_mrow a b = Mpresentation.Mrow(a,b) let p_mphantom a b = Mpresentation.Mphantom(a,b) let b_ink a = Box.Ink a +module K = Content +module P = Mpresentation + let sequent2pres term2pres (_,_,context,ty) = - let module K = Content in - let module P = Mpresentation in let context2pres context = let rec aux accum = function @@ -80,10 +81,7 @@ let sequent2pres term2pres (_,_,context,ty) = aux (r::accum) tl | _::_ -> assert false in aux [] context in - let pres_context = - (Box.b_v - [] - (context2pres context)) in + let pres_context = (Box.b_v [] (context2pres context)) in let pres_goal = term2pres ty in (Box.b_h [] [ Box.b_space; @@ -92,25 +90,15 @@ let sequent2pres term2pres (_,_,context,ty) = pres_context; b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *) Box.b_space; - pres_goal]) - ]) -;; - -(* -let sequent2pres ~ids_to_inner_sorts = - sequent2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) -;; -*) + pres_goal])]) let sequent2pres ~ids_to_inner_sorts = sequent2pres (fun annterm -> - let (ast, ids_to_uris) as arg = - Acic2Ast.ast_of_acic ids_to_inner_sorts annterm + let ast, ids_to_uris = + CicNotationRew.ast_of_acic ids_to_inner_sorts annterm in - let astbox = Ast2pres.ast2astBox arg in - Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astbox) + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris + (CicNotationRew.pp_ast ast))) diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli index e1c9da1dd..615c8e35f 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.mli +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -35,5 +35,5 @@ val sequent2pres : ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.conjecture -> - unit Mpresentation.mpres Box.box + CicNotationPres.boxml_markup diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml deleted file mode 100644 index 3f4d4226f..000000000 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ /dev/null @@ -1,167 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -type direction = [ `LeftToRight | `RightToLeft ] -type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] - -type loc = CicAst.location - -type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term - -type ('term, 'ident) type_spec = - | Ident of 'ident - | Type of UriManager.uri * int - -type ('term, 'ident) tactic = - | Absurd of loc * 'term - | Apply of loc * 'term - | Assumption of loc - | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *) - | Change of loc * ('term,'ident) pattern * 'term - | Clear of loc * 'ident - | ClearBody of loc * 'ident - | Compare of loc * 'term - | Constructor of loc * int - | Contradiction of loc - | Cut of loc * 'ident option * 'term - | DecideEquality of loc - | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list - | Discriminate of loc * 'term - | Elim of loc * 'term * 'term option * int option * 'ident list - | ElimType of loc * 'term * 'term option * int option * 'ident list - | Exact of loc * 'term - | Exists of loc - | Fail of loc - | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern - | Fourier of loc - | FwdSimpl of loc * string * 'ident list - | Generalize of loc * ('term, 'ident) pattern * 'ident option - | Goal of loc * int (* change current goal, argument is goal number 1-based *) - | IdTac of loc - | Injection of loc * 'term - | Intros of loc * int option * 'ident list - | LApply of loc * int option * 'term list * 'term * 'ident option - | Left of loc - | LetIn of loc * 'term * 'ident - | Reduce of loc * reduction_kind * ('term, 'ident) pattern - | Reflexivity of loc - | Replace of loc * ('term, 'ident) pattern * 'term - | Rewrite of loc * direction * 'term * ('term, 'ident) pattern - | Right of loc - | Ring of loc - | Split of loc - | Symmetry of loc - | Transitivity of loc * 'term - -type thm_flavour = Cic.object_flavour - - (** - * true means inductive, false coinductive *) -type 'term inductive_type = string * bool * 'term * (string * 'term) list - -type search_kind = [ `Locate | `Hint | `Match | `Elim ] - -type print_kind = [ `Env | `Coer ] - -type 'term macro = - (* Whelp's stuff *) - | WHint of loc * 'term - | WMatch of loc * 'term - | WInstance of loc * 'term - | WLocate of loc * string - | WElim of loc * 'term - (* real macros *) -(* | Abort of loc *) - | Print of loc * string - | Check of loc * 'term - | Hint of loc - | Quit of loc -(* | Redo of loc * int option - | Undo of loc * int option *) -(* | Print of loc * print_kind *) - | Search_pat of loc * search_kind * string (* searches with string pattern *) - | Search_term of loc * search_kind * 'term (* searches with term pattern *) - -type alias_spec = - | Ident_alias of string * string (* identifier, uri *) - | Symbol_alias of string * int * string (* name, instance no, description *) - | Number_alias of int * string (* instance no, description *) - -type obj = - | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list - (** parameters, list of loc * mutual inductive types *) - | Theorem of thm_flavour * string * CicAst.term * CicAst.term option - (** flavour, name, type, body - * - name is absent when an unnamed theorem is being proved, tipically in - * interactive usage - * - body is present when its given along with the command, otherwise it - * will be given in proof editing mode using the tactical language - *) - | Record of - (string * CicAst.term) list * string * CicAst.term * - (string * CicAst.term) list - -type ('term,'obj) command = - | Default of loc * string * UriManager.uri list - | Include of loc * string - | Set of loc * string * string - | Drop of loc - | Qed of loc - (** name. - * Name is needed when theorem was started without providing a name - *) - | Coercion of loc * 'term - | Alias of loc * alias_spec - (** parameters, name, type, fields *) - | Obj of loc * 'obj - -type ('term, 'ident) tactical = - | Tactic of loc * ('term, 'ident) tactic - | Do of loc * int * ('term, 'ident) tactical - | Repeat of loc * ('term, 'ident) tactical - | Seq of loc * ('term, 'ident) tactical list (* sequential composition *) - | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list - | First of loc * ('term, 'ident) tactical list - (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) - | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) - | Solve of loc * ('term, 'ident) tactical list - - -type ('term, 'obj, 'ident) code = - | Command of loc * ('term,'obj) command - | Macro of loc * 'term macro - (* Macro are substantially queries, but since we are not the kind of - * peolpe that like to push "start" to turn off the computer - * we added this command *) - | Tactical of loc * ('term, 'ident) tactical - -type ('term, 'obj, 'ident) comment = - | Note of loc * string - | Code of loc * ('term, 'obj, 'ident) code - -type ('term, 'obj, 'ident) statement = - | Executable of loc * ('term, 'obj, 'ident) code - | Comment of loc * ('term, 'obj, 'ident) comment - diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml deleted file mode 100644 index d8f54a49f..000000000 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ /dev/null @@ -1,290 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -open TacticAst - -let tactical_terminator = "." -let tactic_terminator = tactical_terminator -let command_terminator = tactical_terminator - -let pp_term_ast term = CicAstPp.pp_term term -let pp_term_cic term = CicPp.ppterm term - -let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" - -let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms) - -let pp_reduction_kind = function - | `Reduce -> "reduce" - | `Simpl -> "simplify" - | `Whd -> "whd" - | `Normalize -> "normalize" - - -let pp_pattern (t, hyp, goal) = - let pp_hyp_pattern l = - String.concat "; " - (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in - let pp_t t = - match t with - None -> "" - | Some t -> pp_term_ast t - in - pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal - -let pp_intros_specs = function - | None, [] -> "" - | Some num, [] -> Printf.sprintf " names %i" num - | None, idents -> Printf.sprintf " names %s" (pp_idents idents) - | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents) - -let rec pp_tactic = function - | Absurd (_, term) -> "absurd" ^ pp_term_ast term - | Apply (_, term) -> "apply " ^ pp_term_ast term - | Auto _ -> "auto" - | Assumption _ -> "assumption" - | Change (_, where, with_what) -> - sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what) - | Clear (_,id) -> sprintf "clear %s" id - | ClearBody (_,id) -> sprintf "clearbody %s" id - | Compare (_,term) -> "compare " ^ pp_term_ast term - | Constructor (_,n) -> "constructor " ^ string_of_int n - | Contradiction _ -> "contradiction" - | Cut (_, ident, term) -> - "cut " ^ pp_term_ast term ^ - (match ident with None -> "" | Some id -> " as " ^ id) - | DecideEquality _ -> "decide equality" - | Decompose (_, [], what, names) -> - sprintf "decompose %s%s" what (pp_intros_specs (None, names)) - | Decompose (_, types, what, names) -> - let to_ident = function - | Ident id -> id - | Type _ -> assert false - in - let types = List.rev_map to_ident types in - sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) - | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term - | Elim (_, term, using, num, idents) -> - sprintf "elim " ^ pp_term_ast term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) - ^ pp_intros_specs (num, idents) - | ElimType (_, term, using, num, idents) -> - sprintf "elim type " ^ pp_term_ast term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) - ^ pp_intros_specs (num, idents) - | Exact (_, term) -> "exact " ^ pp_term_ast term - | Exists _ -> "exists" - | Fold (_, kind, term, pattern) -> - sprintf "fold %s %s %s" (pp_reduction_kind kind) - (pp_term_ast term) (pp_pattern pattern) - | FwdSimpl (_, hyp, idents) -> - sprintf "fwd %s%s" hyp - (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | Generalize (_, pattern, ident) -> - sprintf "generalize %s%s" (pp_pattern pattern) - (match ident with None -> "" | Some id -> " as " ^ id) - | Goal (_, n) -> "goal " ^ string_of_int n - | Fail _ -> "fail" - | Fourier _ -> "fourier" - | IdTac _ -> "id" - | Injection (_, term) -> "injection " ^ pp_term_ast term - | Intros (_, None, []) -> "intro" - | Intros (_, num, idents) -> - sprintf "intros%s%s" - (match num with None -> "" | Some num -> " " ^ string_of_int num) - (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | LApply (_, level_opt, terms, term, ident_opt) -> - sprintf "lapply %s%s%s%s" - (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") - (pp_term_ast term) - (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms) - (match ident_opt with None -> "" | Some ident -> " using " ^ ident) - | Left _ -> "left" - | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident - | Reduce (_, kind, pat) -> - sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat) - | Reflexivity _ -> "reflexivity" - | Replace (_, pattern, t) -> - sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t) - | Rewrite (_, pos, t, pattern) -> - sprintf "rewrite %s %s %s" - (if pos = `LeftToRight then ">" else "<") - (pp_term_ast t) - (pp_pattern pattern) - | Right _ -> "right" - | Ring _ -> "ring" - | Split _ -> "split" - | Symmetry _ -> "symmetry" - | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term - -let pp_flavour = function - | `Definition -> "Definition" - | `Fact -> "Fact" - | `Goal -> "Goal" - | `Lemma -> "Lemma" - | `Remark -> "Remark" - | `Theorem -> "Theorem" - | `Variant -> "Variant" - -let pp_search_kind = function - | `Locate -> "locate" - | `Hint -> "hint" - | `Match -> "match" - | `Elim -> "elim" - | `Instance -> "instance" - -let pp_macro pp_term = function - (* Whelp *) - | WInstance (_, term) -> "whelp instance " ^ pp_term term - | WHint (_, t) -> "whelp hint " ^ pp_term t - | WLocate (_, s) -> "whelp locate " ^ s - | WElim (_, t) -> "whelp elim " ^ pp_term t - | WMatch (_, term) -> "whelp match " ^ pp_term term - (* real macros *) -(* | Abort _ -> "Abort" *) - | Check (_, term) -> sprintf "Check %s" (pp_term term) - | Hint _ -> "hint" -(* | Redo (_, None) -> "Redo" - | Redo (_, Some n) -> sprintf "Redo %d" n *) - | Search_pat (_, kind, pat) -> - sprintf "search %s \"%s\"" (pp_search_kind kind) pat - | Search_term (_, kind, term) -> - sprintf "search %s %s" (pp_search_kind kind) (pp_term term) -(* | Undo (_, None) -> "Undo" - | Undo (_, Some n) -> sprintf "Undo %d" n *) - | Print (_, name) -> sprintf "Print \"%s\"" name - | Quit _ -> "Quit" - -let pp_macro_ast = pp_macro pp_term_ast -let pp_macro_cic = pp_macro pp_term_cic - -let pp_alias = function - | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri - | Symbol_alias (symb, instance, desc) -> - sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" - symb instance desc - | Number_alias (instance,desc) -> - sprintf "alias num (instance %d) = \"%s\"" instance desc - -let pp_params = function - | [] -> "" - | params -> - " " ^ - String.concat " " - (List.map - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) - params) - -let pp_fields fields = - (if fields <> [] then "\n" else "") ^ - String.concat ";\n" - (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields) - -let pp_obj = function - | Inductive (params, types) -> - let pp_constructors constructors = - String.concat "\n" - (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) - constructors) - in - let pp_type (name, _, typ, constructors) = - sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) - (pp_constructors constructors) - in - (match types with - | [] -> assert false - | (name, inductive, typ, constructors) :: tl -> - let fst_typ_pp = - sprintf "%sinductive %s%s: %s \\def\n%s" - (if inductive then "" else "co") name (pp_params params) - (pp_term_ast typ) (pp_constructors constructors) - in - fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Theorem (flavour, name, typ, body) -> - sprintf "%s %s: %s %s" - (pp_flavour flavour) - name - (pp_term_ast typ) - (match body with - | None -> "" - | Some body -> "\\def " ^ pp_term_ast body) - | Record (params,name,ty,fields) -> - "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ - pp_fields fields ^ "}" - -let pp_command = function - | Include (_,path) -> "include " ^ path - | Qed _ -> "qed" - | Drop _ -> "drop" - | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term) - | Alias (_,s) -> pp_alias s - | Obj (_,obj) -> pp_obj obj - | Default (_,what,uris) -> - sprintf "default \"%s\" %s" what - (String.concat " " (List.map UriManager.string_of_uri uris)) - -let rec pp_tactical = function - | Tactic (_, tac) -> pp_tactic tac - | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) - | Repeat (_, tac) -> "repeat " ^ pp_tactical tac - | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs - | Then (_, tac, tacs) -> - sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs) - | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) - | Try (_, tac) -> "try " ^ pp_tactical tac - | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) - -and pp_tacticals ~sep tacs = - String.concat sep (List.map pp_tactical tacs) - -let pp_tactical tac = pp_tactical tac ^ tactical_terminator -let pp_tactic tac = pp_tactic tac ^ tactic_terminator -let pp_command tac = pp_command tac ^ command_terminator - -let pp_executable = function - | Macro (_,x) -> pp_macro_ast x - | Tactical (_,x) -> pp_tactical x - | Command (_,x) -> pp_command x - -let pp_comment = function - | Note (_,str) -> sprintf "(* %s *)" str - | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code) - -let pp_statement = function - | Executable (_, ex) -> pp_executable ex - | Comment (_, c) -> pp_comment c - -let pp_cic_command = function - | Include (_,path) -> "include " ^ path - | Qed _ -> "qed" - | Drop _ -> "drop" - | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term) - | Set (_, _, _) - | Alias (_,_) - | Default (_,_,_) - | Obj (_,_) -> assert false (* not implemented *) -- 2.39.2