From 29969baf115afff7eb9ea9e2ca98d40ab7006dcc Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 13 Oct 2004 08:16:45 +0000 Subject: [PATCH] transformations no longer use Content_expression, but rather CicAst --- helm/ocaml/cic_transformations/.depend | 55 +- helm/ocaml/cic_transformations/Makefile | 24 +- helm/ocaml/cic_transformations/acic2Ast.ml | 89 ++- helm/ocaml/cic_transformations/acic2Ast.mli | 2 +- .../applyTransformation.ml | 10 +- helm/ocaml/cic_transformations/ast2pres.ml | 613 ++++++++++++++---- helm/ocaml/cic_transformations/ast2pres.mli | 31 +- helm/ocaml/cic_transformations/box.ml | 58 +- helm/ocaml/cic_transformations/box.mli | 11 +- helm/ocaml/cic_transformations/boxPp.ml | 11 +- helm/ocaml/cic_transformations/boxPp.mli | 2 +- helm/ocaml/cic_transformations/cexpr2pres.ml | 473 -------------- helm/ocaml/cic_transformations/cexpr2pres.mli | 70 -- .../cic_transformations/cexpr2pres_hashtbl.ml | 497 -------------- .../cexpr2pres_hashtbl.mli | 49 -- .../ocaml/cic_transformations/content2pres.ml | 15 +- .../content_expressions.ml | 445 ------------- .../content_expressions.mli | 62 -- .../cic_transformations/mpresentation.ml | 6 +- .../ocaml/cic_transformations/sequent2pres.ml | 13 +- .../cic_transformations/sequent2pres.mli | 6 +- .../cic_transformations/tacticAst2Box.ml | 65 +- .../cic_transformations/tacticAst2Box.mli | 2 +- 23 files changed, 752 insertions(+), 1857 deletions(-) delete mode 100644 helm/ocaml/cic_transformations/cexpr2pres.ml delete mode 100644 helm/ocaml/cic_transformations/cexpr2pres.mli delete mode 100644 helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml delete mode 100644 helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli delete mode 100644 helm/ocaml/cic_transformations/content_expressions.ml delete mode 100644 helm/ocaml/cic_transformations/content_expressions.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 3678d39ba..8ec300590 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,12 +1,9 @@ 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 @@ -16,30 +13,24 @@ contentTable.cmo: cicAst.cmo contentTable.cmi 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 @@ -50,14 +41,10 @@ applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi 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 diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 95d86a7cd..ca3fe7324 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -1,24 +1,32 @@ 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 diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index 1bc76ebb8..24d2e07f3 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -25,6 +25,8 @@ open Printf +module Ast = CicAst + let symbol_table = Hashtbl.create 1024 let sort_of_string = function @@ -60,16 +62,18 @@ let constructor_of_inductive_type uri i j = 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); @@ -211,5 +215,82 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = 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) diff --git a/helm/ocaml/cic_transformations/acic2Ast.mli b/helm/ocaml/cic_transformations/acic2Ast.mli index 3db26629a..c0f1309bf 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.mli +++ b/helm/ocaml/cic_transformations/acic2Ast.mli @@ -25,8 +25,8 @@ 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) diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index ee01f55a9..e1b36ea5c 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -36,6 +36,10 @@ 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 = @@ -43,7 +47,7 @@ let mml_of_cic_sequent metasenv sequent = 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) @@ -65,7 +69,7 @@ let mml_of_cic_object ~explode_all uri acic 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))); @@ -80,7 +84,9 @@ let mml_of_cic_object ~explode_all uri acic | _ -> assert false ;; +(* let _ = Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount ;; +*) diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index 470019835..65e1c32c7 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -33,6 +33,7 @@ (**************************************************************************) module A = CicAst;; +module P = Mpresentation;; let symbol_table = Hashtbl.create 503;; let symbol_table_charcount = Hashtbl.create 503;; @@ -98,109 +99,172 @@ let is_big t = ((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 @@ -210,8 +274,8 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = | (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 = @@ -223,11 +287,11 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = (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? *) @@ -235,9 +299,9 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = 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); @@ -253,75 +317,364 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = | 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 "\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 "/"); diff --git a/helm/ocaml/cic_transformations/ast2pres.mli b/helm/ocaml/cic_transformations/ast2pres.mli index 32531a232..20e909869 100644 --- a/helm/ocaml/cic_transformations/ast2pres.mli +++ b/helm/ocaml/cic_transformations/ast2pres.mli @@ -32,24 +32,23 @@ (* *) (**************************************************************************) -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 diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_transformations/box.ml index 764a491eb..386fabd0b 100644 --- a/helm/ocaml/cic_transformations/box.ml +++ b/helm/ocaml/cic_transformations/box.ml @@ -49,32 +49,45 @@ let skip = Space([None,"width","1em"]);; 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 "\n" ; Xml.xml_cdata "\n"; Xml.xml_nempty ~prefix "box" @@ -84,6 +97,7 @@ let document_of_box pres = 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) diff --git a/helm/ocaml/cic_transformations/box.mli b/helm/ocaml/cic_transformations/box.mli index e4d4bbe76..8d65c27f0 100644 --- a/helm/ocaml/cic_transformations/box.mli +++ b/helm/ocaml/cic_transformations/box.mli @@ -48,7 +48,16 @@ val smallskip : 'expr box 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 diff --git a/helm/ocaml/cic_transformations/boxPp.ml b/helm/ocaml/cic_transformations/boxPp.ml index ea6813cf2..073bf633d 100644 --- a/helm/ocaml/cic_transformations/boxPp.ml +++ b/helm/ocaml/cic_transformations/boxPp.ml @@ -38,10 +38,17 @@ let to_string object_to_string b = 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))) diff --git a/helm/ocaml/cic_transformations/boxPp.mli b/helm/ocaml/cic_transformations/boxPp.mli index 98c693a0a..de984d26e 100644 --- a/helm/ocaml/cic_transformations/boxPp.mli +++ b/helm/ocaml/cic_transformations/boxPp.mli @@ -25,5 +25,5 @@ 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 diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml deleted file mode 100644 index 5789232bb..000000000 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ /dev/null @@ -1,473 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 28/6/2003 *) -(* *) -(**************************************************************************) - -module 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) -;; - - - diff --git a/helm/ocaml/cic_transformations/cexpr2pres.mli b/helm/ocaml/cic_transformations/cexpr2pres.mli deleted file mode 100644 index 376d459be..000000000 --- a/helm/ocaml/cic_transformations/cexpr2pres.mli +++ /dev/null @@ -1,70 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 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 diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml deleted file mode 100644 index 7cb3ba13c..000000000 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml +++ /dev/null @@ -1,497 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 28/6/2003 *) -(* *) -(**************************************************************************) - -module 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,"/")))) -;; diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli deleted file mode 100644 index 61c351963..000000000 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 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 -;; diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index a2a010f7d..1301d1017 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -53,7 +53,7 @@ let rec split n l = 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 @@ -126,7 +126,7 @@ let is_big_general countterm p = (size > maxsize) ;; -let is_big = is_big_general (Cexpr2pres.countterm) +let is_big = is_big_general (Ast2pres.countterm) ;; let get_xref = @@ -834,10 +834,21 @@ let content2pres term2pres (id,params,metasenv,obj) = | _ -> 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) diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml deleted file mode 100644 index 8c88fd01f..000000000 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ /dev/null @@ -1,445 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 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 -;; - - - - - - - - - - - diff --git a/helm/ocaml/cic_transformations/content_expressions.mli b/helm/ocaml/cic_transformations/content_expressions.mli deleted file mode 100644 index e945d96d2..000000000 --- a/helm/ocaml/cic_transformations/content_expressions.mli +++ /dev/null @@ -1,62 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 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 diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index a160c7e22..9ba9d848e 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -73,8 +73,8 @@ and mtd = Mtd of attr * mpres 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]);; @@ -102,7 +102,7 @@ let two_rows_table_without_brackets attr a b op = 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]) diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml index 2b159e1c8..57d7d9140 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.ml +++ b/helm/ocaml/cic_transformations/sequent2pres.ml @@ -92,13 +92,22 @@ let sequent2pres term2pres (_,_,context,ty) = 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) diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli index 669f4e1c0..5f4e5cf0c 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.mli +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -33,7 +33,7 @@ (***************************************************************************) 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 diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 4b79607f5..1d82c0aeb 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -40,8 +40,8 @@ let rec count_tactic current_size tac = 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 *) @@ -98,7 +98,7 @@ let is_big_tac tac = ;; (* prova *) -let rec small_tactic2box ?(attr = []) tac = +let rec small_tactic2box tac = Box.Text([], TacticAstPp.pp_tactic tac) let string_of_kind = function @@ -106,19 +106,32 @@ 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 = @@ -131,17 +144,15 @@ and big_tactic2box ?(attr = []) = function 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 @@ -160,25 +171,23 @@ and big_tactic2box ?(attr = []) = function | 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"); @@ -200,19 +209,17 @@ and big_tactic2box ?(attr = []) = function 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") @@ -221,12 +228,12 @@ and big_tactic2box ?(attr = []) = function | 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 diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.mli b/helm/ocaml/cic_transformations/tacticAst2Box.mli index 0eeef6c53..f9daa4270 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.mli +++ b/helm/ocaml/cic_transformations/tacticAst2Box.mli @@ -34,7 +34,7 @@ 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 -- 2.39.2