From ebe70c001a623e0440f21cd16dc88f585edcf0ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Dec 2005 10:57:26 +0000 Subject: [PATCH] 1. matitaEngine splitted into disambiguation (now in grafite_parser) and in evaluation (now in grafite2) 2. .moo files are now grafite ASTs at the CIC level; they used to be at the content (or even presentation?) level 3. coq.ma is no longer a special file; added "-I .." in tests to make them include coq.ma Modified Files in ocaml: Makefile.in grafite/grafiteAst.ml grafite/grafiteAstPp.ml grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml grafite/grafiteMarshal.mli grafite/grafiteParser.ml grafite/grafiteParser.mli library/libraryClean.ml Modified Files in matita: .depend Makefile.in configure.ac coq.ma dump_moo.ml matita.ml matitaEngine.ml matitaEngine.mli matitaExcPp.ml matitaGtkMisc.ml matitaGui.ml matitaGuiTypes.mli matitaMathView.ml matitaMisc.ml matitaMisc.mli matitaScript.ml matitaScript.mli matitaTypes.ml matitaTypes.mli matitacLib.ml matitaclean.ml matitadep.ml tests/Makefile Added Files in ocaml: METAS/meta.helm-grafite2.src METAS/meta.helm-grafite_parser.src grafite2/.cvsignore grafite2/.depend grafite2/Makefile grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml grafite2/grafiteTypes.mli grafite2/matitaSync.ml grafite2/matitaSync.mli grafite_parser/.cvsignore grafite_parser/.depend grafite_parser/Makefile grafite_parser/grafiteDisambiguate.cmi grafite_parser/grafiteDisambiguate.cmo grafite_parser/grafiteDisambiguate.cmx grafite_parser/grafiteDisambiguate.ml grafite_parser/grafiteDisambiguate.mli grafite_parser/grafiteDisambiguate.o grafite_parser/grafite_parser.a grafite_parser/grafite_parser.cma grafite_parser/grafite_parser.cmxa grafite_parser/matitaDisambiguator.cmi grafite_parser/matitaDisambiguator.cmo grafite_parser/matitaDisambiguator.cmx grafite_parser/matitaDisambiguator.ml grafite_parser/matitaDisambiguator.mli grafite_parser/matitaDisambiguator.o Removed Files in matita: disambiguatePp.ml disambiguatePp.mli matitaDisambiguator.ml matitaDisambiguator.mli matitaSync.ml matitaSync.mli --- helm/matita/.depend | 77 ++- helm/matita/Makefile.in | 6 - helm/matita/configure.ac | 2 + helm/matita/coq.ma | 2 + helm/matita/disambiguatePp.ml | 83 --- helm/matita/disambiguatePp.mli | 34 -- helm/matita/dump_moo.ml | 2 +- helm/matita/matita.ml | 6 +- helm/matita/matitaDisambiguator.ml | 176 ------ helm/matita/matitaDisambiguator.mli | 53 -- helm/matita/matitaEngine.ml | 832 +--------------------------- helm/matita/matitaEngine.mli | 25 +- helm/matita/matitaExcPp.ml | 4 +- helm/matita/matitaGtkMisc.ml | 4 +- helm/matita/matitaGui.ml | 12 +- helm/matita/matitaGuiTypes.mli | 2 +- helm/matita/matitaMathView.ml | 11 +- helm/matita/matitaMisc.ml | 54 -- helm/matita/matitaMisc.mli | 10 - helm/matita/matitaScript.ml | 44 +- helm/matita/matitaScript.mli | 6 +- helm/matita/matitaSync.ml | 181 ------ helm/matita/matitaSync.mli | 49 -- helm/matita/matitaTypes.ml | 216 +------- helm/matita/matitaTypes.mli | 83 +-- helm/matita/matitacLib.ml | 18 +- helm/matita/matitaclean.ml | 4 +- helm/matita/matitadep.ml | 6 +- helm/matita/tests/Makefile | 2 +- 29 files changed, 117 insertions(+), 1887 deletions(-) delete mode 100644 helm/matita/disambiguatePp.ml delete mode 100644 helm/matita/disambiguatePp.mli delete mode 100644 helm/matita/matitaDisambiguator.ml delete mode 100644 helm/matita/matitaDisambiguator.mli delete mode 100644 helm/matita/matitaSync.ml delete mode 100644 helm/matita/matitaSync.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 368d18f28..cf6cf8522 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,45 +1,29 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi -disambiguatePp.cmo: disambiguatePp.cmi -disambiguatePp.cmx: disambiguatePp.cmi dump_moo.cmo: buildTimeConf.cmo dump_moo.cmx: buildTimeConf.cmx -matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi -matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitaTypes.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \ - matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi -matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx -matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi -matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi -matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi -matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi -matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi \ - matitaDisambiguator.cmi matitaEngine.cmi -matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx \ - matitaDisambiguator.cmx matitaEngine.cmi -matitaExcPp.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaExcPp.cmi -matitaExcPp.cmx: matitaTypes.cmx matitaDisambiguator.cmx matitaExcPp.cmi +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ + buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ + buildTimeConf.cmx +matitaEngine.cmo: matitaEngine.cmi +matitaEngine.cmx: matitaEngine.cmi +matitaExcPp.cmo: matitaExcPp.cmi +matitaExcPp.cmx: matitaExcPp.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ - matitaGeneratedGui.cmi matitaExcPp.cmi matitaDisambiguator.cmi \ - buildTimeConf.cmo matitaGui.cmi + matitaGeneratedGui.cmi matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ - matitaGeneratedGui.cmx matitaExcPp.cmx matitaDisambiguator.cmx \ - buildTimeConf.cmx matitaGui.cmi + matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi -matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi -matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ applyTransformation.cmi matitaMathView.cmi @@ -48,27 +32,28 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.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 \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ - buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ - buildTimeConf.cmx -matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaSync.cmi \ - matitaMisc.cmi matitaEngine.cmi matitaDisambiguator.cmi \ - disambiguatePp.cmi buildTimeConf.cmo matitaScript.cmi -matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaSync.cmx \ - matitaMisc.cmx matitaEngine.cmx matitaDisambiguator.cmx \ - disambiguatePp.cmx buildTimeConf.cmx matitaScript.cmi -matitaSync.cmo: matitaTypes.cmi disambiguatePp.cmi matitaSync.cmi -matitaSync.cmx: matitaTypes.cmx disambiguatePp.cmx matitaSync.cmi +matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi -matitaDisambiguator.cmi: matitaTypes.cmi -matitaEngine.cmi: matitaTypes.cmi +matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi +matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx +matitacLib.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx matitacLib.cmi +matitaclean.cmo: matitaInit.cmi matitaclean.cmi +matitaclean.cmx: matitaInit.cmx matitaclean.cmi +matitadep.cmo: matitaInit.cmi matitadep.cmi +matitadep.cmx: matitaInit.cmx matitadep.cmi +matitamake.cmo: matitamakeLib.cmi matitaInit.cmi +matitamake.cmx: matitamakeLib.cmx matitaInit.cmx +matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi +matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi -matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi +matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaScript.cmi: matitaTypes.cmi -matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 32eccedd4..9b7d720ac 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -40,9 +40,6 @@ CMOS = \ matitaMisc.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ - disambiguatePp.cmo \ - matitaSync.cmo \ - matitaDisambiguator.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ matitacLib.cmo \ @@ -60,9 +57,6 @@ CCMOS = \ matitaMisc.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ - disambiguatePp.cmo \ - matitaSync.cmo \ - matitaDisambiguator.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ matitacLib.cmo \ diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 21a02fbc4..2edd078bb 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -35,6 +35,8 @@ fi FINDLIB_COMREQUIRES="\ helm-cic_disambiguation \ helm-grafite \ +helm-grafite2 \ +helm-grafite_parser \ helm-hgdome \ helm-tactics \ " diff --git a/helm/matita/coq.ma b/helm/matita/coq.ma index 10a3de677..1b284799d 100644 --- a/helm/matita/coq.ma +++ b/helm/matita/coq.ma @@ -1,3 +1,5 @@ +set "baseuri" "cic:/Coq/". + (* aritmetic operators *) interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). diff --git a/helm/matita/disambiguatePp.ml b/helm/matita/disambiguatePp.ml deleted file mode 100644 index c3a48e409..000000000 --- a/helm/matita/disambiguatePp.ml +++ /dev/null @@ -1,83 +0,0 @@ -(* 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) diff --git a/helm/matita/disambiguatePp.mli b/helm/matita/disambiguatePp.mli deleted file mode 100644 index 69b6e8451..000000000 --- a/helm/matita/disambiguatePp.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* 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 diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml index 045a7b91b..cf872bdeb 100644 --- a/helm/matita/dump_moo.ml +++ b/helm/matita/dump_moo.ml @@ -48,7 +48,7 @@ let _ = let commands, metadata = GrafiteMarshal.load_moo ~fname in List.iter (fun cmd -> - printf " %s\n" (GrafiteAstPp.pp_command cmd); flush stdout) + printf " %s\n" (GrafiteAstPp.pp_cic_command cmd); flush stdout) commands; List.iter (fun m -> diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 33e2d14c0..0a83b737e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -26,7 +26,7 @@ open Printf open MatitaGtkMisc -open MatitaTypes +open GrafiteTypes (** {2 Initialization} *) @@ -141,7 +141,7 @@ let _ = let status = (MatitaScript.current ())#status in let moo, metadata = status.moo_content_rev in List.iter (fun cmd -> prerr_endline - (GrafiteAstPp.pp_command cmd)) (List.rev moo); + (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo); List.iter (fun m -> prerr_endline (GrafiteAstPp.pp_metadata m)) metadata); addDebugItem "print metasenv goals and stack to stderr" @@ -150,7 +150,7 @@ let _ = (List.map (fun (g, _, _) -> string_of_int g) (MatitaScript.current ())#proofMetasenv)); prerr_endline ("stack: " ^ Continuationals.Stack.pp - (MatitaTypes.get_stack (MatitaScript.current ())#status))); + (GrafiteTypes.get_stack (MatitaScript.current ())#status))); (* addDebugItem "ask record choice" (fun _ -> HLog.debug (string_of_int diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml deleted file mode 100644 index 325e290a7..000000000 --- a/helm/matita/matitaDisambiguator.ml +++ /dev/null @@ -1,176 +0,0 @@ -(* Copyright (C) 2004-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 Printf - -open MatitaTypes - -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * (Token.flocation option * string Lazy.t) list list - -type choose_uris_callback = - id:string -> UriManager.uri list -> UriManager.uri list - -type choose_interp_callback = (string * string) list list -> int list - -let mono_uris_callback ~id = - if Helm_registry.get_bool "matita.auto_disambiguation" then - function l -> l - else - raise Ambiguous_input - -let mono_interp_callback _ = raise Ambiguous_input - -let _choose_uris_callback = ref mono_uris_callback -let _choose_interp_callback = ref mono_interp_callback -let set_choose_uris_callback f = _choose_uris_callback := f -let set_choose_interp_callback f = _choose_interp_callback := f - -module Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - !_choose_uris_callback ~id uris - - let interactive_interpretation_choice interp = - !_choose_interp_callback interp - - let input_or_locate_uri ~(title:string) ?id = - (* Zack: I try to avoid using this callback. I therefore assume that - * the presence of an identifier that can't be resolved via "locate" - * query is a syntax error *) - let msg = match id with Some id -> id | _ -> "_" in - raise (Unbound_identifier msg) - end - -module Disambiguator = Disambiguate.Make (Callbacks) - -(* implement module's API *) - -let disambiguate_thing ~aliases ~universe - ~(f:?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - 'a -> 'b) - ~(drop_aliases: 'b -> 'b) - ~(drop_aliases_and_clear_diff: 'b -> 'b) - (thing: 'a) -= - assert (universe <> None); - let library = false, DisambiguateTypes.Environment.empty, None in - let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in - let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in - let passes = (* *) - [ (false, mono_aliases, false); - (false, multi_aliases, false); - (true, mono_aliases, false); - (true, multi_aliases, false); - (true, mono_aliases, true); - (true, multi_aliases, true); - (true, library, true); - ] - in - let try_pass (fresh_instances, (_, aliases, universe), use_coercions) = - CoercDb.use_coercions := use_coercions; - f ~fresh_instances ~aliases ~universe thing - in - let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = - if use_mono_aliases && not instances then - drop_aliases res - else if user_asked then - drop_aliases res (* one shot aliases *) - else - drop_aliases_and_clear_diff res - in - let rec aux errors = - function - | [ pass ] -> - (try - set_aliases pass (try_pass pass) - with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, errors @ [newerrors]))) - | hd :: tl -> - (try - set_aliases hd (try_pass hd) - with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> - aux (errors @ [newerrors]) tl) - | [] -> assert false - in - let saved_use_coercions = !CoercDb.use_coercions in - try - let res = aux [] passes in - CoercDb.use_coercions := saved_use_coercions; - res - with exn -> - CoercDb.use_coercions := saved_use_coercions; - raise exn - -type disambiguator_thing = - { do_it : - 'a 'b. - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - f:(?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> - 'a -> 'b * bool) -> - drop_aliases:('b * bool -> 'b * bool) -> - drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool - } - -let disambiguate_thing = - let profiler = HExtlib.profile "disambiguate_thing" in - { do_it = - fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing - -> profiler.HExtlib.profile - (disambiguate_thing ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff) thing - } - -let drop_aliases (choices, user_asked) = - (List.map (fun (d, a, b, c) -> d, a, b, c) choices), - user_asked - -let drop_aliases_and_clear_diff (choices, user_asked) = - (List.map (fun (_, a, b, c) -> [], a, b, c) choices), - user_asked - -let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph - ~aliases ~universe term - = - assert (fresh_instances = None); - let f = - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph - in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff term - -let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = - assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~dbd ~uri in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff obj diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli deleted file mode 100644 index 4cd1bd0dd..000000000 --- a/helm/matita/matitaDisambiguator.mli +++ /dev/null @@ -1,53 +0,0 @@ -(* Copyright (C) 2004-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 MatitaTypes - -(** raised when ambiguous input is found but not expected (e.g. in the batch - * compiler) *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * (Token.flocation option * string Lazy.t) list list - -type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = (string * string) list list -> int list - -val set_choose_uris_callback: choose_uris_callback -> unit -val set_choose_interp_callback: choose_interp_callback -> unit - -(** @raise Ambiguous_input if called, default value for internal - * choose_uris_callback if not set otherwise with set_choose_uris_callback - * above *) -val mono_uris_callback: choose_uris_callback - -(** @raise Ambiguous_input if called, default value for internal - * choose_interp_callback if not set otherwise with set_choose_interp_callback - * above *) -val mono_interp_callback: choose_interp_callback - -(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) - -include Disambiguate.Disambiguator diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index fc8e19621..e682adfcc 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -25,827 +25,11 @@ open Printf -open MatitaTypes - -exception Drop;; -exception UnableToInclude of string -exception IncludedFileNotCompiled of string +open GrafiteTypes let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -type options = { - do_heavy_checks: bool ; - include_paths: string list ; - clean_baseuri: bool -} - -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - -let tactic_of_ast ast = - let module PET = ProofEngineTypes in - match ast with - | GrafiteAst.Absurd (_, term) -> Tactics.absurd term - | GrafiteAst.Apply (_, term) -> Tactics.apply term - | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> - AutoTactic.auto_tac ?depth ?width ?paramodulation ?full - ~dbd:(LibraryDb.instance ()) () - | GrafiteAst.Change (_, pattern, with_what) -> - Tactics.change ~pattern with_what - | GrafiteAst.Clear (_,id) -> Tactics.clear id - | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id - | GrafiteAst.Contradiction _ -> Tactics.contradiction - | GrafiteAst.Compare (_, term) -> Tactics.compare term - | GrafiteAst.Constructor (_, n) -> Tactics.constructor n - | GrafiteAst.Cut (_, ident, term) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.DecideEquality _ -> Tactics.decide_equality - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = LibraryDb.instance () in - let mk_fresh_name_callback = namer_of names in - Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what - | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term - | GrafiteAst.Elim (_, what, using, depth, names) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what - | GrafiteAst.ElimType (_, what, using, depth, names) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what - | GrafiteAst.Exact (_, term) -> Tactics.exact term - | GrafiteAst.Exists _ -> Tactics.exists - | GrafiteAst.Fail _ -> Tactics.fail - | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> - let reduction = - match reduction_kind with - | `Normalize -> - PET.const_lazy_reduction - (CicReduction.normalize ~delta:false ~subst:[]) - | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce - | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl - | `Unfold None -> - PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) - | `Unfold (Some lazy_term) -> - (fun context metasenv ugraph -> - let what, metasenv, ugraph = lazy_term context metasenv ugraph in - ProofEngineReduction.unfold ~what, metasenv, ugraph) - | `Whd -> - PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[]) - in - Tactics.fold ~reduction ~term ~pattern - | GrafiteAst.Fourier _ -> Tactics.fourier - | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) - ~dbd:(LibraryDb.instance ()) hyp - | GrafiteAst.Generalize (_,pattern,ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern - | GrafiteAst.Goal (_, n) -> Tactics.set_goal n - | GrafiteAst.IdTac _ -> Tactics.id - | GrafiteAst.Injection (_,term) -> Tactics.injection term - | GrafiteAst.Intros (_, None, names) -> - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.Intros (_, Some num, names) -> - PrimitiveTactics.intros_tac ~howmany:num - ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many - ~to_what what - | GrafiteAst.Left _ -> Tactics.left - | GrafiteAst.LetIn (loc,term,name) -> - Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) - | GrafiteAst.Reduce (_, reduction_kind, pattern) -> - (match reduction_kind with - | `Normalize -> Tactics.normalize ~pattern - | `Reduce -> Tactics.reduce ~pattern - | `Simpl -> Tactics.simpl ~pattern - | `Unfold what -> Tactics.unfold ~pattern what - | `Whd -> Tactics.whd ~pattern) - | GrafiteAst.Reflexivity _ -> Tactics.reflexivity - | GrafiteAst.Replace (_, pattern, with_what) -> - Tactics.replace ~pattern ~with_what - | GrafiteAst.Rewrite (_, direction, t, pattern) -> - EqualityTactics.rewrite_tac ~direction ~pattern t - | GrafiteAst.Right _ -> Tactics.right - | GrafiteAst.Ring _ -> Tactics.ring - | GrafiteAst.Split _ -> Tactics.split - | GrafiteAst.Symmetry _ -> Tactics.symmetry - | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term - -let singleton = function - | [x], _ -> x - | _ -> assert false - - (** @param term not meaningful when context is given *) -let disambiguate_term ?context status_ref goal term = - let status = !status_ref in - let context = - match context with - | Some c -> c - | None -> MatitaTypes.get_proof_context status goal - in - let (diff, metasenv, cic, _) = - singleton - (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) - ~aliases:status.aliases ~universe:(Some status.multi_aliases) - ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term) - in - let status = MatitaTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status diff in - status_ref := status; - cic - - (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term - * rationale: lazy_term will be invoked in different context to obtain a term, - * each invocation will disambiguate the term and can add aliases. Once all - * disambiguations have been performed, the first returned function can be - * used to obtain the resulting aliases *) -let disambiguate_lazy_term status_ref term = - (fun context metasenv ugraph -> - let status = !status_ref in - let (diff, metasenv, cic, ugraph) = - singleton - (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) - ~initial_ugraph:ugraph ~aliases:status.aliases - ~universe:(Some status.multi_aliases) ~context ~metasenv term) - in - let status = MatitaTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status diff in - status_ref := status; - cic, metasenv, ugraph) - -let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = - let interp path = Disambiguate.interpretate_path [] path in - let goal_path = interp goal_path in - let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - let wanted = - match wanted with - None -> None - | Some wanted -> - let wanted = disambiguate_lazy_term status_ref wanted in - Some wanted - in - (wanted, hyp_paths ,goal_path) - -let disambiguate_reduction_kind aliases_ref = function - | `Unfold (Some t) -> - let t = disambiguate_lazy_term aliases_ref t in - `Unfold (Some t) - | `Normalize - | `Reduce - | `Simpl - | `Unfold None - | `Whd as kind -> kind - -let disambiguate_tactic status goal tactic = - let status_ref = ref status in - let tactic = - match tactic with - | GrafiteAst.Absurd (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Absurd (loc, cic) - | GrafiteAst.Apply (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Apply (loc, cic) - | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> - GrafiteAst.Auto (loc,depth,width,paramodulation,full) - | GrafiteAst.Change (loc, pattern, with_what) -> - let with_what = disambiguate_lazy_term status_ref with_what in - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Change (loc, pattern, with_what) - | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id) - | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compare (loc,term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Compare (loc,term) - | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n) - | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc - | GrafiteAst.Cut (loc, ident, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc - | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate types = function - | GrafiteAst.Type _ -> assert false - | GrafiteAst.Ident id -> - (match disambiguate_term status_ref goal - (CicNotationPt.Ident (id, None)) - with - | Cic.MutInd (uri, tyno, _) -> - (GrafiteAst.Type (uri, tyno) :: types) - | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]]))) - in - let types = List.fold_left disambiguate [] types in - GrafiteAst.Decompose (loc, types, what, names) - | GrafiteAst.Discriminate (loc,term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Discriminate(loc,term) - | GrafiteAst.Exact (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Exact (loc, cic) - | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref goal what in - let using = disambiguate_term status_ref goal using in - GrafiteAst.Elim (loc, what, Some using, depth, idents) - | GrafiteAst.Elim (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref goal what in - GrafiteAst.Elim (loc, what, None, depth, idents) - | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref goal what in - let using = disambiguate_term status_ref goal using in - GrafiteAst.ElimType (loc, what, Some using, depth, idents) - | GrafiteAst.ElimType (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref goal what in - GrafiteAst.ElimType (loc, what, None, depth, idents) - | GrafiteAst.Exists loc -> GrafiteAst.Exists loc - | GrafiteAst.Fail loc -> GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,red_kind, term, pattern) -> - let pattern = disambiguate_pattern status_ref pattern in - let term = disambiguate_lazy_term status_ref term in - let red_kind = disambiguate_reduction_kind status_ref red_kind in - GrafiteAst.Fold (loc, red_kind, term, pattern) - | GrafiteAst.FwdSimpl (loc, hyp, names) -> - GrafiteAst.FwdSimpl (loc, hyp, names) - | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc - | GrafiteAst.Generalize (loc,pattern,ident) -> - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Generalize (loc,pattern,ident) - | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g) - | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc - | GrafiteAst.Injection (loc, term) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.Injection (loc,term) - | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) - | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> - let f term to_what = - let term = disambiguate_term status_ref goal term in - term :: to_what - in - let to_what = List.fold_right f to_what [] in - let what = disambiguate_term status_ref goal what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) - | GrafiteAst.Left loc -> GrafiteAst.Left loc - | GrafiteAst.LetIn (loc, term, name) -> - let term = disambiguate_term status_ref goal term in - GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, red_kind, pattern) -> - let pattern = disambiguate_pattern status_ref pattern in - let red_kind = disambiguate_reduction_kind status_ref red_kind in - GrafiteAst.Reduce(loc, red_kind, pattern) - | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc - | GrafiteAst.Replace (loc, pattern, with_what) -> - let pattern = disambiguate_pattern status_ref pattern in - let with_what = disambiguate_lazy_term status_ref with_what in - GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern) -> - let term = disambiguate_term status_ref goal t in - let pattern = disambiguate_pattern status_ref pattern in - GrafiteAst.Rewrite (loc, dir, term, pattern) - | GrafiteAst.Right loc -> GrafiteAst.Right loc - | GrafiteAst.Ring loc -> GrafiteAst.Ring loc - | GrafiteAst.Split loc -> GrafiteAst.Split loc - | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc - | GrafiteAst.Transitivity (loc, term) -> - let cic = disambiguate_term status_ref goal term in - GrafiteAst.Transitivity (loc, cic) - in - status_ref, tactic - -let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= - let module PEH = ProofEngineHelpers in -(* let print_m name metasenv = - prerr_endline (">>>>> " ^ name); - prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) - in *) - (* phase one calculates: - * new_goals_from_refine: goals added by refine - * head_goal: the first goal opened by ythe tactic - * other_goals: other goals opened by the tactic - *) - let new_goals_from_refine = PEH.compare_metasenvs start refine in - let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in - let head_goal, other_goals, goals = - match goals with - | [] -> None,[],goals - | hd::tl -> - (* assert (List.mem hd new_goals_from_tactic); - * invalidato dalla goal_tac - * *) - Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>) - hd) goals - in - let produced_goals = - match head_goal with - | None -> new_goals_from_refine @ other_goals - | Some x -> x :: new_goals_from_refine @ other_goals - in - (* extract the metas generated by refine and tactic *) - let metas_for_tactic_head = - match head_goal with - | None -> [] - | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in - let metas_for_tactic_goals = - List.map - (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic) - goals - in - let metas_for_refine_goals = - List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in - let produced_metas, goals = - let produced_metas = - if always_opens_a_goal then - metas_for_tactic_head @ metas_for_refine_goals @ - metas_for_tactic_goals - else begin -(* print_m "metas_for_refine_goals" metas_for_refine_goals; - print_m "metas_for_tactic_head" metas_for_tactic_head; - print_m "metas_for_tactic_goals" metas_for_tactic_goals; *) - metas_for_refine_goals @ metas_for_tactic_head @ - metas_for_tactic_goals - end - in - let goals = List.map (fun (metano, _, _) -> metano) produced_metas in - produced_metas, goals - in - (* residual metas, preserving the original order *) - let before, after = - let rec split e = - function - | [] -> [],[] - | (metano, _, _) :: tl when metano = e -> - [], List.map (fun (x,_,_) -> x) tl - | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a - in - let find n metasenv = - try - Some (List.find (fun (metano, _, _) -> metano = n) metasenv) - with Not_found -> None - in - let extract l = - List.fold_right - (fun n acc -> - match find n tactic with - | Some x -> x::acc - | None -> acc - ) l [] in - let before_l, after_l = split current_goal start in - let before_l = - List.filter (fun x -> not (List.mem x produced_goals)) before_l in - let after_l = - List.filter (fun x -> not (List.mem x produced_goals)) after_l in - let before = extract before_l in - let after = extract after_l in - before, after - in -(* |+ DEBUG CODE +| - print_m "BEGIN" start; - prerr_endline ("goal was: " ^ string_of_int current_goal); - prerr_endline ("and metas from refine are:"); - List.iter - (fun t -> prerr_string (" " ^ string_of_int t)) - new_goals_from_refine; - prerr_endline ""; - print_m "before" before; - print_m "metas_for_tactic_head" metas_for_tactic_head; - print_m "metas_for_refine_goals" metas_for_refine_goals; - print_m "metas_for_tactic_goals" metas_for_tactic_goals; - print_m "produced_metas" produced_metas; - print_m "after" after; -|+ FINE DEBUG CODE +| *) - before @ produced_metas @ after, goals - -(* maybe we only need special cases for apply and goal *) -let classify_tactic tactic = - match tactic with - (* tactics that can't close the goal (return a goal we want to "select") *) - | GrafiteAst.Rewrite _ - | GrafiteAst.Split _ - | GrafiteAst.Replace _ - | GrafiteAst.Reduce _ - | GrafiteAst.Injection _ - | GrafiteAst.IdTac _ - | GrafiteAst.Generalize _ - | GrafiteAst.Elim _ - | GrafiteAst.Cut _ - | GrafiteAst.Decompose _ -> true, true - (* tactics we don't want to reorder goals. I think only Goal needs this. *) - | GrafiteAst.Goal _ -> false, true - (* tactics like apply *) - | _ -> true, false - -let apply_tactic tactic (status, goal) = -(* prerr_endline "apply_tactic"; *) -(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *) - let starting_metasenv = MatitaTypes.get_proof_metasenv status in - let before = List.map (fun g, _, _ -> g) starting_metasenv in -(* prerr_endline "disambiguate"; *) - let status_ref, tactic = disambiguate_tactic status goal tactic in - let metasenv_after_refinement = MatitaTypes.get_proof_metasenv !status_ref in - let proof = MatitaTypes.get_current_proof !status_ref in - let proof_status = proof, goal in - let needs_reordering, always_opens_a_goal = classify_tactic tactic in - let tactic = tactic_of_ast tactic in - (* apply tactic will change the status pointed by status_ref ... *) -(* prerr_endline "apply_tactic bassa"; *) - let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in - let after = ProofEngineTypes.goals_of_proof proof in - let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in -(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before)); -prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after)); -prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *) -(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals)); -prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) - let proof, opened_goals = - if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty = proof in -(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) - let reordered_metasenv, opened_goals = - reorder_metasenv - starting_metasenv - metasenv_after_refinement metasenv_after_tactic - opened goal always_opens_a_goal - in - let proof' = uri, reordered_metasenv, t, ty in -(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) - proof', opened_goals - end - else - proof, opened_goals - in - let incomplete_proof = - match !status_ref.proof_status with - | Incomplete_proof p -> p - | _ -> assert false - in - { !status_ref with proof_status = - Incomplete_proof { incomplete_proof with proof = proof } }, - opened_goals, closed_goals - -module MatitaStatus = -struct - type input_status = MatitaTypes.status * ProofEngineTypes.goal - - type output_status = - MatitaTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list - - type tactic = input_status -> output_status - - let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) - let mk_tactic tac = tac - let apply_tactic tac = tac - let goals (_, opened, closed) = opened, closed - let set_goals (opened, closed) (status, _, _) = (status, opened, closed) - let get_stack (status, _) = MatitaTypes.get_stack status - - let set_stack stack (status, opened, closed) = - MatitaTypes.set_stack stack status, opened, closed - - let inject (status, _) = (status, [], []) - let focus goal (status, _, _) = (status, goal) -end - -module MatitaTacticals = Tacticals.Make (MatitaStatus) - -let eval_tactical status tac = - let rec tactical_of_ast l tac = - match tac with - | GrafiteAst.Tactic (loc, tactic) -> - MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic)) - | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - assert (l > 0); - MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals) - | GrafiteAst.Do (loc, n, tactical) -> - MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Repeat (loc, tactical) -> - MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - assert (l > 0); - MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical) - ~continuations:(List.map (tactical_of_ast (l+1)) tacticals) - | GrafiteAst.First (loc, tacticals) -> - MatitaTacticals.first - ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) - | GrafiteAst.Try (loc, tactical) -> - MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical) - | GrafiteAst.Solve (loc, tacticals) -> - MatitaTacticals.solve_tactics - ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) - - | GrafiteAst.Skip loc -> MatitaTacticals.skip - | GrafiteAst.Dot loc -> MatitaTacticals.dot - | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon - | GrafiteAst.Branch loc -> MatitaTacticals.branch - | GrafiteAst.Shift loc -> MatitaTacticals.shift - | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i - | GrafiteAst.Merge loc -> MatitaTacticals.merge - | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals - | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus - in - let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in - let status = (* is proof completed? *) - match status.proof_status with - | Incomplete_proof { stack = stack; proof = proof } - when Continuationals.Stack.is_empty stack -> - { status with proof_status = Proof proof } - | _ -> status - in - status - -let eval_coercion status ~add_composites coercion = - let uri = CicUtil.uri_of_term coercion in - let status = MatitaSync.add_coercion status ~add_composites uri in - {status with proof_status = No_proof} - -(* to avoid a long list of recursive functions *) -let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; - -let disambiguate_obj status obj = - let uri = - match obj with - | CicNotationPt.Inductive (_,(name,_,_,_)::_) - | CicNotationPt.Record (_,name,_,_) -> - Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind")) - | CicNotationPt.Inductive _ -> assert false - | CicNotationPt.Theorem _ -> None in - let (diff, metasenv, cic, _) = - singleton - (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) - ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof _ - | Proof _ -> command_error "imbricated proofs not allowed" - | Intermediate _ -> assert false - in - let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status diff in - status, cic - -let disambiguate_command status = - function - | GrafiteAst.Alias _ - | GrafiteAst.Default _ - | GrafiteAst.Drop _ - | GrafiteAst.Dump _ - | GrafiteAst.Include _ - | GrafiteAst.Interpretation _ - | GrafiteAst.Metadata _ - | GrafiteAst.Notation _ - | GrafiteAst.Qed _ - | GrafiteAst.Render _ - | GrafiteAst.Set _ as cmd -> - status,cmd - | GrafiteAst.Coercion (loc, term, add_composites) -> - let status_ref = ref status in - let term = disambiguate_term ~context:[] status_ref ~-1 term in - !status_ref, GrafiteAst.Coercion (loc,term,add_composites) - | GrafiteAst.Obj (loc,obj) -> - let status,obj = disambiguate_obj status obj in - status, GrafiteAst.Obj (loc,obj) - -let make_absolute paths path = - if path = "coq.ma" then path - else - let rec aux = function - | [] -> ignore (Unix.stat path); path - | p :: tl -> - let path = p ^ "/" ^ path in - try - ignore (Unix.stat path); path - with Unix.Unix_error _ -> aux tl - in - try - aux paths - with Unix.Unix_error _ -> raise (UnableToInclude path) -;; - -let eval_command opts status cmd = - let status,cmd = disambiguate_command status cmd in - let cmd,notation_ids' = CicNotation.process_notation cmd in - let status = - { status with notation_ids = notation_ids' @ status.notation_ids } in - let basedir = Helm_registry.get "matita.basedir" in - match cmd with - | GrafiteAst.Default (loc, what, uris) as cmd -> - LibraryObjects.set_default what uris; - add_moo_content [cmd] status - | GrafiteAst.Include (loc, path) -> - let absolute_path = make_absolute opts.include_paths path in - let moopath = MatitaMisc.obj_file_of_script ~basedir absolute_path in - let status = ref status in - if not (Sys.file_exists moopath) then - raise (IncludedFileNotCompiled moopath); - !eval_from_moo_ref status moopath (fun _ _ -> ()); - !status - | GrafiteAst.Metadata (loc, m) -> - (match m with - | GrafiteAst.Dependency uri -> MatitaTypes.add_moo_metadata [m] status - | GrafiteAst.Baseuri _ -> status) - | GrafiteAst.Set (loc, name, value) -> - let status = - if name = "baseuri" then begin - let value = - let v = MatitaMisc.strip_trailing_slash value in - try - ignore (String.index v ' '); - command_error "baseuri can't contain spaces" - with Not_found -> v - in - if not (MatitaMisc.is_empty value) && opts.clean_baseuri then begin - HLog.warn ("baseuri " ^ value ^ " is not empty"); - HLog.message ("cleaning baseuri " ^ value); - LibraryClean.clean_baseuris ~basedir [value] - end; - add_moo_metadata [GrafiteAst.Baseuri value] status - end else - status - in - set_option status name value - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = - match status.proof_status with - | Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | Proof (None, metasenv, body, ty) -> - command_error - ("Someone allows to start a thm without giving the "^ - "name/uri. This should be fixed!") - | _-> command_error "You can't Qed an incomplete theorem" - in - if metasenv <> [] then - command_error "Proof not completed! metasenv is not empty!"; - let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name,Some bo,ty,[],[]) in - MatitaSync.add_obj uri obj {status with proof_status = No_proof} - | GrafiteAst.Coercion (loc, coercion, add_composites) -> - eval_coercion status ~add_composites coercion - | GrafiteAst.Alias (loc, spec) -> - let diff = - (*CSC: Warning: this code should be factorized with the corresponding - code in DisambiguatePp *) - match spec with - | GrafiteAst.Ident_alias (id,uri) -> - [DisambiguateTypes.Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] - | GrafiteAst.Symbol_alias (symb, instance, desc) -> - [DisambiguateTypes.Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc] - | GrafiteAst.Number_alias (instance,desc) -> - [DisambiguateTypes.Num instance, - DisambiguateChoices.lookup_num_by_dsc desc] - in - MatitaSync.set_proof_aliases status diff - | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> - let status = add_moo_content [stm] status in - let uris = - List.map - (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri)) - (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern) - in - let diff = - [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] - in - let status = MatitaSync.set_proof_aliases status diff in - let status = MatitaTypes.add_moo_metadata uris status in - status - | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status - | GrafiteAst.Obj (loc,obj) -> - let ext,name = - match obj with - Cic.Constant (name,_,_,_,_) - | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name - | Cic.InductiveDefinition (types,_,_,_) -> - ".ind", - (match types with (name,_,_,_)::_ -> name | _ -> assert false) - | _ -> assert false in - let uri = - UriManager.uri_of_string (MatitaTypes.qualify status name ^ ext) - in - let metasenv = MatitaTypes.get_proof_metasenv status in - match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> - let name = UriManager.name_of_uri uri in - if not(CicPp.check name ty) then - HLog.error ("Bad name: " ^ name); - if opts.do_heavy_checks then - begin - let dbd = LibraryDb.instance () in - let similar = Whelp.match_term ~dbd ty in - let similar_len = List.length similar in - if similar_len> 30 then - (HLog.message - ("Duplicate check will compare your theorem with " ^ - string_of_int similar_len ^ - " theorems, this may take a while.")); - let convertible = - List.filter ( - fun u -> - let t = CicUtil.term_of_uri u in - let ty',g = - CicTypeChecker.type_of_aux' - metasenv' [] t CicUniv.empty_ugraph - in - fst(CicReduction.are_convertible [] ty' ty g)) - similar - in - (match convertible with - | [] -> () - | x::_ -> - HLog.warn - ("Theorem already proved: " ^ UriManager.string_of_uri x ^ - "\nPlease use a variant.")); - end; - assert (metasenv = metasenv'); - let goalno = - match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false - in - let initial_proof = (Some uri, metasenv, bo, ty) in - let initial_stack = Continuationals.Stack.of_metasenv metasenv in - { status with proof_status = - Incomplete_proof { proof = initial_proof; stack = initial_stack } } - | _ -> - if metasenv <> [] then - command_error ( - "metasenv not empty while giving a definition with body: " ^ - CicMetaSubst.ppmetasenv [] metasenv); - MatitaSync.add_obj uri obj {status with proof_status = No_proof} - -let eval_executable opts status ex = - match ex with - | GrafiteAst.Tactical (_, tac, None) -> eval_tactical status tac - | GrafiteAst.Tactical (_, tac, Some punct) -> - let status = eval_tactical status tac in - eval_tactical status punct - | GrafiteAst.Command (_, cmd) -> eval_command opts status cmd - | GrafiteAst.Macro (_, mac) -> - command_error (sprintf "The macro %s can't be in a script" - (GrafiteAstPp.pp_macro_ast mac)) - -let eval_comment status c = status - -let eval_ast - ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st -= - let opts = { - do_heavy_checks = do_heavy_checks ; - include_paths = include_paths; - clean_baseuri = clean_baseuri } - in - match st with - | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex - | GrafiteAst.Comment (_,c) -> eval_comment status c - -let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname cb -= - let ast_of_cmd cmd = - GrafiteAst.Executable (DisambiguateTypes.dummy_floc, - GrafiteAst.Command (DisambiguateTypes.dummy_floc, - (GrafiteAst.reash_cmd_uris cmd))) - in - let moo, metadata = GrafiteMarshal.load_moo fname in - List.iter - (fun ast -> - let ast = ast_of_cmd ast in - cb !status ast; - status := - eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast) - moo; - List.iter - (fun m -> - let ast = - ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m)) - in - cb !status ast; - status := - eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast) - metadata - let eval_from_stream ?do_heavy_checks ?include_paths ?clean_baseuri status str cb = @@ -854,13 +38,13 @@ let eval_from_stream let ast = GrafiteParser.parse_statement str in cb !status ast; status := - eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done with End_of_file -> () -(* to avoid a long list of recursive functions *) -let _ = eval_from_moo_ref := eval_from_moo - let eval_from_stream_greedy ?do_heavy_checks ?include_paths ?clean_baseuri status str cb = @@ -869,7 +53,11 @@ let eval_from_stream_greedy flush stdout; let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast + status := + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done ;; diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index e8cdbad0e..9f8cb44a6 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -23,41 +23,28 @@ * http://helm.cs.unibo.it/ *) -exception Drop -exception UnableToInclude of string -exception IncludedFileNotCompiled of string - (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) val eval_string: ?do_heavy_checks:bool -> ?include_paths:string list -> ?clean_baseuri:bool -> - MatitaTypes.status ref -> string -> unit + GrafiteTypes.status ref -> string -> unit val eval_from_stream: ?do_heavy_checks:bool -> ?include_paths:string list -> ?clean_baseuri:bool -> - MatitaTypes.status ref -> Ulexing.lexbuf -> - (MatitaTypes.status -> GrafiteParser.statement -> unit) -> + GrafiteTypes.status ref -> Ulexing.lexbuf -> + (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> unit val eval_from_stream_greedy: ?do_heavy_checks:bool -> ?include_paths:string list -> ?clean_baseuri:bool -> - MatitaTypes.status ref-> Ulexing.lexbuf -> - (MatitaTypes.status -> GrafiteParser.statement -> unit) -> + GrafiteTypes.status ref-> Ulexing.lexbuf -> + (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> unit -val eval_ast: - ?do_heavy_checks:bool -> - ?include_paths:string list -> - ?clean_baseuri:bool -> - MatitaTypes.status -> - GrafiteParser.statement -> - MatitaTypes.status - -val initial_status: MatitaTypes.status lazy_t - +val initial_status: GrafiteTypes.status lazy_t diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index fcb022345..d58ceaf7a 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -31,11 +31,11 @@ let rec to_string = let _,msg = to_string exn in let (x, y) = HExtlib.loc_of_floc floc in Some floc, sprintf "Error at %d-%d: %s" x y msg - | MatitaTypes.Option_error ("baseuri", "not found" ) -> + | GrafiteTypes.Option_error ("baseuri", "not found" ) -> None, "Baseuri not set for this script. " ^ "Use 'set \"baseuri\" \"\".' to set it." - | MatitaTypes.Command_error msg -> None, "Error: " ^ msg + | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index c969f1bcd..619c1eadb 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -26,8 +26,6 @@ exception PopupClosed open Printf -open MatitaTypes - let wrap_callback f = f let connect_button (button: #GButton.button) callback = @@ -391,7 +389,7 @@ let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false) connect_button dialog#emptyDialogCancelButton (fun _ ->return None); dialog#emptyDialog#show (); GtkThread.main (); - (match !result with None -> raise Cancel | Some r -> r) + (match !result with None -> raise MatitaTypes.Cancel | Some r -> r) type combo_status = Free of string | Locked of string diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e4c107242..6b4afa3cf 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -63,22 +63,22 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri status = try - let baseuri = MatitaTypes.get_string_option status "baseuri" in + let baseuri = GrafiteTypes.get_string_option status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir [baseuri] - with MatitaTypes.Option_error _ -> () + with GrafiteTypes.Option_error _ -> () let ask_and_save_moo_if_needed parent fname status = let basedir = Helm_registry.get "matita.basedir" in let save () = - let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in + let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in GrafiteMarshal.save_moo moo_fname - status.MatitaTypes.moo_content_rev in + status.GrafiteTypes.moo_content_rev in if (MatitaScript.current ())#eos && - status.MatitaTypes.proof_status = MatitaTypes.No_proof + status.GrafiteTypes.proof_status = GrafiteTypes.No_proof then begin - let mooname = MatitaMisc.obj_file_of_script ~basedir fname in + let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in let rc = MatitaGtkMisc.ask_confirmation ~title:"A .moo can be generated" diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index 52dca43f7..efb704579 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -117,7 +117,7 @@ object method reset: unit method load_logo: unit method load_logo_with_qed: unit - method load_sequents: MatitaTypes.incomplete_proof -> unit + method load_sequents: GrafiteTypes.incomplete_proof -> unit method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 15a4a126d..b637eb8dc 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -25,7 +25,7 @@ open Printf -open MatitaTypes +open GrafiteTypes open MatitaGtkMisc module Stack = Continuationals.Stack @@ -849,7 +849,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadList l method private setEntry entry = - win#browserUri#entry#set_text (string_of_entry entry); + win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry); current_entry <- entry method private _loadObj obj = @@ -892,10 +892,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) | txt -> - (try - entry_of_string txt + (try + MatitaTypes.entry_of_string txt with Invalid_argument _ -> - command_error (sprintf "unsupported uri: %s" txt)) + raise + (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt))) in self#_load entry; self#_historyAdd entry diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 077809a17..389ee2325 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -24,27 +24,12 @@ *) open Printf -open MatitaTypes (** Functions "imported" from Http_getter_misc *) -let strip_trailing_slash = Http_getter_misc.strip_trailing_slash let normalize_dir = Http_getter_misc.normalize_dir let strip_suffix = Http_getter_misc.strip_suffix -let baseuri_of_baseuri_decl st = - match st with - | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None - -let is_empty buri = - List.for_all - (function - Http_getter_types.Ls_section _ -> true - | Http_getter_types.Ls_object _ -> false) - (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) - let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file @@ -163,42 +148,3 @@ let list_tl_at ?(equality=(==)) e l = | hd :: tl -> aux tl in aux l - -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Ulexing.from_utf8_channel ic in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - match baseuri_of_baseuri_decl stm with - | Some buri -> - let u = strip_trailing_slash buri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve u) - with - | Http_getter_types.Unresolvable_URI _ -> - HLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | Http_getter_types.Key_not_found _ -> ()); - uri := Some u; - raise End_of_file - | None -> () - with - CicNotationParser.Parse_error err -> - HLog.error ("Unable to parse: " ^ file); - HLog.error ("Parse error: " ^ err); - () - done - with End_of_file -> close_in ic); - match !uri with - | Some uri -> uri - | None -> failwith ("No baseuri defined in " ^ file) - -let obj_file_of_script ~basedir f = - if f = "coq.ma" then BuildTimeConf.coq_notation_script else - let baseuri = baseuri_of_file f in - LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri - diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 253625106..170a87c9b 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -23,12 +23,6 @@ * http://helm.cs.unibo.it/ *) -val baseuri_of_baseuri_decl: - ('a, 'b, 'c, 'd, 'e) GrafiteAst.statement -> string option - - (** check whether no objects are defined below a given baseuri *) -val is_empty: string -> bool - val absolute_path: string -> string (** @return true if file is a (textual) proof script *) @@ -41,7 +35,6 @@ val is_proof_object: string -> bool * it *) val append_phrase_sep: string -> string -val strip_trailing_slash: string -> string val normalize_dir: string -> string (** add trailing "/" if missing *) val strip_suffix: suffix:string -> string -> string @@ -80,6 +73,3 @@ val singleton: (unit -> 'a) -> (unit -> 'a) (** given the base name of an image, returns its full path *) val image_path: string -> string - -val baseuri_of_file: string -> string -val obj_file_of_script : basedir:string -> string -> string diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 9b9e87085..c35fb9307 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,7 +24,7 @@ *) open Printf -open MatitaTypes +open GrafiteTypes module TA = GrafiteAst @@ -108,7 +108,9 @@ let eval_with_engine guistuff status user_goal parsed_text st = initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *) | _ -> initial_space,status,[] in let new_status = - MatitaEngine.eval_ast + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command ~include_paths:include_ ~do_heavy_checks:true new_status st in let new_aliases = @@ -126,7 +128,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - let baseuri = MatitaTypes.get_string_option new_status "baseuri" in + let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in List.fold_left ( fun (initial_space,status,acc) (k,((v,_) as value)) -> let b = @@ -161,8 +163,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = try eval_with_engine guistuff status user_goal parsed_text st with - | MatitaEngine.UnableToInclude what - | MatitaEngine.IncludedFileNotCompiled what as exc -> + | GrafiteEngine.UnableToInclude what + | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in let refresh_cb () = @@ -215,8 +217,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in let dbd = LibraryDb.instance () in - let metasenv = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv status in + let context = GrafiteTypes.get_proof_context status user_goal in let interps = MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in @@ -276,7 +278,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = MatitaTypes.get_current_proof status in + let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in @@ -290,7 +292,11 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = TA.Apply (loc, CicNotationPt.Uri (suri, None))), Some (TA.Dot loc)))) in - let new_status = MatitaEngine.eval_ast status ast in + let new_status = + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast @@ -304,8 +310,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = ) selected; assert false) | TA.Check (_,term) -> - let metasenv = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv status in + let context = GrafiteTypes.get_proof_context status user_goal in let interps = MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term @@ -350,10 +356,10 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try - (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> - if not (MatitaMisc.is_empty u) then + if not (GrafiteMisc.is_empty u) then match guistuff.ask_confirmation ~title:"Baseuri redefinition" @@ -419,7 +425,7 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView.source_view) - ~(init: MatitaTypes.status) + ~(init: GrafiteTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -590,7 +596,7 @@ object (self) val mutable observers = [] - method addObserver (o: MatitaTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = @@ -737,10 +743,10 @@ object (self) | Intermediate _ -> assert false (* method proofStatus = MatitaTypes.get_proof_status self#status *) - method proofMetasenv = MatitaTypes.get_proof_metasenv self#status - method proofContext = MatitaTypes.get_proof_context self#status userGoal - method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal - method stack = MatitaTypes.get_stack self#status + method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status + method proofContext = GrafiteTypes.get_proof_context self#status userGoal + method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal + method stack = GrafiteTypes.get_stack self#status method setGoal n = userGoal <- n method goal = userGoal diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index f3523c15b..e407b090a 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -31,11 +31,11 @@ object method error_tag : GText.tag (** @return current status *) - method status: MatitaTypes.status + method status: GrafiteTypes.status (** {2 Observers} *) - method addObserver : (MatitaTypes.status -> unit) -> unit + method addObserver : (GrafiteTypes.status -> unit) -> unit (** {2 History} *) @@ -81,7 +81,7 @@ end * "*") on the side of a script name *) val script: source_view:GSourceView.source_view -> - init:MatitaTypes.status -> + init:GrafiteTypes.status -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> develcreator: (containing:string option -> unit) -> diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml deleted file mode 100644 index b06aedf30..000000000 --- a/helm/matita/matitaSync.ml +++ /dev/null @@ -1,181 +0,0 @@ -(* Copyright (C) 2004-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 Printf - -open MatitaTypes - -let alias_diff ~from status = - let module Map = DisambiguateTypes.Environment in - Map.fold - (fun domain_item (description1,_ as codomain_item) acc -> - try - let description2,_ = Map.find domain_item from.aliases in - if description1 <> description2 then - (domain_item,codomain_item)::acc - else - acc - with - Not_found -> - (domain_item,codomain_item)::acc) - status.aliases [] - -let alias_diff = - let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in - fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status - -let set_proof_aliases status new_aliases = - let commands_of_aliases = - List.map - (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias)) - in - let deps_of_aliases = - HExtlib.filter_map - (function - | GrafiteAst.Ident_alias (_, suri) -> - let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in - Some (GrafiteAst.Dependency buri) - | _ -> None) - in - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status.aliases new_aliases in - let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in - let new_status = - { status with multi_aliases = multi_aliases ; aliases = aliases} - in - if new_aliases = [] then - new_status - else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases - in - let status = add_moo_content (commands_of_aliases aliases) new_status in - let status = add_moo_metadata (deps_of_aliases aliases) status in - status - -(** given a uri and a type list (the contructors types) builds a list of pairs - * (name,uri) that is used to generate automatic aliases **) -let extract_alias types uri = - fst(List.fold_left ( - fun (acc,i) (name, _, _, cl) -> - (name, UriManager.uri_of_uriref uri i None) :: - (fst(List.fold_left ( - fun (acc,j) (name,_) -> - (((name,UriManager.uri_of_uriref uri i - (Some j)) :: acc) , j+1) - ) (acc,1) cl)),i+1 - ) ([],0) types) - -let build_aliases = - List.map - (fun (name,uri) -> - DisambiguateTypes.Id name, - (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) - -let add_aliases_for_inductive_def status types uri = - let aliases = build_aliases (extract_alias types uri) in - set_proof_aliases status aliases - -let add_alias_for_constant status uri = - let name = UriManager.name_of_uri uri in - let new_env = build_aliases [(name,uri)] in - set_proof_aliases status new_env - -let add_aliases_for_object status uri = - function - Cic.InductiveDefinition (types,_,_,_) -> - add_aliases_for_inductive_def status types uri - | Cic.Constant _ -> add_alias_for_constant status uri - | Cic.Variable _ - | Cic.CurrentProof _ -> assert false - -let add_obj uri obj status = - let basedir = Helm_registry.get "matita.basedir" in - let lemmas = LibrarySync.add_obj uri obj basedir in - let status = {status with objects = uri::status.objects} in - List.fold_left add_alias_for_constant - (add_aliases_for_object status uri obj) lemmas - -let add_obj = - let profiler = HExtlib.profile "add_obj" in - fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status - -let add_coercion status ~add_composites uri = - let basedir = Helm_registry.get "matita.basedir" in - let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in - let status = {status with coercions = uri :: status.coercions} in - let statement_of name = - GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, - (CicNotationPt.Ident (name, None)), false) in - let moo_content = [statement_of (UriManager.name_of_uri uri)] in - let status = MatitaTypes.add_moo_content moo_content status in - List.fold_left add_alias_for_constant status lemmas - -module OrderedUri = -struct - type t = UriManager.uri * string - let compare (u1, _) (u2, _) = UriManager.compare u1 u2 -end - -module OrderedId = -struct - type t = CicNotation.notation_id - let compare = Pervasives.compare -end - -module UriSet = Set.Make (OrderedUri) -module IdSet = Set.Make (OrderedId) - - (** @return l2 \ l1 *) -let uri_list_diff l2 l1 = - let module S = UriManager.UriSet in - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - - (** @return l2 \ l1 *) -let id_list_diff l2 l1 = - let module S = IdSet in - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - -let time_travel ~present ~past = - let objs_to_remove = uri_list_diff present.objects past.objects in - let coercions_to_remove = uri_list_diff present.coercions past.coercions in - let notation_to_remove = - id_list_diff present.notation_ids past.notation_ids - in - let debug_list = ref [] in - List.iter - (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)) - coercions_to_remove; - List.iter LibrarySync.remove_obj objs_to_remove; - List.iter CicNotation.remove_notation notation_to_remove diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli deleted file mode 100644 index 13023a854..000000000 --- a/helm/matita/matitaSync.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2004-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 add_obj: - UriManager.uri -> Cic.obj -> - MatitaTypes.status -> MatitaTypes.status - -val add_coercion: - MatitaTypes.status -> add_composites:bool -> UriManager.uri -> - MatitaTypes.status - -val time_travel: - present:MatitaTypes.status -> past:MatitaTypes.status -> unit - - (** perform a diff between the aliases contained in two statuses, assuming - * that the second one can only have more aliases than the first one - * @return the list of aliases that should be added to aliases of from in - * order to be equal to aliases of the second argument *) -val alias_diff: - from:MatitaTypes.status -> MatitaTypes.status -> - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list - - (** set the proof aliases enriching the moo_content *) -val set_proof_aliases : - MatitaTypes.status -> - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> - MatitaTypes.status diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index dc692f890..d956af009 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -24,180 +24,11 @@ *) open Printf +open GrafiteTypes (** user hit the cancel button *) exception Cancel - (** statement invoked in the wrong context (e.g. tactic with no ongoing proof) - *) -exception Statement_error of string -let statement_error msg = raise (Statement_error msg) - -exception Command_error of string -let command_error msg = raise (Command_error msg) - - (** parameters are: option name, error message *) -exception Option_error of string * string - -exception Unbound_identifier of string - -type incomplete_proof = { - proof: ProofEngineTypes.proof; - stack: Continuationals.Stack.t; -} - -type proof_status = - | No_proof - | Incomplete_proof of incomplete_proof - | Proof of ProofEngineTypes.proof - | Intermediate of Cic.metasenv - (* Status in which the proof could be while it is being processed by the - * engine. No status entering/exiting the engine could be in it. *) - -module StringMap = Map.Make (String) - -type option_value = - | String of string - | Int of int -type options = option_value StringMap.t -let no_options = StringMap.empty - -type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command -type moo = ast_command list * GrafiteAst.metadata list - -type status = { - aliases: DisambiguateTypes.environment; - multi_aliases: DisambiguateTypes.multiple_environment; - moo_content_rev: moo; - proof_status: proof_status; - options: options; - objects: UriManager.uri list; - coercions: UriManager.uri list; - notation_ids: CicNotation.notation_id list; -} - -let set_metasenv metasenv status = - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) -> - Incomplete_proof - { incomplete_proof with proof = (uri, metasenv, proof, ty) } - | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false - in - { status with proof_status = proof_status } - -let dump_status status = - HLog.message "status.aliases:\n"; - HLog.message "status.proof_status:"; - HLog.message - (match status.proof_status with - | No_proof -> "no proof\n" - | Incomplete_proof _ -> "incomplete proof\n" - | Proof _ -> "proof\n" - | Intermediate _ -> "Intermediate\n"); - HLog.message "status.options\n"; - StringMap.iter (fun k v -> - let v = - match v with - | String s -> s - | Int i -> string_of_int i - in - HLog.message (k ^ "::=" ^ v)) status.options; - HLog.message "status.coercions\n"; - HLog.message "status.objects:\n"; - List.iter - (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects - -let get_option status name = - try - StringMap.find name status.options - with Not_found -> raise (Option_error (name, "not found")) - -let get_string_option status name = - match get_option status name with - | String s -> s - | _ -> raise (Option_error (name, "not a string value")) - -let set_option status name value = - let mangle_dir s = - let s = Str.global_replace (Str.regexp "//+") "/" s in - let s = Str.global_replace (Str.regexp "/$") "" s in - s - in - let types = [ "baseuri", (`String, mangle_dir); ] in - let ty_and_mangler = - try - List.assoc name types - with Not_found -> command_error (sprintf "Unknown option \"%s\"" name) - in - let value = - match ty_and_mangler with - | `String, f -> String (f value) - | `Int, f -> - (try - Int (int_of_string (f value)) - with Failure _ -> - command_error (sprintf "Not an integer value \"%s\"" value)) - in - if StringMap.mem name status.options && name = "baseuri" then - command_error "Redefinition of 'baseuri' is forbidden." - else - { status with options = StringMap.add name value status.options } - -let add_moo_content cmds status = - let content, metadata = status.moo_content_rev in - let content' = - List.fold_right - (fun cmd acc -> -(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *) - match cmd with - | GrafiteAst.Interpretation _ - | GrafiteAst.Default _ -> - if List.mem cmd content then acc - else cmd :: acc - | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *) - cmd :: (List.filter ((<>) cmd) acc) - | _ -> cmd :: acc) - cmds content - in -(* prerr_endline ("new moo content: " ^ String.concat " " (List.map - GrafiteAstPp.pp_command content')); *) - { status with moo_content_rev = content', metadata } - -let add_moo_metadata new_metadata status = - let content, metadata = status.moo_content_rev in - let metadata' = - List.fold_left - (fun acc m -> - match m with - | GrafiteAst.Dependency buri -> - let is_self = (* self dependency *) - try - get_string_option status "baseuri" = buri - with Option_error _ -> false (* baseuri not yet set *) - in - if is_self - || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *) - then acc - else m :: acc - | _ -> m :: acc) - metadata new_metadata - in - { status with moo_content_rev = content, metadata' } - - (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) -class type console = - object - method clear : unit -> unit - method echo_error : string -> unit - method echo_message : string -> unit - method wrap_exn : 'a. (unit -> 'a) -> 'a option - method choose_uri : string list -> string - method show : ?msg:string -> unit -> unit - end - type abouts = [ `Blank | `Current_proof @@ -239,48 +70,3 @@ class type mathViewer = method show_uri_list: ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit end - -let qualify status name = get_string_option status "baseuri" ^ "/" ^ name - -let get_current_proof status = - match status.proof_status with - | Incomplete_proof { proof = p } -> p - | _ -> statement_error "no ongoing proof" - -let get_proof_metasenv status = - match status.proof_status with - | No_proof -> [] - | Proof (_, metasenv, _, _) - | Incomplete_proof { proof = (_, metasenv, _, _) } - | Intermediate metasenv -> - metasenv - -let get_proof_context status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, context, _) = CicUtil.lookup_meta goal metasenv in - context - | _ -> [] - -let get_proof_conclusion status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in - conclusion - | _ -> statement_error "no ongoing proof" - -let get_stack status = - match status.proof_status with - | Incomplete_proof p -> p.stack - | Proof _ -> Continuationals.Stack.empty - | _ -> assert false - -let set_stack stack status = - match status.proof_status with - | Incomplete_proof p -> - { status with proof_status = Incomplete_proof { p with stack = stack } } - | Proof _ -> - assert (Continuationals.Stack.is_empty stack); - status - | _ -> assert false - diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index ebf208b92..be77c4435 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -24,65 +24,6 @@ *) exception Cancel -exception Statement_error of string -val statement_error : string -> 'a - -exception Command_error of string -val command_error : string -> 'a - -exception Option_error of string * string -exception Unbound_identifier of string - -type incomplete_proof = { - proof: ProofEngineTypes.proof; - stack: Continuationals.Stack.t; -} - -type proof_status = - No_proof - | Incomplete_proof of incomplete_proof - | Proof of ProofEngineTypes.proof - | Intermediate of Cic.metasenv - -module StringMap : Map.S with type key = String.t - -type option_value = - | String of string - | Int of int -type options = option_value StringMap.t -val no_options : 'a StringMap.t - -type status = { - aliases: DisambiguateTypes.environment; (** disambiguation aliases *) - multi_aliases: DisambiguateTypes.multiple_environment; - moo_content_rev: GrafiteMarshal.moo; - proof_status: proof_status; (** logical status *) - options: options; - objects: UriManager.uri list; (** in-scope objects *) - coercions: UriManager.uri list; (** defined coercions *) - notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) -} - -val set_metasenv: Cic.metasenv -> status -> status - - (** list is not reversed, head command will be the first emitted *) -val add_moo_content: GrafiteMarshal.ast_command list -> status -> status -val add_moo_metadata: GrafiteAst.metadata list -> status -> status - -val dump_status : status -> unit -val get_option : status -> string -> option_value -val get_string_option : status -> string -> string -val set_option : status -> string -> string -> status - -class type console = - object - method choose_uri : string list -> string - method clear : unit -> unit - method echo_error : string -> unit - method echo_message : string -> unit - method show : ?msg:string -> unit -> unit - method wrap_exn : (unit -> 'a) -> 'a option - end type abouts = [ `Blank | `Current_proof | `Us ] @@ -94,17 +35,8 @@ type mathViewer_entry = | `Uri of UriManager.uri | `Whelp of string * UriManager.uri list ] -val string_of_entry : - [< `About of [< `Blank | `Current_proof | `Us ] - | `Check of 'a - | `Cic of 'b * 'c - | `Dir of string - | `Uri of UriManager.uri - | `Whelp of string * 'd ] -> - string - -val entry_of_string : - string -> [> `About of [> `Blank | `Current_proof | `Us ] ] +val string_of_entry : mathViewer_entry -> string +val entry_of_string : string -> mathViewer_entry class type mathViewer = object @@ -112,14 +44,3 @@ class type mathViewer = method show_uri_list : ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit end - -val qualify: status -> string -> string - -val get_current_proof: status -> ProofEngineTypes.proof -val get_proof_metasenv: status -> Cic.metasenv -val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context -val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term -val get_stack: status -> Continuationals.Stack.t - -val set_stack: Continuationals.Stack.t -> status -> status - diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index fe22c9da7..55c5f2a02 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -25,7 +25,7 @@ open Printf -open MatitaTypes +open GrafiteTypes (** {2 Initialization} *) @@ -57,7 +57,7 @@ let run_script is eval_function = try eval_function status is cb with - | MatitaEngine.Drop + | GrafiteEngine.Drop | End_of_file | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> @@ -86,11 +86,11 @@ let clean_exit n = None -> opt_exit n | Some status -> try - let baseuri = MatitaTypes.get_string_option !status "baseuri" in + let baseuri = GrafiteTypes.get_string_option !status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri]; opt_exit n - with MatitaTypes.Option_error("baseuri", "not found") -> + with GrafiteTypes.Option_error("baseuri", "not found") -> (* no baseuri ==> nothing to clean yet *) opt_exit n @@ -102,9 +102,9 @@ let rec interactive_loop () = ~include_paths:(Helm_registry.get_list Helm_registry.string "matita.includes")) with - | MatitaEngine.Drop -> pp_ocaml_mode () + | GrafiteEngine.Drop -> pp_ocaml_mode () | Sys.Break -> HLog.error "user break!"; interactive_loop () - | MatitaTypes.Command_error _ -> interactive_loop () + | GrafiteTypes.Command_error _ -> interactive_loop () | End_of_file -> print_newline (); clean_exit (Some 0) @@ -175,7 +175,7 @@ let main ~mode = | Some s -> !s.proof_status, !s.moo_content_rev, !s | None -> assert false in - if proof_status <> MatitaTypes.No_proof then + if proof_status <> GrafiteTypes.No_proof then begin HLog.error "there are still incomplete proofs at the end of the script"; @@ -184,7 +184,7 @@ let main ~mode = else begin let basedir = Helm_registry.get "matita.basedir" in - let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in + let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in GrafiteMarshal.save_moo moo_fname moo_content_rev; HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); @@ -197,7 +197,7 @@ let main ~mode = clean_exit (Some ~-1) else pp_ocaml_mode () - | MatitaEngine.Drop -> + | GrafiteEngine.Drop -> if mode = `COMPILER then clean_exit (Some 1) else diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 807f54525..b8c2bb4c2 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -55,7 +55,7 @@ let main () = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> files_to_remove := suri :: !files_to_remove; - let u = MatitaMisc.baseuri_of_file suri in + let u = GrafiteMisc.baseuri_of_file suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); @@ -67,7 +67,7 @@ let main () = files); LibraryClean.clean_baseuris ~basedir !uris_to_remove; let moos = - List.map (MatitaMisc.obj_file_of_script ~basedir) !files_to_remove + List.map (GrafiteMisc.obj_file_of_script ~basedir) !files_to_remove in List.iter HExtlib.safe_remove moos diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 34f7744a0..c40f1636d 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -67,12 +67,12 @@ let main () = let uri = UriManager.string_of_uri uri in Hashtbl.add uri_deps file uri | GrafiteAst.BaseuriDep uri -> - let uri = MatitaMisc.strip_trailing_slash uri in + let uri = Http_getter_misc.strip_trailing_slash uri in Hashtbl.add baseuri_of file uri | GrafiteAst.IncludeDep path -> try let ma_file = if path <> "coq.ma" then find path else path in - let moo_file = MatitaMisc.obj_file_of_script ~basedir ma_file in + let moo_file = GrafiteMisc.obj_file_of_script ~basedir ma_file in Hashtbl.add include_deps file moo_file with Sys_error _ -> HLog.warn @@ -94,7 +94,7 @@ let main () = let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in let deps = file :: deps in - let moo = MatitaMisc.obj_file_of_script ~basedir file in + let moo = GrafiteMisc.obj_file_of_script ~basedir file in Printf.printf "%s: %s\n" moo (String.concat " " deps); Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) (Helm_registry.get_list Helm_registry.string "matita.args") diff --git a/helm/matita/tests/Makefile b/helm/matita/tests/Makefile index 33d458929..1ea16550d 100644 --- a/helm/matita/tests/Makefile +++ b/helm/matita/tests/Makefile @@ -1,6 +1,6 @@ SRC=$(wildcard *.ma) -MATITA_FLAGS = +MATITA_FLAGS = -I .. NODB=false ifeq ($(NODB),true) MATITA_FLAGS += -nodb -- 2.39.2