-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"
cic_omdoc \
metadata \
tactics \
- cic_transformations \
cic_notation \
+ cic_transformations \
cic_textual_parser2 \
paramodulation \
$(NULL)
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
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
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 \
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 \
cicNotationRew.mli \
cicNotationParser.mli \
grafiteParser.mli \
+ mpresentation.mli \
+ box.mli \
cicNotationPres.mli \
cicNotation.mli \
$(NULL)
* 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
- 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
--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 13/2/2004 *)
+(* *)
+(*************************************************************************)
+
+type
+ 'expr box =
+ Text of attr * string
+ | Space of attr
+ | Ink of attr
+ | H of attr * ('expr box) list
+ | V of attr * ('expr box) list
+ | HV of attr * ('expr box) list
+ | HOV of attr * ('expr box) list
+ | Object of attr * 'expr
+ | Action of attr * ('expr box) list
+
+and attr = (string option * string * string) list
+
+let smallskip = Space([None,"width","0.5em"]);;
+let skip = Space([None,"width","1em"]);;
+
+let indent t = H([],[skip;t]);;
+
+(* BoxML prefix *)
+let prefix = "b";;
+
+let tag_of_box = function
+ | H _ -> "h"
+ | V _ -> "v"
+ | HV _ -> "hv"
+ | HOV _ -> "hov"
+ | _ -> assert false
+
+let box2xml ~obj2xml box =
+ let rec aux =
+ let module X = Xml in
+ function
+ Text (attr,s) -> X.xml_nempty ~prefix "text" attr (X.xml_cdata s)
+ | Space attr -> X.xml_empty ~prefix "space" attr
+ | Ink attr -> X.xml_empty ~prefix "ink" attr
+ | H (attr,l)
+ | V (attr,l)
+ | HV (attr,l)
+ | HOV (attr,l) as box ->
+ X.xml_nempty ~prefix (tag_of_box box) attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
+ >]
+ | Object (attr,m) ->
+ X.xml_nempty ~prefix "obj" attr [< obj2xml m >]
+ | Action (attr,l) ->
+ X.xml_nempty ~prefix "action" attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >]
+ in
+ aux box
+;;
+
+let rec map f = function
+ | (Text _) as box -> box
+ | (Space _) as box -> box
+ | (Ink _) as box -> box
+ | H (attr, l) -> H (attr, List.map (map f) l)
+ | V (attr, l) -> V (attr, List.map (map f) l)
+ | HV (attr, l) -> HV (attr, List.map (map f) l)
+ | HOV (attr, l) -> HOV (attr, List.map (map f) l)
+ | Action (attr, l) -> Action (attr, List.map (map f) l)
+ | Object (attr, obj) -> Object (attr, f obj)
+;;
+
+(*
+let document_of_box ~obj2xml pres =
+ [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ Xml.xml_cdata "\n";
+ Xml.xml_nempty ~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"
+ ] (print_box 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 (RenderingAttrs.object_keyword_attributes `BoxML)
+
--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 13/2/2004 *)
+(* *)
+(*************************************************************************)
+
+type
+ 'expr box =
+ Text of attr * string
+ | Space of attr
+ | Ink of attr
+ | H of attr * ('expr box) list
+ | V of attr * ('expr box) list
+ | HV of attr * ('expr box) list
+ | HOV of attr * ('expr box) list
+ | Object of attr * 'expr
+ | Action of attr * ('expr box) list
+
+and attr = (string option * string * string) list
+
+val smallskip : 'expr box
+val skip: 'expr box
+val indent : 'expr box -> 'expr box
+
+val box2xml:
+ obj2xml:('a -> Xml.token Stream.t) -> 'a box ->
+ Xml.token Stream.t
+
+val map: ('a -> 'b) -> 'a box -> 'b box
+
+(*
+val document_of_box :
+ ~obj2xml:('a -> Xml.token Stream.t) -> 'a box -> Xml.token Stream.t
+*)
+
+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
+val b_space: 'expr box
+val b_kw: string -> 'expr box
+
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 ]
| _ -> 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
(* (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" ]
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 _
type term_t = Cic.annterm
let classify = function
+ | Pt.ImplicitPattern
| Pt.VarPattern _ -> Variable
- | _ -> Constructor
+ | Pt.UriPattern _
+ | Pt.ApplPattern _ -> Constructor
end
module M = Matcher (Pattern32)
type rule_id
val extend:
- CicNotationPt.term ->
+ CicNotationPt.term -> (* level 1 pattern *)
precedence:int ->
associativity:Gramext.g_assoc ->
(CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) ->
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"
| `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
| Sort `Prop -> "Prop"
| Sort `Type -> "Type"
| Sort `CProp -> "CProp"
- | Symbol (name, _) -> name
+ | Symbol (name, _) -> "'" ^ name
| UserInput -> ""
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
| [] -> []
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
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
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 ]
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 &&
@ 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
| `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
| 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 =
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
| `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
| `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
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
* @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
+
| `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
| 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 =
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
| [] -> 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 ->
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
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
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
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
-
in
aux []
-let dress sauce =
+let dress ~sep:sauce =
let rec aux =
function
| [] -> []
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
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
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
| 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
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"
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)
[ "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 =
| 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: [
]
];
interpretation: [
- [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+ [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
(s, args, t)
]
];
| 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)
--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 16/62003 *)
+(* *)
+(**************************************************************************)
+
+type 'a mpres =
+ Mi of attr * string
+ | Mn of attr * string
+ | Mo of attr * string
+ | Mtext of attr * string
+ | Mspace of attr
+ | Ms of attr * string
+ | Mgliph of attr * string
+ | Mrow of attr * 'a mpres list
+ | Mfrac of attr * 'a mpres * 'a mpres
+ | Msqrt of attr * 'a mpres
+ | Mroot of attr * 'a mpres * 'a mpres
+ | Mstyle of attr * 'a mpres
+ | Merror of attr * 'a mpres
+ | Mpadded of attr * 'a mpres
+ | Mphantom of attr * 'a mpres
+ | Mfenced of attr * 'a mpres list
+ | Menclose of attr * 'a mpres
+ | Msub of attr * 'a mpres * 'a mpres
+ | Msup of attr * 'a mpres * 'a mpres
+ | Msubsup of attr * 'a mpres * 'a mpres *'a mpres
+ | Munder of attr * 'a mpres * 'a mpres
+ | Mover of attr * 'a mpres * 'a mpres
+ | Munderover of attr * 'a mpres * 'a mpres *'a mpres
+(* | Multiscripts of ??? NOT IMPLEMEMENTED *)
+ | Mtable of attr * 'a row list
+ | Maction of attr * 'a mpres list
+ | Mobject of attr * 'a
+and 'a row = Mtr of attr * 'a mtd list
+and 'a mtd = Mtd of attr * 'a mpres
+and attr = (string option * string * string) list
+;;
+
+let smallskip = Mspace([None,"width","0.5em"]);;
+let indentation = Mspace([None,"width","1em"]);;
+
+let indented elem =
+ Mrow([],[indentation;elem]);;
+
+let standard_tbl_attr =
+ [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"]
+;;
+
+let two_rows_table attr a b =
+ Mtable(attr@standard_tbl_attr,
+ [Mtr([],[Mtd([],a)]);
+ Mtr([],[Mtd([],b)])]);;
+
+let two_rows_table_with_brackets attr a b op =
+ (* only the open bracket is added; the closed bracket must be in b *)
+ Mtable(attr@standard_tbl_attr,
+ [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]);
+ Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
+
+let two_rows_table_without_brackets attr a b op =
+ Mtable(attr@standard_tbl_attr,
+ [Mtr([],[Mtd([],a)]);
+ Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
+
+let row_with_brackets attr a b op =
+ (* by analogy with two_rows_table_with_brackets we only add the
+ open brackets *)
+ Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")])
+
+let row_without_brackets attr a b op =
+ Mrow(attr,[a;op;b])
+
+(* MathML prefix *)
+let prefix = "m";;
+
+let print_mpres obj_printer mpres =
+ let module X = Xml in
+ let rec aux =
+ function
+ Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
+ | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
+ | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
+ | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
+ | Mspace attr -> X.xml_empty ~prefix "mspace" attr
+ | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)
+ | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s)
+ (* General Layout Schemata *)
+ | Mrow (attr,l) ->
+ X.xml_nempty ~prefix "mrow" attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
+ >]
+ | Mfrac (attr,m1,m2) ->
+ X.xml_nempty ~prefix "mfrac" attr [< aux m1; aux m2 >]
+ | Msqrt (attr,m) ->
+ X.xml_nempty ~prefix "msqrt" attr [< aux m >]
+ | Mroot (attr,m1,m2) ->
+ X.xml_nempty ~prefix "mroot" attr [< aux m1; aux m2 >]
+ | Mstyle (attr,m) -> X.xml_nempty ~prefix "mstyle" attr [< aux m >]
+ | Merror (attr,m) -> X.xml_nempty ~prefix "merror" attr [< aux m >]
+ | Mpadded (attr,m) -> X.xml_nempty ~prefix "mpadded" attr [< aux m >]
+ | Mphantom (attr,m) -> X.xml_nempty ~prefix "mphantom" attr [< aux m >]
+ | Mfenced (attr,l) ->
+ X.xml_nempty ~prefix "mfenced" attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
+ >]
+ | Menclose (attr,m) -> X.xml_nempty ~prefix "menclose" attr [< aux m >]
+ (* Script and Limit Schemata *)
+ | Msub (attr,m1,m2) ->
+ X.xml_nempty ~prefix "msub" attr [< aux m1; aux m2 >]
+ | Msup (attr,m1,m2) ->
+ X.xml_nempty ~prefix "msup" attr [< aux m1; aux m2 >]
+ | Msubsup (attr,m1,m2,m3) ->
+ X.xml_nempty ~prefix "msubsup" attr [< aux m1; aux m2; aux m3 >]
+ | Munder (attr,m1,m2) ->
+ X.xml_nempty ~prefix "munder" attr [< aux m1; aux m2 >]
+ | Mover (attr,m1,m2) ->
+ X.xml_nempty ~prefix "mover" attr [< aux m1; aux m2 >]
+ | Munderover (attr,m1,m2,m3) ->
+ X.xml_nempty ~prefix "munderover" attr [< aux m1; aux m2; aux m3 >]
+ (* | Multiscripts of ??? NOT IMPLEMEMENTED *)
+ (* Tables and Matrices *)
+ | Mtable (attr, rl) ->
+ X.xml_nempty ~prefix "mtable" attr
+ [< (List.fold_right (fun x i -> [< (aux_mrow x) ; i >]) rl [<>]) >]
+ (* Enlivening Expressions *)
+ | Maction (attr, l) ->
+ X.xml_nempty ~prefix "maction" attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >]
+ | Mobject (attr, 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
+ Mtr (attr, l) ->
+ X.xml_nempty ~prefix "mtr" attr
+ [< (List.fold_right (fun x i -> [< (aux_mtd x) ; i >]) l [<>])
+ >]
+ and aux_mtd =
+ let module X = Xml in
+ function
+ Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr
+ [< (aux m) ;
+ X.xml_nempty ~prefix "mphantom" []
+ (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >]
+ in
+ aux mpres
+;;
+
+let document_of_mpres pres =
+ [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ Xml.xml_cdata "\n";
+ Xml.xml_nempty ~prefix "math"
+ [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
+ Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
+ Some "xmlns","xlink","http://www.w3.org/1999/xlink"
+ ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None,
+ "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres))
+ >]
+
--- /dev/null
+(* 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/.
+ *)
+
+type 'a mpres =
+ (* token elements *)
+ Mi of attr * string
+ | Mn of attr * string
+ | Mo of attr * string
+ | Mtext of attr * string
+ | Mspace of attr
+ | Ms of attr * string
+ | Mgliph of attr * string
+ (* General Layout Schemata *)
+ | Mrow of attr * 'a mpres list
+ | Mfrac of attr * 'a mpres * 'a mpres
+ | Msqrt of attr * 'a mpres
+ | Mroot of attr * 'a mpres * 'a mpres
+ | Mstyle of attr * 'a mpres
+ | Merror of attr * 'a mpres
+ | Mpadded of attr * 'a mpres
+ | Mphantom of attr * 'a mpres
+ | Mfenced of attr * 'a mpres list
+ | Menclose of attr * 'a mpres
+ (* Script and Limit Schemata *)
+ | Msub of attr * 'a mpres * 'a mpres
+ | Msup of attr * 'a mpres * 'a mpres
+ | Msubsup of attr * 'a mpres * 'a mpres *'a mpres
+ | Munder of attr * 'a mpres * 'a mpres
+ | Mover of attr * 'a mpres * 'a mpres
+ | Munderover of attr * 'a mpres * 'a mpres *'a mpres
+ (* Tables and Matrices *)
+ | Mtable of attr * 'a row list
+ (* Enlivening Expressions *)
+ | Maction of attr * 'a mpres list
+ (* Embedding *)
+ | Mobject of attr * 'a
+
+and 'a row = Mtr of attr * 'a mtd list
+
+and 'a mtd = Mtd of attr * 'a mpres
+
+ (** XML attribute: namespace, name, value *)
+and attr = (string option * string * string) list
+
+;;
+
+val smallskip : 'a mpres
+val indented : 'a mpres -> 'a mpres
+val standard_tbl_attr : attr
+val two_rows_table : attr -> 'a mpres -> 'a mpres -> 'a mpres
+val two_rows_table_with_brackets :
+ attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
+val two_rows_table_without_brackets :
+ attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
+val row_with_brackets :
+ attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
+val row_without_brackets :
+ attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
+val print_mpres : ('a -> Xml.token Stream.t) -> 'a mpres -> Xml.token Stream.t
+val document_of_mpres : 'a mpres -> Xml.token Stream.t
+
--- /dev/null
+(* Copyright (C) 2005, 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 xml_attribute = string option * string * string
+type markup = [ `MathML | `BoxML ]
+
+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 _ = []
+
--- /dev/null
+(* Copyright (C) 2005, 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/
+ *)
+
+(** 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
+
cic:/
file:///projects/helm/library/coq_contribs/
</key>
+ <key name="prefix">
+ cic:/matita/
+ file:///home/zacchiro/helm/matita/.matita/xml/matita/
+ </key>
</section>
<section name="notation">
<key name="core_file">../../matita/core_notation.ma</key>
| 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"
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
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));
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);
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"
eprintf "%s\e[01;31m%s\e[00m%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
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)
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 = \
-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
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 =
+++ /dev/null
-(* 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 <name, type> 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)
-
+++ /dev/null
-(* 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 *)
-
(***************************************************************************)
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,
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 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 "<?xml version=\"1.0\" ?>\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 ":");
-
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 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
-
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 13/2/2004 *)
-(* *)
-(*************************************************************************)
-
-type
- 'expr box =
- Text of attr * string
- | Space of attr
- | Ink of attr
- | H of attr * ('expr box) list
- | V of attr * ('expr box) list
- | HV of attr * ('expr box) list
- | HOV of attr * ('expr box) list
- | Object of attr * 'expr
- | Action of attr * ('expr box) list
-
-and attr = (string option * string * string) list
-
-let smallskip = Space([None,"width","0.5em"]);;
-let skip = Space([None,"width","1em"]);;
-
-let indent t = H([],[skip;t]);;
-
-(* BoxML prefix *)
-let prefix = "b";;
-
-let tag_of_box = function
- | H _ -> "h"
- | V _ -> "v"
- | HV _ -> "hv"
- | HOV _ -> "hov"
- | _ -> assert false
-
-let box2xml ~obj2xml box =
- let rec aux =
- let module X = Xml in
- function
- Text (attr,s) -> X.xml_nempty ~prefix "text" attr (X.xml_cdata s)
- | Space attr -> X.xml_empty ~prefix "space" attr
- | Ink attr -> X.xml_empty ~prefix "ink" attr
- | H (attr,l)
- | V (attr,l)
- | HV (attr,l)
- | HOV (attr,l) as box ->
- X.xml_nempty ~prefix (tag_of_box box) attr
- [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
- >]
- | Object (attr,m) ->
- X.xml_nempty ~prefix "obj" attr [< obj2xml m >]
- | Action (attr,l) ->
- X.xml_nempty ~prefix "action" attr
- [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >]
- in
- aux box
-;;
-
-let rec map f = function
- | (Text _) as box -> box
- | (Space _) as box -> box
- | (Ink _) as box -> box
- | H (attr, l) -> H (attr, List.map (map f) l)
- | V (attr, l) -> V (attr, List.map (map f) l)
- | HV (attr, l) -> HV (attr, List.map (map f) l)
- | HOV (attr, l) -> HOV (attr, List.map (map f) l)
- | Action (attr, l) -> Action (attr, List.map (map f) l)
- | Object (attr, obj) -> Object (attr, f obj)
-;;
-
-(*
-let document_of_box ~obj2xml pres =
- [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- Xml.xml_cdata "\n";
- Xml.xml_nempty ~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"
- ] (print_box pres)
- >]
-*)
-
-let b_h a b = H(a,b)
-let b_v 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"]
-
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 13/2/2004 *)
-(* *)
-(*************************************************************************)
-
-type
- 'expr box =
- Text of attr * string
- | Space of attr
- | Ink of attr
- | H of attr * ('expr box) list
- | V of attr * ('expr box) list
- | HV of attr * ('expr box) list
- | HOV of attr * ('expr box) list
- | Object of attr * 'expr
- | Action of attr * ('expr box) list
-
-and attr = (string option * string * string) list
-
-val smallskip : 'expr box
-val skip: 'expr box
-val indent : 'expr box -> 'expr box
-
-val box2xml:
- obj2xml:('a -> Xml.token Stream.t) -> 'a box ->
- Xml.token Stream.t
-
-val map: ('a -> 'b) -> 'a box -> 'b box
-
-(*
-val document_of_box :
- ~obj2xml:('a -> Xml.token Stream.t) -> 'a box -> Xml.token Stream.t
-*)
-
-val b_h: attr -> 'expr box list -> 'expr box
-val b_v: attr -> 'expr box list -> 'expr box
-val b_text: attr -> string -> 'expr box
-val b_object: 'expr -> 'expr box
-val b_indent: 'expr box -> 'expr box
-val b_space: 'expr box
-val b_kw: string -> 'expr box
-
+++ /dev/null
-(* 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)))
-
+++ /dev/null
-(* 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 to_string : ('expr -> string) -> 'expr Box.box -> string list
-
-val pp_term : ?ids_to_uris: (Cic.id, string) Hashtbl.t -> CicAst.term -> string
-
+++ /dev/null
-(* 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
-*)
+++ /dev/null
-(* 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, <pattern,action> 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
-*)
+++ /dev/null
-(* 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 ^ ")"
-
+++ /dev/null
-(* 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
-
-(* 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
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)
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
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
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
| 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
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 = []) &
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
| (`Definition _) as x -> ce2pres x
and ce2pres =
- let module Con = Content in
function
`Declaration d ->
(match d.Con.dec_name with
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 =
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
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
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
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
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
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
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 ->
| {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
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
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 ->
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
[presdecl;
suchthat;
presacontext]);
- | _ -> assert false in
+ | _ -> assert false
-proof2pres p
-;;
+ in
+ proof2pres p
-exception ToDo;;
+exception ToDo
let counter = ref 0
(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
(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 ])))
(* 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 =
| `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 =
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)
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])
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 ->
(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)))
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
+++ /dev/null
-
-(* 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" ;;
-
+++ /dev/null
-
-val lookup_symbol:
- string ->
- (Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) ->
- CicAst.term)
-
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 16/62003 *)
-(* *)
-(**************************************************************************)
-
-type 'a mpres =
- Mi of attr * string
- | Mn of attr * string
- | Mo of attr * string
- | Mtext of attr * string
- | Mspace of attr
- | Ms of attr * string
- | Mgliph of attr * string
- | Mrow of attr * 'a mpres list
- | Mfrac of attr * 'a mpres * 'a mpres
- | Msqrt of attr * 'a mpres
- | Mroot of attr * 'a mpres * 'a mpres
- | Mstyle of attr * 'a mpres
- | Merror of attr * 'a mpres
- | Mpadded of attr * 'a mpres
- | Mphantom of attr * 'a mpres
- | Mfenced of attr * 'a mpres list
- | Menclose of attr * 'a mpres
- | Msub of attr * 'a mpres * 'a mpres
- | Msup of attr * 'a mpres * 'a mpres
- | Msubsup of attr * 'a mpres * 'a mpres *'a mpres
- | Munder of attr * 'a mpres * 'a mpres
- | Mover of attr * 'a mpres * 'a mpres
- | Munderover of attr * 'a mpres * 'a mpres *'a mpres
-(* | Multiscripts of ??? NOT IMPLEMEMENTED *)
- | Mtable of attr * 'a row list
- | Maction of attr * 'a mpres list
- | Mobject of attr * 'a
-and 'a row = Mtr of attr * 'a mtd list
-and 'a mtd = Mtd of attr * 'a mpres
-and attr = (string option * string * string) list
-;;
-
-let smallskip = Mspace([None,"width","0.5em"]);;
-let indentation = Mspace([None,"width","1em"]);;
-
-let indented elem =
- Mrow([],[indentation;elem]);;
-
-let standard_tbl_attr =
- [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"]
-;;
-
-let two_rows_table attr a b =
- Mtable(attr@standard_tbl_attr,
- [Mtr([],[Mtd([],a)]);
- Mtr([],[Mtd([],b)])]);;
-
-let two_rows_table_with_brackets attr a b op =
- (* only the open bracket is added; the closed bracket must be in b *)
- Mtable(attr@standard_tbl_attr,
- [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]);
- Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
-
-let two_rows_table_without_brackets attr a b op =
- Mtable(attr@standard_tbl_attr,
- [Mtr([],[Mtd([],a)]);
- Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
-
-let row_with_brackets attr a b op =
- (* by analogy with two_rows_table_with_brackets we only add the
- open brackets *)
- Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")])
-
-let row_without_brackets attr a b op =
- Mrow(attr,[a;op;b])
-
-(* MathML prefix *)
-let prefix = "m";;
-
-let print_mpres obj_printer mpres =
- let module X = Xml in
- let rec aux =
- function
- Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
- | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
- | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
- | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
- | Mspace attr -> X.xml_empty ~prefix "mspace" attr
- | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)
- | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s)
- (* General Layout Schemata *)
- | Mrow (attr,l) ->
- X.xml_nempty ~prefix "mrow" attr
- [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
- >]
- | Mfrac (attr,m1,m2) ->
- X.xml_nempty ~prefix "mfrac" attr [< aux m1; aux m2 >]
- | Msqrt (attr,m) ->
- X.xml_nempty ~prefix "msqrt" attr [< aux m >]
- | Mroot (attr,m1,m2) ->
- X.xml_nempty ~prefix "mroot" attr [< aux m1; aux m2 >]
- | Mstyle (attr,m) -> X.xml_nempty ~prefix "mstyle" attr [< aux m >]
- | Merror (attr,m) -> X.xml_nempty ~prefix "merror" attr [< aux m >]
- | Mpadded (attr,m) -> X.xml_nempty ~prefix "mpadded" attr [< aux m >]
- | Mphantom (attr,m) -> X.xml_nempty ~prefix "mphantom" attr [< aux m >]
- | Mfenced (attr,l) ->
- X.xml_nempty ~prefix "mfenced" attr
- [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
- >]
- | Menclose (attr,m) -> X.xml_nempty ~prefix "menclose" attr [< aux m >]
- (* Script and Limit Schemata *)
- | Msub (attr,m1,m2) ->
- X.xml_nempty ~prefix "msub" attr [< aux m1; aux m2 >]
- | Msup (attr,m1,m2) ->
- X.xml_nempty ~prefix "msup" attr [< aux m1; aux m2 >]
- | Msubsup (attr,m1,m2,m3) ->
- X.xml_nempty ~prefix "msubsup" attr [< aux m1; aux m2; aux m3 >]
- | Munder (attr,m1,m2) ->
- X.xml_nempty ~prefix "munder" attr [< aux m1; aux m2 >]
- | Mover (attr,m1,m2) ->
- X.xml_nempty ~prefix "mover" attr [< aux m1; aux m2 >]
- | Munderover (attr,m1,m2,m3) ->
- X.xml_nempty ~prefix "munderover" attr [< aux m1; aux m2; aux m3 >]
- (* | Multiscripts of ??? NOT IMPLEMEMENTED *)
- (* Tables and Matrices *)
- | Mtable (attr, rl) ->
- X.xml_nempty ~prefix "mtable" attr
- [< (List.fold_right (fun x i -> [< (aux_mrow x) ; i >]) rl [<>]) >]
- (* Enlivening Expressions *)
- | Maction (attr, l) ->
- 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)
- and aux_mrow =
- let module X = Xml in
- function
- Mtr (attr, l) ->
- X.xml_nempty ~prefix "mtr" attr
- [< (List.fold_right (fun x i -> [< (aux_mtd x) ; i >]) l [<>])
- >]
- and aux_mtd =
- let module X = Xml in
- function
- Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr
- [< (aux m) ;
- X.xml_nempty ~prefix "mphantom" []
- (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >]
- in
- aux mpres
-;;
-
-let document_of_mpres pres =
- [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- Xml.xml_cdata "\n";
- Xml.xml_nempty ~prefix "math"
- [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
- Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
- Some "xmlns","xlink","http://www.w3.org/1999/xlink"
- ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None,
- "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres))
- >]
-
+++ /dev/null
-(* 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/.
- *)
-
-type 'a mpres =
- (* token elements *)
- Mi of attr * string
- | Mn of attr * string
- | Mo of attr * string
- | Mtext of attr * string
- | Mspace of attr
- | Ms of attr * string
- | Mgliph of attr * string
- (* General Layout Schemata *)
- | Mrow of attr * 'a mpres list
- | Mfrac of attr * 'a mpres * 'a mpres
- | Msqrt of attr * 'a mpres
- | Mroot of attr * 'a mpres * 'a mpres
- | Mstyle of attr * 'a mpres
- | Merror of attr * 'a mpres
- | Mpadded of attr * 'a mpres
- | Mphantom of attr * 'a mpres
- | Mfenced of attr * 'a mpres list
- | Menclose of attr * 'a mpres
- (* Script and Limit Schemata *)
- | Msub of attr * 'a mpres * 'a mpres
- | Msup of attr * 'a mpres * 'a mpres
- | Msubsup of attr * 'a mpres * 'a mpres *'a mpres
- | Munder of attr * 'a mpres * 'a mpres
- | Mover of attr * 'a mpres * 'a mpres
- | Munderover of attr * 'a mpres * 'a mpres *'a mpres
- (* Tables and Matrices *)
- | Mtable of attr * 'a row list
- (* Enlivening Expressions *)
- | Maction of attr * 'a mpres list
- (* Embedding *)
- | Mobject of attr * 'a
-
-and 'a row = Mtr of attr * 'a mtd list
-
-and 'a mtd = Mtd of attr * 'a mpres
-
- (** XML attribute: namespace, name, value *)
-and attr = (string option * string * string) list
-
-;;
-
-val smallskip : 'a mpres
-val indented : 'a mpres -> 'a mpres
-val standard_tbl_attr : attr
-val two_rows_table : attr -> 'a mpres -> 'a mpres -> 'a mpres
-val two_rows_table_with_brackets :
- attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
-val two_rows_table_without_brackets :
- attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
-val row_with_brackets :
- attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
-val row_without_brackets :
- attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres
-val print_mpres : ('a -> Xml.token Stream.t) -> 'a mpres -> Xml.token Stream.t
-val document_of_mpres : 'a mpres -> Xml.token Stream.t
-
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
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;
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)))
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
+++ /dev/null
-(* 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
-
- (** <name, inductive/coinductive, type, constructor list>
- * 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
-
+++ /dev/null
-(* 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 *)
+++ /dev/null
-(* 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_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
projects / helm.git / commitdiff