From f7b2e35a7bdadb4fdf0e640428e694703ddf67a5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 16 Jul 2003 14:12:02 +0000 Subject: [PATCH] Several changes (the beginning of a new era???) 1. stuff related to transformations (stylesheets and so on) moved from gTopLevel to the new library cic_transformations 2. porting of the stylesheets to old plain ocaml code by Andrea Asperti. Also in cic_transformations. Disclaimer: A. the ocaml transformations are still incomplete and under development. They are a bit more performant, though. (just a few order of magnitudes) B. the cic_transformation library seems a bit of a mess right now. Much clean-up needed. --- helm/gTopLevel/.depend | 53 +- helm/gTopLevel/Makefile | 35 +- helm/gTopLevel/content2cic.ml | 161 +++ helm/gTopLevel/content2cic.mli | 44 + helm/gTopLevel/eta_fixing.ml | 191 ++++ helm/gTopLevel/eta_fixing.mli | 28 + helm/gTopLevel/gTopLevel.ml | 5 +- helm/gTopLevel/rootcontent.xsl | 12 +- helm/gTopLevel/script.sh | 29 +- helm/gTopLevel/termViewer.ml | 71 +- helm/gTopLevel/termViewer.mli | 2 + helm/ocaml/.cvsignore | 1 + helm/ocaml/META.helm-cic_transformations.src | 5 + helm/ocaml/Makefile.in | 2 +- helm/ocaml/cic_transformations/.cvsignore | 1 + helm/ocaml/cic_transformations/.depend | 43 + helm/ocaml/cic_transformations/Makefile | 14 + .../cic_transformations}/applyStylesheets.ml | 0 .../cic_transformations}/applyStylesheets.mli | 0 helm/ocaml/cic_transformations/cexpr2pres.ml | 396 ++++++++ helm/ocaml/cic_transformations/cexpr2pres.mli | 70 ++ .../cic_transformations/cexpr2pres_hashtbl.ml | 419 ++++++++ .../cexpr2pres_hashtbl.mli | 49 + .../cic_transformations}/cic2Xml.ml | 0 .../cic_transformations}/cic2Xml.mli | 0 .../cic_transformations}/cic2acic.ml | 0 .../cic_transformations}/cic2acic.mli | 0 helm/ocaml/cic_transformations/cic2content.ml | 944 ++++++++++++++++++ .../ocaml/cic_transformations/cic2content.mli | 106 ++ .../ocaml/cic_transformations/content2pres.ml | 598 +++++++++++ .../cic_transformations/content2pres.mli | 46 + helm/ocaml/cic_transformations/contentPp.ml | 144 +++ helm/ocaml/cic_transformations/contentPp.mli | 28 + .../content_expressions.ml | 388 +++++++ .../content_expressions.mli | 60 ++ .../doubleTypeInference.ml | 0 .../doubleTypeInference.mli | 0 .../cic_transformations}/misc.ml | 0 .../cic_transformations}/misc.mli | 0 .../cic_transformations/mpresentation.ml | 218 ++++ .../cic_transformations/mpresentation.mli | 84 ++ .../cic_transformations}/sequentPp.ml | 0 .../cic_transformations}/sequentPp.mli | 0 .../cic_transformations}/xml2Gdome.ml | 0 .../cic_transformations}/xml2Gdome.mli | 0 .../cic_transformations/xml2Gdomexmath.ml | 111 ++ .../cic_transformations/xml2Gdomexmath.mli | 27 + 47 files changed, 4301 insertions(+), 84 deletions(-) create mode 100644 helm/gTopLevel/content2cic.ml create mode 100644 helm/gTopLevel/content2cic.mli create mode 100644 helm/gTopLevel/eta_fixing.ml create mode 100644 helm/gTopLevel/eta_fixing.mli create mode 100644 helm/ocaml/META.helm-cic_transformations.src create mode 100644 helm/ocaml/cic_transformations/.cvsignore create mode 100644 helm/ocaml/cic_transformations/.depend create mode 100644 helm/ocaml/cic_transformations/Makefile rename helm/{gTopLevel => ocaml/cic_transformations}/applyStylesheets.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/applyStylesheets.mli (100%) create mode 100644 helm/ocaml/cic_transformations/cexpr2pres.ml create mode 100644 helm/ocaml/cic_transformations/cexpr2pres.mli create mode 100644 helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml create mode 100644 helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli rename helm/{gTopLevel => ocaml/cic_transformations}/cic2Xml.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/cic2Xml.mli (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/cic2acic.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/cic2acic.mli (100%) create mode 100644 helm/ocaml/cic_transformations/cic2content.ml create mode 100644 helm/ocaml/cic_transformations/cic2content.mli create mode 100644 helm/ocaml/cic_transformations/content2pres.ml create mode 100644 helm/ocaml/cic_transformations/content2pres.mli create mode 100644 helm/ocaml/cic_transformations/contentPp.ml create mode 100644 helm/ocaml/cic_transformations/contentPp.mli create mode 100644 helm/ocaml/cic_transformations/content_expressions.ml create mode 100644 helm/ocaml/cic_transformations/content_expressions.mli rename helm/{gTopLevel => ocaml/cic_transformations}/doubleTypeInference.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/doubleTypeInference.mli (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/misc.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/misc.mli (100%) create mode 100644 helm/ocaml/cic_transformations/mpresentation.ml create mode 100644 helm/ocaml/cic_transformations/mpresentation.mli rename helm/{gTopLevel => ocaml/cic_transformations}/sequentPp.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/sequentPp.mli (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/xml2Gdome.ml (100%) rename helm/{gTopLevel => ocaml/cic_transformations}/xml2Gdome.mli (100%) create mode 100644 helm/ocaml/cic_transformations/xml2Gdomexmath.ml create mode 100644 helm/ocaml/cic_transformations/xml2Gdomexmath.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index de8a83a5c..e6194df96 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,49 +1,32 @@ -xml2Gdome.cmo: xml2Gdome.cmi -xml2Gdome.cmx: xml2Gdome.cmi -proofEngine.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi -proofEngine.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmi -doubleTypeInference.cmo: doubleTypeInference.cmi -doubleTypeInference.cmx: doubleTypeInference.cmi -cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi -cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi -cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi -cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi -cic2Xml.cmi: cic2acic.cmi +proofEngine.cmo: proofEngine.cmi +proofEngine.cmx: proofEngine.cmi +eta_fixing.cmo: eta_fixing.cmi +eta_fixing.cmx: eta_fixing.cmi +content2cic.cmo: content2cic.cmi +content2cic.cmx: content2cic.cmi logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi -sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi -sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi -misc.cmo: misc.cmi -misc.cmx: misc.cmi disambiguate.cmo: disambiguate.cmi disambiguate.cmx: disambiguate.cmi termEditor.cmo: disambiguate.cmi termEditor.cmi termEditor.cmx: disambiguate.cmx termEditor.cmi termEditor.cmi: disambiguate.cmi -texTermEditor.cmo: disambiguate.cmi misc.cmi texTermEditor.cmi -texTermEditor.cmx: disambiguate.cmx misc.cmx texTermEditor.cmi +texTermEditor.cmo: disambiguate.cmi texTermEditor.cmi +texTermEditor.cmx: disambiguate.cmx texTermEditor.cmi texTermEditor.cmi: disambiguate.cmi -applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ - applyStylesheets.cmi -applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ - applyStylesheets.cmi -applyStylesheets.cmi: cic2acic.cmi -termViewer.cmo: applyStylesheets.cmi cic2acic.cmi logicalOperations.cmi \ - misc.cmi termViewer.cmi -termViewer.cmx: applyStylesheets.cmx cic2acic.cmx logicalOperations.cmx \ - misc.cmx termViewer.cmi -termViewer.cmi: cic2acic.cmi +termViewer.cmo: logicalOperations.cmi termViewer.cmi +termViewer.cmx: logicalOperations.cmx termViewer.cmi invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ termViewer.cmi invokeTactics.cmi invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ termViewer.cmx invokeTactics.cmi invokeTactics.cmi: termEditor.cmi termViewer.cmi -hbugs.cmo: invokeTactics.cmi misc.cmi proofEngine.cmi hbugs.cmi -hbugs.cmx: invokeTactics.cmx misc.cmx proofEngine.cmx hbugs.cmi +hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi +hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi hbugs.cmi: invokeTactics.cmi -gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi hbugs.cmi \ - invokeTactics.cmi logicalOperations.cmi misc.cmi proofEngine.cmi \ - sequentPp.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi -gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx hbugs.cmx \ - invokeTactics.cmx logicalOperations.cmx misc.cmx proofEngine.cmx \ - sequentPp.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx +gTopLevel.cmo: eta_fixing.cmi hbugs.cmi invokeTactics.cmi \ + logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi \ + texTermEditor.cmi +gTopLevel.cmx: eta_fixing.cmx hbugs.cmx invokeTactics.cmx \ + logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx \ + texTermEditor.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index f5bc93d9f..6dfa38622 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -2,7 +2,8 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ helm-mathql helm-mathql_interpreter helm-mathql_generator \ - helm-tactics threads hbugs-client mathml-editor + helm-tactics threads hbugs-client mathml-editor \ + helm-cic_transformations PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLFIND = ocamlfind @@ -17,22 +18,18 @@ all: styles gTopLevel opt: styles gTopLevel.opt DEPOBJS = \ - xml2Gdome.ml xml2Gdome.mli proofEngine.ml proofEngine.mli \ - doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml cic2acic.mli\ - cic2Xml.ml cic2Xml.mli logicalOperations.ml logicalOperations.mli \ - sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \ - mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \ - disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \ - texTermEditor.ml texTermEditor.mli applyStylesheets.ml \ - applyStylesheets.mli termViewer.ml termViewer.mli invokeTactics.ml \ - invokeTactics.mli hbugs.ml hbugs.mli gTopLevel.ml + proofEngine.ml proofEngine.mli eta_fixing.ml eta_fixing.mli \ + content2cic.ml content2cic.mli logicalOperations.ml \ + logicalOperations.mli disambiguate.ml disambiguate.mli termEditor.ml \ + termEditor.mli texTermEditor.ml texTermEditor.mli termViewer.ml \ + termViewer.mli invokeTactics.ml invokeTactics.mli hbugs.ml hbugs.mli \ + gTopLevel.ml TOPLEVELOBJS = \ - xml2Gdome.cmo doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - proofEngine.cmo logicalOperations.cmo sequentPp.cmo \ - mQueryLevels2.cmo misc.cmo disambiguate.cmo \ - termEditor.cmo texTermEditor.cmo applyStylesheets.cmo termViewer.cmo \ - invokeTactics.cmo hbugs.cmo gTopLevel.cmo + doubleTypeInference.cmo eta_fixing.cmo content2cic.cmo \ + proofEngine.cmo logicalOperations.cmo \ + disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \ + invokeTactics.cmo hbugs.cmo gTopLevel.cmo styles: @echo "***********************************************************************" @@ -77,3 +74,11 @@ uninstall: ifneq ($(MAKECMDGOALS), depend) include .depend endif + + + + + + + + diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml new file mode 100644 index 000000000..17ba99ed8 --- /dev/null +++ b/helm/gTopLevel/content2cic.ml @@ -0,0 +1,161 @@ +(* 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 *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +exception TO_DO;; + +let proof2cic term2cic p = + let rec proof2cic premise_env p = + let module C = Cic in + let module Con = Cic2content in + let rec extend_premise_env current_env = + function + [] -> current_env + | p::atl -> + extend_premise_env + ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in + let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in + let body = conclude2cic new_premise_env p.Con.proof_conclude in + context2cic premise_env p.Con.proof_context body + + and context2cic premise_env context body = + List.fold_right (ce2cic premise_env) context body + + and ce2cic premise_env ce target = + let module C = Cic in + let module Con = Cic2content in + match ce with + Con.Declaration d -> + (match d.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic d.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target)) + | Con.Hypothesis h -> + (match h.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic h.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target)) + | Con.Proof p -> + (match p.Con.proof_name with + Some s -> + C.LetIn (C.Name s, proof2cic premise_env p, target) + | None -> + C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + | Con.Definition d -> + (match d.Con.def_name with + Some s -> + C.LetIn (C.Name s, proof2cic premise_env p, target) + | None -> + C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + | Con.Joint ho -> + raise TO_DO + + and conclude2cic premise_env conclude = + let module C = Cic in + let module Con = Cic2content in + if conclude.Con.conclude_method = "TD_Conversion" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2cic [] p (* empty! *) + | _ -> prerr_endline "1"; assert false) + else if conclude.Con.conclude_method = "BU_Conversion" then + (match conclude.Con.conclude_args with + [Con.Premise prem] -> + (try List.assoc prem.Con.premise_xref premise_env + with Not_found -> + prerr_endline ("Not_found: " ^ prem.Con.premise_xref); + raise Not_found) + | _ -> prerr_endline "2"; assert false) + else if conclude.Con.conclude_method = "Exact" then + (match conclude.Con.conclude_args with + [Con.Term t] -> term2cic t + | _ -> prerr_endline "3"; assert false) + else if conclude.Con.conclude_method = "Intros+LetTac" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2cic [] p (* empty! *) + | _ -> prerr_endline "4"; assert false) + else if (conclude.Con.conclude_method = "ByInduction") then + (match (List.tl conclude.Con.conclude_args) with + Con.Term (C.AAppl + id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> + let subst = + List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in + let cargs = args2cic premise_env args in + let cparams_and_IP = List.map term2cic params_and_IP in + C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs) + | _ -> prerr_endline "5"; assert false) + else if (conclude.Con.conclude_method = "Rewrite") then + (match conclude.Con.conclude_args with + Con.Term (C.AConst (sid,uri,exp_named_subst))::args -> + let subst = + List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in + let cargs = args2cic premise_env args in + C.Appl (C.Const(uri,subst)::cargs) + | _ -> prerr_endline "6"; assert false) + else if (conclude.Con.conclude_method = "Apply") then + let cargs = (args2cic premise_env conclude.Con.conclude_args) in + C.Appl cargs + else (prerr_endline "7"; assert false) + + and args2cic premise_env l = + List.map (arg2cic premise_env) l + + and arg2cic premise_env = + let module C = Cic in + let module Con = Cic2content in + function + Con.Aux n -> prerr_endline "8"; assert false + | Con.Premise prem -> + (match prem.Con.premise_n with + Some n -> + C.Rel n + | _ -> + (try List.assoc prem.Con.premise_xref premise_env + with Not_found -> + prerr_endline ("Not_found: " ^ prem.Con.premise_xref); + raise Not_found)) + | Con.Term t -> + term2cic t + | Con.ArgProof p -> + proof2cic [] p (* empty! *) + | Con.ArgMethod s -> raise TO_DO + +in proof2cic [] p +;; + + + + + + diff --git a/helm/gTopLevel/content2cic.mli b/helm/gTopLevel/content2cic.mli new file mode 100644 index 000000000..75f14dd7b --- /dev/null +++ b/helm/gTopLevel/content2cic.mli @@ -0,0 +1,44 @@ +(* 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 proof2cic : + (Cic.annterm -> Cic.term) -> + Cic.annterm Cic2content.proof -> Cic.term + + + + + + + diff --git a/helm/gTopLevel/eta_fixing.ml b/helm/gTopLevel/eta_fixing.ml new file mode 100644 index 000000000..c3b84b605 --- /dev/null +++ b/helm/gTopLevel/eta_fixing.ml @@ -0,0 +1,191 @@ +(* 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/. + *) + +exception ReferenceToVariable;; +exception RferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +let rec fix_lambdas_wrt_type ty te = + let module C = Cic in + let module S = CicSubstitution in +(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; *) + (* cast e altra porcheria ???? *) + match ty,te with + C.Prod (_,_,ty'), C.Lambda (n,s,te') -> + C.Lambda (n,s,fix_lambdas_wrt_type ty' te') + | C.Prod (_,s,ty'), C.Appl l -> + prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; + let l' = List.map (S.lift 1) l in + C.Lambda (C.Name "x",s, + fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1]))) + | C.Prod (_,s,ty'), _ -> + prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; + let te' = S.lift 1 te in + C.Lambda (C.Name "x",s, + fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1])) + | _, _ -> te +;; + +let fix_according_to_type ty hd tl = + let module C = Cic in + let module S = CicSubstitution in + let rec aux ty tl res = + (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); + flush stderr ; *) + match ty with + C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> + (match tl with + [] -> C.Appl res + | _ -> + prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); + flush stderr ; + C.LetIn + (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + | C.Cast (v,t) -> aux v tl res + | C.Prod (n,s,t) -> + (match tl with + [] -> + prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); + flush stderr ; + let res' = List.map (S.lift 1) res + in + C.Lambda + (C.Name "x", (* Andrea: to do: generate a fresh name *) + s, + aux t [] (res'@[C.Rel 1])) + | hd::tl' -> + let hd' = fix_lambdas_wrt_type s hd + in + aux (S.subst hd' t) tl' (res@[hd'])) + | C.Lambda _ -> assert false + | C.LetIn (n,s,t) -> aux (S.subst s t) tl res + | C.Appl _ + | C.Const _ + | C.MutInd _ + | C.MutConstruct _ + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> (* ???? *) + (match tl with + [] -> C.Appl res + | _ -> (* Andrea: to do: generate a fresh name *) + C.LetIn + (C.Name "H", + C.Appl res, + C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + in + aux ty tl [hd] +;; + +let eta_fix metasenv t = + let rec eta_fix' t = +(* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); + flush stderr ; *) + let module C = Cic in + match t with + C.Rel n -> C.Rel n + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (n,l) -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in + let l' = + List.map2 + (fun ct t -> + match (ct, t) with + None, _ -> None + | _, Some t -> Some (eta_fix' t) + | Some _, None -> assert false (* due to typing rules *)) + canonical_context l + in + C.Meta (n,l') + | C.Sort s -> C.Sort s + | C.Implicit -> C.Implicit + | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t) + | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t) + | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t) + | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t) + | C.Appl l -> + let l' = List.map eta_fix' l + in + (match l' with + C.Const(uri,exp_named_subst)::l'' -> + let constant_type = + (match CicEnvironment.get_obj uri with + C.Constant (_,_,ty,_) -> ty + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in + fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' + | _ -> C.Appl l' ) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.MutInd (uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.MutConstruct (uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> + C.MutCase (uri, tyno, eta_fix' outty, + eta_fix' term, List.map eta_fix' patterns) + | C.Fix (funno, funs) -> + C.Fix (funno, + List.map + (fun (name, no, ty, bo) -> + (name, no, eta_fix' ty, eta_fix' bo)) funs) + | C.CoFix (funno, funs) -> + C.CoFix (funno, + List.map + (fun (name, ty, bo) -> + (name, eta_fix' ty, eta_fix' bo)) funs) + in + eta_fix' t +;; + diff --git a/helm/gTopLevel/eta_fixing.mli b/helm/gTopLevel/eta_fixing.mli new file mode 100644 index 000000000..6da260aab --- /dev/null +++ b/helm/gTopLevel/eta_fixing.mli @@ -0,0 +1,28 @@ +(* 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/. + *) + +val eta_fix : Cic.metasenv -> Cic.term -> Cic.term + + diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index f1710cfce..0aefe5393 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -561,6 +561,9 @@ let refresh_proof (output : TermViewer.proof_viewer) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> + let bo_fixed = Eta_fixing.eta_fix metasenv bo in + let ty_fixed = Eta_fixing.eta_fix metasenv ty in + ProofEngine.proof := Some(uri,metasenv,bo_fixed,ty_fixed); if List.length metasenv = 0 then begin !qed_set_sensitive true ; @@ -574,7 +577,7 @@ prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ; end ; (*CSC: Wrong: [] is just plainly wrong *) uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, [])) in ignore (output#load_proof uri currentproof) with diff --git a/helm/gTopLevel/rootcontent.xsl b/helm/gTopLevel/rootcontent.xsl index 3adf8e223..96c92aeea 100644 --- a/helm/gTopLevel/rootcontent.xsl +++ b/helm/gTopLevel/rootcontent.xsl @@ -70,16 +70,8 @@ - - - - - - + + diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh index 29dd0a396..6be688132 100755 --- a/helm/gTopLevel/script.sh +++ b/helm/gTopLevel/script.sh @@ -1,19 +1,22 @@ #!/bin/bash -export OCAMLPATH=/projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib:/home/claudio/miohelm/helm/ocaml:/home/claudio/miohelm/helm:/home/claudio/miohelm/helm/hbugs/meta +#export OCAMLPATH=/projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib:/home/luca/miohelm/helm/ocaml:/home/luca/miohelm/helm:/home/luca/miohelm/helm/hbugs/meta:/home/luca/miohelm/helm/gTopLevel -export HELM_ANNOTATIONS_DIR=/home/claudio/miohelm/objects -export HELM_ANNOTATIONS_URL=file:///home/claudio/miohelm/objects -#export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081/ -#export HELM_PROCESSOR_URL=http://mowgli.cs.unibo.it:58080/ -export HELM_GETTER_URL=http://localhost:58081/ -export HELM_PROCESSOR_URL=http://localhost:58080/ +export OCAMLPATH=/home/asperti/helm/ocaml:/home/asperti/helm/hbugs/meta:/local/helm/galax/sources/natile-galax-0.1-alpha-installed/lib -export GTOPLEVEL_PROOFFILE=/public/sacerdot/currentproof -export GTOPLEVEL_PROOFFILETYPE=/public/sacerdot/currentprooftype -export GTOPLEVEL_INNERTYPESFILE=/public/sacerdot/innertypes -export GTOPLEVEL_CONSTANTTYPEFILE=/public/sacerdot/constanttype -export POSTGRESQL_CONNECTION_STRING="dbname=mowgli" -#export POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=mowgli user=helm password=awH21Un" +export HELM_ANNOTATIONS_DIR=/home/luca/miohelm/objects +export HELM_ANNOTATIONS_URL=file:///home/luca/miohelm/objects +export HELM_GETTER_URL=http://localhost:58081/ +export HELM_PROCESSOR_URL=http://localhost:8080/helm/servlet/uwobo/ +#export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081/ +#export HELM_PROCESSOR_URL=http://mowgli.cs.unibo.it:8081/mowgli/servlet/uwobo/ export HELM_TMP_DIR=/tmp + +export GTOPLEVEL_PROOFFILE=/tmp/asperti_currentproof +export GTOPLEVEL_PROOFFILETYPE=/tmp/asperti_currentprooftype +export GTOPLEVEL_INNERTYPESFILE=/tmp/asperti_innertypes +export GTOPLEVEL_CONSTANTTYPEFILE=/tmp/asperti_constanttype +export POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=mowgli user=helm password=awH21Un" +#export POSTGRESQL_CONNECTION_STRING="dbname=helm_mowgli_new_schema user=helm" +#export POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 9a9c9c9b8..192bbb413 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -33,6 +33,8 @@ (* *) (******************************************************************************) +let use_stylesheets = ref true;;(* false performs the transformations in OCaml*) + (* List utility functions *) exception Skip;; @@ -194,15 +196,62 @@ class proof_viewer obj = = Cic2acic.acic_object_of_cic_object currentproof in - let mml = - ApplyStylesheets.mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types - in - self#load_doc ~dom:mml ; - current_infos <- - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; - (acic, ids_to_inner_types, ids_to_inner_sorts) + if !use_stylesheets then + let mml = + ApplyStylesheets.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in + self#load_doc ~dom:mml ; + current_infos <- + Some + (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; + else + (match acic with + Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> + let time1 = Sys.time () in + let content = + Cic2content.acic2content + (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts + ~ids_to_inner_types bo in + let content2pres = + (Content2pres.proof2pres + (function p -> + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p)))) in + let pres = content2pres content in + let time2 = Sys.time () in + (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) + let xmlpres = + Xml.xml_nempty "math" + ["xmlns","http://www.w3.org/1998/Math/MathML" ; + "xmlns:helm","http://www.cs.unibo.it/helm" ; + "xmlns:xlink","http://www.w3.org/1999/xlink" + ] (Mpresentation.print_mpres pres) in + let time25 = Sys.time () in + (* + prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); + Xml.pp xmlpres (Some "tmp"); + let time3 = Sys.time () in + prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); + *) + (try + (* prerr_endline "(******** INIZIO DOM **********)"; *) + let mml = Xml2Gdomexmath.document_of_xml Misc.domImpl xmlpres in + let time3 = Sys.time () in + (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) + (* prerr_endline "(******** FINE DOM **********)"; *) + self#load_doc ~dom:mml; + prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2))) + (* + self#load_uri "tmp"; + let time4 = Sys.time () in + prerr_endline + ("Fine loading:" ^ (string_of_float (time4 -. time3))) + *) + with (GdomeInit.DOMException (_,s)) as e -> + prerr_endline s; raise e) + | _ -> assert false); + (acic, ids_to_inner_types, ids_to_inner_sorts) end ;; @@ -228,3 +277,7 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; + +let _ = + Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount +;; diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli index c043f5cb6..5a5105035 100644 --- a/helm/gTopLevel/termViewer.mli +++ b/helm/gTopLevel/termViewer.mli @@ -35,6 +35,8 @@ (** A widget to render sequents **) +val use_stylesheets: bool ref;; (* false performs the transformations in OCaml*) + class sequent_viewer : Gtk_mathview.math_view Gtk.obj -> object diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index dc4fce342..53ffeac63 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -15,6 +15,7 @@ META.helm-pxp META.helm-tactics META.helm-urimanager META.helm-xml +META.helm-cic_transformations Makefile Makefile.common autom4te.cache diff --git a/helm/ocaml/META.helm-cic_transformations.src b/helm/ocaml/META.helm-cic_transformations.src new file mode 100644 index 000000000..1888f9d39 --- /dev/null +++ b/helm/ocaml/META.helm-cic_transformations.src @@ -0,0 +1,5 @@ +requires="helm-xml helm-cic_proof_checking gdome2-xslt" +version="0.0.1" +archive(byte)="cic_transformations.cma" +archive(native)="cic_transformations.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index c53affed3..aaf8595b1 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,7 +2,7 @@ MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mathql_generator tactics + mathql_generator tactics cic_transformations OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic_transformations/.cvsignore b/helm/ocaml/cic_transformations/.cvsignore new file mode 100644 index 000000000..6b3eba302 --- /dev/null +++ b/helm/ocaml/cic_transformations/.cvsignore @@ -0,0 +1 @@ +*.cm[iaox] *.cmxa diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend new file mode 100644 index 000000000..2640418cd --- /dev/null +++ b/helm/ocaml/cic_transformations/.depend @@ -0,0 +1,43 @@ +cic2Xml.cmi: cic2acic.cmi +cic2content.cmi: cic2acic.cmi +contentPp.cmi: cic2content.cmi +cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi +content2pres.cmi: cic2content.cmi mpresentation.cmi +cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi +applyStylesheets.cmi: cic2acic.cmi +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi +cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi +cic2content.cmo: cic2acic.cmi cic2content.cmi +cic2content.cmx: cic2acic.cmx cic2content.cmi +content_expressions.cmo: cic2acic.cmi content_expressions.cmi +content_expressions.cmx: cic2acic.cmx content_expressions.cmi +contentPp.cmo: cic2content.cmi contentPp.cmi +contentPp.cmx: cic2content.cmx contentPp.cmi +mpresentation.cmo: mpresentation.cmi +mpresentation.cmx: mpresentation.cmi +cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi +cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi +content2pres.cmo: cexpr2pres.cmi cic2content.cmi mpresentation.cmi \ + content2pres.cmi +content2pres.cmx: cexpr2pres.cmx cic2content.cmx mpresentation.cmx \ + content2pres.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 +misc.cmo: misc.cmi +misc.cmx: misc.cmi +xml2Gdome.cmo: xml2Gdome.cmi +xml2Gdome.cmx: xml2Gdome.cmi +xml2Gdomexmath.cmo: xml2Gdomexmath.cmi +xml2Gdomexmath.cmx: xml2Gdomexmath.cmi +sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi +sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi +applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ + applyStylesheets.cmi +applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ + applyStylesheets.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile new file mode 100644 index 000000000..dae324ab3 --- /dev/null +++ b/helm/ocaml/cic_transformations/Makefile @@ -0,0 +1,14 @@ +PACKAGE = cic_transformations +REQUIRES = helm-xml helm-cic_proof_checking gdome2-xslt +PREDICATES = + +INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli cic2Xml.mli \ + cic2content.mli content_expressions.mli contentPp.mli \ + mpresentation.mli cexpr2pres.mli content2pres.mli \ + cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli \ + xml2Gdomexmath.mli sequentPp.mli applyStylesheets.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/ocaml/cic_transformations/applyStylesheets.ml similarity index 100% rename from helm/gTopLevel/applyStylesheets.ml rename to helm/ocaml/cic_transformations/applyStylesheets.ml diff --git a/helm/gTopLevel/applyStylesheets.mli b/helm/ocaml/cic_transformations/applyStylesheets.mli similarity index 100% rename from helm/gTopLevel/applyStylesheets.mli rename to helm/ocaml/cic_transformations/applyStylesheets.mli diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml new file mode 100644 index 000000000..841ccf3da --- /dev/null +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -0,0 +1,396 @@ +(* 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;; + +let symbol_table = Hashtbl.create 503;; +let symbol_table_charcount = Hashtbl.create 503;; + +let maxsize = 25;; + +let countterm current_size t = + let module CE = Content_expressions in + let rec aux 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) -> current_size + (String.length name) + | CE.Num (_,value) -> current_size + (String.length value) + | CE.Appl (_,l) -> + List.fold_left aux current_size l + | CE.Binder (_, _,(n,s),body) -> + let cs = aux (current_size + 2 + (String.length n)) s in + aux cs body + | CE.Letin (_,(n,s),body) -> + let cs = aux (current_size + 3 + (String.length n)) s in + aux cs body + | CE.Letrec (_,defs,body) -> + let cs = + List.fold_left + (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in + aux cs body + | CE.Case (_,a,np) -> + let cs = aux (current_size + 4) a in + List.fold_left + (fun c (n,bo) -> aux (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 + (aux c1 expr)) current_size subst + in + (aux current_size t) +;; + +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 -> (List.hd l1,s)::(make_attributes (List.tl l1) tl) +;; + +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 + ["helm:xref";"xlink:href"] [xref;uri] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow([],P.Mi (attr,name)::tail) + | CE.Symbol (xref,name,Some subst,uri) -> + let attr = + make_attributes + ["helm:xref";"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([],"]")::tail)) + | CE.LocalVar (xref,name) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow([],P.Mi (attr,name)::tail) + | CE.Meta (xref,name) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow([],P.Mi (attr,name)::tail) + | CE.Num (xref,value) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mn (attr,value) + else P.Mrow([],P.Mn (attr,value)::tail) + | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) -> + let aattr = make_attributes ["helm:xref"] [axref] in + let sattr = make_attributes ["helm:xref";"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([],")")::tail))) + | CE.Appl (xref,l) as t -> + let attr = make_attributes ["helm:xref"] [xref] in + P.Mrow(attr, + P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail)) + | CE.Binder (xref, kind,(n,s),body) -> + let attr = make_attributes ["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([("mathcolor","Blue")],binder):: + P.Mtext([],n ^ ":"):: + (aux s):: + P.Mo([],"."):: + (aux body)::tail) + | CE.Letin (xref,(n,s),body) -> + let attr = make_attributes ["helm:xref"] [xref] in + P.Mrow (attr, + P.Mtext([],("let ")):: + P.Mtext([],(n ^ "=")):: + (aux s):: + P.Mtext([]," in "):: + (aux body)::tail) + | CE.Letrec (xref,defs,body) -> + let attr = make_attributes ["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)::tail)) + | CE.Case (xref,a,np) -> + let attr = make_attributes ["helm:xref"] [xref] in + let rec make_patterns = + (function + [] -> [] + | [(n,p)] -> + [P.Mtext([],(n ^ " -> "));(aux p)] + | (n,p)::tl -> + P.Mtext([],(n ^ " -> ")):: + (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in + P.Mrow (attr, + P.Mtext([],("case ")):: + (aux a):: + P.Mtext([],(" of ")):: + (make_patterns np)@tail) in + aux t + +and + +make_args ?(priority = 0) ?(assoc = false) ?(tail = []) = + let module P = Mpresentation in + function + [] -> tail + | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl) +;; + +let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = + let module P = Mpresentation in + function + [] -> [] + | [a] -> + [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])] + | (a::tl) as l -> + let c = List.fold_left countterm 0 l in + if c > maxsize then + P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))]):: + (make_args_charcount ~tail:tail tl) + else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(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 = + 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 + ["helm:xref";"xlink:href"] [xref;uri] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow ([],P.Mi (attr,name)::tail) + | CE.Symbol (xref,name,Some subst,uri) -> + let attr = + make_attributes + ["helm:xref";"xlink:href"] [xref;uri] in + let rec make_subst = + (function + [] -> assert false + | [(uri,a)] -> + [(cexpr2pres a); + P.Mtext([],"/"); + P.Mi([],UriManager.name_of_uri uri)] + | (uri,a)::tl -> + (cexpr2pres 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([],"]")::tail)) + | CE.LocalVar (xref,name) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow ([],P.Mi (attr,name)::tail) + | CE.Meta (xref,name) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mi (attr,name) + else P.Mrow ([],P.Mi (attr,name)::tail) + | CE.Num (xref,value) -> + let attr = make_attributes ["helm:xref"] [xref] in + if tail = [] then + P.Mn (attr,value) + else P.Mrow ([],P.Mn (attr,value)::tail) + | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) -> + let aattr = make_attributes ["helm:xref"] [axref] in + let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in + if (is_big t) then + (try + (let f = Hashtbl.find symbol_table_charcount n in + f tl ~priority ~assoc ~tail aattr sattr) + with notfound -> + P.Mtable (aattr@P.standard_tbl_attr, + P.Mtr([],[P.Mtd([],P.Mrow([], + [P.Mtext([],"("); + cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))]):: + make_args_charcount ~tail:(P.Mtext([],")")::tail) tl)) + else cexpr2pres t + | CE.Appl (xref,l) as t -> + let attr = make_attributes ["helm:xref"] [xref] in + if (is_big t) then + P.Mtable (attr@P.standard_tbl_attr, + P.Mtr([],[P.Mtd([],P.Mrow([], + [P.Mtext([],"("); + cexpr2pres_charcount (List.hd l)]))]):: + make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l)) + else cexpr2pres t + | CE.Binder (xref, kind,(n,s),body) as t -> + if (is_big t) then + let attr = make_attributes ["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.Mtable (attr@P.standard_tbl_attr, + [P.Mtr ([],[P.Mtd ([], + P.Mrow([], + [P.Mtext([("mathcolor","Blue")],binder); + P.Mtext([],n ^ ":"); + cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]); + P.Mtr ([],[P.Mtd ([], + P.indented (cexpr2pres_charcount body ~tail:tail))])]) + else (cexpr2pres t ~tail:tail) + | CE.Letin (xref,(n,s),body) as t -> + if (is_big t) then + let attr = make_attributes ["helm:xref"] [xref] in + P.Mtable (attr@P.standard_tbl_attr, + [P.Mtr ([],[P.Mtd ([], + P.Mrow([], + [P.Mtext([("mathcolor","Blue")],"let"); + P.smallskip; + P.Mtext([],n ^ "="); + cexpr2pres_charcount s; + P.smallskip; + P.Mtext([],"in"); + ]))]); + P.Mtr ([],[P.Mtd ([], + P.indented (cexpr2pres_charcount body))])]) + else (cexpr2pres t) + | CE.Letrec (xref,defs,body) -> + let attr = make_attributes ["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)]) + | CE.Case (xref,a,np) -> + let attr = make_attributes ["helm:xref"] [xref] in + let rec make_patterns = + (function + [] -> [] + | [(n,p)] -> + [P.Mtext([],(n ^ " -> "));(aux p)] + | (n,p)::tl -> + P.Mtext([],(n ^ " -> ")):: + (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in + P.Mrow (attr, + P.Mtext([],("case ")):: + (aux a):: + P.Mtext([],(" of ")):: + (make_patterns np)) in + aux t +;; diff --git a/helm/ocaml/cic_transformations/cexpr2pres.mli b/helm/ocaml/cic_transformations/cexpr2pres.mli new file mode 100644 index 000000000..968e9a9cc --- /dev/null +++ b/helm/ocaml/cic_transformations/cexpr2pres.mli @@ -0,0 +1,70 @@ +(* 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:Mpresentation.mpres list -> + (string * string) list -> + (string * string) list -> + Mpresentation.mpres + ) Hashtbl.t + +val symbol_table_charcount : + (string, + Content_expressions.cexpr list -> + priority:int -> + assoc:bool -> + tail:Mpresentation.mpres list -> + (string * string) list -> + (string * string) list -> + Mpresentation.mpres + ) Hashtbl.t + +val maxsize : int +val countterm : int -> Content_expressions.cexpr -> int +val cexpr2pres : + ?priority:int -> + ?assoc:bool -> + ?tail:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres +val cexpr2pres_charcount : + ?priority:int -> + ?assoc:bool -> + ?tail:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml new file mode 100644 index 000000000..657464270 --- /dev/null +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml @@ -0,0 +1,419 @@ +(* 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 init + ~(cexpr2pres: + ?priority:int -> + ?assoc:bool -> + ?tail:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres) + ~(cexpr2pres_charcount: + ?priority:int -> + ?assoc:bool -> + ?tail:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres) += + +(* arrow *) +Hashtbl.add C2P.symbol_table "arrow" (binary + (fun a b ~priority ~assoc ~tail aattr sattr -> + if (priority > 5) || (priority = 5 && assoc) then + P.row_with_brackets aattr + (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a) + (cexpr2pres ~priority:5 ~assoc:true + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:true + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192)) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"=")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"=")) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:20 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:20 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227)) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:10 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:10 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228)) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:5 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:5 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4)) + else + P.two_rows_table_without_brackets 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([],[ + P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC); + cexpr2pres a;P.Mtext([],")")]))); + +(* leq *) +Hashtbl.add C2P.symbol_table "leq" (binary + (fun a b ~priority ~assoc ~tail aattr sattr -> + if (priority > 40) || (priority = 40 && assoc) then + P.row_with_brackets aattr + (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264)) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"<")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"<")) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265)) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,">")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:40 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,">")) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:60 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"+")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:60 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"+")) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:70 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"*")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:70 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"*")) + else + P.two_rows_table_without_brackets 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 + P.row_with_brackets aattr + (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a) + (cexpr2pres ~priority:60 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"-")) + else + P.row_without_brackets 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 + P.two_rows_table_with_brackets aattr + (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a) + (cexpr2pres_charcount ~priority:60 ~assoc:false + ~tail:(P.Mtext([],")")::tail) b) + (P.Mo(sattr,"-")) + else + P.two_rows_table_without_brackets 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 new file mode 100644 index 000000000..e6202582e --- /dev/null +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.mli @@ -0,0 +1,49 @@ +(* 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:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres) -> + cexpr2pres_charcount: + (?priority:int -> + ?assoc:bool -> + ?tail:Mpresentation.mpres list -> + Content_expressions.cexpr -> + Mpresentation.mpres) -> + unit +;; diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml similarity index 100% rename from helm/gTopLevel/cic2Xml.ml rename to helm/ocaml/cic_transformations/cic2Xml.ml diff --git a/helm/gTopLevel/cic2Xml.mli b/helm/ocaml/cic_transformations/cic2Xml.mli similarity index 100% rename from helm/gTopLevel/cic2Xml.mli rename to helm/ocaml/cic_transformations/cic2Xml.mli diff --git a/helm/gTopLevel/cic2acic.ml b/helm/ocaml/cic_transformations/cic2acic.ml similarity index 100% rename from helm/gTopLevel/cic2acic.ml rename to helm/ocaml/cic_transformations/cic2acic.ml diff --git a/helm/gTopLevel/cic2acic.mli b/helm/ocaml/cic_transformations/cic2acic.mli similarity index 100% rename from helm/gTopLevel/cic2acic.mli rename to helm/ocaml/cic_transformations/cic2acic.mli diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_transformations/cic2content.ml new file mode 100644 index 000000000..d4b729606 --- /dev/null +++ b/helm/ocaml/cic_transformations/cic2content.ml @@ -0,0 +1,944 @@ +(* 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 *) +(* 16/62003 *) +(* *) +(**************************************************************************) +type id = string;; +type recursion_kind = NoRecursive | Recursive | CoRecursive;; + +type 'term cobj = + Def of id * id option * string * (* name, *) + 'term option * 'term * (* body, type, *) + UriManager.uri list (* parameters *) + | Theorem of id * id option * string * (* name, *) + ('term proof) option * 'term * (* body, type, *) + UriManager.uri list (* parameters *) + | Variable of id * + string * 'term option * 'term * (* name, body, type *) + UriManager.uri list +(* (* parameters *) + | CurrentProof of id * id * + string * annmetasenv * (* name, conjectures, *) + 'term proof * 'term * UriManager.uri list (* value,type,parameters *) +*) + | InductiveDefinition of id * + 'term cinductiveType list * (* inductive types , *) + UriManager.uri list * int (* parameters,n ind. pars *) + +and 'term cinductiveType = + id * string * bool * 'term * (* typename, inductive, arity *) + 'term cconstructor list (* constructors *) + +and 'term cconstructor = + string * 'term (* id, type *) + +and + 'term proof = + { proof_name : string option; + proof_id : string ; + proof_kind : recursion_kind ; + proof_context : ('term context_element) list ; + proof_apply_context: ('term proof) list; + proof_conclude : 'term conclude_item; + } +and + 'term context_element = + Declaration of 'term declaration + | Hypothesis of 'term declaration + | Proof of 'term proof + | Definition of 'term definition + | Joint of 'term joint +and + 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +and + 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +and + 'term joint = + { joint_id : string ; + joint_kind : recursion_kind ; + joint_defs : 'term context_element list + } +and + 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } +and + 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) +and + premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + + +(* e se mettessi la conversione di BY nell'apply_context ? *) +(* sarebbe carino avere l'invariante che la proof2pres +generasse sempre prove con contesto vuoto *) + +let gen_id seed = + let res = "p" ^ string_of_int !seed in + incr seed ; + res +;; + +let name_of = function + Cic.Anonymous -> None + | Cic.Name b -> Some b;; + +exception Not_a_proof;; +exception NotImplemented;; +exception NotApplicable;; +exception ToDo;; + +(* we do not care for positivity, here, that in any case is enforced by + well typing. Just a brutal search *) + +let rec occur uri = + let module C = Cic in + function + C.Rel _ -> false + | C.Var _ -> false + | C.Meta _ -> false + | C.Sort _ -> false + | C.Implicit -> raise NotImplemented + | C.Prod (_,s,t) -> (occur uri s) or (occur uri t) + | C.Cast (te,ty) -> (occur uri te) + | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *) + | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t) + | C.Appl l -> + List.fold_left + (fun b a -> + if b then b + else (occur uri a)) false l + | C.Const (_,_) -> false + | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false + | C.MutConstruct (_,_,_,_) -> false + | C.MutCase _ -> false (* presuming too much?? *) + | C.Fix _ -> false (* presuming too much?? *) + | C.CoFix (_,_) -> false (* presuming too much?? *) +;; + +let get_id = + let module C = Cic in + function + C.ARel (id,_,_,_) -> id + | C.AVar (id,_,_) -> id + | C.AMeta (id,_,_) -> id + | C.ASort (id,_) -> id + | C.AImplicit _ -> raise NotImplemented + | C.AProd (id,_,_,_) -> id + | C.ACast (id,_,_) -> id + | C.ALambda (id,_,_,_) -> id + | C.ALetIn (id,_,_,_) -> id + | C.AAppl (id,_) -> id + | C.AConst (id,_,_) -> id + | C.AMutInd (id,_,_,_) -> id + | C.AMutConstruct (id,_,_,_,_) -> id + | C.AMutCase (id,_,_,_,_,_) -> id + | C.AFix (id,_,_) -> id + | C.ACoFix (id,_,_) -> id +;; + +let test_for_lifting ~ids_to_inner_types = + let module C = Cic in + let module C2A = Cic2acic in + (* atomic terms are never lifted, according to my policy *) + function + C.ARel (id,_,_,_) -> false + | C.AVar (id,_,_) -> false + | C.AMeta (id,_,_) -> false + | C.ASort (id,_) -> false + | C.AImplicit _ -> raise NotImplemented + | C.AProd (id,_,_,_) -> false + | C.ACast (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.ALambda (id,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.ALetIn (id,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AAppl (id,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AConst (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AMutInd (id,_,_,_) -> false + | C.AMutConstruct (id,_,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + (* oppure: false *) + | C.AMutCase (id,_,_,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AFix (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.ACoFix (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) +;; + +let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = + let module C = Cic in + let rec aux l subrpoofs = + match l with + [] -> [] + | t::l1 -> + if (test_for_lifting t ~ids_to_inner_types) then + (match subproofs with + [] -> assert false + | p::tl -> + let new_arg = + Premise + { premise_id = gen_id seed; + premise_xref = p.proof_id; + premise_binder = p.proof_name; + premise_n = None + } + in new_arg::(aux l1 tl)) + else + let hd = + (match t with + C.ARel (idr,idref,n,b) -> + let sort = + (try Hashtbl.find ids_to_inner_sorts idr + with notfound -> "Type") in + if sort ="Prop" then + Premise + { premise_id = gen_id seed; + premise_xref = idr; + premise_binder = Some b; + premise_n = Some n + } + else (Term t) + | _ -> (Term t)) in + hd::(aux l1 subproofs) + in aux l subproofs +;; + +(* transform a proof p into a proof list, concatenating the last +conclude element to the apply_context list, in case context is +empty. Otherwise, it just returns [p] *) + +let flat seed p = + if (p.proof_context = []) then + if p.proof_apply_context = [] then [p] + else + let p1 = + { proof_name = p.proof_name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = []; + proof_conclude = p.proof_conclude; + } in + p.proof_apply_context@[p1] + else + [p] +;; + +let rec serialize seed = + function + [] -> [] + | p::tl -> (flat seed p)@(serialize seed tl);; + +(* top_down = true if the term is a LAMBDA or a decl *) +let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = + let module C2A = Cic2acic in + let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected) + with Not_found -> None) + in + match exp with + None -> inner_proof + | Some expty -> + if inner_proof.proof_conclude.conclude_method = "Intros+LetTac" then + { proof_name = None ; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [] ; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "TD_Conversion"; + conclude_args = [ArgProof inner_proof]; + conclude_conclusion = Some expty + }; + } + else + { proof_name = None ; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [] ; + proof_apply_context = [inner_proof]; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "BU_Conversion"; + conclude_args = + [Premise + { premise_id = gen_id seed; + premise_xref = inner_proof.proof_id; + premise_binder = None; + premise_n = None + } + ]; + conclude_conclusion = Some expty + }; + } +;; + +let generate_exact seed t id name ~ids_to_inner_types = + let module C2A = Cic2acic in + { proof_name = name; + proof_id = id ; + proof_kind = NoRecursive; + proof_context = [] ; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Exact"; + conclude_args = [Term t]; + conclude_conclusion = + try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } +;; + +let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types = + let module C2A = Cic2acic in + let module C = Cic in + { proof_name = name; + proof_id = id ; + proof_kind = NoRecursive; + proof_context = [] ; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Intros+LetTac"; + conclude_args = [ArgProof inner_proof]; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> + (match inner_proof.proof_conclude.conclude_conclusion with + None -> None + | Some t -> + if is_intro then Some (C.AProd ("gen"^id,n,s,t)) + else Some (C.ALetIn ("gen"^id,n,s,t))) + }; + } +;; + +let build_decl_item seed id n s ~ids_to_inner_sorts = + let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in + if sort = "Prop" then + Hypothesis + { dec_name = name_of n; + dec_id = gen_id seed; + dec_inductive = false; + dec_aref = id; + dec_type = s + } + else + Declaration + { dec_name = name_of n; + dec_id = gen_id seed; + dec_inductive = false; + dec_aref = id; + dec_type = s + } +;; + +let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + else + Definition + { def_name = name_of n; + def_id = gen_id seed; + def_aref = id; + def_term = t + } + +(* the following function must be called with an object of sort +Prop. For debugging purposes this is tested again, possibly raising an +Not_a_proof exception *) + +and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = + let rec aux ?(name = None) t = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + let module C2A = Cic2acic in + let t1 = + match t with + C.ARel (id,idref,n,b) as t -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + generate_exact seed t id name ~ids_to_inner_types + else raise Not_a_proof + | C.AVar (id,uri,exp_named_subst) as t -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + generate_exact seed t id name ~ids_to_inner_types + else raise Not_a_proof + | C.AMeta (id,n,l) as t -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + generate_exact seed t id name ~ids_to_inner_types + else raise Not_a_proof + | C.ASort (id,s) -> raise Not_a_proof + | C.AImplicit _ -> raise NotImplemented + | C.AProd (_,_,_,_) -> raise Not_a_proof + | C.ACast (id,v,t) -> aux v + | C.ALambda (id,n,s,t) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + let proof = aux t ~name:None in + let proof' = + if proof.proof_conclude.conclude_method = "Intros+LetTac" then + match proof.proof_conclude.conclude_args with + [ArgProof p] -> p + | _ -> assert false + else proof in + let proof'' = + { proof_name = None; + proof_id = proof'.proof_id; + proof_kind = proof'.proof_kind ; + proof_context = + (build_decl_item seed id n s ids_to_inner_sorts):: + proof'.proof_context; + proof_apply_context = proof'.proof_apply_context; + proof_conclude = proof'.proof_conclude; + } + in + generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types + else raise Not_a_proof + | C.ALetIn (id,n,s,t) -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + let proof = aux t in + let proof' = + if proof.proof_conclude.conclude_method = "Intros+LetTac" then + match proof.proof_conclude.conclude_args with + [ArgProof p] -> p + | _ -> assert false + else proof in + let proof'' = + { proof_name = name; + proof_id = proof'.proof_id; + proof_kind = proof'.proof_kind ; + proof_context = + (build_def_item seed id n s ids_to_inner_sorts + ids_to_inner_types)::proof'.proof_context; + proof_apply_context = proof'.proof_apply_context; + proof_conclude = proof'.proof_conclude; + } + in + generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types + else raise Not_a_proof + | C.AAppl (id,li) -> + (try rewrite + seed name id li ids_to_inner_types ids_to_inner_sorts + with NotApplicable -> + try inductive + seed name id li ids_to_inner_types ids_to_inner_sorts + with NotApplicable -> + let args_to_lift = + List.filter (test_for_lifting ~ids_to_inner_types) li in + let subproofs = + match args_to_lift with + [_] -> List.map aux args_to_lift + | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + let args = build_args seed li subproofs + ~ids_to_inner_types ~ids_to_inner_sorts in + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = serialize seed subproofs; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Apply"; + conclude_args = args; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + }) + | C.AConst (id,uri,exp_named_subst) as t -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + generate_exact seed t id name ~ids_to_inner_types + else raise Not_a_proof + | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof + | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t -> + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + generate_exact seed t id name ~ids_to_inner_types + else raise Not_a_proof + | C.AMutCase (id,uri,typeno,ty,te,patterns) -> + let teid = get_id te in + let pp = List.map (function p -> (ArgProof (aux p))) patterns in + (match + (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized + with notfound -> None) + with + Some tety -> (* we must lift up the argument *) + let p = (aux te) in + { proof_name = Some "name"; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = flat seed p; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Case"; + conclude_args = (Term ty)::(Term te)::pp; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + | None -> + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Case"; + conclude_args = (Term ty)::(Term te)::pp; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + ) + | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> + let proof = (aux bo) in (* must be recursive !! *) + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [Proof proof]; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Exact"; + conclude_args = + [ Premise + { premise_id = gen_id seed; + premise_xref = proof.proof_id; + premise_binder = proof.proof_name; + premise_n = Some 1; + } + ]; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + | C.AFix (id, no, funs) -> + let proofs = + List.map (function (id1,n,_,ty,bo) -> (Proof (aux bo))) funs in + let jo = + { joint_id = gen_id seed; + joint_kind = Recursive; + joint_defs = proofs + } + in + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [Joint jo]; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Exact"; + conclude_args = + [ Premise + { premise_id = gen_id seed; + premise_xref = jo.joint_id; + premise_binder = Some "tiralo fuori"; + premise_n = Some no; + } + ]; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> + let proof = (aux bo) in (* must be recursive !! *) + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [Proof proof]; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Exact"; + conclude_args = + [ Premise + { premise_id = gen_id seed; + premise_xref = proof.proof_id; + premise_binder = proof.proof_name; + premise_n = Some 1; + } + ]; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + | C.ACoFix (id,no,funs) -> + let proofs = + List.map (function (id1,n,ty,bo) -> (Proof (aux bo))) funs in + let jo = + { joint_id = gen_id seed; + joint_kind = Recursive; + joint_defs = proofs + } + in + { proof_name = name; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = [Joint jo]; + proof_apply_context = []; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Exact"; + conclude_args = + [ Premise + { premise_id = gen_id seed; + premise_xref = jo.joint_id; + premise_binder = Some "tiralo fuori"; + premise_n = Some no; + } + ]; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + in + let id = get_id t in + generate_conversion seed false id t1 ~ids_to_inner_types +in aux ~name:name t + +and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = + let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in + let module C2A = Cic2acic in + let module C = Cic in + match li with + C.AConst (idc,uri,exp_named_subst)::args -> + let uri_str = UriManager.string_of_uri uri in + let suffix = Str.regexp_string "_ind.con" in + let len = String.length uri_str in + let n = (try (Str.search_backward suffix uri_str len) + with Not_found -> -1) in + if n<0 then raise NotApplicable + else + let prefix = String.sub uri_str 0 n in + let ind_str = (prefix ^ ".ind") in + let ind_uri = UriManager.uri_of_string ind_str in + let inductive_types,noparams = + (match CicEnvironment.get_obj ind_uri with + Cic.Constant _ -> assert false + | Cic.Variable _ -> assert false + | Cic.CurrentProof _ -> assert false + | Cic.InductiveDefinition (l,_,n) -> (l,n) + ) in + let rec split n l = + if n = 0 then ([],l) else + let p,a = split (n-1) (List.tl l) in + ((List.hd l::p),a) in + let params_and_IP,tail_args = split (noparams+1) args in + let constructors = + (match inductive_types with + [(_,_,_,l)] -> l + | _ -> raise NotApplicable) (* don't care for mutual ind *) in + let constructors1 = + let rec clean_up n t = + if n = 0 then t else + (match t with + (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t) + | _ -> assert false) in + List.map (clean_up noparams) constructors in + let no_constructors= List.length constructors in + let args_for_cases, other_args = + split no_constructors tail_args in + let args_to_lift = + List.filter (test_for_lifting ~ids_to_inner_types) other_args in + let subproofs = + match args_to_lift with + [_] -> List.map aux args_to_lift + | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + prerr_endline "****** end subproofs *******"; flush stderr; + let other_method_args = + build_args seed other_args subproofs + ~ids_to_inner_types ~ids_to_inner_sorts in +(* + let rparams,inductive_arg = + let rec aux = + function + [] -> assert false + | [ia] -> [],ia + | a::tl -> let (p,ia) = aux tl in (a::p,ia) in + aux other_method_args in +*) + prerr_endline "****** end other *******"; flush stderr; + let method_args= + let rec build_method_args = + function + [],_-> [] (* extra args are ignored ???? *) + | (name,ty)::tlc,arg::tla -> + let idarg = get_id arg in + let sortarg = + (try (Hashtbl.find ids_to_inner_sorts idarg) + with Not_found -> "Type") in + let hdarg = + if sortarg = "Prop" then + let (co,bo) = + let rec bc = + function + Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) -> + let ce = + build_decl_item + seed idl n s1 ~ids_to_inner_sorts in + if (occur ind_uri s) then + ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; + match t1 with + Cic.ALambda(id2,n2,s2,t2) -> + let inductive_hyp = + Hypothesis + { dec_name = name_of n2; + dec_id = gen_id seed; + dec_inductive = true; + dec_aref = id2; + dec_type = s2 + } in + let (context,body) = bc (t,t2) in + (ce::inductive_hyp::context,body) + | _ -> assert false) + else + ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; + let (context,body) = bc (t,t1) in + (ce::context,body)) + | _ , t -> ([],aux t ~name:None) in + bc (ty,arg) in + ArgProof + { proof_name = Some name; + proof_id = bo.proof_id; + proof_kind = NoRecursive; + proof_context = co; + proof_apply_context = bo.proof_apply_context; + proof_conclude = bo.proof_conclude; + }; + else (Term arg) in + hdarg::(build_method_args (tlc,tla)) + | _ -> assert false in + build_method_args (constructors1,args_for_cases) in + { proof_name = None; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = subproofs; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "ByInduction"; + conclude_args = + Aux no_constructors + ::Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) + ::method_args@other_method_args; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + | _ -> raise NotApplicable + +and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = + let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in + let module C2A = Cic2acic in + let module C = Cic in + match li with + C.AConst (sid,uri,exp_named_subst)::args -> + let uri_str = UriManager.string_of_uri uri in + if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or + uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then + let subproof = aux (List.nth args 3) in + let method_args = + let rec ma_aux n = function + [] -> [] + | a::tl -> + let hd = + if n = 0 then + Premise + { premise_id = gen_id seed; + premise_xref = subproof.proof_id; + premise_binder = None; + premise_n = None + } + else + let aid = get_id a in + let asort = (try (Hashtbl.find ids_to_inner_sorts aid) + with Not_found -> "Type") in + if asort = "Prop" then + ArgProof (aux a) + else Term a in + hd::(ma_aux (n-1) tl) in + (ma_aux 3 args) in + { proof_name = None; + proof_id = gen_id seed; + proof_kind = NoRecursive; + proof_context = []; + proof_apply_context = [subproof]; + proof_conclude = + { conclude_id = gen_id seed; + conclude_aref = id; + conclude_method = "Rewrite"; + conclude_args = + Term (C.AConst (sid,uri,exp_named_subst))::method_args; + conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + }; + } + else raise NotApplicable + | _ -> raise NotApplicable +;; + +let annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = + let module C = Cic in + let module C2A = Cic2acic in + let seed = ref 0 in + function + C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> + assert false (* TO DO *) + | C.AConstant (id,idbody,n,bo,ty,params) -> + (match idbody with + Some idb -> + let sort = + (try Hashtbl.find ids_to_inner_sorts idb + with notfound -> "Type") in + if sort = "Prop" then + let proof = + (match bo with + Some body -> + acic2content seed ~name:None ~ids_to_inner_sorts + ~ids_to_inner_types body + | None -> assert false) in + Theorem(id,idbody,n,Some proof,ty,params) + else + Def(id,idbody,n,bo,ty,params) + | None -> Def(id,idbody,n,bo,ty,params)) + | C.AVariable (id,n,bo,ty,params) -> + Variable(id,n,bo,ty,params) + | C.AInductiveDefinition (id,tys,params,nparams) -> + InductiveDefinition(id,tys,params,nparams) + +(* +and 'term cinductiveType = + id * string * bool * 'term * (* typename, inductive, arity *) + 'term cconstructor list (* constructors *) + +and 'term cconstructor = + string * 'term +*) + diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_transformations/cic2content.mli new file mode 100644 index 000000000..8e26bb897 --- /dev/null +++ b/helm/ocaml/cic_transformations/cic2content.mli @@ -0,0 +1,106 @@ +(* 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 *) +(* 16/62003 *) +(* *) +(**************************************************************************) + +type recursion_kind = NoRecursive | Recursive | CoRecursive;; + +type + 'term proof = + { proof_name : string option; + proof_id : string ; + proof_kind : recursion_kind ; + proof_context : ('term context_element) list ; + proof_apply_context: ('term proof) list; + proof_conclude : 'term conclude_item; + } +and + 'term context_element = + Declaration of 'term declaration + | Hypothesis of 'term declaration + | Proof of 'term proof + | Definition of 'term definition + | Joint of 'term joint +and + 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +and + 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +and + 'term joint = + { joint_id : string ; + joint_kind : recursion_kind ; + joint_defs : 'term context_element list + } +and + 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } +and + 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) +and + premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + +val acic2content : + int ref -> (* seed *) + ?name:string option -> (* name *) + ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> + (* ids_to_inner_sorts *) + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> + (* ids_to_inner_types *) + Cic.annterm -> (* annotated term *) + Cic.annterm proof diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml new file mode 100644 index 000000000..019538169 --- /dev/null +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -0,0 +1,598 @@ +(* 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 *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +let rec split n l = + if n = 0 then [],l + else let l1,l2 = + split (n-1) (List.tl l) in + (List.hd l)::l1,l2 +;; + + +let is_big_general countterm p = + let maxsize = Cexpr2pres.maxsize in + let module Con = Cic2content in + let rec countp current_size p = + if current_size > maxsize then current_size + else + let c1 = (countcontext current_size p.Con.proof_context) in + if c1 > maxsize then c1 + else + let c2 = (countapplycontext c1 p.Con.proof_apply_context) in + if c2 > maxsize then c2 + else + countconclude c2 p.Con.proof_conclude + + and + countcontext current_size c = + List.fold_left countcontextitem current_size c + and + countcontextitem current_size e = + if current_size > maxsize then maxsize + else + (match e with + Con.Declaration d -> + (match d.Con.dec_name with + Some s -> current_size + 4 + (String.length s) + | None -> prerr_endline "NO NAME!!"; assert false) + | Con.Hypothesis h -> + (match h.Con.dec_name with + Some s -> current_size + 4 + (String.length s) + | None -> prerr_endline "NO NAME!!"; assert false) + | Con.Proof p -> countp current_size p + | Con.Definition d -> + (match d.Con.def_name with + Some s -> + let c1 = (current_size + 4 + (String.length s)) in + (countterm c1 d.Con.def_term) + | None -> + prerr_endline "NO NAME!!"; assert false) + | Con.Joint ho -> maxsize + 1) (* we assume is big *) + and + countapplycontext current_size ac = + List.fold_left countp current_size ac + and + countconclude current_size co = + if current_size > maxsize then current_size + else + let c1 = countargs current_size co.Con.conclude_args in + if c1 > maxsize then c1 + else + (match co.Con.conclude_conclusion with + Some concl -> countterm c1 concl + | None -> c1) + and + countargs current_size args = + List.fold_left countarg current_size args + and + countarg current_size arg = + if current_size > maxsize then current_size + else + (match arg with + Con.Aux _ -> current_size + | Con.Premise prem -> + (match prem.Con.premise_binder with + Some s -> current_size + (String.length s) + | None -> current_size + 7) + | Con.Term t -> countterm current_size t + | Con.ArgProof p -> countp current_size p + | Con.ArgMethod s -> (maxsize + 1)) in + let size = (countp 0 p) in + (size > maxsize) +;; + +let is_big = is_big_general (Cexpr2pres.countterm) +;; + +let make_row items concl = + let module P = Mpresentation in + (match concl with + P.Mtable _ -> (* big! *) + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]); + P.Mtr ([],[P.Mtd ([],P.indented concl)])]) + | _ -> (* small *) + P.Mrow([],items@[P.Mspace([("width","0.1cm")]);concl])) +;; + +let make_concl verb concl = + let module P = Mpresentation in + (match concl with + P.Mtable _ -> (* big! *) + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr([],[P.Mtd ([],P.Mtext([("mathcolor","Red")],verb))]); + P.Mtr ([],[P.Mtd ([],P.indented concl)])]) + | _ -> (* small *) + P.Mrow([], + [P.Mtext([("mathcolor","Red")],verb); + P.Mspace([("width","0.1cm")]); + concl])) +;; + +let make_args_for_apply term2pres args = + let module Con = Cic2content in + let module P = Mpresentation in + let rec make_arg_for_apply is_first arg row = + (match arg with + Con.Aux n -> assert false + | Con.Premise prem -> + let name = + (match prem.Con.premise_binder with + None -> "previous" + | Some s -> s) in + P.Mi([],name)::row + | Con.Term t -> + if is_first then + (term2pres t)::row + else P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row + | Con.ArgProof _ + | Con.ArgMethod _ -> + P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row) in + match args with + hd::tl -> + make_arg_for_apply true hd + (List.fold_right (make_arg_for_apply false) tl []) + | _ -> assert false;; + +let rec justification term2pres p = + let module Con = Cic2content in + let module P = Mpresentation in + if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or + ((p.Con.proof_context = []) & + (p.Con.proof_apply_context = []) & + (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then + let pres_args = + make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in + P.Mrow([], + P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")]):: + P.Mo([],"(")::pres_args@[P.Mo([],")")]) + else proof2pres term2pres p + +and proof2pres term2pres p = + let rec proof2pres p = + let module Con = Cic2content in + let module P = Mpresentation in + let indent = + let is_decl e = + (match e with + Con.Declaration _ + | Con.Hypothesis _ -> true + | _ -> false) in + ((List.filter is_decl p.Con.proof_context) != []) in + let concl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> None + | Some t -> Some (term2pres t)) in + let body = + let presconclude = conclude2pres p.Con.proof_conclude indent in + let presacontext = + acontext2pres p.Con.proof_apply_context presconclude indent in + context2pres p.Con.proof_context presacontext in +(* + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + (context2pres_old p.Con.proof_context)@ + (acontext2pres_old p.Con.proof_apply_context indent)@ + [conclude2pres_old p.Con.proof_conclude indent]) in *) + match p.Con.proof_name with + None -> body + | Some name -> + let ac = + (match concl with + None -> P.Mtext([],"NO PROOF!!!") + | Some c -> c) in + let action = + P.Maction([("actiontype","toggle")], + [(make_concl "proof of" ac); + body]) in + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); + P.Mtr ([],[P.Mtd ([], P.indented action)])]) + + and context2pres c continuation = + let module P = Mpresentation in + List.fold_right + (fun ce continuation -> + P.Mtable([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr([],[P.Mtd ([],ce2pres ce)]); + P.Mtr([],[P.Mtd ([], continuation)])])) c continuation + + and context2pres_old c = + let module P = Mpresentation in + List.map + (function ce -> P.Mtr ([], [P.Mtd ([], ce2pres ce)])) c + + and ce2pres = + let module P = Mpresentation in + let module Con = Cic2content in + function + Con.Declaration d -> + (match d.Con.dec_name with + Some s -> + let ty = term2pres d.Con.dec_type in + P.Mrow ([], + [P.Mtext([("mathcolor","Red")],"Assume"); + P.Mspace([("width","0.1cm")]); + P.Mi([],s); + P.Mtext([],":"); + ty]) + | None -> + prerr_endline "NO NAME!!"; assert false) + | Con.Hypothesis h -> + (match h.Con.dec_name with + Some s -> + let ty = term2pres h.Con.dec_type in + P.Mrow ([], + [P.Mtext([("mathcolor","Red")],"Suppose"); + P.Mspace([("width","0.1cm")]); + P.Mtext([],"("); + P.Mi ([],s); + P.Mtext([],")"); + P.Mspace([("width","0.1cm")]); + ty]) + | None -> + prerr_endline "NO NAME!!"; assert false) + | Con.Proof p -> proof2pres p + | Con.Definition d -> + (match d.Con.def_name with + Some s -> + let term = term2pres d.Con.def_term in + P.Mrow ([], + [P.Mtext([],"Let "); + P.Mi([],s); + P.Mtext([]," = "); + term]) + | None -> + prerr_endline "NO NAME!!"; assert false) + | Con.Joint ho -> + P.Mtext ([],"jointdef") + + and acontext2pres ac continuation indent = + let module P = Mpresentation in + List.fold_right + (fun p continuation -> + let hd = + if indent then + P.indented (proof2pres p) + else + proof2pres p in + P.Mtable([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr([],[P.Mtd ([],hd)]); + P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation + + and acontext2pres_old ac indent = + let module P = Mpresentation in + List.map + (function p -> + if indent then + P.Mtr ([], [P.Mtd ([], P.indented (proof2pres p))]) + else + P.Mtr ([], + [P.Mtd ([], proof2pres p)])) ac + + and conclude2pres conclude indent = + let module P = Mpresentation in + if indent then + P.indented (conclude_aux conclude) + else + conclude_aux conclude + + and conclude2pres_old conclude indent = + let module P = Mpresentation in + if indent then + P.Mtr ([], [P.Mtd ([], P.indented (conclude_aux conclude))]) + else + P.Mtr ([], + [P.Mtd ([], conclude_aux conclude)]) + + and conclude_aux conclude = + let module Con = Cic2content in + let module P = Mpresentation in + if conclude.Con.conclude_method = "TD_Conversion" then + let expected = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO EXPECTED!!!") + | Some c -> term2pres c) in + let subproof = + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> p + | _ -> assert false) in + let synth = + (match subproof.Con.proof_conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO SYNTH!!!") + | Some c -> (term2pres c)) in + P.Mtable + ([("align","baseline 1");("equalrows","false");("columnalign","left")], + [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); + P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); + P.Mtr([],[P.Mtd([],proof2pres subproof)])]) + else if conclude.Con.conclude_method = "BU_Conversion" then + let conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO Conclusion!!!") + | Some c -> term2pres c) in + make_concl "that is equivalent to" conclusion + else if conclude.Con.conclude_method = "Exact" then + let conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO Conclusion!!!") + | Some c -> term2pres c) in + let arg = + (match conclude.Con.conclude_args with + [Con.Term t] -> term2pres t + | _ -> assert false) in + make_row + [arg;P.Mspace([("width","0.1cm")]);P.Mtext([],"proves")] conclusion + else if conclude.Con.conclude_method = "Intros+LetTac" then + let conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO Conclusion!!!") + | Some c -> term2pres c) in + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> + P.Mtable + ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr([],[P.Mtd([],proof2pres p)]); + P.Mtr([],[P.Mtd([], + (make_concl "we proved *" conclusion))])]); + | _ -> assert false) + else if (conclude.Con.conclude_method = "ByInduction") then + byinduction conclude + else if (conclude.Con.conclude_method = "Rewrite") then + let justif = + (match (List.nth conclude.Con.conclude_args 6) with + Con.ArgProof p -> justification term2pres p + | _ -> assert false) in + let term1 = + (match List.nth conclude.Con.conclude_args 2 with + Con.Term t -> term2pres t + | _ -> assert false) in + let term2 = + (match List.nth conclude.Con.conclude_args 5 with + Con.Term t -> term2pres t + | _ -> assert false) in + let conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"NO Conclusion!!!") + | Some c -> term2pres c) in + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ + P.Mtext([("mathcolor","Red")],"rewrite"); + P.Mspace([("width","0.1cm")]);term1; + P.Mspace([("width","0.1cm")]); + P.Mtext([("mathcolor","Red")],"with"); + P.Mspace([("width","0.1cm")]);term2]))]); + P.Mtr ([],[P.Mtd ([],P.indented justif)]); + P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])]) + else if conclude.Con.conclude_method = "Apply" then + let pres_args = + make_args_for_apply term2pres conclude.Con.conclude_args in + let by = + P.Mrow([], + P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")]):: + P.Mo([],"(")::pres_args@[P.Mo([],")")]) in + match conclude.Con.conclude_conclusion with + None -> P.Mrow([],[P.Mtext([],"QUA");by]) + | Some t -> + let concl = (term2pres t) in + let ann_concl = make_concl "we proved" concl in + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr ([],[P.Mtd ([],by)]); + P.Mtr ([],[P.Mtd ([],ann_concl)])]) + else let body = + P.Mtable + ([("align","baseline 1");("equalrows","false");("columnalign","left")], + [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); + P.Mtr ([], + [P.Mtd ([], + (P.indented + (P.Mtable + ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + args2pres conclude.Con.conclude_args))))])]) in + match conclude.Con.conclude_conclusion with + None -> body + | Some t -> + let concl = (term2pres t) in + let ann_concl = make_concl "we proved" concl in + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + [P.Mtr ([],[P.Mtd ([],body)]); + P.Mtr ([],[P.Mtd ([],ann_concl)])]) + + and args2pres l = + let module P = Mpresentation in + List.map + (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l + + and arg2pres = + let module P = Mpresentation in + let module Con = Cic2content in + function + Con.Aux n -> + P.Mtext ([],"aux " ^ string_of_int n) + | Con.Premise prem -> + P.Mtext ([],"premise") + | Con.Term t -> + term2pres t + | Con.ArgProof p -> + proof2pres p + | Con.ArgMethod s -> + P.Mtext ([],"method") + + and byinduction conclude = + let module P = Mpresentation in + let module Con = Cic2content in + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"No conclusion???") + | Some t -> term2pres t) in + let inductive_arg,args_for_cases = + (match conclude.Con.conclude_args with + Con.Aux(n)::_::tl -> + let l1,l2 = split n tl in + let last_pos = (List.length l2)-1 in + List.nth l2 last_pos,l1 + | _ -> assert false) in + let induction_on = + let arg = + (match inductive_arg with + Con.Aux n -> + P.Mtext ([],"an aux???") + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> P.Mtext ([],"the previous result") + | Some n -> P.Mi([],n)) + | Con.Term t -> + term2pres t + | Con.ArgProof p -> + P.Mtext ([],"a proof???") + | Con.ArgMethod s -> + P.Mtext ([],"a method???")) in + (make_concl "we proceede by induction on" arg) in + let to_prove = + (make_concl "to prove" proof_conclusion) in + let we_proved = + (make_concl "we proved" proof_conclusion) in + P.Mtable + ([("align","baseline 1");("equalrows","false");("columnalign","left")], + P.Mtr ([],[P.Mtd ([],induction_on)]):: + P.Mtr ([],[P.Mtd ([],to_prove)]):: + (make_cases args_for_cases) @ + [P.Mtr ([],[P.Mtd ([],we_proved)])]) + + and make_cases args_for_cases = + let module P = Mpresentation in + List.map + (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases + + and make_case = + let module P = Mpresentation in + let module Con = Cic2content in + function + Con.ArgProof p -> + let name = + (match p.Con.proof_name with + None -> P.Mtext([],"no name for case!!") + | Some n -> P.Mi([],n)) in + let indhyps,args = + List.partition + (function + Con.Hypothesis h -> h.Con.dec_inductive + | _ -> false) p.Con.proof_context in + let pattern_aux = + List.fold_right + (fun e p -> + let dec = + (match e with + Con.Declaration h + | Con.Hypothesis h -> + let name = + (match h.Con.dec_name with + None -> "NO NAME???" + | Some n ->n) in + [P.Mspace([("width","0.1cm")]); + P.Mi ([],name); + P.Mtext([],":"); + (term2pres h.Con.dec_type)] + | _ -> [P.Mtext ([],"???")]) in + dec@p) args [] in + let pattern = + P.Mtr ([],[P.Mtd ([],P.Mrow([], + P.Mtext([],"Case")::P.Mspace([("width","0.1cm")])::name::pattern_aux@ + [P.Mspace([("width","0.1cm")]); + P.Mtext([],"->")]))]) in + let subconcl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> P.Mtext([],"No conclusion!!!") + | Some t -> term2pres t) in + let asubconcl = + P.Mtr([],[P.Mtd([], + make_concl "the thesis becomes" subconcl)]) in + let induction_hypothesis = + (match indhyps with + [] -> [] + | _ -> + let text = + P.Mtr([],[P.Mtd([], P.indented + (P.Mtext([],"by induction hypothesis we know:")))]) in + let make_hyp = + function + Con.Hypothesis h -> + let name = + (match h.Con.dec_name with + None -> "no name" + | Some s -> s) in + P.indented (P.Mrow ([], + [P.Mtext([],"("); + P.Mi ([],name); + P.Mtext([],")"); + P.Mspace([("width","0.1cm")]); + term2pres h.Con.dec_type])) + | _ -> assert false in + let hyps = + List.map + (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) + indhyps in + text::hyps) in + (* let acontext = + acontext2pres_old p.Con.proof_apply_context true in *) + let body = conclude2pres p.Con.proof_conclude true in + let presacontext = + acontext2pres p.Con.proof_apply_context body true in + P.Mtable ([("align","baseline 1");("equalrows","false"); + ("columnalign","left")], + pattern::asubconcl::induction_hypothesis@ + [P.Mtr([],[P.Mtd([],presacontext)])]) + | _ -> assert false in + +proof2pres p +;; + +(* +let content2pres = + proof2pres + (function p -> Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr p)) +;; *) + + + diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli new file mode 100644 index 000000000..6a99f1b99 --- /dev/null +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -0,0 +1,46 @@ +(* 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 proof2pres : + ('a -> Mpresentation.mpres) -> + 'a Cic2content.proof -> + Mpresentation.mpres + +(* val content2pres : Cic.annterm Cic2content.proof -> Mpresentation.mpres *) + + + + + + diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml new file mode 100644 index 000000000..4206404f5 --- /dev/null +++ b/helm/ocaml/cic_transformations/contentPp.ml @@ -0,0 +1,144 @@ +(* 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 *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +exception ContentPpInternalError;; +exception NotEnoughElements;; + +(* Utility functions *) + + +let string_of_name = + function + Some s -> s + | None -> "_" +;; + +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise NotEnoughElements +;; + +let rec blanks n = + if n = 0 then "" + else (" " ^ (blanks (n-1)));; + +let rec pproof p indent = + let module Con = Cic2content in + let new_indent = + (match p.Con.proof_name with + Some s -> + prerr_endline + ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1) + | None ->indent) in + let new_indent1 = + if (p.Con.proof_context = []) then new_indent + else + (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in + papply_context p.Con.proof_apply_context new_indent1; + pconclude p.Con.proof_conclude new_indent1; + +and pcontext c indent = + List.iter (pcontext_element indent) c + +and pcontext_element indent = + let module Con = Cic2content in + function + Con.Declaration d -> + (match d.Con.dec_name with + Some s -> + prerr_endline + ((blanks indent) + ^ "Assume " ^ s ^ " : " + ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | Con.Hypothesis h -> + (match h.Con.dec_name with + Some s -> + prerr_endline + ((blanks indent) + ^ "Suppose " ^ s ^ " : " + ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | Con.Proof p -> pproof p indent + | Con.Definition d -> + (match d.Con.def_name with + Some s -> + prerr_endline + ((blanks indent) ^ "Let " ^ s ^ " = " + ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | Con.Joint ho -> + prerr_endline ((blanks indent) ^ "Joint Def"); + flush stderr + +and papply_context ac indent = + List.iter(function p -> (pproof p indent)) ac + +and pconclude concl indent = + let module Con = Cic2content in + prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr; + pargs concl.Con.conclude_args indent; + match concl.Con.conclude_conclusion with + None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr + | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr + +and pargs args indent = + List.iter (parg indent) args + +and parg indent = + let module Con = Cic2content in + function + Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr + | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr + | Con.Term t -> + prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t))); + flush stderr + | Con.ArgProof p -> pproof p (indent+1) + | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr + +;; + +let print_proof p = pproof p 0; + + diff --git a/helm/ocaml/cic_transformations/contentPp.mli b/helm/ocaml/cic_transformations/contentPp.mli new file mode 100644 index 000000000..ddaf76b23 --- /dev/null +++ b/helm/ocaml/cic_transformations/contentPp.mli @@ -0,0 +1,28 @@ +(* 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/. + *) + +val print_proof: Cic.annterm Cic2content.proof -> unit + + diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml new file mode 100644 index 000000000..bb062f9cc --- /dev/null +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -0,0 +1,388 @@ +(* 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 substitutons *) + +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 (* h:xref, name *) + | 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 +;; + +(* NOTATION *) + +let symbol_table = Hashtbl.create 503;; + +(* eq *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#(/1/0)" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "eq", + None, Some "cic:/Coq/Init/Logic/eq.ind#(/1/0)")) + :: List.map acic2cexpr (List.tl args)));; + +Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#(/1/0)" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "eq", + None, Some "cic:/Coq/Init/Logic/eqT.ind#(/1/0)")) + :: List.map acic2cexpr (List.tl args)));; + +(* and *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#(/1/0)" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "and", + None, Some "cic:/Coq/Init/Logic/and.ind#(/1/0)")) + :: List.map acic2cexpr args));; + +(* or *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#(/1/0)" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "or", + None, Some "cic:/Coq/Init/Logic/or.ind#(/1/0)")) + :: List.map acic2cexpr args));; + +(* iff *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "iff", + None, Some "cic:/Coq/Init/Logic/iff.con")) + :: List.map acic2cexpr args));; + +(* not *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "not", + None, Some "cic:/Coq/Init/Logic/not.con")) + :: List.map acic2cexpr args));; + +(* exists *) +Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#(/1/0)" + (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);; + +Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#(/1/0)" + (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 "cic:/Coq/Init/Peano/le.ind#(/1/0)" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "leq", + None, Some "cic:/Coq/Init/Peano/le.ind#(/1/0)")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "leq", + None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con")) + :: List.map acic2cexpr args));; + +(* lt *) +Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "lt", + None, Some "cic:/Coq/Init/Peano/lt.con")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "lt", + None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con")) + :: List.map acic2cexpr args));; + +(* geq *) +Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "geq", + None, Some "cic:/Coq/Init/Peano/ge.con")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "geq", + None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con")) + :: List.map acic2cexpr args));; + +(* gt *) +Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "gt", + None, Some "cic:/Coq/Init/Peano/gt.con")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "gt", + None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con")) + :: List.map acic2cexpr args));; + +(* plus *) +Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "plus", + None, Some "cic:/Coq/Init/Peano/plus.con")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "plus", + None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con")) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "plus", + None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con")) + :: List.map acic2cexpr args));; + +(* times *) +Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "times", + None, Some "cic:/Coq/Init/Peano/mult.con")) + :: List.map acic2cexpr args));; + + +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "times", + None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con")) + :: List.map acic2cexpr args));; +(* minus *) +Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "minus", + None, Some "cic:/Coq/Arith/Minus/mult.con")) + :: List.map acic2cexpr args));; + + + + +(* END NOTATION *) + + +let string_of_sort = + function + Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type -> "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) -> Meta (Some id,("?" ^ (string_of_int n))) + | 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) -> + (match n with + Cic.Anonymous -> assert false + | Cic.Name name -> + 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 notfound -> + 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 ^ "#(/1/" ^ (string_of_int i) ^ ")") in + (try + (let f = Hashtbl.find symbol_table puri_str in + f aid sid tl acic2cexpr) + with notfound -> + Appl (Some aid, Symbol (Some sid, name, + make_subst subst, Some puri_str)::List.map acic2cexpr tl)) + | C.AAppl (id,li) -> + Appl (Some id, List.map acic2cexpr li) + | C.AConst (id,uri,subst) -> + 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 + let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ ")") in + Symbol (Some id, name, make_subst subst, Some puri_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 + let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ "/" ^ (string_of_int j) ^ ")") in + Symbol (Some id, name, make_subst subst, Some puri_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 new file mode 100644 index 000000000..5eb2e503c --- /dev/null +++ b/helm/ocaml/cic_transformations/content_expressions.mli @@ -0,0 +1,60 @@ +(* 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 (* h:xref, name *) + | 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 +;; + + +val acic2cexpr : + (Cic.id, string) Hashtbl.t -> Cic.annterm -> cexpr diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/ocaml/cic_transformations/doubleTypeInference.ml similarity index 100% rename from helm/gTopLevel/doubleTypeInference.ml rename to helm/ocaml/cic_transformations/doubleTypeInference.ml diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/ocaml/cic_transformations/doubleTypeInference.mli similarity index 100% rename from helm/gTopLevel/doubleTypeInference.mli rename to helm/ocaml/cic_transformations/doubleTypeInference.mli diff --git a/helm/gTopLevel/misc.ml b/helm/ocaml/cic_transformations/misc.ml similarity index 100% rename from helm/gTopLevel/misc.ml rename to helm/ocaml/cic_transformations/misc.ml diff --git a/helm/gTopLevel/misc.mli b/helm/ocaml/cic_transformations/misc.mli similarity index 100% rename from helm/gTopLevel/misc.mli rename to helm/ocaml/cic_transformations/misc.mli diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml new file mode 100644 index 000000000..116b845b5 --- /dev/null +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -0,0 +1,218 @@ +(* 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 *) +(* 16/62003 *) +(* *) +(**************************************************************************) + +type + mpres = + (* token elements *) + Mi of attr * string + | Mn of attr * string + | Mo of attr * string + | Mtext of attr * string + | Mspace of attr + | Ms of attr * string + | Mgliph of attr * string + (* General Layout Schemata *) + | Mrow of attr * mpres list + | Mfrac of attr * mpres * mpres + | Msqrt of attr * mpres + | Mroot of attr * mpres * mpres + | Mstyle of attr * mpres + | Merror of attr * mpres + | Mpadded of attr * mpres + | Mphantom of attr * mpres + | Mfenced of attr * mpres list + | Menclose of attr * mpres + (* Script and Limit Schemata *) + | Msub of attr * mpres * mpres + | Msup of attr * mpres * mpres + | Msubsup of attr * mpres * mpres *mpres + | Munder of attr * mpres * mpres + | Mover of attr * mpres * mpres + | Munderover of attr * mpres * mpres *mpres +(* | Multiscripts of ??? NOT IMPLEMEMENTED *) + (* Tables and Matrices *) + | Mtable of attr * row list + (* Enlivening Expressions *) + | Maction of attr * mpres list + +and + + row = Mtr of attr * mtd list + +and + + mtd = Mtd of attr * mpres + +and + + attr = (string * string) list + +;; + +let smallskip = Mspace([("width","0.1cm")]);; +let indentation = Mspace([("width","0.3cm")]);; + +let indented elem = + Mrow([],[indentation;elem]);; + +let standard_tbl_attr = + [("align","baseline 1");("equalrows","false");("columnalign","left")];; + +let two_rows_table attr a b = + Mtable(attr@standard_tbl_attr, + [Mtr([],[Mtd([],a)]); + Mtr([],[Mtd([],b)])]);; + +let two_rows_table_with_brackets attr a b op = + (* only the open bracket is added; the closed bracket must be in b *) + Mtable(attr@standard_tbl_attr, + [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]); + Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + +let two_rows_table_without_brackets attr a b op = + Mtable(attr@standard_tbl_attr, + [Mtr([],[Mtd([],a)]); + Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);; + +let row_with_brackets attr a b op = + (* by analogy with two_rows_table_with_brackets we only add the + open brackets *) + Mrow(attr,[Mtext([],"(");a;smallskip;op;smallskip;b]) + +let row_without_brackets attr a b op = + Mrow(attr,[a;smallskip;op;smallskip;b]) + +let rec print_mpres = + let module X = Xml in + function + Mi (attr,s) -> X.xml_nempty "mi" attr (X.xml_cdata s) + | Mn (attr,s) -> X.xml_nempty "mn" attr (X.xml_cdata s) + | Mo (attr,s) -> X.xml_nempty "mo" attr (X.xml_cdata s) + | Mtext (attr,s) -> X.xml_nempty "mtext" attr (X.xml_cdata s) + | Mspace attr -> X.xml_empty "mspace" attr + | Ms (attr,s) -> X.xml_nempty "ms" attr (X.xml_cdata s) + | Mgliph (attr,s) -> X.xml_nempty "mgliph" attr (X.xml_cdata s) + (* General Layout Schemata *) + | Mrow (attr,l) -> + X.xml_nempty "mrow" attr + [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) + >] + | Mfrac (attr,m1,m2) -> + X.xml_nempty "mfrac" attr + [< print_mpres m1; + print_mpres m2 + >] + | Msqrt (attr,m) -> + X.xml_nempty "msqrt" attr [< print_mpres m >] + | Mroot (attr,m1,m2) -> + X.xml_nempty "mroot" attr + [< print_mpres m1; + print_mpres m2 + >] + | Mstyle (attr,m) -> + X.xml_nempty "mstyle" attr [< print_mpres m >] + | Merror (attr,m) -> + X.xml_nempty "merror" attr [< print_mpres m >] + | Mpadded (attr,m) -> + X.xml_nempty "mpadded" attr [< print_mpres m >] + | Mphantom (attr,m) -> + X.xml_nempty "mphantom" attr [< print_mpres m >] + | Mfenced (attr,l) -> + X.xml_nempty "mfenced" attr + [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) + >] + | Menclose (attr,m) -> + X.xml_nempty "menclose" attr [< print_mpres m >] + (* Script and Limit Schemata *) + | Msub (attr,m1,m2) -> + X.xml_nempty "msub" attr + [< print_mpres m1; + print_mpres m2 + >] + | Msup (attr,m1,m2) -> + X.xml_nempty "msup" attr + [< print_mpres m1; + print_mpres m2 + >] + | Msubsup (attr,m1,m2,m3) -> + X.xml_nempty "msubsup" attr + [< print_mpres m1; + print_mpres m2; + print_mpres m3 + >] + | Munder (attr,m1,m2) -> + X.xml_nempty "munder" attr + [< print_mpres m1; + print_mpres m2 + >] + | Mover (attr,m1,m2) -> + X.xml_nempty "mover" attr + [< print_mpres m1; + print_mpres m2 + >] + | Munderover (attr,m1,m2,m3) -> + X.xml_nempty "munderover" attr + [< print_mpres m1; + print_mpres m2; + print_mpres m3 + >] +(* | Multiscripts of ??? NOT IMPLEMEMENTED *) + (* Tables and Matrices *) + | Mtable (attr, rl) -> + X.xml_nempty "mtable" attr + [< (List.fold_right (fun x i -> [< (print_mrow x) ; i >]) rl [<>]) + >] + (* Enlivening Expressions *) + | Maction (attr, l) -> + X.xml_nempty "maction" attr + [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) + >] + +and print_mrow = + let module X = Xml in + function + Mtr (attr, l) -> + X.xml_nempty "mtr" attr + [< (List.fold_right (fun x i -> [< (print_mtd x) ; i >]) l [<>]) + >] + +and print_mtd = + let module X = Xml in + function + Mtd (attr,m) -> X.xml_nempty "mtd" attr (print_mpres m) +;; + + + + diff --git a/helm/ocaml/cic_transformations/mpresentation.mli b/helm/ocaml/cic_transformations/mpresentation.mli new file mode 100644 index 000000000..53eb9927e --- /dev/null +++ b/helm/ocaml/cic_transformations/mpresentation.mli @@ -0,0 +1,84 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type + mpres = + (* token elements *) + Mi of attr * string + | Mn of attr * string + | Mo of attr * string + | Mtext of attr * string + | Mspace of attr + | Ms of attr * string + | Mgliph of attr * string + (* General Layout Schemata *) + | Mrow of attr * mpres list + | Mfrac of attr * mpres * mpres + | Msqrt of attr * mpres + | Mroot of attr * mpres * mpres + | Mstyle of attr * mpres + | Merror of attr * mpres + | Mpadded of attr * mpres + | Mphantom of attr * mpres + | Mfenced of attr * mpres list + | Menclose of attr * mpres + (* Script and Limit Schemata *) + | Msub of attr * mpres * mpres + | Msup of attr * mpres * mpres + | Msubsup of attr * mpres * mpres *mpres + | Munder of attr * mpres * mpres + | Mover of attr * mpres * mpres + | Munderover of attr * mpres * mpres *mpres +(* | Multiscripts of ??? NOT IMPLEMEMENTED *) + (* Tables and Matrices *) + | Mtable of attr * row list + (* Enlivening Expressions *) + | Maction of attr * mpres list + +and + + row = Mtr of attr * mtd list + +and + + mtd = Mtd of attr * mpres + +and + + attr = (string * string) list + +;; + +val smallskip : mpres +val indented : mpres -> mpres +val standard_tbl_attr : attr +val two_rows_table : attr -> mpres -> mpres -> mpres +val two_rows_table_with_brackets : attr -> mpres -> mpres -> mpres -> mpres +val two_rows_table_without_brackets : attr -> mpres -> mpres -> mpres -> mpres +val row_with_brackets : attr -> mpres -> mpres -> mpres -> mpres +val row_without_brackets : attr -> mpres -> mpres -> mpres -> mpres +val print_mpres : + mpres -> Xml.token Stream.t + diff --git a/helm/gTopLevel/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml similarity index 100% rename from helm/gTopLevel/sequentPp.ml rename to helm/ocaml/cic_transformations/sequentPp.ml diff --git a/helm/gTopLevel/sequentPp.mli b/helm/ocaml/cic_transformations/sequentPp.mli similarity index 100% rename from helm/gTopLevel/sequentPp.mli rename to helm/ocaml/cic_transformations/sequentPp.mli diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/ocaml/cic_transformations/xml2Gdome.ml similarity index 100% rename from helm/gTopLevel/xml2Gdome.ml rename to helm/ocaml/cic_transformations/xml2Gdome.ml diff --git a/helm/gTopLevel/xml2Gdome.mli b/helm/ocaml/cic_transformations/xml2Gdome.mli similarity index 100% rename from helm/gTopLevel/xml2Gdome.mli rename to helm/ocaml/cic_transformations/xml2Gdome.mli diff --git a/helm/ocaml/cic_transformations/xml2Gdomexmath.ml b/helm/ocaml/cic_transformations/xml2Gdomexmath.ml new file mode 100644 index 000000000..0b2db0d99 --- /dev/null +++ b/helm/ocaml/cic_transformations/xml2Gdomexmath.ml @@ -0,0 +1,111 @@ +(* Copyright (C) 2000-2002, 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/. + *) + +(* cut and paste from xml2Gdome.ml: there was the namespace problem. + This is a fst patch: we generate a fixed namespace for math *) +let document_of_xml (domImplementation : Gdome.domImplementation) strm = + let module G = Gdome in + let module X = Xml in + let namespace = "http://www.w3.org/1998/Math/MathML" in + let root_name,root_attributes,root_content = + (* + ignore (Stream.next strm) ; (* to skip the declaration *) + ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *) + *) + match Stream.next strm with + X.Empty(n,l) -> n,l,[<>] + | X.NEmpty(n,l,c) -> n,l,c + | _ -> assert false + in + let document = + domImplementation#createDocument ~namespaceURI:(Some (Gdome.domString namespace)) + ~qualifiedName:(Gdome.domString ("m:" ^ root_name)) ~doctype:None + in + document#get_documentElement#setAttribute (Gdome.domString "xmlns:m") (Gdome.domString namespace); + let rec aux (node : Gdome.node) = + parser + [< 'X.Str a ; s >] -> + let textnode = document#createTextNode ~data:(Gdome.domString a) in + ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ; + aux node s + | [< 'X.Empty(n,l) ; s >] -> + let element = document#createElementNS + ~namespaceURI:(Some (Gdome.domString namespace)) + ~qualifiedName:(Gdome.domString ("m:" ^ n)) in + List.iter + (function (n,v) -> + let i = + (try String.index n ':' + with Not_found -> 0) in + if i = 0 then + element#setAttribute + ~name:(Gdome.domString n) ~value:(Gdome.domString v) + else + let ns_label = String.sub n 0 i in + let ns = + if ns_label = "helm" then "http://www.cs.unibo.it/helm" + else if ns_label = "xlink" then "http://www.w3.org/1999/xlink" + else assert false in + element#setAttributeNS + ~namespaceURI:(Some (Gdome.domString ns)) + ~qualifiedName:(Gdome.domString n) + ~value:(Gdome.domString v)) l ; + ignore + (node#appendChild ~newChild:(element : Gdome.element :> Gdome.node)) ; + aux node s + | [< 'X.NEmpty(n,l,c) ; s >] -> + let element = document#createElementNS + ~namespaceURI:(Some (Gdome.domString namespace)) + ~qualifiedName:(Gdome.domString ("m:" ^ n)) in + List.iter + (function (n,v) -> + let i = + (try String.index n ':' + with Not_found -> 0) in + if i = 0 then + element#setAttribute + ~name:(Gdome.domString n) ~value:(Gdome.domString v) + else + let ns_label = String.sub n 0 i in + let ns = + if ns_label = "helm" then "http://www.cs.unibo.it/helm" + else if ns_label = "xlink" then "http://www.w3.org/1999/xlink" + else assert false in + element#setAttributeNS + ~namespaceURI:(Some (Gdome.domString ns)) + ~qualifiedName:(Gdome.domString n) + ~value:(Gdome.domString v)) l ; + ignore (node#appendChild ~newChild:(element :> Gdome.node)) ; + aux (element :> Gdome.node) c ; + aux node s + | [< >] -> () + in + let root = document#get_documentElement in + List.iter (function (n,v) -> root#setAttribute + ~name:(Gdome.domString n) ~value:(Gdome.domString v)) root_attributes ; + aux (root : Gdome.element :> Gdome.node) root_content ; + document +;; + diff --git a/helm/ocaml/cic_transformations/xml2Gdomexmath.mli b/helm/ocaml/cic_transformations/xml2Gdomexmath.mli new file mode 100644 index 000000000..45d0e9532 --- /dev/null +++ b/helm/ocaml/cic_transformations/xml2Gdomexmath.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2000-2002, 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/. + *) + +val document_of_xml : + Gdome.domImplementation -> Xml.token Stream.t -> Gdome.document -- 2.39.2