+applyTransformation.cmo: applyTransformation.cmi
+applyTransformation.cmx: applyTransformation.cmi
+disambiguatePp.cmo: disambiguatePp.cmi
+disambiguatePp.cmx: disambiguatePp.cmi
dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo
dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx
matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \
matitamake.cmx: matitamakeLib.cmx matitaInit.cmx
matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
- buildTimeConf.cmo matitaMathView.cmi
+ buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi
matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \
- buildTimeConf.cmx matitaMathView.cmi
+ buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi
matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \
matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi
matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \
- matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi
+ matitaDisambiguator.cmi matitaDb.cmi disambiguatePp.cmi buildTimeConf.cmo \
+ matitaScript.cmi
matitaScript.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \
matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaEngine.cmx \
- matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmi
+ matitaDisambiguator.cmx matitaDb.cmx disambiguatePp.cmx buildTimeConf.cmx \
+ matitaScript.cmi
matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- matitaSync.cmi
+ disambiguatePp.cmi matitaSync.cmi
matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- matitaSync.cmi
+ disambiguatePp.cmx matitaSync.cmi
matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi
matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi
matitaDisambiguator.cmi: matitaTypes.cmi
matitaMisc.cmo \
matitaDb.cmo \
matitamakeLib.cmo \
- matitaInit.cmo \
+ matitaInit.cmo \
+ disambiguatePp.cmo \
matitaSync.cmo \
matitaDisambiguator.cmo \
matitaExcPp.cmo \
matitaScript.cmo \
matitaGeneratedGui.cmo \
matitaGtkMisc.cmo \
+ applyTransformation.cmo \
matitaMathView.cmo \
matitaGui.cmo \
$(NULL)
matitaMisc.cmo \
matitaDb.cmo \
matitamakeLib.cmo \
- matitaInit.cmo \
+ matitaInit.cmo \
+ disambiguatePp.cmo \
matitaSync.cmo \
matitaDisambiguator.cmo \
matitaExcPp.cmo \
--- /dev/null
+(* 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/.
+ *)
+
+(***************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Andrea Asperti <asperti@cs.unibo.it> *)
+(* 21/11/2003 *)
+(* *)
+(* *)
+(***************************************************************************)
+
+let mpres_document pres_box =
+ Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
+
+let mml_of_cic_sequent metasenv sequent =
+ let unsh_sequent,(asequent,ids_to_terms,
+ ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
+ =
+ Cic2acic.asequent_of_sequent metasenv sequent
+ in
+ let content_sequent = Acic2content.map_sequent asequent in
+ let pres_sequent =
+ (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
+ in
+ let xmlpres = mpres_document pres_sequent in
+ (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
+ unsh_sequent,
+ (asequent,
+ (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
+
+let mml_of_cic_object obj =
+ let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
+ =
+ Cic2acic.acic_object_of_cic_object obj
+ in
+ let content =
+ Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
+ in
+ let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
+ let xmlpres = mpres_document pres in
+ let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
+ (mathml,(annobj,
+ (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
+ ids_to_inner_sorts,ids_to_inner_types)))
+
--- /dev/null
+(* 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/.
+ *)
+
+(***************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Andrea Asperti <asperti@cs.unibo.it> *)
+(* 21/11/2003 *)
+(* *)
+(* *)
+(***************************************************************************)
+
+val mml_of_cic_sequent:
+ Cic.metasenv -> (* metasenv *)
+ Cic.conjecture -> (* sequent *)
+ Gdome.document * (* Math ML *)
+ Cic.conjecture * (* unshared sequent *)
+ (Cic.annconjecture * (* annsequent *)
+ ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *)
+
+val mml_of_cic_object:
+ Cic.obj -> (* object *)
+ Gdome.document * (* Math ML *)
+ (Cic.annobj * (* annobj *)
+ ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
+ (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *)
+
AC_MSG_ERROR(could not find camlp4o)
fi
FINDLIB_COMREQUIRES="\
-pcre \
-mysql \
-helm-registry \
-helm-extlib \
-helm-hmysql \
-helm-cic_notation \
-helm-tactics \
helm-cic_disambiguation \
-helm-cic_transformations \
+helm-grafite \
+helm-hgdome \
+helm-tactics \
"
FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES"
FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES"
lablgtkmathview \
lablgtksourceview \
helm-xmldiff \
-helm-cic_transformations \
-helm-tactics \
-helm-cic_disambiguation \
helm-paramodulation \
"
for r in $FINDLIB_REQUIRES
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open DisambiguateTypes
+
+let parse_environment str =
+ let stream = Ulexing.from_utf8_string str in
+ let environment = ref Environment.empty in
+ let multiple_environment = ref Environment.empty in
+ try
+ while true do
+ let alias =
+ match GrafiteParser.parse_statement stream with
+ GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
+ -> alias
+ | _ -> assert false in
+ let key,value =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in MatitaEngine *)
+ match alias with
+ GrafiteAst.Ident_alias (id,uri) ->
+ Id id,
+ (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+ | GrafiteAst.Symbol_alias (symb,instance,desc) ->
+ Symbol (symb,instance),
+ DisambiguateChoices.lookup_symbol_by_dsc symb desc
+ | GrafiteAst.Number_alias (instance,desc) ->
+ Num instance,
+ DisambiguateChoices.lookup_num_by_dsc desc
+ in
+ environment := Environment.add key value !environment;
+ multiple_environment := Environment.cons key value !multiple_environment;
+ done;
+ assert false
+ with End_of_file ->
+ !environment, !multiple_environment
+
+let alias_of_domain_and_codomain_items domain_item (dsc,_) =
+ match domain_item with
+ Id id -> GrafiteAst.Ident_alias (id, dsc)
+ | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
+ | Num i -> GrafiteAst.Number_alias (i, dsc)
+
+let aliases_of_environment env =
+ Environment.fold
+ (fun domain_item codomain_item acc ->
+ alias_of_domain_and_codomain_items domain_item codomain_item::acc
+ ) env []
+
+let aliases_of_domain_and_codomain_items_list l =
+ List.fold_left
+ (fun acc (domain_item,codomain_item) ->
+ alias_of_domain_and_codomain_items domain_item codomain_item::acc
+ ) [] l
+
+let pp_environment env =
+ let aliases = aliases_of_environment env in
+ let strings =
+ List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases
+ in
+ String.concat "\n" (List.sort compare strings)
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val parse_environment:
+ string ->
+ DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
+
+val aliases_of_domain_and_codomain_items_list:
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+ GrafiteAst.alias_spec list
+
+val pp_environment: DisambiguateTypes.environment -> string
let disambiguate_obj status obj =
let uri =
match obj with
- GrafiteAst.Inductive (_,(name,_,_,_)::_)
- | GrafiteAst.Record (_,name,_,_) ->
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) ->
Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
- | GrafiteAst.Inductive _ -> assert false
- | GrafiteAst.Theorem _ -> None in
+ | CicNotationPt.Inductive _ -> assert false
+ | CicNotationPt.Theorem _ -> None in
let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
if opts.do_heavy_checks then
begin
let dbd = MatitaDb.instance () in
- let similar = MetadataQuery.match_term ~dbd ty in
+ let similar = Whelp.match_term ~dbd ty in
let similar_len = List.length similar in
if similar_len> 30 then
(MatitaLog.message
in
let _, _, _, annterm = acic_sequent in
let ast, ids_to_uris =
- CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
+ TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
in
- let pped_ast = CicNotationRew.pp_ast ast in
+ let pped_ast = TermContentPres.pp_ast ast in
let markup = CicNotationPres.render ids_to_uris pped_ast in
BoxPp.render_to_string text_width markup
in
let current_proof_uri = BuildTimeConf.current_proof_uri
type term_source =
- [ `Ast of DisambiguateTypes.term
+ [ `Ast of CicNotationPt.term
| `Cic of Cic.term * Cic.metasenv
| `String of string
]
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
let term = disambiguate_macro_term term status user_goal in
- let l = MQ.match_term ~dbd term in
+ let l = Whelp.match_term ~dbd term in
let query_url =
MatitaMisc.strip_suffix ~suffix:"."
(HExtlib.trim_blanks unparsed_text)
[], parsed_text_length
| TA.WInstance (loc, term) ->
let term = disambiguate_macro_term term status user_goal in
- let l = MQ.instance ~dbd term in
+ let l = Whelp.instance ~dbd term in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WLocate (loc, s) ->
- let l = MQ.locate ~dbd s in
+ let l = Whelp.locate ~dbd s in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
| _ -> failwith "Not a MutInd"
in
- let l = MQ.elim ~dbd uri in
+ let l = Whelp.elim ~dbd uri in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
type options = option_value StringMap.t
let no_options = StringMap.empty
-type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list
type status = {
type options = option_value StringMap.t
val no_options : 'a StringMap.t
-type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
type status = {
projects / helm.git / commitdiff