contentTable.cmi: cicAst.cmo
-box.cmi: mpresentation.cmi
-cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi
-content2pres.cmi: box.cmi mpresentation.cmi
+acic2Ast.cmi: cicAst.cmo
cicAstPp.cmi: cicAst.cmo
-ast2pres.cmi: box.cmi cicAst.cmo
+ast2pres.cmi: box.cmi cicAst.cmo mpresentation.cmi
+content2pres.cmi: box.cmi mpresentation.cmi
sequent2pres.cmi: box.cmi mpresentation.cmi
-cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi
-acic2Ast.cmi: cicAst.cmo
tacticAstPp.cmi: cicAst.cmo tacticAst.cmo
boxPp.cmi: box.cmi cicAst.cmo
tacticAst2Box.cmi: box.cmi cicAst.cmo tacticAst.cmo
contentTable.cmx: cicAst.cmx contentTable.cmi
cic2Xml.cmo: cic2Xml.cmi
cic2Xml.cmx: cic2Xml.cmi
-content_expressions.cmo: content_expressions.cmi
-content_expressions.cmx: content_expressions.cmi
mpresentation.cmo: mpresentation.cmi
mpresentation.cmx: mpresentation.cmi
-box.cmo: mpresentation.cmi box.cmi
-box.cmx: mpresentation.cmx box.cmi
-cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi
-cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi
-content2pres.cmo: box.cmi cexpr2pres.cmi content_expressions.cmi \
- mpresentation.cmi content2pres.cmi
-content2pres.cmx: box.cmx cexpr2pres.cmx content_expressions.cmx \
- mpresentation.cmx content2pres.cmi
+box.cmo: box.cmi
+box.cmx: box.cmi
+acic2Ast.cmo: cicAst.cmo acic2Ast.cmi
+acic2Ast.cmx: cicAst.cmx acic2Ast.cmi
cicAstPp.cmo: cicAst.cmo cicAstPp.cmi
cicAstPp.cmx: cicAst.cmx cicAstPp.cmi
-ast2pres.cmo: box.cmi cicAst.cmo cicAstPp.cmi ast2pres.cmi
-ast2pres.cmx: box.cmx cicAst.cmx cicAstPp.cmx ast2pres.cmi
-sequent2pres.cmo: box.cmi cexpr2pres.cmi content_expressions.cmi \
- mpresentation.cmi sequent2pres.cmi
-sequent2pres.cmx: box.cmx cexpr2pres.cmx content_expressions.cmx \
- mpresentation.cmx sequent2pres.cmi
-cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \
- mpresentation.cmi cexpr2pres_hashtbl.cmi
-cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \
- mpresentation.cmx cexpr2pres_hashtbl.cmi
+ast2pres.cmo: box.cmi cicAst.cmo mpresentation.cmi ast2pres.cmi
+ast2pres.cmx: box.cmx cicAst.cmx mpresentation.cmx ast2pres.cmi
+content2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \
+ content2pres.cmi
+content2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \
+ content2pres.cmi
+sequent2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \
+ sequent2pres.cmi
+sequent2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \
+ sequent2pres.cmi
misc.cmo: misc.cmi
misc.cmx: misc.cmi
xml2Gdome.cmo: xml2Gdome.cmi
applyStylesheets.cmi
applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \
applyStylesheets.cmi
-applyTransformation.cmo: box.cmi cexpr2pres.cmi cexpr2pres_hashtbl.cmi \
- content2pres.cmi misc.cmi sequent2pres.cmi xml2Gdome.cmi \
- applyTransformation.cmi
-applyTransformation.cmx: box.cmx cexpr2pres.cmx cexpr2pres_hashtbl.cmx \
- content2pres.cmx misc.cmx sequent2pres.cmx xml2Gdome.cmx \
- applyTransformation.cmi
-acic2Ast.cmo: cicAst.cmo acic2Ast.cmi
-acic2Ast.cmx: cicAst.cmx acic2Ast.cmi
+applyTransformation.cmo: ast2pres.cmi box.cmi content2pres.cmi misc.cmi \
+ mpresentation.cmi sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi
+applyTransformation.cmx: ast2pres.cmx box.cmx content2pres.cmx misc.cmx \
+ mpresentation.cmx sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi
tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi
tacticAstPp.cmx: cicAstPp.cmx tacticAst.cmx tacticAstPp.cmi
boxPp.cmo: ast2pres.cmi box.cmi cicAstPp.cmi boxPp.cmi
PACKAGE = cic_transformations
REQUIRES = \
gdome2-xslt \
- helm-xml helm-cic_proof_checking helm-cic_omdoc helm-registry
+ helm-xml helm-cic_proof_checking helm-cic_omdoc helm-registry \
+ helm-utf8_macros
PREDICATES =
# modules which have both a .ml and a .mli
INTERFACE_FILES = \
contentTable.mli \
- cic2Xml.mli content_expressions.mli \
- mpresentation.mli box.mli cexpr2pres.mli content2pres.mli \
- cicAstPp.mli ast2pres.mli \
+ cic2Xml.mli \
+ mpresentation.mli box.mli \
+ acic2Ast.mli \
+ cicAstPp.mli ast2pres.mli content2pres.mli \
sequent2pres.mli \
- cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \
+ misc.mli xml2Gdome.mli sequentPp.mli \
applyStylesheets.mli applyTransformation.mli \
- acic2Ast.mli tacticAstPp.mli boxPp.mli tacticAst2Box.mli
+ tacticAstPp.mli boxPp.mli tacticAst2Box.mli
IMPLEMENTATION_FILES = \
- cicAst.ml \
- tacticAst.ml \
+ cicAst.ml tacticAst.ml \
$(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
+all:
+
+clean: extra_clean
+distclean: extra_clean
+extra_clean:
+ rm -f make_table
+
include ../Makefile.common
open Printf
+module Ast = CicAst
+
let symbol_table = Hashtbl.create 1024
let sort_of_string = function
fst (List.nth (constructors_of_inductive_type uri i) (j-1))
with Not_found -> assert false)
-let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
+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
sort_of_string (Hashtbl.find ids_to_inner_sorts id)
with Not_found -> assert false
in
- let module Ast = CicAst in
let idref id t = Ast.AttributedTerm (`IdRef id, t) in
- let rec aux = function
+ let rec aux =
+prerr_endline "Acic2ast.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);
context
in
- aux acic, ids_to_uris
+ let res = aux acic, ids_to_uris in
+prerr_endline "/Acic2ast.aux";
+ res
+
+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, -1)) ::
+ 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", -1)) ::
+ 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", -1)));
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", -1)));
+ (* 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", -1)) ::
+ 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), -1))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
val ast_of_acic :
(Cic.id, string) Hashtbl.t -> (* id -> sort *)
- (Cic.id, string) Hashtbl.t -> (* id -> uri *)
(*
+ (Cic.id, string) Hashtbl.t -> (* id -> uri *)
(string,
Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) ->
CicAst.term)
let reload_stylesheets = ignore
;;
+let mpres_document pres_box =
+ Ast2pres.add_xml_declaration
+ (Box.box2xml ~obj2xml:Mpresentation.print_mpres 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 =
let content_sequent = Cic2content.map_sequent asequent in
let pres_sequent =
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
- let xmlpres = Box.document_of_box pres_sequent in
+ let xmlpres = mpres_document pres_sequent in
(* Xml.pp_to_outchan xmlpres stdout ; *)
try
Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
let time2 = Sys.time () in
(* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
- let xmlpres = Box.document_of_box pres in
+ let xmlpres = mpres_document pres in
let time25 = Sys.time () in
(* alternative: printing to file
prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
| _ -> assert false
;;
+(*
let _ =
Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
;;
+*)
(**************************************************************************)
module A = CicAst;;
+module P = Mpresentation;;
let symbol_table = Hashtbl.create 503;;
let symbol_table_charcount = Hashtbl.create 503;;
((countterm 0 t) > maxsize)
;;
-let map_attribute =
+let rec make_attributes l1 =
function
- `Loc floc ->
- let (n, m) = CicAst.loc_of_floc floc in
- (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
- | `IdRef s ->
- (Some "helm","xref",s)
+ [] -> []
+ | 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_attributes = List.map map_attribute
+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 resolve_binder = function
- `Lambda -> Box.Text([],"\\lambda")
- | `Pi -> Box.Text([],"\\Pi")
- | `Exists -> Box.Text([],"\\exists")
- | `Forall -> Box.Text([],"\\forall")
-let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
- if is_big t then
- bigast2box ~priority ~assoc ~attr t
- else Box.Object (map_attributes attr, t)
-and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
- function
- A.AttributedTerm (attr1, t) ->
- (* attr should be empty, since AtrtributedTerm are not
- supposed to be directly nested *)
- bigast2box ~priority ~assoc ~attr:(attr1::~attr) t
- | A.Appl l ->
- Box.H
- (map_attributes attr,
- [Box.Text([],"(");
- Box.V([],List.map ast2box l);
- Box.Text([],")")])
+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 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 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, _) ->
+ (match idref with
+ | None -> assert false
+ | Some idref -> `Symbol (name, idref))
+ | _ -> `None
+ in
+ let aattr = make_attributes [Some "helm","xref"] [xref] in
+ (match find_symbol None hd with
+ | `Symbol (name, sxref) ->
+ let sattr = make_std_attributes (Some 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(map_attributes attr,
- [Box.H([],[(match typ with
- | None -> Box.Text([], "?")
- | Some typ -> ast2box typ);
- Box.smallskip;
- Box.Text([], "\\to")]);
- Box.indent(ast2box 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(map_attributes attr,
- [Box.H([],[resolve_binder kind;
- Box.smallskip;
- make_var var;
- Box.Text([],".")]);
- Box.indent (ast2box 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 sep ((constr,vars),rhs) =
+ 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;
+ make_pattern constr vars;
Box.smallskip;
- Box.Text([],"\\Rightarrow")]);
- Box.indent (bigast2box rhs)])
+ 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([],"\\Rightarrow");
+ Box.Text([],map_tex unicode "Rightarrow");
Box.smallskip;
Box.Object([],rhs)]) in
let plbox = match pl with
[] -> Box.Text([],"[]")
| r::tl ->
- Box.H([],
- [Box.V([],
- (make_rule "[" r)::(List.map (make_rule "|") tl));
- Box.Text([],"]")]) in
+ 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 ty;
+ ast2box ~tail ty;
Box.Text([],"]")]) ]
| None -> []
in
if is_big arg then
- Box.V(map_attributes attr,
+ Box.V(make_attributes [Some "helm","xref"] [xref],
ty_box @
[Box.Text([],"match");
- Box.H([],[Box.skip;
- bigast2box arg;
- Box.smallskip;
- Box.Text([],"with")]);
- plbox])
+ Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
+ Box.Text([],"with");
+ Box.indent plbox])
else
- Box.V(map_attributes attr,
+ Box.V(make_attributes [Some "helm","xref"] [xref],
ty_box @
- [Box.H(map_attributes attr,
+ [Box.H(make_attributes [Some "helm","xref"] [xref],
[Box.Text([],"match");
Box.smallskip;
- ast2box arg;
+ ast2box ~tail arg;
Box.smallskip;
Box.Text([],"with")]);
- plbox])
+ Box.indent plbox])
| A.LetIn (var, s, t) ->
- Box.V(map_attributes attr,
- (make_def "let" var s "in")@[ast2box 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,_)::tl ->
(make_def let_txt var s "")@(make_defs "and" tl) in
make_defs "let rec" vars in
- Box.V(map_attributes attr,
- definitions@[ast2box body])
+ Box.V(make_attributes [Some "helm","xref"] [xref],
+ definitions@[ast2box ~tail body])
| A.Ident (s, subst) ->
let subst =
let rec make_substs start_txt =
(make_subst start_txt s t ";")@(make_substs " " tl)
in
match subst with
- | Some subst -> make_substs "\\subst [" subst
+ | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
| None -> []
in
Box.V([], (* attr here or on Vbox? *)
- [Box.Text(map_attributes attr,s);
+ [Box.Text(make_std_attributes xref,s);
Box.indent(Box.V([],subst))])
| A.Implicit ->
Box.Text([],"_") (* big? *)
let local_context =
List.map
(function t ->
- Box.H([],[aux_option t; Box.Text([],";")]))
+ Box.H([],[aux_option ~tail t; Box.Text([],";")]))
l in
- Box.V(map_attributes attr,
+ Box.V(make_attributes [Some "helm","xref"] [xref],
[Box.Text([],"?"^(string_of_int n));
Box.H([],[Box.Text([],"[");
Box.V([],local_context);
| A.Symbol (s, _) ->
Box.Text([],s)
-and aux_option = function
- None -> Box.Text([],"_")
- | Some ast -> ast2box ast
+ and aux_option ~tail = function
+ None -> Box.Text([],"_")
+ | Some ast -> ast2box ~tail ast
-and make_var = function
- (Cic.Anonymous, None) -> Box.Text([],"_:_")
- | (Cic.Anonymous, Some t) ->
- Box.H([],[Box.Text([],"_:");ast2box 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 t)])
- else
- Box.H([],[Box.Text([],s^":");Box.Object([],t)])
+ 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 =
+ 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.Text([]," ")::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]
+ [Box.Text([],start_txt);
+ 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
- [] -> 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.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
- Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
-
+ | 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) ->
+ 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.Appl [] -> assert false
+ | A.Appl ((hd::tl) as l) ->
+ 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, _) ->
+ (match idref with
+ | None -> assert false
+ | Some idref -> `Symbol (name, idref))
+ | term ->
+ `None
+ in
+ let aattr = make_attributes [Some "helm","xref"] [xref] in
+ (match find_symbol None hd with
+ | `Symbol (name, sxref) ->
+ let sattr = make_std_attributes (Some 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.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_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
- [Box.Text([],let_txt);
- Box.smallskip;
- name;
- Box.smallskip;
- Box.Text([],"=")
- ]
- def
- [Box.smallskip;Box.Text([],end_txt)]
+ 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_subst start_txt varname body end_txt =
- pretty_append
- [Box.Text([],start_txt);
- Box.Text([],varname);
- Box.smallskip;
- Box.Text([],"\\Assign")
- ]
- body
- [Box.Text([],end_txt)]
-
-and pretty_append l ast tail =
- prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
- if is_big ast then
- [Box.H([],l);
- Box.H([],Box.skip::(bigast2box ast)::tail)]
- else
- [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
+ 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\" encoding=\"ISO-8859-1\"?>\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 (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 "/");
(* *)
(**************************************************************************)
-val maxsize : int
+val maxsize: int
+val countterm: int -> CicAst.term -> int
+val is_big: CicAst.term -> bool
-val countterm : int -> CicAst.term -> int
+val ast2astBox:
+ ?unicode:bool -> ?priority:int -> ?assoc:bool -> ?tail:string list ->
+ CicAst.term * (Cic.id, string) Hashtbl.t ->
+ CicAst.term Box.box
-val pretty_append :
- (CicAst.term Box.box) list ->
- CicAst.term ->
- (CicAst.term Box.box) list ->
- (CicAst.term Box.box) list
-
-val ast2box:
- ?priority:int ->
- ?assoc:bool ->
- ?attr:CicAst.term_attribute list ->
- CicAst.term -> CicAst.term Box.box
-
-
-
+val ast2mpres:
+ ?priority:int -> ?assoc:bool ->
+ CicAst.term * (Cic.id, string) Hashtbl.t ->
+ 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
let indent t = H([],[skip;t]);;
-(* MathML prefix *)
+(* BoxML prefix *)
let prefix = "b";;
-let rec print_box =
- 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) ->
- X.xml_nempty ~prefix "h" attr
- [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>])
- >]
- | V (attr,l) ->
- X.xml_nempty ~prefix "v" attr
- [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>])
- >]
- | Object (attr,m) ->
- X.xml_nempty ~prefix "obj" attr [< Mpresentation.print_mpres m >]
- | Action (attr,l) ->
- X.xml_nempty ~prefix "action" attr
- [< (List.fold_right (fun x i -> [< (print_box x) ; i >]) l [<>])
- >]
+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) ->
+ X.xml_nempty ~prefix "h" attr
+ [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
+ >]
+ | V (attr,l) ->
+ X.xml_nempty ~prefix "v" 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 document_of_box pres =
+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)
+ | 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","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)
val skip: 'expr box
val indent : 'expr box -> 'expr box
-val document_of_box : Mpresentation.mpres box -> Xml.token Stream.t
+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
aux_h (String.make (String.length current_s) ' ') (Box.V([],bl')::tl)
| 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 t =
- String.concat "\n" (to_string CicAstPp.pp_term (Ast2pres.ast2box t))
+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)))
val to_string : ('expr -> string) -> 'expr Box.box -> string list
-val pp_term : CicAst.term -> string
+val pp_term : ?ids_to_uris: (Cic.id, string) Hashtbl.t -> CicAst.term -> string
+++ /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 P = Mpresentation;;
-module CE = Content_expressions;;
-
-let symbol_table = Hashtbl.create 503;;
-let symbol_table_charcount = Hashtbl.create 503;;
-
-let maxsize = 25;;
-
-let rec countterm current_size t =
- if current_size > maxsize then current_size
- else match t with
- CE.Symbol (_,name,None,_) -> current_size + (String.length name)
- | CE.Symbol (_,name,Some subst,_) ->
- let c1 = current_size + (String.length name) in
- countsubst subst c1
- | CE.LocalVar (_,name) -> current_size + (String.length name)
- | CE.Meta (_,name,l) ->
- List.fold_left
- (fun i t ->
- match t with
- None -> i
- | Some t' -> countterm i t'
- ) (current_size + String.length name) l
- | CE.Num (_,value) -> current_size + (String.length value)
- | CE.Appl (_,l) ->
- List.fold_left countterm current_size l
- | CE.Binder (_, _,(n,s),body) ->
- let cs = countterm (current_size + 2 + (String.length n)) s in
- countterm cs body
- | CE.Letin (_,(n,s),body) ->
- let cs = countterm (current_size + 3 + (String.length n)) s in
- countterm cs body
- | CE.Letrec (_,defs,body) ->
- let cs =
- List.fold_left
- (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in
- countterm cs body
- | CE.Case (_,a,np) ->
- let cs = countterm (current_size + 4) a in
- List.fold_left
- (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size np
-
-and
-countsubst subst current_size =
- List.fold_left
- (fun current_size (uri,expr) ->
- if (current_size > maxsize) then current_size
- else
- let c1 =
- (current_size + (String.length (UriManager.name_of_uri uri))) in
- (countterm c1 expr)) current_size subst
-;;
-
-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 make_math_tail = List.map (fun s -> P.Mtext ([], s))
-
-let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- let module CE = Content_expressions in
- let module P = Mpresentation in
- let rec aux =
- function
- CE.Symbol (xref,name,None,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
- | CE.Symbol (xref,name,Some subst,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- let rec make_subst =
- (function
- [] -> assert false
- | [(uri,a)] ->
- [(aux a);
- P.Mtext([],"/");
- P.Mi([],UriManager.name_of_uri uri)]
- | (uri,a)::tl ->
- (aux a)::
- P.Mtext([],"/")::
- P.Mi([],UriManager.name_of_uri uri)::
- P.Mtext([],"; ")::
- P.smallskip::
- (make_subst tl)) in
- P.Mrow ([],
- P.Mi (attr,name)::
- P.Mtext([],"[")::
- (make_subst subst)@
- (P.Mtext([],"]")::(make_math_tail tail)))
- | CE.LocalVar (xref,name) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
- | CE.Meta (xref,name,l) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let l' =
- List.map
- (function
- None -> P.Mo([],"_")
- | Some t -> cexpr2pres t
- ) l
- in
- if tail = [] then
- P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
- else
- P.Mrow
- ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail))
- | CE.Num (xref,value) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mn (attr,value)
- else P.Mrow([],P.Mn (attr,value)::(make_math_tail tail))
- | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes [Some "helm","xref"] [axref] in
- let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
- (try
- (let f = Hashtbl.find symbol_table n in
- f tl ~priority ~assoc ~tail aattr sattr)
- with notfound ->
- P.Mrow(aattr,
- P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::(make_math_tail tail))))
- | CE.Appl (xref,l) as t ->
- let attr = make_attributes [Some"helm","xref"] [xref] in
- P.Mrow(attr,
- P.Mo([],"(")::(make_args l)@(P.Mo([],")")::(make_math_tail tail)))
- | CE.Binder (xref, kind,(n,s),body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let binder =
- if kind = "Lambda" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
- else if kind = "Prod" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
- else if kind = "Forall" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2200
- else if kind = "Exists" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2203
- else "unknown" in
- P.Mrow (attr,
- P.Mtext([None,"mathcolor","blue"],binder)::
- P.Mtext([],n ^ ":")::
- (aux s)::
- P.Mo([],".")::
- (aux body)::(make_math_tail tail))
- | CE.Letin (xref,(n,s),body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- P.Mrow (attr,
- P.Mtext([],("let "))::
- P.Mtext([],(n ^ "="))::
- (aux s)::
- P.Mtext([]," in ")::
- (aux body)::(make_math_tail tail))
- | CE.Letrec (xref,defs,body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_defs =
- (function
- [] -> assert false
- | [(n,bo)] ->
- [P.Mtext([],(n ^ "="));(aux body)]
- | (n,bo)::tl ->
- P.Mtext([],(n ^ "="))::
- (aux body)::P.Mtext([]," and")::(make_defs tl)) in
- P.Mrow (attr,
- P.Mtext([],("let rec "))::
- (make_defs defs)@
- (P.Mtext([]," in ")::
- (aux body)::(make_math_tail tail)))
- | CE.Case (xref,a,np) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_patterns =
- (function
- [] -> []
- | [(n,p)] -> make_pattern n p
- | (n,p)::tl ->
- (make_pattern n p)@(P.smallskip::
- P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
- and make_pattern n p =
- let rec get_vars_and_body =
- (function
- CE.Binder (_, "Lambda",(n,_),body) ->
- let v,b = get_vars_and_body body in
- n::v,b
- | t -> [],t) in
- let vars,body = get_vars_and_body p in
- let lhs =
- match vars with
- [] -> n ^ " -> "
- | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
- [P.Mtext([],lhs);P.smallskip;aux body] in
- P.Mrow (attr,
- P.Mtext([],"match")::P.smallskip::
- (aux a)::P.smallskip::
- P.Mtext([],"with")::P.smallskip::
- P.Mtext([],"[")::P.smallskip::
- (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail))) in
- aux t
-
-and
-
-make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
- function
- [] -> List.map (fun s -> P.Mtext ([], s)) tail
- | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
-;;
-
-let make_box_tail = List.map (Box.b_text [])
-;;
-
-let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
- function
- [] -> []
- | [a] -> [Box.indent (cexpr2pres_charcount ~tail:tail a)]
- | (a::tl) as l ->
- let c = List.fold_left countterm 0 l in
- if c > maxsize then
- (Box.indent (cexpr2pres_charcount a))::
- (make_args_charcount ~tail:tail tl)
- else
- [Box.indent (Box.b_object (P.Mrow ([], (make_args ~tail:tail l))))]
-
-(*
- function
- [] -> []
- | a::tl ->
- let tlpres =
- let c = List.fold_left countterm 0 tl in
- if c > maxsize then
- P.Mtable ([("align","baseline 1");("equalrows","false");
- ("columnalign","left")],
- (make_args_charcount tl))
- else
- P.Mrow([], make_args tl) in
- [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
- P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
-and
-
-cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- if not (is_big t) then
- Box.b_object (cexpr2pres ~priority ~assoc ~tail t)
- else let aux = cexpr2pres_charcount in
- match t with
- CE.Symbol (xref,name,None,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- if tail = [] then
- Box.b_object (P.Mi (attr,name))
- else
- Box.b_h [] (Box.b_object (P.Mi (attr,name)) :: (make_box_tail tail))
- | CE.Symbol (xref,name,Some subst,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- let rec make_subst =
- (function
- [] -> assert false
- | [(uri,a)] ->
- [Box.b_object (cexpr2pres a);
- Box.b_text [] "/";
- Box.b_object (P.Mi([],UriManager.name_of_uri uri))]
- | (uri,a)::tl ->
- Box.b_object (cexpr2pres a) ::
- Box.b_text [] "/" ::
- Box.b_object (P.Mi([],UriManager.name_of_uri uri)) ::
- Box.b_text [] "; " ::
- Box.smallskip ::
- (make_subst tl)) in
- Box.b_h [] (
- Box.b_object (P.Mi (attr,name))::
- Box.b_text [] "["::
- (make_subst subst)@
- (Box.b_text [] "]")::(make_box_tail tail) )
- | CE.LocalVar (xref,name) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- Box.b_object (P.Mi (attr,name))
- else
- Box.b_object (P.Mrow ([], P.Mi (attr,name)::(make_math_tail tail)))
- | CE.Meta (xref,name,l) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let l' =
- List.map
- (function
- None -> P.Mo([],"_")
- | Some t -> cexpr2pres t
- ) l
- in
- Box.b_object (P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail)))
- | CE.Num (xref,value) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- Box.b_object (P.Mn (attr,value))
- else
- Box.b_object (P.Mrow ([], P.Mn (attr,value)::(make_math_tail tail)))
- | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes [Some "helm","xref"] [axref] in
- let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
- (try
- (let f = Hashtbl.find symbol_table_charcount n in
- f tl ~priority ~assoc ~tail aattr sattr)
- with notfound ->
- Box.b_v aattr (
- Box.b_h [] [
- Box.b_text [] "(";
- Box.b_object (cexpr2pres (CE.Symbol(sxref,n,subst,uri)))
- ] ::
- make_args_charcount ~tail:(")"::tail) tl
- ))
- | CE.Appl (xref,l) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- Box.b_v attr (
- Box.b_h [] [
- Box.b_text [] "(";
- cexpr2pres_charcount (List.hd l)
- ] ::
- make_args_charcount ~tail:(")"::tail) (List.tl l)
- )
- | CE.Binder (xref, kind,(n,s),body) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let binder =
- if kind = "Lambda" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
- else if kind = "Prod" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
- else if kind = "Forall" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2200
- else if kind = "Exists" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2203
- else "unknown" in
- Box.b_v attr [
- Box.b_h [] [
- Box.b_text [None,"color","blue"] binder;
- Box.b_text [] (n ^ ":");
- cexpr2pres_charcount s ~tail:["."]
- ];
- Box.b_h [] [ Box.indent (cexpr2pres_charcount body ~tail:tail) ]
- ]
- | CE.Letin (xref,(n,s),body) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- Box.b_v attr [
- Box.b_h [] [
- Box.b_kw "let";
- Box.smallskip;
- Box.b_text [] (n ^ "=");
- cexpr2pres_charcount s;
- Box.smallskip;
- Box.b_kw "in"
- ];
- Box.indent (cexpr2pres_charcount body)
- ]
- | CE.Letrec (xref,defs,body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_defs =
- (function
- [] -> assert false
- | [(n,bo)] ->
- [Box.b_text [] (n ^ "="); (aux body)]
- | (n,bo)::tl ->
- Box.b_text [] (n ^ "=")::
- (aux body)::
- Box.smallskip::
- Box.b_kw "and"::
- (make_defs tl)) in
- Box.b_h attr (
- Box.b_kw "let" ::
- Box.smallskip ::
- Box.b_kw "rec" ::
- Box.smallskip ::
- make_defs defs @
- [ Box.smallskip; Box.b_kw "in"; Box.smallskip; aux body ]
- )
- | CE.Case (xref,a,np) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let arg =
- if (is_big a) then
- let tail = " with"::tail in (* LUCA: porcheria all'ennesima potenza, TODO ripensare il meccanismo del tail *)
- [ Box.b_h [] [ Box.b_kw "match"; Box.smallskip ];
- aux a ~tail
- ]
- else
- [ Box.b_h [] [
- Box.b_kw "match";
- Box.smallskip;
- aux a ~tail;
- Box.smallskip;
- Box.b_kw "with"
- ]
- ] in
- let rec make_patterns is_first ~tail =
- function
- [] -> []
- | [(n,p)] ->
- let sep = if is_first then "[ " else "| " in
- [ Box.b_h [] [make_pattern sep ~tail n p] ]
- | (n,p)::tl ->
- let sep =
- if is_first then "[ " else "| " in
- [ Box.b_h [] ((make_pattern sep [] n p) :: (make_patterns false ~tail tl)) ]
- and make_pattern sep ~tail n p =
- let rec get_vars_and_body =
- function
- CE.Binder (_, "Lambda",(n,_),body) ->
- let v,b = get_vars_and_body body in
- n::v,b
- | t -> [],t in
- let vars,body = get_vars_and_body p in
- let lhs =
- match vars with
- [] -> sep ^ n ^ " -> "
- | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
- if (is_big body) then
- Box.b_v [] [
- Box.b_text [] lhs;
- Box.indent (aux ~tail body)
- ]
- else
- Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ]
- in
- let patterns =
- make_patterns true np ~tail:("]"::tail) in
- Box.b_v attr (arg@patterns)
-;;
-
-
-
+++ /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> *)
-(* 27/6/2003 *)
-(* *)
-(**************************************************************************)
-
-val symbol_table :
- (string,
- Content_expressions.cexpr list ->
- priority:int ->
- assoc:bool ->
- tail:string list ->
- (string option * string * string) list ->
- (string option * string * string) list ->
- Mpresentation.mpres
- ) Hashtbl.t
-
-val symbol_table_charcount :
- (string,
- Content_expressions.cexpr list ->
- priority:int ->
- assoc:bool ->
- tail:string list ->
- (string option * string * string) list ->
- (string option * string * string) list ->
- Mpresentation.mpres Box.box
- ) Hashtbl.t
-
-val maxsize : int
-val countterm : int -> Content_expressions.cexpr -> int
-val cexpr2pres :
- ?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres
-val cexpr2pres_charcount :
- ?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres Box.box
+++ /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 C2P = Cexpr2pres;;
-module P = Mpresentation;;
-
-let binary f =
- function
- [a;b] -> f a b
- | _ -> assert false
-;;
-
-let unary f =
- function
- [a] -> f a
- | _ -> assert false
-;;
-
-let m_open_fence = P.Mtext([], "(")
-let b_open_fence = Box.b_text [] "("
-(*
-let m_close_fence = P.Mtext([], ")")
-let b_close_fence = Box.b_text [] ")"
-*)
-
-let b_h_with_open_fence attrs a b op =
- Box.b_h attrs [ b_open_fence; a; Box.b_object op; b ]
-let b_h_without_open_fence attrs a b op =
- Box.b_h attrs [ a; Box.b_object op; b ]
-let b_v_with_open_fence attrs a b op =
- Box.b_v attrs [
- Box.b_h [] [ b_open_fence; a];
- Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
- ]
-let b_v_without_open_fence attrs a b op =
- Box.b_v attrs [
- a;
- Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
- ]
-
-let m_row_with_open_fence = P.row_with_brackets
-let m_row_without_open_fence = P.row_without_brackets
-
-let m_close_fence = ")"
-let b_close_fence = ")"
-
-let init
- ~(cexpr2pres:
- ?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres)
- ~(cexpr2pres_charcount:
- ?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres Box.box)
-=
-
-(* arrow *)
-Hashtbl.add C2P.symbol_table "arrow" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:true
- ~tail:((m_close_fence)::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
-
-Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:true
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
-
-(* eq *)
-Hashtbl.add C2P.symbol_table "eq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"="))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"="))));
-
-Hashtbl.add C2P.symbol_table_charcount "eq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"="))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"="))));
-
-(* and *)
-Hashtbl.add C2P.symbol_table "and" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 20) || (priority = 20 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:20 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
-
-Hashtbl.add C2P.symbol_table_charcount "and" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 20) || (priority = 20 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:20 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
-
-(* or *)
-Hashtbl.add C2P.symbol_table "or" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 10) || (priority = 10 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:10 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
-
-Hashtbl.add C2P.symbol_table_charcount "or" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 10) || (priority = 10 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:10 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
-
-(* iff *)
-Hashtbl.add C2P.symbol_table "iff" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
-
-Hashtbl.add C2P.symbol_table_charcount "iff" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
-
-(* not *)
-Hashtbl.add C2P.symbol_table "not" (unary
- (fun a ~priority ~assoc ~tail attr sattr ->
- (P.Mrow([], [
- m_open_fence; P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
- cexpr2pres a; P.Mtext ([], m_close_fence)])))) ;
-
-(* inv *)
-Hashtbl.add C2P.symbol_table "inv" (unary
- (fun a ~priority ~assoc ~tail attr sattr ->
- P.Msup([],
- P.Mrow([],[
- m_open_fence;
- cexpr2pres a;
- P.Mtext ([], m_close_fence)]),
- P.Mrow([],[
- P.Mo([],"-");
- P.Mn([],"1")]))));
-
-(* opp *)
-Hashtbl.add C2P.symbol_table "opp" (unary
- (fun a ~priority ~assoc ~tail attr sattr ->
- P.Mrow([],[
- P.Mo([],"-");
- m_open_fence;
- cexpr2pres a;
- P.Mtext ([], m_close_fence)])));
-
-(* leq *)
-Hashtbl.add C2P.symbol_table "leq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
-
-Hashtbl.add C2P.symbol_table_charcount "leq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
-
-(* lt *)
-Hashtbl.add C2P.symbol_table "lt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"<"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"<"))));
-
-Hashtbl.add C2P.symbol_table_charcount "lt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"<"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-(* geq *)
-Hashtbl.add C2P.symbol_table "geq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-Hashtbl.add C2P.symbol_table_charcount "geq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-(* gt *)
-Hashtbl.add C2P.symbol_table "gt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,">"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,">"))));
-
-Hashtbl.add C2P.symbol_table_charcount "gt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,">"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,">"))));
-
-(* plus *)
-Hashtbl.add C2P.symbol_table "plus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"+"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"+"))));
-
-Hashtbl.add C2P.symbol_table_charcount "plus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"+"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"+"))));
-
-(* times *)
-Hashtbl.add C2P.symbol_table "times" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 70) || (priority = 70 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:70 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"*"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"*"))));
-
-Hashtbl.add C2P.symbol_table_charcount "times" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 70) || (priority = 70 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:70 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"*"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"*"))));
-
-(* minus *)
-Hashtbl.add C2P.symbol_table "minus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"-"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"-"))));
-
-Hashtbl.add C2P.symbol_table_charcount "minus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"-"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"-"))));
-
-(* div *)
-Hashtbl.add C2P.symbol_table "div" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- m_row_with_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false
- ~tail:(m_close_fence::tail) b)
- (P.Mo(sattr,"/"))
- else
- m_row_without_open_fence aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"/"))));
-
-Hashtbl.add C2P.symbol_table_charcount "div" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- b_v_with_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false
- ~tail:(b_close_fence::tail) b)
- (P.Mo(sattr,"/"))
- else
- b_v_without_open_fence aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"/"))))
-;;
+++ /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> *)
-(* 27/6/2003 *)
-(* *)
-(**************************************************************************)
-
-val init:
- cexpr2pres:
- (?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres) ->
- cexpr2pres_charcount:
- (?priority:int ->
- ?assoc:bool ->
- ?tail:string list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres Box.box) ->
- unit
-;;
let is_big_general countterm p =
- let maxsize = Cexpr2pres.maxsize in
+ let maxsize = Ast2pres.maxsize in
let module Con = Content in
let rec countp current_size p =
if current_size > maxsize then current_size
(size > maxsize)
;;
-let is_big = is_big_general (Cexpr2pres.countterm)
+let is_big = is_big_general (Ast2pres.countterm)
;;
let get_xref =
| _ -> 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
+ in
+ let astBox = Ast2pres.ast2astBox arg in
+ Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox)
+++ /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> *)
-(* 27/6/2003 *)
-(* *)
-(**************************************************************************)
-
-
-(* the type cexpr is inspired by OpenMath. A few primitive constructors
- have been added, in order to take into account some special features
- of functional expressions. Most notably: case, let in, let rec, and
- explicit substitutions *)
-
-type cexpr =
- Symbol of string option * string * subst option * string option
- (* h:xref, name, subst, definitionURL *)
- | LocalVar of (string option) * string (* h:xref, name *)
- | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
- | Num of string option * string (* h:xref, value *)
- | Appl of string option * cexpr list (* h:xref, args *)
- | Binder of string option * string * decl * cexpr
- (* h:xref, name, decl, body *)
- | Letin of string option * def * cexpr (* h:xref, def, body *)
- | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
- | Case of string option * cexpr * ((string * cexpr) list)
- (* h:xref, case_expr, named-pattern list *)
-
-and
- decl = string * cexpr (* name, type *)
-and
- def = string * cexpr (* name, body *)
-and
- subst = (UriManager.uri * cexpr) list
-and
- meta_subst = cexpr option list
-;;
-
-(* NOTATION *)
-
-let symbol_table = Hashtbl.create 503;;
-
-(* eq *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "eq",
- None, Some HelmLibraryObjects.Logic.eq_SURI))
- :: List.map acic2cexpr (List.tl args)));;
-
-(* and *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "and",
- None, Some HelmLibraryObjects.Logic.and_SURI))
- :: List.map acic2cexpr args));;
-
-(* or *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "or",
- None, Some HelmLibraryObjects.Logic.or_SURI))
- :: List.map acic2cexpr args));;
-
-(* iff *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "iff",
- None, Some HelmLibraryObjects.Logic.iff_SURI))
- :: List.map acic2cexpr args));;
-
-(* not *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "not",
- None, Some HelmLibraryObjects.Logic.not_SURI))
- :: List.map acic2cexpr args));;
-
-(* Rinv *)
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "inv",
- None, Some HelmLibraryObjects.Reals.rinv_SURI))
- :: List.map acic2cexpr args));;
-
-(* Ropp *)
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "opp",
- None, Some HelmLibraryObjects.Reals.ropp_SURI))
- :: List.map acic2cexpr args));;
-
-(* exists *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
- (fun aid sid args acic2cexpr ->
- match (List.tl args) with
- [Cic.ALambda (_,Cic.Name n,s,t)] ->
- Binder
- (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
- | _ -> raise Not_found);;
-
-(* leq *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "leq",
- None, Some HelmLibraryObjects.Peano.le_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "leq",
- None, Some HelmLibraryObjects.Reals.rle_SURI))
- :: List.map acic2cexpr args));;
-
-(* lt *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "lt",
- None, Some HelmLibraryObjects.Peano.lt_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "lt",
- None, Some HelmLibraryObjects.Reals.rlt_SURI))
- :: List.map acic2cexpr args));;
-
-(* geq *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "geq",
- None, Some HelmLibraryObjects.Peano.ge_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "geq",
- None, Some HelmLibraryObjects.Reals.rge_SURI))
- :: List.map acic2cexpr args));;
-
-(* gt *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "gt",
- None, Some HelmLibraryObjects.Peano.gt_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "gt",
- None, Some HelmLibraryObjects.Reals.rgt_SURI))
- :: List.map acic2cexpr args));;
-
-(* plus *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "plus",
- None, Some HelmLibraryObjects.Peano.plus_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "plus",
- None, Some HelmLibraryObjects.BinInt.zplus_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
- (fun aid sid args acic2cexpr ->
- let appl () =
- Appl
- (Some aid, (Symbol (Some sid, "plus",
- None, Some HelmLibraryObjects.Reals.rplus_SURI))
- :: List.map acic2cexpr 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 ->
- Num (Some aid, string_of_int (acc + 2))
- | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
- UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
- aux (acc + 1) args
- | _ -> appl ())
- | _ -> appl ()
- in
- aux 0 args)
-;;
-
-(* zero and one *)
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
- (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
- (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
-
-(* times *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "times",
- None, Some HelmLibraryObjects.Peano.mult_SURI))
- :: List.map acic2cexpr args));;
-
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "times",
- None, Some HelmLibraryObjects.Reals.rmult_SURI))
- :: List.map acic2cexpr args));;
-(* minus *)
-Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "minus",
- None, Some HelmLibraryObjects.Peano.minus_SURI))
- :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "minus",
- None, Some HelmLibraryObjects.Reals.rminus_SURI))
- :: List.map acic2cexpr args));;
-
-(* div *)
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "div",
- None, Some HelmLibraryObjects.Reals.rdiv_SURI))
- :: List.map acic2cexpr args));;
-
-
-
-
-(* END NOTATION *)
-
-
-let string_of_sort =
- function
- Cic.Prop -> "Prop"
- | Cic.Set -> "Set"
- | Cic.Type _ -> "Type" (* TASSI *)
- | Cic.CProp -> "Type"
-;;
-
-let get_constructors uri i =
- let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
- ) in
- let (_,_,_,constructors) = List.nth inductive_types i in
- constructors
-;;
-
-exception NotImplemented;;
-
-let acic2cexpr ids_to_inner_sorts t =
- let rec acic2cexpr t =
- let module C = Cic in
- let module X = Xml in
- let module U = UriManager in
- let module C2A = Cic2acic in
- let make_subst =
- function
- [] -> None
- | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
- match t with
- C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
- | C.AVar (id,uri,subst) ->
- Symbol (Some id, UriManager.name_of_uri uri,
- make_subst subst, Some (UriManager.string_of_uri uri))
- | C.AMeta (id,n,l) ->
- let l' =
- List.rev_map
- (function
- None -> None
- | Some t -> Some (acic2cexpr t)
- ) l
- in
- Meta (Some id,("?" ^ (string_of_int n)),l')
- | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
- | C.AImplicit _ -> raise NotImplemented
- | C.AProd (id,n,s,t) ->
- (match n with
- Cic.Anonymous ->
- Appl (Some id, [Symbol (None, "arrow",None,None);
- acic2cexpr s; acic2cexpr t])
- | Cic.Name name ->
- let sort =
- (try Hashtbl.find ids_to_inner_sorts id
- with Not_found ->
- (* if the Prod does not have the sort, it means
- that it has been generated by cic2content, and
- thus is a statement *)
- "Prop") in
- let binder = if sort = "Prop" then "Forall" else "Prod" in
- let decl = (name, acic2cexpr s) in
- Binder (Some id,binder,decl,acic2cexpr t))
- | C.ACast (id,v,t) -> acic2cexpr v
- | C.ALambda (id,n,s,t) ->
- let name =
- (match n with
- Cic.Anonymous -> "_"
- | Cic.Name name -> name) in
- let decl = (name, acic2cexpr s) in
- Binder (Some id,"Lambda",decl,acic2cexpr t)
- | C.ALetIn (id,n,s,t) ->
- (match n with
- Cic.Anonymous -> assert false
- | Cic.Name name ->
- let def = (name, acic2cexpr s) in
- Letin (Some id,def,acic2cexpr t))
- | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
- let uri_str = UriManager.string_of_uri uri in
- (try
- (let f = Hashtbl.find symbol_table uri_str in
- f aid sid tl acic2cexpr)
- with Not_found ->
- Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
- make_subst subst, Some uri_str)::List.map acic2cexpr tl))
- | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
- let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
- ) in
- let (name,_,_,_) = List.nth inductive_types i in
- let uri_str = UriManager.string_of_uri uri in
- let puri_str =
- uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
- (try
- (let f = Hashtbl.find symbol_table puri_str in
- f aid sid tl acic2cexpr)
- with Not_found ->
- Appl (Some aid, Symbol (Some sid, name,
- make_subst subst, Some uri_str)::List.map acic2cexpr tl))
- | C.AAppl (id,li) ->
- Appl (Some id, List.map acic2cexpr li)
- | C.AConst (id,uri,subst) ->
- let uri_str = UriManager.string_of_uri uri in
- (try
- let f = Hashtbl.find symbol_table uri_str in
- f "dummy" id [] acic2cexpr
- with Not_found ->
- Symbol (Some id, UriManager.name_of_uri uri,
- make_subst subst, Some (UriManager.string_of_uri uri)))
- | C.AMutInd (id,uri,i,subst) ->
- let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
- ) in
- let (name,_,_,_) = List.nth inductive_types i in
- let uri_str = UriManager.string_of_uri uri in
- Symbol (Some id, name, make_subst subst, Some uri_str)
- | C.AMutConstruct (id,uri,i,j,subst) ->
- let constructors = get_constructors uri i in
- let (name,_) = List.nth constructors (j-1) in
- let uri_str = UriManager.string_of_uri uri in
- Symbol (Some id, name, make_subst subst, Some uri_str)
- | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
- let constructors = get_constructors uri typeno in
- let named_patterns =
- List.map2 (fun c p -> (fst c, acic2cexpr p))
- constructors patterns in
- Case (Some id, acic2cexpr te, named_patterns)
- | C.AFix (id, no, funs) ->
- let defs =
- List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
- let (name,_) = List.nth defs no in
- let body = LocalVar (None, name) in
- Letrec (Some id, defs, body)
- | C.ACoFix (id,no,funs) ->
- let defs =
- List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
- let (name,_) = List.nth defs no in
- let body = LocalVar (None, name) in
- Letrec (Some id, defs, body) in
- acic2cexpr 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> *)
-(* 27/6/2003 *)
-(* *)
-(**************************************************************************)
-
-type
- cexpr =
- Symbol of string option * string * (subst option) * string option
- (* h:xref, name, subst, definitionURL *)
- | LocalVar of string option * string (* h:xref, name *)
- | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
- | Num of string option * string (* h:xref, value *)
- | Appl of string option * cexpr list (* h:xref, args *)
- | Binder of string option *string * decl * cexpr
- (* h:xref, name, decl, body *)
- | Letin of string option * def * cexpr (* h:xref, def, body *)
- | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
- | Case of string option * cexpr * ((string * cexpr) list)
- (* h:xref, case_expr, named-pattern list *)
-
-and
- decl = string * cexpr (* name, type *)
-and
- def = string * cexpr (* name, body *)
-and
- subst = (UriManager.uri * cexpr) list
-and
- meta_subst = cexpr option list
-;;
-
-
-val acic2cexpr :
- (Cic.id, string) Hashtbl.t -> Cic.annterm -> cexpr
and attr = (string option * string * string) list
;;
-let smallskip = Mspace([None,"width","0.1cm"]);;
-let indentation = Mspace([None,"width","0.3cm"]);;
+let smallskip = Mspace([None,"width","0.5em"]);;
+let indentation = Mspace([None,"width","1em"]);;
let indented elem =
Mrow([],[indentation;elem]);;
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])
+ Mrow(attr,[Mtext([],"(");a;op;b;Mtext([],")")])
let row_without_brackets attr a b op =
Mrow(attr,[a;op;b])
pres_goal])
;;
+(*
let sequent2pres ~ids_to_inner_sorts =
sequent2pres
(function p ->
(Cexpr2pres.cexpr2pres_charcount
(Content_expressions.acic2cexpr ids_to_inner_sorts p)))
;;
+*)
-
-
+let sequent2pres ~ids_to_inner_sorts =
+prerr_endline "Sequent2pres.sequent2pres";
+ sequent2pres
+ (fun annterm ->
+ let (ast, ids_to_uris) as arg =
+ Acic2Ast.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)
(***************************************************************************)
val sequent2pres :
-ids_to_inner_sorts:(Cic.id, string) Hashtbl.t ->
- Cic.annterm Content.conjecture -> Mpresentation.mpres Box.box
-
+ ids_to_inner_sorts:(Cic.id, string) Hashtbl.t ->
+ Cic.annterm Content.conjecture ->
+ Mpresentation.mpres Box.box
if current_size > maxsize then current_size
else match tac with
LocatedTactic (_, tac) -> count_tactic current_size tac
- | Absurd -> current_size + 6
- | Apply term -> countterm (current_size+6) term
+ | Absurd term -> countterm (current_size + 6) term
+ | Apply term -> countterm (current_size + 6) term
| Assumption -> current_size + 10
| Change (t1, t2, where) ->
let size1 = countterm (current_size + 12) t1 in (* change, with *)
;;
(* prova *)
-let rec small_tactic2box ?(attr = []) tac =
+let rec small_tactic2box tac =
Box.Text([], TacticAstPp.pp_tactic tac)
let string_of_kind = function
| `Simpl -> "simpl"
| `Whd -> "whd"
-let rec tactic2box ?(attr = []) tac =
+let dummy_tbl = Hashtbl.create 0
+
+let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
+
+let pretty_append l ast =
+ if is_big ast then
+ [Box.H([],l);
+ Box.H([],[Box.skip; ast2astBox ast])]
+ else
+ [Box.H([],l@[Box.smallskip; ast2astBox ast])]
+
+let rec tactic2box tac =
if (is_big_tac tac) then
- big_tactic2box ~attr tac
+ big_tactic2box tac
else
- small_tactic2box ~attr tac
+ small_tactic2box tac
-and big_tactic2box ?(attr = []) = function
+and big_tactic2box = function
LocatedTactic (loc, tac) ->
- big_tactic2box ~attr tac
- | Absurd -> Box.Text([],"absurd")
+ big_tactic2box tac
+ | Absurd term ->
+ Box.V([],[Box.Text([],"absurd");
+ ast2astBox term])
| Apply term ->
Box.V([],[Box.Text([],"apply");
- ast2box ~attr term])
+ ast2astBox term])
| Assumption -> Box.Text([],"assumption")
| Change (t1, t2, where) ->
let where =
Box.V([],
(pretty_append
[Box.Text([],"change")]
- t1
- [])@
+ t1)@
(pretty_append
[Box.Text([],"with")]
- t2
- [])@where)
+ t2)@where)
| Change_pattern (_, _, _) -> assert false (* TODO *)
| Contradiction -> Box.Text([],"contradiction")
| Cut term ->
Box.V([],[Box.Text([],"cut");
- Box.indent(ast2box term)])
+ Box.indent(ast2astBox term)])
| Decompose (ident, principles) ->
let principles =
List.map (fun x -> Box.Text([],x)) principles in
| Some term ->
(pretty_append
[Box.Text([],"using")]
- term
- [])) in
+ term)) in
Box.V([],
(pretty_append
[Box.Text([],"elim")]
- term
- [])@using)
+ term)@using)
| ElimType term ->
Box.V([],[Box.Text([],"elim type");
- Box.indent(ast2box term)])
+ Box.indent(ast2astBox term)])
| Exact term ->
Box.V([],[Box.Text([],"exact");
- Box.indent(ast2box term)])
+ Box.indent(ast2astBox term)])
| Exists -> Box.Text([],"exists")
| Fold (kind, term) ->
Box.V([],[Box.H([],[Box.Text([],"fold");
Box.smallskip;
Box.Text([],string_of_kind kind)]);
- Box.indent(ast2box term)])
+ Box.indent(ast2astBox term)])
| Fourier -> Box.Text([],"fourier")
| Injection ident ->
Box.V([],[Box.Text([],"transitivity");
Box.Text([],ident);
Box.smallskip;
Box.Text([],"=")]);
- Box.indent (ast2box term)])
+ Box.indent (ast2astBox term)])
| Reduce (_, _, _) -> assert false (* TODO *)
| Reflexivity -> Box.Text([],"reflexivity")
| Replace (t1, t2) ->
Box.V([],
(pretty_append
[Box.Text([],"replace")]
- t1
- [])@
+ t1)@
(pretty_append
[Box.Text([],"with")]
- t2
- []))
+ t2))
| Replace_pattern (_, _) -> assert false (* TODO *)
| Rewrite (_, _, _) -> assert false (* TODO *)
| Right -> Box.Text([],"right")
| Symmetry -> Box.Text([],"symmetry")
| Transitivity term ->
Box.V([],[Box.Text([],"transitivity");
- Box.indent (ast2box term)])
+ Box.indent (ast2astBox term)])
;;
open TacticAst
-let rec tactical2box ?(attr = []) = function
+let rec tactical2box = function
| LocatedTactical (loc, tac) -> tactical2box tac
| Tactic tac -> tactic2box tac
val tactical2box:
- ?attr:'a list -> (CicAst.term, string) TacticAst.tactical ->
+ (CicAst.term, string) TacticAst.tactical ->
CicAst.term Box.box
val tacticalPp: (CicAst.term, string) TacticAst.tactical -> string
projects / helm.git / commitdiff