From a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Dec 2005 10:57:02 +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/ocaml/METAS/meta.helm-grafite2.src | 5 + helm/ocaml/METAS/meta.helm-grafite_parser.src | 5 + helm/ocaml/Makefile.in | 4 +- helm/ocaml/grafite/grafiteAst.ml | 18 +- helm/ocaml/grafite/grafiteAstPp.ml | 4 +- helm/ocaml/grafite/grafiteAstPp.mli | 10 +- helm/ocaml/grafite/grafiteMarshal.ml | 2 +- helm/ocaml/grafite/grafiteMarshal.mli | 2 +- helm/ocaml/grafite/grafiteParser.ml | 2 +- helm/ocaml/grafite/grafiteParser.mli | 2 +- helm/ocaml/grafite2/.cvsignore | 5 + helm/ocaml/grafite2/.depend | 14 + helm/ocaml/grafite2/Makefile | 13 + helm/ocaml/grafite2/disambiguatePp.ml | 83 +++ helm/ocaml/grafite2/disambiguatePp.mli | 34 + helm/ocaml/grafite2/grafiteEngine.ml | 686 ++++++++++++++++++ helm/ocaml/grafite2/grafiteEngine.mli | 48 ++ helm/ocaml/grafite2/grafiteMisc.ml | 74 ++ helm/ocaml/grafite2/grafiteMisc.mli | 35 + helm/ocaml/grafite2/grafiteTypes.ml | 218 ++++++ helm/ocaml/grafite2/grafiteTypes.mli | 77 ++ helm/ocaml/grafite2/matitaSync.ml | 181 +++++ helm/ocaml/grafite2/matitaSync.mli | 49 ++ helm/ocaml/grafite_parser/.cvsignore | 5 + helm/ocaml/grafite_parser/.depend | 4 + helm/ocaml/grafite_parser/Makefile | 10 + .../grafite_parser/grafiteDisambiguate.cmi | Bin 0 -> 1836 bytes .../grafite_parser/grafiteDisambiguate.cmo | Bin 0 -> 36185 bytes .../grafite_parser/grafiteDisambiguate.cmx | Bin 0 -> 1766 bytes .../grafite_parser/grafiteDisambiguate.ml | 253 +++++++ .../grafite_parser/grafiteDisambiguate.mli | 36 + .../grafite_parser/grafiteDisambiguate.o | Bin 0 -> 17472 bytes helm/ocaml/grafite_parser/grafite_parser.a | Bin 0 -> 31080 bytes helm/ocaml/grafite_parser/grafite_parser.cma | Bin 0 -> 57777 bytes helm/ocaml/grafite_parser/grafite_parser.cmxa | Bin 0 -> 3467 bytes .../grafite_parser/matitaDisambiguator.cmi | Bin 0 -> 2972 bytes .../grafite_parser/matitaDisambiguator.cmo | Bin 0 -> 20471 bytes .../grafite_parser/matitaDisambiguator.cmx | Bin 0 -> 2318 bytes .../grafite_parser/matitaDisambiguator.ml | 176 +++++ .../grafite_parser/matitaDisambiguator.mli | 51 ++ .../grafite_parser/matitaDisambiguator.o | Bin 0 -> 11092 bytes helm/ocaml/library/libraryClean.ml | 4 +- 42 files changed, 2084 insertions(+), 26 deletions(-) create mode 100644 helm/ocaml/METAS/meta.helm-grafite2.src create mode 100644 helm/ocaml/METAS/meta.helm-grafite_parser.src create mode 100644 helm/ocaml/grafite2/.cvsignore create mode 100644 helm/ocaml/grafite2/.depend create mode 100644 helm/ocaml/grafite2/Makefile create mode 100644 helm/ocaml/grafite2/disambiguatePp.ml create mode 100644 helm/ocaml/grafite2/disambiguatePp.mli create mode 100644 helm/ocaml/grafite2/grafiteEngine.ml create mode 100644 helm/ocaml/grafite2/grafiteEngine.mli create mode 100644 helm/ocaml/grafite2/grafiteMisc.ml create mode 100644 helm/ocaml/grafite2/grafiteMisc.mli create mode 100644 helm/ocaml/grafite2/grafiteTypes.ml create mode 100644 helm/ocaml/grafite2/grafiteTypes.mli create mode 100644 helm/ocaml/grafite2/matitaSync.ml create mode 100644 helm/ocaml/grafite2/matitaSync.mli create mode 100644 helm/ocaml/grafite_parser/.cvsignore create mode 100644 helm/ocaml/grafite_parser/.depend create mode 100644 helm/ocaml/grafite_parser/Makefile create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.cmi create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.cmo create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.cmx create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.ml create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.mli create mode 100644 helm/ocaml/grafite_parser/grafiteDisambiguate.o create mode 100644 helm/ocaml/grafite_parser/grafite_parser.a create mode 100644 helm/ocaml/grafite_parser/grafite_parser.cma create mode 100644 helm/ocaml/grafite_parser/grafite_parser.cmxa create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.cmi create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.cmo create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.cmx create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.ml create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.mli create mode 100644 helm/ocaml/grafite_parser/matitaDisambiguator.o diff --git a/helm/ocaml/METAS/meta.helm-grafite2.src b/helm/ocaml/METAS/meta.helm-grafite2.src new file mode 100644 index 000000000..c6603db5c --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-grafite2.src @@ -0,0 +1,5 @@ +requires="helm-library helm-tactics helm-cic_disambiguation" +version="0.0.1" +archive(byte)="grafite2.cma" +archive(native)="grafite2.cmxa" +linkopts="" diff --git a/helm/ocaml/METAS/meta.helm-grafite_parser.src b/helm/ocaml/METAS/meta.helm-grafite_parser.src new file mode 100644 index 000000000..389007b5b --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-grafite_parser.src @@ -0,0 +1,5 @@ +requires="helm-grafite2" +version="0.0.1" +archive(byte)="grafite_parser.cma" +archive(native)="grafite_parser.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 306dc2695..aa9fb9c41 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -23,8 +23,10 @@ MODULES = \ cic_unification \ whelp \ tactics \ - cic_disambiguation \ paramodulation \ + cic_disambiguation \ + grafite2 \ + grafite_parser \ $(NULL) OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index f3687789b..a7b0f3eea 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -23,11 +23,9 @@ * http://helm.cs.unibo.it/ *) -module Ast = CicNotationPt - type direction = [ `LeftToRight | `RightToLeft ] -type loc = Ast.location +type loc = CicNotationPt.location type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term @@ -36,11 +34,11 @@ type ('term, 'ident) type_spec = | Ident of 'ident | Type of UriManager.uri * int -type reduction = +type 'lazy_term reduction = [ `Normalize | `Reduce | `Simpl - | `Unfold of CicNotationPt.term option + | `Unfold of 'lazy_term option | `Whd ] type ('term, 'lazy_term, 'reduction, 'ident) tactic = @@ -124,7 +122,7 @@ let eq_metadata = (=) (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 3 +let magic = 4 type ('term,'obj) command = | Default of loc * string * UriManager.uri list @@ -139,12 +137,12 @@ type ('term,'obj) command = | Alias of loc * alias_spec (** parameters, name, type, fields *) | Obj of loc * 'obj - | Notation of loc * direction option * Ast.term * Gramext.g_assoc * - int * Ast.term + | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * + int * CicNotationPt.term (* direction, l1 pattern, associativity, precedence, l2 pattern *) | Interpretation of loc * - string * (string * Ast.argument_pattern list) * - Ast.cic_appl_pattern + string * (string * CicNotationPt.argument_pattern list) * + CicNotationPt.cic_appl_pattern (* description (i.e. id), symbol, arg pattern, appl pattern *) | Metadata of loc * metadata diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 28f42ca6d..7687bc522 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -27,8 +27,6 @@ open Printf open GrafiteAst -module Ast = CicNotationPt - let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator @@ -186,7 +184,7 @@ let pp_alias = function sprintf "alias num (instance %d) = \"%s\"" instance desc let pp_argument_pattern = function - | Ast.IdentArg (eta_depth, name) -> + | CicNotationPt.IdentArg (eta_depth, name) -> let eta_buf = Buffer.create 5 in for i = 1 to eta_depth do Buffer.add_string eta_buf "\\eta." diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli index 79900a342..eefcd9ccb 100644 --- a/helm/ocaml/grafite/grafiteAstPp.mli +++ b/helm/ocaml/grafite/grafiteAstPp.mli @@ -24,7 +24,7 @@ *) val pp_tactic: - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string) + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic -> string @@ -34,19 +34,19 @@ val pp_metadata: GrafiteAst.metadata -> string val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string val pp_comment: - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.comment -> string val pp_executable: - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.code -> string val pp_statement: - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.statement -> string @@ -55,7 +55,7 @@ val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string val pp_macro_cic: Cic.term GrafiteAst.macro -> string val pp_tactical: - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string) + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactical -> string diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index b1601911e..dd9febedb 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -27,7 +27,7 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string -type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command +type ast_command = (Cic.term, Cic.obj) GrafiteAst.command type moo = ast_command list * GrafiteAst.metadata list (** *) let marshal_flags = [] diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli index 663d2fa43..8fb1b2398 100644 --- a/helm/ocaml/grafite/grafiteMarshal.mli +++ b/helm/ocaml/grafite/grafiteMarshal.mli @@ -28,7 +28,7 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string -type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command +type ast_command = (Cic.term, Cic.obj) GrafiteAst.command type moo = ast_command list * GrafiteAst.metadata list (** *) val save_moo: fname:string -> moo -> unit diff --git a/helm/ocaml/grafite/grafiteParser.ml b/helm/ocaml/grafite/grafiteParser.ml index 90198052f..3d0ea500b 100644 --- a/helm/ocaml/grafite/grafiteParser.ml +++ b/helm/ocaml/grafite/grafiteParser.ml @@ -28,7 +28,7 @@ open Printf module Ast = CicNotationPt type statement = - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.statement diff --git a/helm/ocaml/grafite/grafiteParser.mli b/helm/ocaml/grafite/grafiteParser.mli index 256e2ef27..7b33c6e42 100644 --- a/helm/ocaml/grafite/grafiteParser.mli +++ b/helm/ocaml/grafite/grafiteParser.mli @@ -24,7 +24,7 @@ *) type statement = - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) GrafiteAst.statement diff --git a/helm/ocaml/grafite2/.cvsignore b/helm/ocaml/grafite2/.cvsignore new file mode 100644 index 000000000..8697eb7ee --- /dev/null +++ b/helm/ocaml/grafite2/.cvsignore @@ -0,0 +1,5 @@ +*.cm[iaox] +*.cmxa +test_dep +test_parser +print_grammar diff --git a/helm/ocaml/grafite2/.depend b/helm/ocaml/grafite2/.depend new file mode 100644 index 000000000..28de95ab3 --- /dev/null +++ b/helm/ocaml/grafite2/.depend @@ -0,0 +1,14 @@ +matitaSync.cmi: grafiteTypes.cmi +grafiteEngine.cmi: grafiteTypes.cmi +grafiteTypes.cmo: grafiteTypes.cmi +grafiteTypes.cmx: grafiteTypes.cmi +disambiguatePp.cmo: disambiguatePp.cmi +disambiguatePp.cmx: disambiguatePp.cmi +matitaSync.cmo: grafiteTypes.cmi disambiguatePp.cmi matitaSync.cmi +matitaSync.cmx: grafiteTypes.cmx disambiguatePp.cmx matitaSync.cmi +grafiteMisc.cmo: grafiteMisc.cmi +grafiteMisc.cmx: grafiteMisc.cmi +grafiteEngine.cmo: matitaSync.cmi grafiteTypes.cmi grafiteMisc.cmi \ + grafiteEngine.cmi +grafiteEngine.cmx: matitaSync.cmx grafiteTypes.cmx grafiteMisc.cmx \ + grafiteEngine.cmi diff --git a/helm/ocaml/grafite2/Makefile b/helm/ocaml/grafite2/Makefile new file mode 100644 index 000000000..5a8d64fad --- /dev/null +++ b/helm/ocaml/grafite2/Makefile @@ -0,0 +1,13 @@ +PACKAGE = grafite2 +PREDICATES = + +INTERFACE_FILES = \ + grafiteTypes.mli \ + disambiguatePp.mli \ + matitaSync.mli \ + grafiteMisc.mli \ + grafiteEngine.mli \ + $(NULL) +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +include ../Makefile.common diff --git a/helm/ocaml/grafite2/disambiguatePp.ml b/helm/ocaml/grafite2/disambiguatePp.ml new file mode 100644 index 000000000..c3a48e409 --- /dev/null +++ b/helm/ocaml/grafite2/disambiguatePp.ml @@ -0,0 +1,83 @@ +(* 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/ocaml/grafite2/disambiguatePp.mli b/helm/ocaml/grafite2/disambiguatePp.mli new file mode 100644 index 000000000..69b6e8451 --- /dev/null +++ b/helm/ocaml/grafite2/disambiguatePp.mli @@ -0,0 +1,34 @@ +(* 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/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml new file mode 100644 index 000000000..fe67c2fc4 --- /dev/null +++ b/helm/ocaml/grafite2/grafiteEngine.ml @@ -0,0 +1,686 @@ +(* 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/ + *) + +exception Drop +exception UnableToInclude of string +exception IncludedFileNotCompiled of string + +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 + +(* 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 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 + +let apply_tactic ~disambiguate_tactic tactic (status, goal) = +(* prerr_endline "apply_tactic"; *) +(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *) + let starting_metasenv = GrafiteTypes.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 = GrafiteTypes.get_proof_metasenv !status_ref in + let proof = GrafiteTypes.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.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof p -> p + | _ -> assert false + in + { !status_ref with GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { incomplete_proof with GrafiteTypes.proof = proof } }, + opened_goals, closed_goals + +type eval_ast = + {ea_go: + 'term 'lazy_term 'reduction 'obj 'ident. + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status ref * + (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + ('term, 'obj) GrafiteAst.command -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> + + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + GrafiteTypes.status + } + +type 'a eval_command = + {ec_go: 'term 'obj. + disambiguate_command: + (GrafiteTypes.status -> + ('term,'obj) GrafiteAst.command -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> + options -> GrafiteTypes.status -> ('term,'obj) GrafiteAst.command -> + GrafiteTypes.status + } + +type 'a eval_executable = + {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status ref * + (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + ('term, 'obj) GrafiteAst.command -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> + + options -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> GrafiteTypes.status + } + +type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit } + +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 GrafiteTypes.proof_status = GrafiteTypes.No_proof} + +let eval_tactical ~disambiguate_tactic status tac = + let apply_tactic = apply_tactic ~disambiguate_tactic in + let module MatitaStatus = + struct + type input_status = GrafiteTypes.status * ProofEngineTypes.goal + + type output_status = + GrafiteTypes.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, _) = GrafiteTypes.get_stack status + + let set_stack stack (status, opened, closed) = + GrafiteTypes.set_stack stack status, opened, closed + + let inject (status, _) = (status, [], []) + let focus goal (status, _, _) = (status, goal) + end + in + let module MatitaTacticals = Tacticals.Make (MatitaStatus) in + 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.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof + { GrafiteTypes.stack = stack; proof = proof } + when Continuationals.Stack.is_empty stack -> + { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof } + | _ -> status + in + status + +let make_absolute paths path = + 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_comment status c = status + +let rec eval_command = {ec_go = fun ~disambiguate_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 + GrafiteTypes.notation_ids = + notation_ids' @ status.GrafiteTypes.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; + GrafiteTypes.add_moo_content [cmd] status + | GrafiteAst.Include (loc, path) -> + let absolute_path = make_absolute opts.include_paths path in + let moopath = GrafiteMisc.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.efm_go status moopath; + !status + | GrafiteAst.Metadata (loc, m) -> + (match m with + | GrafiteAst.Dependency uri -> GrafiteTypes.add_moo_metadata [m] status + | GrafiteAst.Baseuri _ -> status) + | GrafiteAst.Set (loc, name, value) -> + let status = + if name = "baseuri" then begin + let value = + let v = Http_getter_misc.strip_trailing_slash value in + try + ignore (String.index v ' '); + raise (GrafiteTypes.Command_error "baseuri can't contain spaces") + with Not_found -> v + in + if not (GrafiteMisc.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; + GrafiteTypes.add_moo_metadata [GrafiteAst.Baseuri value] status + end else + status + in + GrafiteTypes.set_option status name value + | GrafiteAst.Drop loc -> raise Drop + | GrafiteAst.Qed loc -> + let uri, metasenv, bo, ty = + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> + uri, metasenv, body, ty + | GrafiteTypes.Proof (None, metasenv, body, ty) -> + raise (GrafiteTypes.Command_error + ("Someone allows to start a theorem without giving the "^ + "name/uri. This should be fixed!")) + | _-> + raise + (GrafiteTypes.Command_error "You can't Qed an incomplete theorem") + in + if metasenv <> [] then + raise + (GrafiteTypes.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 GrafiteTypes.proof_status = GrafiteTypes.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 = GrafiteTypes.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 = GrafiteTypes.add_moo_metadata uris status in + status + | GrafiteAst.Notation _ as stm -> GrafiteTypes.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 (GrafiteTypes.qualify status name ^ ext) + in + let metasenv = GrafiteTypes.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 GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { GrafiteTypes.proof = initial_proof; stack = initial_stack } } + | _ -> + if metasenv <> [] then + raise (GrafiteTypes.Command_error ( + "metasenv not empty while giving a definition with body: " ^ + CicMetaSubst.ppmetasenv [] metasenv)); + MatitaSync.add_obj uri obj + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} + +} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex -> + match ex with + | GrafiteAst.Tactical (_, tac, None) -> + eval_tactical ~disambiguate_tactic status tac + | GrafiteAst.Tactical (_, tac, Some punct) -> + let status = eval_tactical ~disambiguate_tactic status tac in + eval_tactical ~disambiguate_tactic status punct + | GrafiteAst.Command (_, cmd) -> + eval_command.ec_go ~disambiguate_command opts status cmd + | GrafiteAst.Macro (_, mac) -> +(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO + raise (Command_error + (Printf.sprintf "The macro %s can't be in a script" + (GrafiteAstPp.pp_macro_ast mac))) +*) assert false + +} and eval_from_moo = {efm_go = fun status fname -> + 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 + status := + eval_ast.ea_go + ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic) + ~disambiguate_command:(fun status cmd -> status,cmd) + !status ast) + moo; + List.iter + (fun m -> + let ast = + ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m)) + in + status := + eval_ast.ea_go + ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic) + ~disambiguate_command:(fun status cmd -> status,cmd) + !status ast) + metadata + +} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command + ?(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.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex + | GrafiteAst.Comment (_,c) -> eval_comment status c +} + +let eval_ast = eval_ast.ea_go diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite2/grafiteEngine.mli new file mode 100644 index 000000000..efebbf048 --- /dev/null +++ b/helm/ocaml/grafite2/grafiteEngine.mli @@ -0,0 +1,48 @@ +(* 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/ + *) + +exception Drop +exception UnableToInclude of string +exception IncludedFileNotCompiled of string + +val eval_ast : + disambiguate_tactic: + (GrafiteTypes.status -> + ProofEngineTypes.goal -> + ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + GrafiteTypes.status ref * + (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> + + disambiguate_command: + (GrafiteTypes.status -> + ('term, 'obj) GrafiteAst.command -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> + + ?do_heavy_checks:bool -> + ?include_paths:string list -> + ?clean_baseuri:bool -> + GrafiteTypes.status -> + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + GrafiteTypes.status diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite2/grafiteMisc.ml new file mode 100644 index 000000000..910f8a483 --- /dev/null +++ b/helm/ocaml/grafite2/grafiteMisc.ml @@ -0,0 +1,74 @@ +(* 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/ + *) + +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 baseuri_of_baseuri_decl st = + match st with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> + Some buri + | _ -> None + +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 = Http_getter_misc.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 = + let baseuri = baseuri_of_file f in + LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite2/grafiteMisc.mli new file mode 100644 index 000000000..8cc384abc --- /dev/null +++ b/helm/ocaml/grafite2/grafiteMisc.mli @@ -0,0 +1,35 @@ +(* 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 baseuri_of_baseuri_decl : + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + string option + + (** check whether no objects are defined below a given baseuri *) +val is_empty: string -> bool + +val baseuri_of_file : string -> string + +val obj_file_of_script : basedir:string -> string -> string diff --git a/helm/ocaml/grafite2/grafiteTypes.ml b/helm/ocaml/grafite2/grafiteTypes.ml new file mode 100644 index 000000000..2e2daf4e7 --- /dev/null +++ b/helm/ocaml/grafite2/grafiteTypes.ml @@ -0,0 +1,218 @@ +(* 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/ + *) + +exception Option_error of string * string +exception Statement_error of string +exception Command_error of string + +let command_error msg = raise (Command_error msg) + +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 status = { + aliases: DisambiguateTypes.environment; + multi_aliases: DisambiguateTypes.multiple_environment; + moo_content_rev: GrafiteMarshal.moo; + proof_status: proof_status; + options: options; + objects: UriManager.uri list; + coercions: UriManager.uri list; + notation_ids: CicNotation.notation_id list; +} + +let get_current_proof status = + match status.proof_status with + | Incomplete_proof { proof = p } -> p + | _ -> raise (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_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 + +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 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 + | _ -> raise (Statement_error "no ongoing proof") + +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 get_option status name = + try + StringMap.find name status.options + with Not_found -> raise (Option_error (name, "not found")) + +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 (Printf.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 (Printf.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 get_string_option status name = + match get_option status name with + | String s -> s + | _ -> raise (Option_error (name, "not a string value")) + +let qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +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' } + +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 diff --git a/helm/ocaml/grafite2/grafiteTypes.mli b/helm/ocaml/grafite2/grafiteTypes.mli new file mode 100644 index 000000000..17544d5bd --- /dev/null +++ b/helm/ocaml/grafite2/grafiteTypes.mli @@ -0,0 +1,77 @@ +(* 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/ + *) + +exception Option_error of string * string +exception Statement_error of string +exception Command_error 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 + +type option_value = + | String of string + | Int of int +type options +val no_options: options + +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 dump_status : status -> unit + + (** 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 get_option : status -> string -> option_value +val get_string_option : status -> string -> string +val set_option : status -> string -> string -> status + +val qualify: status -> string -> string + +val get_current_proof: status -> ProofEngineTypes.proof +val get_proof_metasenv: status -> Cic.metasenv +val get_stack: status -> Continuationals.Stack.t +val get_proof_context : status -> int -> Cic.context +val get_proof_conclusion : status -> int -> Cic.term + +val set_stack: Continuationals.Stack.t -> status -> status +val set_metasenv: Cic.metasenv -> status -> status diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml new file mode 100644 index 000000000..26ebbd032 --- /dev/null +++ b/helm/ocaml/grafite2/matitaSync.ml @@ -0,0 +1,181 @@ +(* 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 GrafiteTypes + +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, CicUtil.term_of_uri uri, false) in + let moo_content = [statement_of (UriManager.name_of_uri uri)] in + let status = GrafiteTypes.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/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli new file mode 100644 index 000000000..df4f111ab --- /dev/null +++ b/helm/ocaml/grafite2/matitaSync.mli @@ -0,0 +1,49 @@ +(* 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 -> + GrafiteTypes.status -> GrafiteTypes.status + +val add_coercion: + GrafiteTypes.status -> add_composites:bool -> UriManager.uri -> + GrafiteTypes.status + +val time_travel: + present:GrafiteTypes.status -> past:GrafiteTypes.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:GrafiteTypes.status -> GrafiteTypes.status -> + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list + + (** set the proof aliases enriching the moo_content *) +val set_proof_aliases : + GrafiteTypes.status -> + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> + GrafiteTypes.status diff --git a/helm/ocaml/grafite_parser/.cvsignore b/helm/ocaml/grafite_parser/.cvsignore new file mode 100644 index 000000000..8697eb7ee --- /dev/null +++ b/helm/ocaml/grafite_parser/.cvsignore @@ -0,0 +1,5 @@ +*.cm[iaox] +*.cmxa +test_dep +test_parser +print_grammar diff --git a/helm/ocaml/grafite_parser/.depend b/helm/ocaml/grafite_parser/.depend new file mode 100644 index 000000000..8baa095bc --- /dev/null +++ b/helm/ocaml/grafite_parser/.depend @@ -0,0 +1,4 @@ +matitaDisambiguator.cmo: matitaDisambiguator.cmi +matitaDisambiguator.cmx: matitaDisambiguator.cmi +grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile new file mode 100644 index 000000000..afb05493e --- /dev/null +++ b/helm/ocaml/grafite_parser/Makefile @@ -0,0 +1,10 @@ +PACKAGE = grafite_parser +PREDICATES = + +INTERFACE_FILES = \ + matitaDisambiguator.mli \ + grafiteDisambiguate.mli \ + $(NULL) +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +include ../Makefile.common diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmi b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmi new file mode 100644 index 0000000000000000000000000000000000000000..51403bfa4f6517993fc3db73d55b630e2bbfc815 GIT binary patch literal 1836 zcmZ=x%*`>hw6ydzFf?eHx@;c<0}DR`1H*F$24-0X2ByagjNOY8(=tm^T{4RkbCWXD zOA|{{7cAJo;BTCQBobeem|T*X?66?N0fh~lHcr^!paazxQdy8%?5I{;l2}q&%<$h~ zf&&xl*M|%YuQwcE;f5$R2q?WJW24`Rp6lLb6JHW-?!dag-OoZ7PkXlrhSe#h~3^V1T)HJwlgo5)Y+^}CTqwoZj zGBBVpg6BI_BW84H<|I~C#-oMiH!SvG2__;<`vQ0WSD?8p9&qkwIO_*A<@|=yf1vbV zDE-d?lr95IP|{^`er|4JUJ58-vP>Z^Wj+8Zorjs&)S*Vfql7?edjt(1G-b;9Nm)o~ z@*&)NkKu`cP+UL967m?X!y3g;p*q2mXfAmIcgZtofWCmzFQN1+2M0(I!SoVXL}V~9 zFirB) z8VeSvhU90b<{7LsR-DEd`{X=$lN2CiSy&bfUOzV$@riWpwlRh2-+Iy{(=(3l@Na z+<^P>{0ZhM!kjC5CHlcn0a$kD@qLJ zm`&PLSt9ZNz5`%@y7z@i;kz$NAs z8?ZC36S!H{Uv(^aYuULKqBj;SFhnl@!G*Lzc-?f{>pf&qmGy;PU zQC=BH=0sN8?C{+`;p!xXO`%600bTB&lx0v-_v3*2)M+mszq)*bWg_!iU{nW}6s0ES z8qD%Bu1t31aE)_~@{ai5Wdlk%iNzTuNjV0JpQQL7-bt%|{vzaS@xi9;pb!KWX9nuK sR=UmBY+H6__u>~prEfkiSb&;S4Pq_xYI>L|9^9RAVg85bXZ|?=0Nd3Q<^TWy literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmo b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmo new file mode 100644 index 0000000000000000000000000000000000000000..d78935a1bc1f88b40c29bfc8099a531a062b638d GIT binary patch literal 36185 zcmdVD33OCN7C+q8U6piqa#LflYLu(Pm(f`B5T7)XF7prSa6;=U{2?|0v;elHPc=KR0^Ip6sjs$NySdvD#k_tvfD z)qAO`S=_Mah!Gl z1|Xy(uzuES?-P&pbVKOtrg@*`#J6|7qi{oTtg6bRv7cLcW4@ON+eqMIhfSk0bC$yJ8#s_Cs3A zMFSA_M2I6yN0^JS2;o$O3lZ88o<-P(@C$+o!DbK+LKu%Q4PiFId<6U#c~A~j2v+aB z(nj+T!U*iMl&jz7*hVWiB*piT9{bj)|BJNI><+ZcT-xN9JlH;M`x@)-;lj|S*$%dk z{(=3C{)6^LJFvcp_d5sbj6Mvcq<*GJJI$p{I>aFz(j`BX2g}$;`nq}EW1nT7cE>=N z3Iy^-zAf#Y&=>0?O~R0-#fc+LIKl%=c=_PJz|(&H@UQI#{{K|x^aZ3%ekm8)-GAbp zcI4;f9v7Z%w0a~jgrUw!^HvvTce1v86PI$Kt+LG8?C$K9und$vudItYU|p@d;fJ#K z^K-TfLtCPL$QSiXebJ`a7M9bl*jEN4P$nCH+qH|fL7sTE{)y=l1kzw&o>$r)`C^{+ zQ;+0vpwPCpptr|G$>Ap9jC3H@I^CztLCNxBav^ zE>nlJdFq|ENZk{Lc1D{!X*V#mCqK+G7smFX-T4#JXB+Jp!aVu0V~n-Co+x7<>Wg6Q zl2^i7f5N&M*f+`J^xg1S;KJB;Omt!X$X;z-6~K$RxYpJW_z$@3i|nWVcCn1@A+16L z^2#=m*8wgqzdi}i5JxCNAUxcdz;}1y{W>akVQ@=e@^?ei`T$;8xAhnQ&7XF0Y1_8{ zf;`jzi`+O?kavswnVYsgigKcj&<;qCI;9-Q6Whmf%cp z%(j(n>pUm5yj9>H*TAfcxa8+Dgg>f_^6}dv^OUQjcBTPZ;(awy6ri%7RyG zU$kA?bZ0rx2HEa7LKy5R@RS{??42$fiMiGA#g27f5klcAuh*#%9%g% z#xe%lH|54O`wxE&2tU0#urSUHeghC#mz6E)vW&ivKh{CpB3)idvyYpOW_gDq!!tPIHy+d2WkwukoR zmj&y!vIrqfov@9hNga?!TSi!GUz9WF5XAAyJ(uX~YruW80{^5zOFs#`+r`4Fno7Tom4k8Ridxz@gg` z04NQpqL#hKHPg)UUskhtUj4%5H7#}R!x#R(aOmQOqm?dJx=*~~#v9vwzq>mA z;>n7V`o@;{mN%#`mjfZmwAs-;zki zgXY`!0ux!BNLEx-#FGUO`ev9)*hfjvSfLkwmhsRp%yjR=m|gpUhf- z&L&Lkzo4mkaZSrU9)+ov)FC!;uuV*fSGyHU?Oqg5PAY3!(o)|9wk_~9;iUB7rbcP> z^rppi;KolSb`z3jroh>mCzdV_x4*-(_FKdT0&9fy4FhD*&6gq?Rv{mN{5v$ z1hC$c3{32^5@xm@|D1YN@b$n16?~V`zv8xz`*l&gs#SN5SLhN3!ThW7WMFdt`Av;2bt_xk zrlPOi;xu}Fvh6NNwxp_leuV`J>`GOW{%~NDGEXo%3Q_Qr)Scj`%t`uGwQ1$MDIsj8zA;gX2vt1@~IXhuIzRTSNcd?>(*K4I)i zM`CDz>n9zbK-Tv34-1aj53X%mTvOjT7h}d^KbLpFZ~Otu9`l?20O?NGRMKxxNiF?0 z@RlA2Z;J*ju4}1TR@b;fn&}xzs@z{ctW2fD*9YoL=GV{fgz-C>-bLt2K%e55WSc%A z#YgmRfJBo3Ikf`_+xTB?Xe)6aV)vz!&;!QPH|QhBwkGvs)o~Whp2!}Y)E87T3%7B% zQIYsKxfh?ndsRu@Ycdc9PC|727`by#m0Z@aQ&(1#&PPnfC&z97&N1q}cB8f~QE3mV zw1?p^z6F_etrZp^)2NRC@L`imJ4L14ThUsne@eFNe!4*CR>O-=YSm#Ew(tj|J_GCy z2X=M5!l-~wo8(a|{KlxS0P$s`N~=_9CxDt!2IThCJ#~+2`1OfCa$Al15x_q-U~My^$YI*+@Q?YD(%2lbXhtdePKd3CG`AM7w(S^GqbUNMa57|4B+OM)y>6( zWyvDHIkZv1Ro1+!nY)$I*jCiqhl+{ogCU&>xKfyUv>sKZ4~UOVakI$;ySAHP7l)ez z$PFE#QQZ={3}!-V^%Bp2c8!Ad_=haGUh`tF?IE{Qy)`Jg8@pq01#zEsChrfMW9SY(}J9ZG#c!=mn z=>4ap(5p>w3eYDnQf41zhEo}H^Z_1=aTA=1`-d!0`a5NYwi-2@%00#r-5QAQTph2} zC+m}{&}+t|=ngQ!BY-!{!PBI>P^WwMi%oD2?jKpF^fslxLBBBSxMW~fAE(c*H);wP zHZ_dqN)LjSXO4xA^fjn&L%W`#*Xh>EDt)0(S=s~_gKEQkr5{oHG1hvb?v|=G_Jav7 z!TqLrN?)V&weh%7C!-~>(i=eZN_|C@z6|p=*YIOoOmGFjmj|j<^bi%D-f^G=$7_;- zNqg4%=FD?be!YFbLGEamL}N~%1Ktk(!muwgs@6$eidH(QD~+n8_Vst3=aC`iM>~rC zL<-;7+_%i_w7D;s``G6G&D=-vqzat&2g9LJE5%}sT9K+QW0nf6RvArR!4fIJR_tmO z{a)gqB>tJCPwzB>88y$t+*9CwkrJ|@ee*skzYl#if&PdsD zYMg7+7kOy=322(c5s9NjJF{%LxC0M~KKp-g8X3cdNQT5&5@(a(S^fclBWh^xDdL0;KF=uc%7km5NVB><@{@!<9lxESHi z^~OB(CJ$t&fD{tsJik;xDBFV?CQwC$I^W+^Kz-~%9WGEa2(_jYRHFw~BTz@DhQ2b6 zWl7!Q3|!Td=xaILwV7a}JKXI%5d+*383%QjDM*)a*gJwuv+KDC%5Vh>lkh`p(BAi+rf?e0_xjz#5caiZZe@`05LaEp&}2d z$Ty_^Z&Dww%RzZ4LVuxNru$W6eva`rMg0;JIu^L~F7BhC{*{hQO1Y&aCIl}RYB*Iz zj#Uv%*xUi~^n_lL(DeyD&ze)Qr~yxCU`btDEA+39+nx-H)w;M+j{+M9B0xN7=>DE3 zjV&^v(^1E1P95ku?ywj9Q$qKEo`qz0*NZH&1?5uQ!@1i{GG!d~igef1kP@3}LYIQ{ z`jb`oLlqe&qn=T9mc|G{8zlp@E=>(|1wWWj0%+HqsKU3a@LlxnrMiELY{3o_+KBtt zouI-OsPH=a_A*RC2I>Y5@(a=AIz14rJjNTP3Z5~cTYz(OV4BJdtIQ0agEwkVnE2}9 z9lX1<2)9#r3=Iz(6@zGydWi4IV1|`vof6&nqYu{4M2HI~E?()vk(%8YFm^3(R(>+s2(H^$>y@(wx@a|w>2f6o1 z?y3&T)3v09)*T7+42|+I_G95Ov{_#T!&z9zk^D>#a$ncjpY)0<#HL>L3b?~$g7sd3 zou)_Qmgj?PVzf<+l2&+qD2h=M&FW)kh~vg#Tv%9zF(aufIYyjaElZ_Z8AdqbBu(f+ zES0!uy3HAEMos`+VvLM4EPg|Vk_pz`7PK3^7U4onMKjJ(8JE)8!?ASH+3+h-2JxPe z`1lmcO-94T>Ggp_RK^!7<9qrQ_y85y;Ft7zeVcF(|BN=2Q4@dm--lpt)RQUSoAm@< zZq;KQ!G^+~*!H3vLtVUry+yFMc?J7e>FsF~# zzX+_qxmfo@n)~UnC+*b++hay=2~1QOwJKu){d^g8>8to8qhAHcKe4ZrQJ^x8k>%!K z4z4x&NIkn!&(agB^wjvcR_y3HJKP0xjD80=Z@W0ycQa})oj%S-c9zi}0Ob9^cx?P& zE?2=J2sY2*qXBHz>qV7%fj+!S9~~d-YtdAL%`~Gwb?~BJkn}-1?2Sxuqjv(}^T0Ul zB&cW`0c77$uK?*52uUy1^Qv@xd`xRLZ>dmb%V2shAc13Ap&EmRv0*iJU?3FHYqcYhCNltnndfHt^bCa578Q7$( zs6@)BkknR{s%)z06-<RA|KU4Cjr1GmJe**K)j4cY$h|y1=fhYAy7`K>t(CJjZ zZU6ksjrl8V^YOr8D)Ua2d9REKmp~ecKB*0Hqno`3{8a=tSK^~6w(DF#7}~37w|>Bb zeVo?!FBFEZ@Cw^mxRr$gukbO)Ky};(sWD^hC!~-In zdm#`#k|PKQ+dGWeBkrvE29Ci{vTwDFvU+rUjOTdsFEQpfNaokTOqIDxW!}nx&>kVd^v28tNsPT`%Zt0c&Gjx@f-Se zuf4CbMS}gh#DDj-aEp}8wv`+y*_k$bm}IB3UtRCt$KYD}|INQPW3Eg!q&QavHmafx z5@XGT^jL|pX|qukz98|f63gAf$&$u|aHEQSA@NlbW15SS9L5FTOMHXG@Yg6=Au-%6 z(%5@LjFlDQFys6kjPvG6+?R3gza?HP@luKLQp-k_b2VekeHgzbG1eSNZ>5y}((ysp z{~{yE!t+tZ*`!r;0^>p_#-i^SMoLkae#5DWJOX-wyT!Z`03 ziF-57-7c|6Dn}$9eUBy4Z4!UTHr!B#hr%uO?jAGrEUUCZ?gQP5Wi1shfb*pAzqb)B ze9zN1{0LgOigBS6PmnY$6fOLWaluB3S4+H1;%O2OmAH?@c)o%bik9-QZbREXl345_ zM=T;c%udRGVBymg3q{ogj0q#TO-yIwPy@j@tQz%<_@k6pGU}<$1)Dn;^mBYtXcc>Q zT3)KE!soo?v+zprO@s)YA#mIya>mG5e=k|)crT-#^Vi~Z_Ee`Xd@+H?*}AXeydcUg zY)9eKTEUw+Gz*`SW|l|;qfP^{50*MwlBzNPIfCTeAb=UE;_P%5L`AAmk#qDD+Q*HZ zH$>3lV<9%*atm6#UPV78^i6(iYSWjJ4!#G3pb%qzvV%m>UiF??q1P-BIZ53g8Nxu+P#7YTw&$jYZLd_#N9U0CJbIr1|0)w zmMK+edxC7dMTQ?uQH=Fv;d`v+8m|yf(M;M$EKKtXd%Fye^@?P@pLV!cfGrCkec}~V zyIjR8Y{Ke0W_JQ&qdo9ZFzDbCJk8;?-UJu%I?n`ac%5v5lj71U&#pdo28-)ep(rtS zfHzpgMv5T*lF+MC735qes@{niO*>aE!)1E8DKDv@%A6{i%qyky9sw!ffrQiF{*SC2x6fX%)#6#T7p9`=u*nvEI#f^aQ9V)jslv`c>d9r^3==*VRL@a?r&LLqD#1D#R8IiaG#}M{gx>KI zFLkJ%=c9VQ-m^-d;iKBygs%YA%T?e>)%Q!)_eW5bp9!u7>7b7^^b1xSC9b1Eg-UAc zn|=0q%|PVqWP+Ts(xTf09s?0@7Z6L^#g0)J2~m2i#0z=P^!KmI+hFraTY~XeXQD3{ z1qlG_I7yF|^kUZta+XMT5lPMRIzyXD_x1~mpq9U=qGg0R!V;H8$nL!UGy!jxzLgb~ zlUmV*%x_~JQxN1YVE$v~F<>LV#&LA%<5E4U=v?}>^jTiPdE%;lgS6fHEjq__bVX;| z#921s?WPvVh^l{<2Z^Y-S(@PR>+Po&U1Tv^y_(muX8kX(;9?7ei6i8&nl?fMsb{yx z6AZ~LbIz$$aPw~tth}-c{tb7Gioibfg0XR?!^E5BoKdOfE#KZ?UUw7e-EJb7ylhr| zldA7$T+^M6%5;%YUE8t6lPhGq;tZQn`TiZkyc`q3eoq9G9S8RTc!#yvBJ@^_d6_0M z6d;&IKcV`rPlY&iI1dp1v*$)n{K7W z2C;t)FzneNT`cKi#FAf>G#{Z$qE=#@%u-4XJifkV(cI$~)yOV^#$#zv;C_HQtV0!I z5C#wS(V-X9Kp!DwQ7`6~GQUakJ(*w5{KJy(;TrHOo{@AF1OCt}=q3d#y@Kx6jJnuF zu}u`&g!iPSC`Np9jy2$2Vtak1aK1;h#A5dG%6bbBpD#KSzoJr`fLn$E=TZ)bcN7sD zcnur4QyN&s{6^+KmwYAjH!?4?fT9XV0AX+TQZ$;ihKsyf4`M<3Enb10m=uk&{2XW# z2iOFr6yR__r;EXtvG1HT4t*!7kLII^6*9gWbx*tDv9CLMV=$jZ9P5m;MzzI#MxT4R zi98F#d`1P@RiCF--zfXkS{QwSQICTL{%^8-B}jI#`ZXr<58%G!;`aGFto|}sz1OF5 z&oPnL0P?B|Jf`}brTRQU@*CJ?`^p3Hp6E?Ry`*#C4W8rPy4}*xJ;_A20uyUR2lGM@ zzg~yO**)Ie@h0*C0Nz)DM^v92)n^}w!h~KyclxbkcjDF|l~f2WVCAzVokyL?SJ9IX5{i)K4e-#Lv`UcMHlEzVRq%V{-_tYdYUE;~K))^fL zNv}=ABO7o&fQT5N(EdL&KZJQ1%nP9h6DemNYkl0m$~D@xsK8wkT`oqO@CvSwg1xW@zXF%2al-uA)0exLJE6&M6b1&-jbm3Y5^+ofUdJZ7YUKI zl*7!9GMD8?=qFizq&0~=a7xMq&y)5($@VW|{#?m#X1;-WnGX~`;mYHAug-R9zPE@f zd|V2=15Sm1wOl=B6Lz1o@DW?G$s_nM))o3&qrc(xbE7}wb-U3Y@%j=TS$Qjs2fdX= z;RDiS?u*ijgQwDpTRGg~*k?2Sz?sg;meK6`t@H_1CU~|9?t!Cut2;P=ViUcr-9#@{ zfrnM^OH}VS*+Z{o56#y(PR|GGIuqOvsONR)|6vow;fd%q7Ig!<=*=Dbzc$go0OWcV zcu4i0u6nnU`W>X+2LoyrC|_-Y)u4Qt|G`?$4<>p$&@j<+(2fM9#ZHtYG*1(VNh%Hz5#1*Bv7;|0Sr~X!<==Od;6JPcXG-fG?=zC^ zgYA9m^Ps`+OmG7lvD5RQIlWDWZZ{br6}U(B>aBX=gp#uyz?xM5g37+~D$~vabYH1v zFm>>CzuLMb_CX_Fr19Q!LC0(Lj>QwBkoy3VI7|o(mv{)teAB7_q!+@ox^jRPn5dKtQCh`MdU6+eGz)=k4xXrEfHj@!1eHht89vD^*0Q0tL3bAxR zL018c9+SZ1jTFfta;uxI0XqYLEVNk+T*wxXv1uK|go?Y4BrWfHt~|vm$63AE&h(ClW`{DBokT*<4Woh9#CIM z$ClJxd35h6__E5XY7;s&?mHQm)7@lT3L{&u0(YyP+f=Xa>?aqYpL8{$3qkM#6FRqD z=Rzogd@hg1*{MeM4wG>Wkg-uM$UQ$rN4ZjmeP_|LKQ2@pVlwUkf!i$sJgL(+=}78;diFgg<1PTe zra*p}>Ny+$w}{v@W;Q&gv1gSD-J-M5_Ki5j?>=qHt~D7C0PlVkxJ~s)s2+cl?q$ra zptRHLSx{r>D(Hnq82eF7vA@K&t$8 zYVRDaf_eJh@jzFR$w^_lMRrygg9O<e^;oHTtah79kM)_?RPA))o>Es48U5Vz)ZpwBx#4)4Vp{KH?{=Gs z9s`!0t{B@v>y2%99GzC=wwp7**1>k8l?naIvK*cda`&-}4)`~+vIm&VqIQ#6r~W(9$Nt0H97Vq%H0nKaf9<$Z4Tcqva2CgW_ZC8J`!JPuro?omox{v3;vu-n) z!%+*I@{OwdM%DdEiru6QKsBFu)wo+)SwcFUQvbBiLhBc?fVLcL5rAxo!`3fI?M7FV zlVVrGV@&8%a5CCEKbp1DWKIVsm}B3dx-V7TIbh*u(#D~>?LJ=i7V?^L_Alh+;|}v< z^o76BQ5$Er9+31Nf}@z$A4odn@|1FE$7QECtfN*)|dr7YH~_(0-$d zP3lm;%+JH?6Y%gn)@Ssag3fKAj0>56L-K2wzlizQC4as%AB}#AYFrCFhyFPu=oQF5 zQFOgmaGnLVyFoF#8x%X!-a5kr{}Ty@Asv~Y8yPBMtx~w!gIZ@Xy`@6zLILu2m|}MC zD0aGZqf;Ga8+`|~rYEAeQ`>cpZ?E7Ss0NzHwvfKZ=-Jgq-|n9YWwn^h&CvZ5q}9D# zbzjVx3h37oe@a{W zu%rJpsz?k`;9_;Qo<)N2jl?^w48NoddtuLvG92Q_kaJ6l?^~m08zmH%7ApXII+br*B0Czj@9fy4ghYK{*d6 zPE@x&Rksl$Iq8+@IF}Z9*GGSxQ2torcPW6a9an4UkXz;EM-p!($a|h|#_ccV#)lHW z$J_6B=vPqB3W_kTL?E`|&0&#fn`F1U63za%WZwtA8s7n5`eo#B_RGx4pkp==vH(Zy zO(rI4#^5O_@*gulgZV2ZzuoDV88i*2UlweWe#xB&x8Or5-~`nz_{b(cu!;9=!oKuc zu+;;9m-vx|wqL$OQ!dycg_R!EXO_gLUfCxCG|nsd+yXg7{zW-V@WhO^ox--g$hO6} z%*s5S`M*g%llillM{mOY47csx#$F7QRrsXuQWeG`QgE(U;J(kTV(Bg`u{4`-UkFz* zIB$%-ip)*yXeP3#Pah?V`UvJKVCY6;p6B&uW1ivlR%4!Y7|ZmYvc`Ilk4*1SYpka* z<{fH{^|EZ(y~voIG{@|b@0bt27>o4qUM9RJuY*l^5U-^sT*7OX2}e_l_gJB~c#p-T zX?bp6HrQWF>N~hSj>Y@=T(EC&rb7F3@_Pq6ca<@4e&z{d9wYD^Zld2N<771sfW>_? zRh+SmzJY)d;~LdjCmIfzGKXrsH2PQk()RDJMhs2R+_-w zX>oC4RsXBQ4t#WjiGB+Z__{xF(hBbK!eCw;}9Kbn~q77{w3VUJDzufX~?My>CtyG&PM-0{5tg% z#}jx;-km0;!4<+28owtjH(Bt6S@48csxHr~E}yWLutqI!d$s6%q4}D`FS(QpNZIwV zX)$9SuEOatpN|cjtP)VhH1B*>SfL6hh>tblLePHJqm34%ale_g3v#7~3nf0Ap7J@b zhp#v3edLC0gJqw?K33s-lAC#1s;d@AH_YGV*lN;wl55gNlH=aaL@n(AJgOgQ(&TKn zodu`u=br^fwaGddEtrB=#Z;kDg`+qN=HY6{bv&NuVg`o?x_H*_f1;cDmdQE{STija zj>KymuTDMD&Ah~9;eF7oSvWwfx?HHbTq=UWgfM(CTKtA58hw%`UnSu{Yg51a&tVA9TKx`!;JaYPhe19iV5EtZ`o zP`uqlUxO8~zo%US9bIhF))J{3*U<-I!Uc?fI<>m4B<)iFqB^tHWMLOB3zON)RhMb1 z%X!q=4D|M1CJnoKY1f;y1bTb6^!Bube@&fPYqIVG?!6ZG2zy?l%BE)1=L-1w7Ozz> z+9ke^njPcUZ1fPoxteVj%`PU)SRd0^gZkzPrwY&sDfREkeG-%QGd0;y1`XY)kAsTw zdVAW>ChdE4s-!NUj^nfrOcSx!ajfh~r2X1KzX6kt_fWFolGdx@b*lIU>i08zsJ$xBt<}Wb|Hi z26~vKcZ^MlC1l?&nAa2Y<=>giYB8BD1Syzf@oEIa8FcMKxwM<)QFv@WT&v$SJx0$S@>kQKIo@aW4Nnb=HzcYBDgEL5P@*7LW0F!+d zM13aSYg0v6s-l;v$iu}Mq@MzUC!6$DDQA$r%I^%KznJW`z(tR8aIb?N=lYxh2L9}e z0I-hl3l;TIMFU+u!Wl%)^_)Ta@m69ZMPf1?&t98y2H{pIzD(j)D&TLvezo3p1{cfi zb-evzXU$$In&tRMpaQ-DA&CP8=g$&fLd?JaPO~3Vv*G;(e1ydtEg08Gyq=n^^lLV2 z0N`BB_7=@{BTSW#={A#9?g8x~Km$_hcbq}`E7YXl8KnOc8hOQ}Z}|_-ApKRpexsM0 z?9ZTr9ejzW@O@R(!{-d}2qJwOPOx-x2JiWuLA1eSe-8rRxdaL^|LNomqKiy6ycAcM z7pOw)3%}!Y2H&8LuTA<+pEKC$cLvb|O^#_dIhc?*$hUWL29dW+P8a~`c(q-{?oqK# zVninLGt~8TM_0h*5p|OPt!U;fiLpU}LtFl7QpDN8IbCkArfTBeZD{7ClxFg=s{M<~ z|A3l_^ZXqY($kqAh2bK@JxsU@%Q|cohP(SGNs-r0&fegEFTCupV#nhZU`hv*B%OoB z1!xR1;WG3vXR9z==HDueBu&nNz&*g?^2LR{eOrZ*7L#)j0AP=2s#t-Fb+FI3rW4wE^H<1mg@MWzhoow>`F)ZsuO`$D9eX!*}# zE%b_|hbb1s^q9>$qw7gRp2w#GPkP-0oe4`3jOr&y+``*Wb=on}S4gLm1%1AKN|pbr zAekkx31bu4xa;Izk5g`>2}4ulf2}~DGldA2!By|-bv0p@P&dg zzy`5Pgvdw_bDEGf5pJJ5T|950AROuyOqGI(!bkR>6S}u|Yo*+>?{MW!mh4zdX`E!M z*|vjx3PEd*fCJOhQ*7ivv+?E4^6PCiTOqN3DEkh z2|r4g!g+nBjQ`=sxMZ{sO(L^Q4jfs|D=q=-hg4{I@zleQNZjPS4uIDJC#bwnRo>UQ zkGD&t3;qM?-nv(%3BSZ=CgJD2H)$i<(K@i-2(giYsYTT4l&V+ z@-PE|Aug5pIJb{~!2ay62gBP;_`E6;e%o8Mh0&eALM2}Yj)#$`yeX&zKP;Y6&tqOa ze6a?!>m{zCk+*l+Vm8>pL2r^?lE+hr1kD>F2**l1k7$p3t_jfav7lNf@qF4zu5W>t zy)>o&yq;o8T~hkb;+)b%V$^>L59PW0i&Z9q2N{t<6Uk#4zJDXr{z$%mmp1&0$sN>g zat8)hsJw{EtDpM`t*L=jkkR02~b1*vF@{ z$tHIKDj6SGrgEpN+!LuYlW_oQ+2qyYJn6`uC6uR8^pEs$-ua|INwZ^rUQht!;cxb# zBHy@)90roQ(2;Ad$k4#d!@q%%Y2K5LaCeit0F2ZHnpN%|DtBKo9+PndDtpMs3C0R& zd8)({$jQTgBZxZlO85={@ko-&@ou-7?AKCOkc%zVzo^`;u9)yLaOz1{WEHf&(nMNV z)?xUH9Pb~#!o?;RPg-*?2rN}OU#Q%HRQ&)My&{-6M$R;m(^8{XMDG_f_xAB@Ysik+ymq&PY`sb0!XvCrqRs)o=1uKgZK| z+t);o0T{Z-D>zvSIA3xG`P@@%;zXM`!6sJOgm>sQ_juxG?d$IA z^N9&qJwpm}JfikVUGAT}veN}9<`tY}$*&M1_WV(FG)-%nbN*-qx0jbV_7$zfrf7wU zj-tsQ#RqV;;*hFL6kk{H*6``GOy1$`ChxF7gUbGg%E{)g>{)Q?_^e+(x-@o_D@}Bo z&IaN{{{gY|$tLd@AkK9Vv)@F&zOcjju=MdJuMQBkf#X#6`6~NGlD-&DBg;gO0(Wyv zbQWshelm#9@(&p42b#P_pe}Y%F9z|ed;><>Hzsc>?k@?{tL!3`-OF~B%mong9bQ*~ z{G)bXFLxg?`!b2U)7tOsv_ec@OtGgQ3$csQPPd6e1*gBnJ&2j?cYJ-VcXG+3pD38r zyMg#A#xR<5fTWJW9H7~IF`r86$($GByB)9{>H=p@qW7EV z-MqCwXMs2rAHByrmy&jy$-}|oyk`OnRn}E1>ro(^%!k0*?Vjkh)AVjqeT>z|P4qdE zba%s}&ztB{)VA3hqtnhXd3eB)_j+J~$~so9^;LD z>rKWhawA9LEZoMMQK?URn%s$ykK3Q2QS`{Zj-R$0;L*>>WDmC=eGXZCW}^RQncV=# ztAD=tnbKC9d>p05*R$(X)&VMOnL9YLy+3pRJNgs%zoTFK_rKF-nfwTl!Y&eze+=_& zf2R#F`Pin*&j`#{IK&sluql$*g~s0ONrLvh)75v*jnd#ui4CQ4OG+vRAFHAnq){4~ zercSNl19#zltvDAGMw!vd9ll6^kK{0q zddy;@1Xp@1jmjQ=vEn|4R z%I-FrOp`weC=&xGs{EMBA3>82;l!58_pQNjdKimlEDSOEK#W-#gaeoxOx_y2d`d}0 z`6^!}dzHzN?*hSm&ymjtnT%(vc+dZ7XT8JZ*P`0_{DfISo+`jR8hX~PEcsnR38*^GY0 zQ)?tzDd<7`9&E(@zNB+I;BJ}%;xCt%S^YKZD!!5`?CjTLT zJcv<2^*m4Yyu|6M;rk%8gHt^aQ=#y3Hny->Vl2v(I;6vqOhAa13Ngb39ES@v)gyp* z4Ni5|!cv}-D#Umoy2z};2;W`aBGrX_v6Q7IcQ)T2#j-Tw7+~f^#{jFm@jsL_`5%J& zZ5Rzz&q=E1S?sU!^bRjvVNHjxoMy+-T>C^ew8rFPFOlB}a1dt3;~Ed{Dy>FB4JQ8! z0N`2hb~RvcHNaWlz^eIkmdG3T_V3xu^}S*b#Gr}dZ6x&8{4^6C=%k`1lb^_wIbGh{ z2@^diC5hrv4u4U@IL}-A7MCSRqKC=kj4!{J$y~&1ACp<#?q}Xr@jzQLz$W@TpQka=f5`ELoN>azfhO}9);!u|9>r_iWX^Uu__IfU zxK!wUK(BZ|DX8!u_P5pSYZLY>UB&jp>BW0_;5@dF^|Z-)idQ^~dyLly@l1}_jV9~5 zc+%1t<{e)s9-1(j&w5n)S(p(#T@>B!W}_cV)*fn!ejwSm?cH}ID`!vU{Lz;(u&bDV zyU8CWe#()0mmH;zRK+h#{G!B9Nqniqqb078xRQP2sFJ36$GUDz9w^@R`)~Xa#8*Y} zeS$ty;wp*9N<5APk4`z&Hj{%{756^>$hEqLa=ub?RIzvbrT82v7*BFF{?EGR_mO3Q z5d7c2j$WLE8IXtFp#0(2(Tnf0TD#NJA-Rpe`4r;o#u{%$`1?6$B?5H}EUzBh45 z;dB=8-2(n+g4YgN(%gi-=`prkA7|(j{MjJ}1zE z4nQW~d*afi3!%Cc(mis38se<|XUSxiquC{0;h4gyJJtUOHDDN4J4WSURO^YOIap2QU}{i} z4Swu_rhMrP6T_LFSj0u@{}bjls*A=q!0q5t?m%Et_o3?lkm`?_kx|`1bpXCM3)029 z2vlR<{%5GSiQ%Y9EDz`BRR6K6|AjK{;sa<9p@{C^5`O|ZWsr{EhvH~81&48Uw>RJS z9){s^fbI{v{d{z_iIspZ_E#Lb*z?3I&l-~}m)GFOCRPTBemGXC`nRh7cst&xz5Nic znAku-48YMrRrZbQpGJt`I>)1NkBQ-_a15)Rw^i9DRfeU7QJfo$!?2%S%`XY0>bu;; z_5^G>PIRcUg{tg6wp6}pd0j%EmCz@odhq}74d>!}L@Za^u5*oKZ-ewVcBf45@#piYH_%=Nu5MaS6b3@p9ida1cl z;$tM9%>IWimCvrDuYg_Qds%n|)hD}R6T1MFuCbL~EX~^u^)*6qE%p%l>O7C>u!&*& zFm{E-Kktw5*9rb5z#pc2rRI<73lqcqF?NH+p9n_x(tT4EsAo*<769Cg(x!~ z%I$7U{PiYXQmOC4A8T-;=B%NJ`*2!8l|G|NpNr$|)po8WENSQllgt<l=%?iHi{;>kWMNeevR&M*Jy* z)Dx~QIH&IR%`WRwl)J2jg~7nGoyAulXYqxCk8)qX<$|U2_T5oFWXO^E{AZ0m*X)G%U2RT{Bq5FW@XQu|;zJ1CMob`L{y) z%c4#9z&qEK7~6D(=QRW0n8Fe5rf`3}!>k5fsRq5^I4fPs&vZLuepigK;HMCMr9!;k zp|E!D)5(_Lp`UK|ZWE)s=bRHd6=>$&Z!&qy~*pgAQ_J zp2QP9rH<_&^ej$dDYdRfWcRAXTPU03yv2}XW3kMXfV%7uxZx7NBJoSaX&72lTRRu_ zw4`Yn{`5@h;dX1%{rh3Iwlu+cO=6jXH2wb5PO%9Io$#vMMlp4HpVch!Sc7Wc@nAj` zn2#L2;i;STgh_pX?4Q6Z(tzdFBRERFZM0uCx8d~F{%w`OO{Va2ND#+gepCa$R)hBC zI&BgL#(aGvwp8()6(~3QHdO*AnZg7xa6Uya2L1@O9O`YV1eTb>jktdu-lI<_=|Sa0|9*w{;J?kSw`>fZ^cbj#Rn!5t=Gj9>-ass%bj%VMSt)o^`j#-GQ--z%u~=d$0D+z_9L>MHPQK|f5v z63O}H8>^P0-OD#N%c1FhcW;LLAvG1-Af+9|5W8o0kcE!GI!U(hB!TsFQ3yjs!*6)xX z@0~f|*^*VsBQNhe0)NwxVlJPZwO7$E`yThw+G8I3y13@umlKJSDK$&V&t2Dd&LLxJ z-}-de);qfX@&y!BHWhy@v1LK|qo@D9ePyWUDVOhe!RT{eIuE8;Ho0ykj?b1?OwXM& z{MfbcO#kz>y}#Z1-~jynMEUzc<-P8URG+uwjAh?HvE_o%)Az&XLC0_Ammf8v@uW4u zm0RDwe9JXoY=7amL}IY-uaK2Lwza5c|H5;+ANAwT?uVV#{Y7m>1`~<$sa%JS zX%|MvKG!5Wu(0v05mUZ<=%DQ7;R8NiIW0E3J!?xM(SQ7yl`ReR^U6m&9{lm7GY$$aJ#ds-^Xcbbp~~qk z&2=@4%decg_p137;W0;#nLTONuJaB|B!;?GPN`{Lwy36|{2!affBWm^DZh?>_r#H# z`XBHn8squ0^79IUJ8#+Rji0y7KYqa@XHICqT^Ao;uPpDKwobp3^|Mi!C{J|$LzpmGX zK11>Jx|Z^5Z|Ie_`K2eX4pmHjVok3x!@;KaM-T>sXA(VwEnoJ9 G{Qm*bfT+6w literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmx b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmx new file mode 100644 index 0000000000000000000000000000000000000000..bef74642368e1ed11df6d9c01157598e84d90e54 GIT binary patch literal 1766 zcmb7Ec~BEq9A1J|M8~tmi*k4&7V8TELgX+3g0v(W4YYXB^(EQBO0vP-B_?8NrN971 zB6S3hR-V;iitRX*dR4*Tt*r`b9q|OTZKz^ZELN>z9|dQEBQtd8{k89X@B4k<`+dJ? zXfy~V63IdUBsuFV4idz`Jp@726NKw01R*%(Mi7$;(Hs`)X`YIqIcU_-DH)Kb&;WrH zp@5#91Zz6Q0guw6VW};-(@ssYRxREzQG(E917bxw;*xoC-L*S2n|F?Xc7FsyQ&lX@@Op4CyS~oi>Xo%Yye6{XTwxpDQBW3|NdYqT z$R#1mY&Xl+%%?>kO+BJ_^a0bp+)14BLXJ(Hi@^ZX#M?hHaAC5H0QNwkRtcQ>;E zR~(66vqlZAzSMH-4TNS!n;4#EuqT)Y8aOb>W#@>?X4}f+>fPqE-@Mg`i;v3C>nRq< z|I(k0Z6AH**9ne~8&xEU{d2mV0-ut}#WQ}|cle=8Kzn(_ZvupXiZz+^awdglsBVup zdCJF{ryOux2vj|))m=Y<(Dd#))mBCe==`T3OHdyExdu&0LdZ2lT|sh18_PN{0 z53|Z5(yAWJx#(3{nA7nTH>)4M-AGw@@MZAm_uDpBpj^q{v$yg3DAYTP zU5${xg4VE*wZ>?Gxz=;bC0MhjBYxD40SfOJ9DoE<8pVK0k#DI>vcsJYpFiYx(^U_g zPUkw<>59Om!qqc_9^_XsM$lqY*~X&7QakxYH5Np%>H7rHuv7i zeLm&vs~!8p_Wic}krLZge(Tas-_tAbtxnw-^|M70HMA+ItWtd5{SjBvOUQ2j>{I7M zf-Wu`@3nDD)9SbT2;7l)A4jR(QSlC-smvWUv&#hS;o literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml new file mode 100644 index 000000000..9e52f92b1 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -0,0 +1,253 @@ +(* 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 GrafiteTypes + +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 -> GrafiteTypes.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:(GrafiteTypes.get_proof_metasenv status) term) + in + let status = GrafiteTypes.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 = GrafiteTypes.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 disambiguate_obj status obj = + let uri = + match obj with + | CicNotationPt.Inductive (_,(name,_,_,_)::_) + | CicNotationPt.Record (_,name,_,_) -> + Some (UriManager.uri_of_string (GrafiteTypes.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 _ -> + raise (GrafiteTypes.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) diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli new file mode 100644 index 000000000..21836853f --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli @@ -0,0 +1,36 @@ +(* 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 disambiguate_tactic: + GrafiteTypes.status -> + ProofEngineTypes.goal -> + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic -> + GrafiteTypes.status ref * + (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic + +val disambiguate_command: + GrafiteTypes.status -> + (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.o b/helm/ocaml/grafite_parser/grafiteDisambiguate.o new file mode 100644 index 0000000000000000000000000000000000000000..14ccd78c4c24546bc7cdd438d28ab23c25c04a80 GIT binary patch literal 17472 zcmcJWeSB2ana9s0H+F#eIHN`xCF&?qsisIEyoj_U0X0zChJ|jUr4AvPkhFPYGQq^M zA29KSyF-L_cm1&a(2B+F(spZU%d)9jj6fT(TG7&~TiddIB|=-QFTBOFzu!5}y}5Uo zjQrF2d@kSfoR{Z3&vRbxz2}Ctw=KFo5C|ye7f|_XL{jR=L{n0xF-eV47dTZl`?sU^ z-oDkU@97(uVejo{^P%ChXV3Pfu2;RsEPH;j(wRq?X+QfI>-8Q9Z6j|j;J?Z7edX3* z`LGHqm0nh??5JI3_3pFw>Ly2D7|~CCdu&$OpRNj}Ya$-ad*4U19o4#Pyqcjeylctu z123m;%hEdBvl8Bn*fvOG)nK``2HENBC~VXY?A_G2^LmPOHmjmSDyp^yD~CToC-d#R z!Ac8xD!nR{zSFp2zbPRK@2VK?JvlCXe;+D{x;dVBg?pYtfl>Fa1&i`_QobuVI8VoL zFrS+3C01W$p@h|r!ffXDEsPCT=vsDQu)<_jmatX`##{+)2*1>|tAai+?RUkPsK=P( zO?@>MIu6jUfSsSNutITFeKNI`B6qwHhf-9GOqOCj+T*X$;w! zKxckhWgX(;ECW;xSAC|NnKaOQtO&CwYA-Dgr7yw1h3sH#T94b&u>G!m(EhO*1P&xT zVo5~24tl%}_k4xHtg`Gy#X$xXflJRXE`+W2<&FkRH%ylYO~zhbVb*TgW>!S+v0xg_ z)3m0!IAS*!E3go>bc^17LBuYS9(VR7PONmf1+h>UF{bGWI#~_1Mb&NtT`}0ZugI*P zp}Aaj?>g~37K0|nAOgb`B4DM1NJSlA3&q!n&)3)JD?D3P9KuLzUop!0ee;6Q7UV#~ zeS6Be?ncwI^a}NQnu15hOL`m4@V3z7EtJ#aXf}^yuE$v{PC9dfa~gi8?+ohIZ`n0g z`p%GDgZRW`cNx&yhb$eY-eZO6Gy+F0tWo&Zzun9MmHu?lv)9Zo4oSC#zCi6^p!8mL zB7$`ZN$(f$LHS@gr<2*=YC>?!N`Kl6Gy37&334ueBs~@lRXU1{h_=k#F}>3-`AM_r zblk@s9qa5rPX*98TR^UoMS_61`ygyEp(vD4{783rbfbyL1Q>l{FBPVO_N&<9uq@L{ ztlrasRFznHh2KJNERr{PEyPTb?O;&7^Q|Q%7>B*o2fe1xAN1`)N4Q@^vA_SyPQkK8 z#m;2(dLHh1=|X2RMr1PDmvF~CTl~O5SZfr?d`~a7^r$&oYqkv}+|x;odUMuyATDEN z=h=5zLk}TdqVO5ocYgXNxcc;_=+QSbL!S(l-@%v1I_BhYR|(j8Lubb!3-OZr-u*Y+ zv)QemUuf!c53aP*6+yc)n63!fm7#P+#IB4C{SWo%NcS0krt8_Z7z1qo)CrQAj@-&d zCZQ8J|GrS@_H1#bjW~*=Lf=DoWb`NYdvE^Xo_!384u65UhvXUihsLn=PJLsQ@yy!( zUbp=P{`LoGp0EA+jo;O-LVdFyack%vYV^b}t35xb+1j6=-=15}u}9kb$A5#{evCW* zW1te_pI&TsA!n$Zrz!uiRJaPpI>QpRufXjClfqsY9QqEmX)m(&f6^V*aZdkhrGKgK zpMSeq-)wrAf9|HoCnMSP>~?H4k@Nyf?@yy|8sVNsx9<>Urk+tS-Ck&=Yl8M&!E`w% z^U!g`)$B*-wZ6x=O2=|QJmdMFkiFxX?he{(urn{VaBJk!5%q+L~Snrq1NO7dCjMX+%6&+^XXI6cJBV*U*8{bn_uLtudCT^WPkV9x7_*{JN5s9 z#ijRy1tIL*?jx%u_hmiEoI>&lk!wfy-n7F#57Q7Gy-S?+XKsaNW>P11kd(Ue}(XZZ!4ZPo%xy|ESwO>iW-?djCG3=aCm!Tf1<1 z#{4>wkCJoemp`8OyUnl27SHcNhZ9e+-@k**X8ZHl&z}r%L&2l5ukw0`~yC-SE{oJx@Qrm}dxkVJJOM?|`TCl)|H~_m?&P4X)B6c%q-5o#)e5-6IEcRyguhDINwd3Ef zF%)J$@T?E6dh<4sxgTVIn!CW&8}nFY7CvuDL*48p<9W*eJmPLNp^?qUiLrm9*+^YF z1lKqljr)uudksc@=mK%f|NQ4)Z?j!h*E;cd5i^tVcnrj0lfOPsxJ=g*o%)aFs{bPv zYEz4){?Vj_A*=okZvE?=`jt}ue4am(Ri?A+{cB&k@@`cb=VlR{n^og9eT&f>vU6B zyQ$y5?UZhDQ;Xfy2i(-|x14%)Zt8M3b>Oc~>1}RmoSWM7rc>JJrb0-`_HNEoN6sUH z;awjc?mZPqEnE9p930?4EOl{uLVCi{c$WKtcansAYPqi61J*&zPJJj*jAh_EBg6gN zJYV7-fAkLXd@V;5PeoB#kGB5Db~X_I!um5RNk^FYn2k{694tBKCH@xQWea_+XPw8ul&B+=MGW4<09(~W57y3HXs#GP9x3rqf9iWum z>a#nAvpfBkjW?sf(3jE77yt0Ca-78Gt+_+g_yc>G)z1y=F=S^3*1v!G)ok>sNneR| zZ_Z%%XDZsXq#s#kAbR&%_K)DNT4KM|yEn8%4@~dApnV*fmYfZ`1Lf^8dBup)=2#4e zTR4&F-RB$xJ!cm7$K8$MJ$F<1FE@3QoBE5pDXc-tJ0EfGXFnU>HE+0g;0)pze&`H+ zgV8wa3g7={2;q&J@o&~q3Uid&EgS|}gSVR_#tU%(^?g`%wts+%-ZHask2EjZhD`aU z5bn|2wtm+rFt;;>qt0u=*;T^Y8Qo`J55l>z<$cM&lCCXgD_LE{~e$s-q8@(HPmbe}c#x zEBhI|ZJaRu>zRV1s=tdVp6m2CGKB{#)nCI@l&LDFaH;-TOcgOTi76~uv;OxY5ySO9 zzZ2{XKRoT~-)J)4UUHUaw#VUxuRh*qeKMxlS!SFFntVL0`O`Q}F{PSXRwSG1 zYEy~&SbMUqt)U~<+LnsdHaEB3lc-lJj~_jTQFjmxO4$Y>TA8eEXi6pKH+9sutY})< ziPn=_npI#J{Y`FaMKgRPL%TAx`4+A_-lrYwE=Ro&quwRwQFjCCogVH?ib9_S9b0uefV5JdN4iMo2h}fizEXb_zNwjy7DoTWmr+MR z(Uk{vno}mC8g-hzSU56fj#6iITg%NUfNfD|3Zhic(Mydzl>h2UAMvEax{Xp>5Et4Q zftTBKIv?pmt!J)VR;a$=rVG?gPkOf}z2B35S*IBVYAa9^F%CsqD`gC$mf3Hidfity zU+uyedh2e{vZ?zAPanrK+Ql;3g*@#}>$=7_M)Mg2()eAdEEr_c1&T*mMSAp%-5=ET z7*%684-07XiF=w5AXL#zBd(sO%ZD{Kn%zLNJQcu0R zJ?TcBHuHp*(c&kuevB`cw)SgU=8QA8Z_u)dYto}@jVJw}PLJ6CYphSlmQA{h^V0OV zMwgj+h$8hRU0%RX9l8dsyIj{{8wxDWjdUJ!Q{Jf5uCWFxI@zW9$ml;f%IC!**iyhNs@!p7h^5Z8%oX zARtbgAl9i#7pRLp=^~xx=qWwIN3bz*E*e>>Ls~ZDdA+CI6i<4#PLIUkEcR-r-}xD3 z-}aP!T$dFfnq19e^qyFSatnJF<5i&3O1%Jqdl7e1{(HzHvtFH+xsQg_ZBpj!YroJk zYdNz4_a|&2QOG7QqV^zJjQxu8YMsu9{gkk0XULzDx>3|vgmeikDpE1DS89ST<1BRg zDnvg;>VPMogFzjG0yRgcm0B8L9{$1acAW=>u$=!^OP$?F zn|AqlfE=k`@8%ciXA?({n%vRdlB!(+rjmw@PAZvbo}5Z_rPO4m>T6TAYVwMX4rn^R z-_@u_YZ(Rp%5nW1_f_Y|InCb$TwHI?ufJ5O&DcX2Rkmk5IEo(>nf~$@y#n_(Peaz@ z?>bzbY*qacJcA(Y)W^1tzMGMzUPs@~i4Z(LM;~r6ZXFi0UYVz!84+VEhQa++!;no- z!ai_|*ZtCG+UE3$q&f`8UZrvJbM!fKHv0dviu$}7DHrJ2O>!HXH8jg3&qTV)BmV=^ zH6FPI=|+#d9_cQRybWpQnP0x*+}rGku;4YMw|nGwklyK$FM^{39=Qbaeve!Q`Itwp zhs>h`^UGK3kmk9ABX2>Pf2-rjJb&OHS2^+_r1>Xij(prr^FEcY3O$1tLG)%pcIE)f zxyGCy$8j0tSk&ZPjQS5lUXDGKKgv&M)ZY)eS{4J#PeDG+?Lg{J#Sk8p4q0CB8B+Gw z4ta;@u4t%V$u4A$S8QU2`= zc_2gPmxy*x`(uy?Jo04{3udvu$r&>5CC-oKpUIFP$dLK*#`&@S(;4!M8S>vUlSs;;)B`Hpj6XyftH(Tk>zUNmj=qO#G8rjK4UWAvh#qZiE@ zy{I&Y9i=&XyCsLpDLKk=#IZC-AWL&ZvNT7$N^?Y|G)GwYC=g$fSlQG%x-WHY^@-ed zblZ4cXENEH!?$|R$w?gN6D_r^_3>%bb41wJqHV=zbSa`k17xHU2rAn8Zt`=Zc`$tM=MdDv@lBmzJ6FH+JS2H=mu&wfA<%(Y_^KI@R=O z+UJa%PUeG_^u)J3PvZp6F_gS9EkFlBsw@ZBuh+GGTg4bk!x=Q%#6gdzPW@oEw%0OS!TAxYunqKWezUVg$-@Z_3`FJLn>Z6#Tf3% zPd2S=WPxwFiHWN^(Q`vL=Blx-I+0vm+kvA@#J6~QB3?Sp1nQH?rjOOO)~-w>hqTZ7%N4@7I|BrTjRFm#-5f`hAa_f_D}eLS9Nj@0G%dB=qvxp8fJY zfaT4?q?E5Gq3Ig|CW&^Zgl9?UEkzsJ%jbQvQn*OSztCX2ZsA%I?Y=<5 zkIf{muaM~Pap5;W>iZcvRjFSwAMXo)B%$vw!gomM8;|GnylG0szyMw_CsCfR)LrBZ zr8-Hxw5=m&;jej($ocnODSuKpKtj(MDbK@mv-VpUAyHl-@&e%}B!892-NLn!zlVhV z2SM8ZI}(Q~N0|>l-V&Z7p}#a}@^2B&C6T{MB4W!jF=$D-E*$FG~KGgj=Qjl$2jO&eSUcsi#NDPJr3{QG~_>yz?dNcnFh{|(`BDZhqxqy7hlHk&~8S`crd6iN>V7(i$ZiPQ4p)Y`M56mAU43o$&75Nt7T*>bO+0R1)_ah9G=;v0Dajca5g~DnnzfWXaxKZ+-75RYhMalm?iFxxDiJMw5 z0{!@4dL4;=NKM0QtPYW%aB{EJI3Zueng(bon!gAq4;TJ%T+rJARB{6RQP2P<2 zFcSB*J>(Rey$XK^=HbkINXq|Ac`nuyS+3M+=0k5D4zA{zm$ai6G+&9jj)u2zFUNIN$C3| zS*g_BB-+)JX!luRlANd1Jz(B^r8baw4%$M_f}Jd?6Rd6Chj zevX_3av#SKsQ|w9%o4ergx^&pJ`7fqSDJ4ZtiPNx_TfenayyBAvWtx2`B{P2m~R(> zYw?YSGUB|M#PjJ^@;dYFB5=L=W)Zl-e2ZXQ_|1Xj`v}Qz4CFx)7r!%*uL@rm9v1#i zctm(i$nOzs_qOn)a9GICfh@O#L19Q35%N0*>qUh{!kDmFI7wI{oFXg}@_mSU`2CSA z7tR+}3HhGH@@nByVU3XANm#yISTAf8riAN+8-)733hlOwyi>SOcu@Gd@QCoZ@T4%9 zZ~8A3#)M_U`NE~b<-%rRmvEhMgK&#*yKtv)K={1yRpAlgNugzlT|)jrIO8-$I7i6u z+RR@jY!r40`Cl|x&Toz6R^blefbfv;u<*E0zptTPknc-ip|DsuML0)TC0r(K7OoMl z7yheot8j;q-(lF#^TOAK{6@=s#rG-NAuJY_3Hdh(EUytZ3)cwworUF_g^vsSh5Lku zgolO4geQeTzE{x>VN6&eoFiN$tP$1=`F(}$*9kWWw+OcjpBC;H@_mo(4hxS9`JeWf zAL9EN7!&eu?}rBspt8j)%cyn=E)gd~vEkc5*HODy+6 zi6879Qqi}!m-=7@@wT+JRx8&=u^K*X)Tl5gymgZP(LrY_AeXO`-;)!K%Z>x{%0^N+o z88WujCs;sBn_FzGwx+3RVNLBVvEt$k3bFE`ZEbe0vSU|sNlSB!G|$RWH10S#(n=`G zp!h}Y&9Tzr;$sWc3`H3fRFN+mV%pl1qB}2bxhLYoIErW#mW;E*9TGzItzPaw$9NGe9D!`t(s+SR}w>+2)Na~CsXKu);3U}@ZZr@9>`=0H3icDS4^Y8Y3gV)%X^OFsE zh;~9!P{=N5m?=mF!BCWphm+Sul2?b4HwATljr88G%@op`D)w z5~n540kjWE&SPu-lkH2+4KgJpQEQU(B202Vmi(RjBS_D^b2F6a%q$E!(+Y#h*}-Hs z0^!b2kn&xYGN(}Otzlqmau|zE1}44LK2_Qfw%U-p@;ONAnj7q$+OI-jtOz;Ty;FmT zR7uFzjnIliVf*e}fCBH;s@}fl$T(7tjx%+B-Pw+ekz`c_kf-w-W@x-~M`U}d zKK6c(*{xdU-sLc6W})(}?McV4tv4tlDec?_vC_`4QX9}`%E?9*RkA$jObt3$htM-A zZDW6Y*6sCaRJ>4z5!COE*M=!`rO+6a=hGN{B(3^jCL+2sne2npmhNaJlGo=K~ z2&c%I8+58dPIXwu|4;4l@0a_Wf!w`%@}^68x$9PUd?&x0pKQxZ&c;OWCax{toxfK{ zFs*eHyzcrh%;E4+b9jvmtK_gcG{3uw>VtvkJQPTTyYn$~kf%oZo# zNA)jg`}5z;Uwvd;Au6a_-nk>xjhdlq7-%xTkv=k0x^oDVG1z%HkjP06+IP~Lr?p`l zOqt0++U%sxujDX_OAdAI3ysT=VD23Ihc6-Z1gs$pHZ)Lw?YL78zvr{ksv?(2iS(+zi39pzxY zI~P0if?W-*X`JmI=i1wm(-l3+xjNXjX*FYfBkqK@zTi zyI~@OdSH1y7)BetUNehW#N@fXW=2b^H(Jg^C~ZAT`wHFU+d5(QX0)%5p(Z~1c=nk3 znCs5dd|M&4q7cqeAB8we!wy!f$5BBL4K_D^1UwaBIUcbV&3710j6J&j-PEd1l?Ksl ztFNItx~5%oL$o%G%x*xWGYmmk=ZF_OS;s~ZyJbKAIK!|eQd{=uAZLD8RX)udvL$tr zbGD=Jt^;?8l38hhg_>{MlH>5Y?*_obBC(Ah?!swsvDEO5^o{T|eP)NW#PhxqaO`)mXNx z!(CJJSR$I?osdF;vdbe1`HFn#mBwn-z&t(-8g)u7hDCgtg=4(x)2I zqhS}1*y-tXdVbn`&957*^bOXPo$Hro^BpTJbv>L`7mv2`^3zEy9AAk8tdc7=CwAuu){Mw9&d@O{z8Ab6?$vGrM(TCt=NcG9AmFw zz}$o%b<~gE^?TZ1(u9>fcn^W^>J#KG#0~e`ka;}0{TOvIrLy`lo=n+eYT6Sm_68Z+ zWy)U$nIAyr*~hCZ(l5sEEDVGova$|CbQl4_KcGD*TAd^K%OOhTDXtR2>LVTI-a-)T zt}w>SAl0wqlzI#Kqna;Iy|2UUXu}tQ1kJ1C!8=GHKV@dCf7M|q57#Oy{(38ZIKq^j zr}EXeAhrN?r}Q28lZRHgwLw+XPj%ct9fzQdw{#p#1sd$O`z17z?Q{gE2wn&@b<0t| zhFJ)qEMAWw9E7ZsQ689nj*YC0%%p1KRP>64JUSmzDuwuF$oM@wNnsd3a3Kes*S z>ab~#8q?OX1lz;FMBHG58;aLAjY-rmOQTdG0f7s6#3r!92>V~X!Oq9zFUI5ybHyRm7LeG?Ev}@#z z1x>lGyg9OehA4fx@@QXO9wv~lOmmn&qDkFW6yse7PFJc39mz7db3}P;GwWu{i(WzNP}Qi^veb7iXu2sF7Qa$JY-a*JMq@M?=*h44Cy z-iYv{7R{w1@73nYR=W{+(Ip}OBZPNZ^r>j*9*h1Q==~Ob73f12T@PA63hB6PbqDBt z{LGcD9z>Woc$enwmrE3v-i0t1GA?}pVXk&uI*iWaI?kmzX1LCE>1m+(9PQEz5H7dq z9175Ol;!-v|1D@UVU( zkhasJ=Yd{h(Mixn7QIDev3{)2OQ2h&jgc4Z zY4m-d-TOrZ@}C5~M&=CX$In53&7$=SLZ1a=ESBLNZHBkv8Qu+Nc&D4;^}l(u=3B!I zFRC-VGcV5I8GN`7` zb|m^A_dqgj%TT?)qc@T%JHtrSZ|lXe>HincBzMGQm@vjACxbQD44;{wQmm%6wJFmG z*2Rg#L#zXv5{qN4iMYNG3E9-Rq%mP4=pq(dTzl-h)KLyjQ(NlewbK@w?7A))bn`bk zK3Ur%#y_aKK7MOW8~o|oVzI)qBDm2QyAi8jR$Jeyy<}Qj^yoCTs$bR|t7wDoTq3rp zrm?9#Zp8TB<4o_FCK%Obuz#9ajBZtZ(~?*mewKJLHSSWeB`t7Nl(1Nu4EGo_EKJEW zAte@DQqvlnn873t_@BU=4DN{6=;qq$ip40kq^QVD1T@W3kqF%c91n`q+dF z_rnzT6<=MYxUcwfSnexWU!9L%V4^%D1Nm$ln50w%5q-W*Zy~q<&5n94dH$U@4GtFB7aFLhj9yzEt8n1XoD< zdP)BkalBH$lk`6den5nr96S#N@Zdfi$a<8JzEY_PMAUV<;4C8QF;6f?ME<2j=&yr_ zcC8S+3rKnQkw(662tGtaz9)#t_cRgto)>%p$b3JO^tVV?VINZHLqcDKXEWxn6s#el zzKe(`uURlbM0s};!G9kS<^7A`gFu$|I%(wFE%*)*`92~}#rPsZeiojwm_H<7RoG9#vqs=D?BfteDm99T@pP5YHxQ>NwUCJU)h4)ti1P0e zykBsw;KRTy@5986!mj!nT=HPjqdN~)EHC?G0q|wemh~VGFbnu^#JvOFaEI5{k^yx(Cc_tC^t|OwIa|LUN zsAmHa`CA2VB_jVS;xv>?1m9DFTLgOrcLCYXKM_%%LxRQF2cg_af>Vf)dp!~LnomT% z77|gf2EnC7l-EH-{yPNkAtL`bh*w~*l?cA41)mdqS@2CD>-8Ry^%6W2&%0S)Q0hV; z%O6FAoXdo+5PFu-HwZmn=!HTr7J7-$|0H;q;6DpKDEKfDHQ4tO`j14&eP8H)reBNs!2Ut}>Ff`*cLeFEQpLm>GCt7m8Kl8?EfMq_ zq2~#Gv(U9d>+u5qB|>BRX?yr1;^&p>fgPmY$K;s!QjSyD%RcZE_p={>Gr=E-qCDdH zX5TX~9PgP(k1+e5fkLGcq%Sc0o}}+2eWBU+3`B8%BYlzC_vE~Pg!IK`-!pKD+3yUD zLcJJ2+U$1*K4nR&a;lPQl*_?ibYeIq*lISLVwXEEME^8sjGmRte4# zTp*YbTqU?haGl^If{zMr7G!@?{wsoS3+@;EP>>s=?4v_Eb)7fIU({QdBL8WGBPp23Zc{vp%g zZNfbZ~$pW>q*jH)2WtTfA5xFZZe0{dc{Q znC?@r+?9(_aUWNS<%mvk9dZ2)*;rpec@$I)N2vajaT|nxZWcV15T}w$!*J@=&2Zim z73Drv(cgJ!Nba3oU=VSWH&Sn|i_{i`jku373VO3PlfF?qJ3xGIHYGc=gI$&SwLhYq zeDQzlnh|yVwE}Q}B4bzOXmLkKYX1n27k;5Bt#m$?%B1*#j52Pt+)7Ob;6qzM|Jkmo zVan7c>n^pOho08$>>G|3>n8M)=eBw)LYDs{9X5v;C+PO^9-+`3J-%P( zz=CHoNaI6IohFCsf~q05pjro+K{JNnLuCAU`=&t4mj4%h$f$z|eX5~>V3JOm`EFbD zq^+sW(!1GKv}}H1SUhLg%h_F1>2Mx$Jxhv?Zf<^Zq8{3IOW~;|tz>KS(^{KnwHCtJ z;(XnrL^P$GA9vW83c_Hn?23MOP+|uE2)43xm{?0vGdS6hhsdIlG3XPzl z#)m%Cy~&ILxF#9zT+I!huoP>%Dd(=-MnxTc+<@*YuInO=*Iasj1#vRKl}0bJ5Xa)> z$-#W@kfghxaSihvqV3@qzg~RTG5eh%a0(Ou-7NuR_EX5YV#S~k&zlc*FsjHCRs2L( zXWzX>BlIdixSawM@P*&5{he{P0H+EPRZ`1yO#NM(ZtEg`kzGTK6fpZ9+^9*us` zZqATv%KWkGPnZw;{wwV+JhRXpjCRX&SH6CVI~ZLzF6VSw%p-+&?L=*jAn~70&I+cO zRzCxhyRw}UwQ;7wg68vJ5we^cgMIfvUn1~%C_yrG^vZ4@ne6Vl{KSEV-a4J-sr zb+XXCu&G&nN3bTOSrmTT{^qV+>+xsj8Gg>r${-JKRECo9Ypo0?;geVy>H87oJjIrn z^DW77dbG_#2RlD=??1F4#*_^VLRWFAb|KFzImnqd&`<;w%I>=|tvso}ee=&d&G2(Oy&kzCp~r8B1A!@hA7qf18*8q}2Q`v3e=_PptpW^91Uf^+2=w_%6@ZpKpDB z!D{RFgi`A>>8Sch{?z_o?d2cj^*^2w*#F5{#tOMz<<7j+ZmIAD40gLE-#Lc|TPlOj zj8NYbl%_|4Z~1&cHT56jmcK&E7yi`o_Z<0+(Zl%bWq0w66&`QsZBNQ+g`tTguL^4W zbZn!MyOIx2rtC0ArXEqKx-%n~#4)WKL&&K z{3j7;O^jv2_!PN>bdedV5vJh#46q`tzRYOYT5_|KrZ^6bC4fAwV} zue-j12^nawzwvvFMd=oBBTJ8Wu^{EV9rkVJ#BH0cQf6?cYkm2f6>Yr*s zE@l1`u;<@o?;9skgJh@S;R%YV! zmekk5QqtB_sp}DU2;c$7Q-Q1FR6}zwWoZ?h?;09!jbe&q&-a}q4NG1BrP{|!JyCq6 zr2G3dj7;id0}z`{sr=lyG)0ea`5(%}{}U$asul|WzPPBtSN>{`{{ol4Qut3~{TZ(^ zgzUMfUMS*)UiidK{jwJt>xJIL2@8|=K`(Tz7utQu zO?}7<{eu_kJLsk^_d-Aa*o|xOLc2b4P%B)|XgF?7PyeuVss3OFo!&pXfi{iNVx~ z^(Qb%K^XWLjobo5k=#Uc_e)Z9{E#{H#*#i3%IN~T!6%jM4XkF$-dQARj13pyIPVxt zE+05LX1@QhP2Y2-hQ9-`DpASpEiES90u-}Yy?3Xucc-7S@njU}dl1=D^q>1wId)>R zmR~7iQWd+0>_;nhKcdqWn`*yO#oU`BCdv1+X215ubU|xocO%MlMCXp6^AogJ&2~QM z+#a5-JEn6-$T@&Wd{H8`qwEsn?g@SrWVXeyxus8cx*I_+>&$)Ec!uIHo>6$z3ytzZ zfA);Ra)j*hhu?m%Y>)#AZ;C zC$KrBPQeD$)2P*v?j8#Iz%+83WG~o=NN(zE{ElD$9snmixp_t_hskLyQyV;Y;0P4PgJDnp*{<9Fq8@{xA|`0(mi;W$mkGRV6cya&N| z)p2-vws2ZKzD3oFkGMs@)Dpj?E!xuD)PX-yRFfZsy0t!<=xD8PQ|s}FbpSv5-?!q| zgI^Ka(~95Y_$es49KTlldhk1d-|g5n*~uR|WGCtsMYtM2#w+Y_7U9>5Uk`pN7c_pi zzlUicZ7*4RpJgMhQy&;w-!ihCH5iTd%_bgq8X-!UZ}$r2a$4EAO1&Y=xh*!Y^9kH*}a?I1G;YW7-nbdj6KCIpR#+S8LknHEzjT zZiVmG;eq+(h5u^h;ploE3UTv2YA*~E$D*O(N26)e zpBGyBimdRZIy|6*Be2zOxzp0peqg0tqtkMrP0r>)+9p;Z-8~zeqr*zQ3gyuj(US7- zE{mpKYc)+f8dlRK%~&y|eyM44xuXI1Czz0Y&?YXTwjo#udqw(I9X4k*$#F{>eS`4k zqlGgO9*r6ms3`Kor%|VI6uM>cq;!Ge8RtShI?XI$9NT**8WTmiFq?}0sBXAX!pu#- z)sZNJd7|JOte-Fb;okU7_P35H;uDYTw5o<*>H(;o@|f3^Hx^;ab>(dy z0m8amdAP-RJWM8EnZ;)`Z0d?`@UCi9gnm^l1GjixF5Aqyxn&}#_Ml;Jv2t>`@?6>v zvt=B(X~#P6Jkn)Ai3JExwCD*4S6TFR2+y_XB?vcI^eTjxS@cGP8E39+#j&^6B~jjP zgg06AM+k4WXr6cOvFOpDU$p2d(EBaA4m7t8%$2QfN0|E#F1-$6`s%ne_aEq7<2?oVZDUj)P)*xa2R?v@29MkDT=w3``8aIP^F`d5i?!|Qa5H7IN z`2vXXyvWb<%TZ%Ct`Pov*V zqYtOi7g;ug^_!SRPfw#~fxcbrFZ++rZmvD%c)uTXlZ+3JcbVUiQcl$V_r8^F%E~b6Qp)<@`);;|=4?#)a{kc!wOBoyo7Q#}>83@&7<%`fn$W9v@ zIHserMw(|Ep5?*uJ4LJ{j>6iJ>7$jphd4s1uQDF#Ul&|Q1m81E2j43azf17{O8NmJ z9=;9|QSM)eMR+DcMTln*A$OSI2qNTiZO?M~9KiG@!MLQaB0}ElL_9<>@m>!0&>lyq^CZ@x1T{BINy9@FODRorU#zRw>rlzyKaFN0J_=6u)D{GhFRNJha_ToQT(g#7QWZ zh;m*AQvT0~kpD};|0F_wF4o(Wdlry#c{Yf0`Q0MQjT0gFpNNoq7m#wg1pf~aa-L&4 z%6mcZ*NjISc*d3Ehu`R9K00j@2NRJmN-Q+%`T(AJD?szC;2g%I-Z9cRQ@V&W^3g4f zsL#M6|JQ~7rr;w)#PhpHtj|utHw8aoI^+hhZl+v)<`wcHpegrEBJxjTI`S`&_y)md zNxzqf_I(e?@%KYXe@3u}2sxihdKT8ry4`~Ob{o?xguY7fT8UpObcf&yiQh&<{dWRc z|KAdEW^f>od5B-vXNL*(UKkTg&vFM5G6> zQ9*i;U@j5y6+&Mnc&)^L8Ay36CH^ad{KgjZZ58?@!Pg}IJ)sW^9+CJn1|uJySM*uR zF*pMcItxbW^NdHm^qE`W)ubUm31s>AlScdlg6oM$KMZ908AA*f0LfPk|Y)4`B@1wbuF@Dk!E$dU9F5>Nks@^wl2FD3og692B?0ZG?qjlr+a z8UyuNW5}H~*vQdmMiCz)jd-3R=J?R<$GCZzG{z0j5@(&O)Q`z`3FfWfzY~!!fOij! zA0(JdM0~N(lLV(o{4yZRSt0TF2zE*OR-s=Kd`;p5crT*M5zHl`oXddJW2MB;5UiH; zJA`%w@0IwiLcb*Vn#BK(h;j1)5jV9^1oH91^a3Kv84YAT$^~{TJYjl3nxLNQy!50PJ5PVzk_ksrmKM@RK zFOhmWMKE7*xZr5P@q*=oGX(DgvfsWT_z)5O_HV?o*bgJ(zP626g#Agu-vaq8Sr1MAUyM5%oV`u$TyWlLV&_A@6!(CB8jEM7}yA@_kV-PMnHw z>;bc;!FPg)bFB53g1-^`qu@b7>V|wn1g`>8-Ymfzh>&+1 z5%s$R$oaKO($@%nod~|)GkvI1f0X!-1V5GZV%R{f2f-;s$e49RqPE5kJ0XAigE|w%{JY-wN&(+%L%Y5zP0Y z;32_&LB0}YdQdPV7#55O>Te@}FJI^a!Kh%N;7GyIf<=O5f_xrgd3^s!EEk+6SS85k zB&Jsj&Jmm|$oC{nUm#c~*dUk?yj^g$pnk4GzD+`J7Th7YQ}AuUy@Ce>4+--BMPd1Q zf>FUT!D)hX1Q!T42`&@7U2wIa`z?n}LT?uA5qw4PEy2BlhXjK`sh1!f!dcHE!O4Pr zug&=Rf(?Sp1bIY*>3r8nTrc>zV2|J~!99Wp1oiV8@`d=k1k4jG6f6>)ELbHtU$9AV zx!@|nuL-Ufd|Z(4VOY*9f^Q4*9WCP(pQl(4!9u|@LHZ;xeXd}W;BrB}XJPtU!AAtU z1$PMU65J!WU+|D%h|g85hhS82wBTgHnS%WOEcxpM`F@4;?SiWX*9r3bvrKAbsyhPZpdhIA5?qaGBs5LH&&-}``;Qs@kER!w( literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/grafite_parser.cma b/helm/ocaml/grafite_parser/grafite_parser.cma new file mode 100644 index 0000000000000000000000000000000000000000..9bdad074f59520c73f3bdabb97096d1e2e8850c8 GIT binary patch literal 57777 zcmeFa34ByV_CMOyU6t;>olnx)*&z@%K}AJWT<9$9peUe#Xbcb_8WIda#TEBmpGE{>i`x(J!El5no`wA^1UnMxTfiAO{+;0eL^OUE!;zl^-1cz%8|VK-GQsb@ z_+@!@a4aVcR{+Pd$n$F`s|3Faj(G#%NSnM7z8H@5?JxPPg{y+ggCk5YIKnfJbtZk% zAuOj?h_oZ|;}+F$j+MR_4PHCa$GVU8LI^ zZf+1J|CG0tCG&>E@sE7WhocNAd(y3hV;kB&wg6$ul;v8PBbaNSH3*X?b%}oy;aIQb za4a_i$G;*ti_d<=Hrp1Cbs!)7+ZXQF@pt@vHY-a@{jy5k8`8vc3|7_k8MTy(y{EJaO~^UW6E|@c}!z_Sy%+S z)scasDx_Cr*YL_+uXV*c2Y=ZVr!m{|zr( z*9_qKXYn?bM|+TjWB(Zi7lk_!HpiyhUz=BtJn~0A*nXqo*j6#PZ~ybtPZ*5lk8M~B zN80Rjq@M^J`Cy!Vl(xXi-0BOGB6jRsfba-7%9*;hDOmQMk#JkUkrz7ZHOpg|e2`~L zlX^scZGU4P>ym-vpY4-OBkoW*%EgwE7sPED%-d8MOkV=Wy3$#Cv`H+Je@vSS$2yW% z{`E|w?XY@id9(1g4puI`0b2=2-pD80jeq|{yIGu`^ehcq#yB4(S7y&R+n#jE@0)=> z*!W)&XFFM1J;N66u>j7-f8T@7wLRjOB2Haon_8R`0vPf`{iufHAKRJjOBq|aFiyFI z^_l#?3!Sy~TONX^90$XZhOIB#a~R-l-K;)Q$H^1_QpgX--~G|`7xG9wAS`X#Rme-> zmu0XYgzLxrR#w*}B-=M7cM?P8ZPK@C1gmu?GfEGfL`4>eZ zTm2&v+4A?D0IrHCZ{c<`8`_)N8|s=?HLO_Fv}|=lduvJKC-q4oOv25+IRqbs} zEz2_6Wb1}5ZEkI7&**q|V%4J7)@Fitc6JV3+R(hJ5uvK~w$+W9Of@J>s#@LBB=i6< zc*ICQb@GtL!&(GOfTj#>XlrX&liApr%|y-DZ$+jtxiec`U7g8Jt!i#s1qwEAdZwDB z_T3K!4IV$fQztvK8#;7Rr!L5J_~CVe!rw?mg+1}I&wk`0U!b#Qctu0dN*{v%Y!A+>_J%%+m9KNPL#Qa`C#mL!=ku7Mu zLmDY>y*N8_C<5DUo6(Kg-5DG=Hlvqi_Z>gCWl7`Grk2Jf^=*xdSGTPKM*WJ`C99ho zYdf>&NZnW1iq}Z=P#ev3YU4{}UM9O>tLjy&8r$0Imo_vtuWs|Pb-GjMcWTdvnxDz; zGp4TTkfv3rXZ@lz^@lgMwbo{`dyksfvZTIsY5meBl$y!T9XWf=s`|#Zw$`@VPTf0` zoxc?m7B#mnJ_vj^5ogZG-CI#s>*|&zh|L~8$(E`IWwLvXnc8wlLvz!T`i8b;t5-C( zw1du&Om^N@v)daMA5`CZNMjpx>`-9tx#b?K+gbLC#ucq?YmhQ)OLTQ(hkEh|^IqbUyGF4U_~ z_lc|;GzfZivlXU_-XjTTz}MP}z6G)MAU||Y>p_hz)g!_6Vzg>&OXQ~zkH9icL$K8ijAPXwVl_ zY~M`w$gzu;x3;cotY6*Mw5on_Lv!;Yh*^4hN49Hl(-Ksv)M3Yiz3?0t%t3=_NTVy&Nc$eg#UiLs=PAP`BH_>P$A$I4k18N1Z_?`7yl20OSuvzCZ-__m>)$h#v(6 z{!Rib==IknB$?5pta*U(`@!_VJ6NVSRrL*ew9oHEa-#>ZsVak3-;PDD zR9Nvm zpQgna%s{tmt5uE7jmXDHfZ?Xms$HU*nL{SD9whZL>S#M0s>D>s$+XBJDlv(mJ5OkA zX;{?USifj>dpn3>IIeHO?;#Cst4Kn7ERL#X)C-QlLK2uu&l$hOo{Y~V)uEUQH9MyE zW7?1vtCr>1T*MSwwsrazVl87_KZEEEj5h1*te9FDUv6Vfj4igYC5-KFWA%*fZex2e zHrd9eFjiw@wTy961mUkuR)&S`w`p5ry9^WEM6O>1d*=f~C63ZZTUy6R!jV3)kw#3q-(Z1AAW5TYogmLtk>gb26cNw_$^#;w?TcJM_jaIH3Fu|wUnKr{E)#r# z4u-m*E1Y8k=Ss$@HhP*wPsXUKB3En~8dou*QukEk@@QgfeKweG=9u#KalyTz0818OB;#;AY|6|vs}63iW=d$d^5$l{ zhA(c#uyR+W@X>qkp3PaAxc8yqpMq1U_a!3d?mllSdo$cCsLKEh>O%2WUtCzJk ztmIg@4Ok{G!%@WCmZn3hx588y6B`V}0urX+Ms;sbu!yM<3WflPzfDMnjdRwl#C&EH zm}+WkZQ;x*OlB6CwuOL$=>Z3upfGmD>gM*QmFSk6A+?8-?CvrhAS+vQ5I?Kbv>^A_wBvMJew`~H)ASAcw=QmHb)K~rUbV%_*uVrE*v$rZwSir1 zU}qZ`@0*6sG2OaV>!JfU)2sBYPgFFw>``7b z*v0^cYP}W^{Dn!YcaW>^ffy9d^>wp{au0z3!@AuhO01#DRAznQ|46A9Z@#*lSL!9U zp%*#68v;U`SL((vM9<1B4Kja?PA{{?AK;3w2fk6GT!I}xJv&%>`&qPwHn6V^EUn0i<)t%0{o2=%qILTZ!6vmxp;5 z6lRUhJzS!8q3W%cXd7oa4{sMzTTIM+y~Uo``p)doC9N3QGTG~0qiud9+_e7YKN)Id zbh}vH|6Eh^-9|(HM$yMjYGZ6~_V4KSP9vUo!I%CQRe7~XRSx=JROJoF(mQDJ*tBeo zuL${%(?r|I6H=9Z9qf}gx-eW+<-FC z({kXR-IwsR1-HH5%d;tQ8%Wqd(gr&9PMvz3jivnkT@`tJ#LBi-ZWnSp3Wkj)d-#-z zhqX61EvnAtg~r!{JRm8rC6n#y>dItI>}711i2>zfvQ=(fQMnUQ-K*TWd1` z?BK})8{1=&z^K980j>eaz7qjLYOQt5(L-nY8PQLs`qX}!f`r<-iJ8pIb2_T+Ui&yimE5XI-mdPbG5S%=6)JV_F5OEPgQ_mdROT>~wAi{gvJekOVkRQVgtu zE@6lp+x`QAa(5=92kKrf`xB#oK=$`iU|uW(=7(e> z%PX60-L5Cq8|dBW*9{Y2?uR=P9~$Fz8Ix>Lc~vTJZ=b21$P~)Fm)?EV#%KyAt5o^W zl?`nTD};ndsII$&60aK52jqJD*&O{Xylu1CEU;%SKjJF10N0 z%Wau0=#2`o%)(-S=uy}m#%u{MhVStFyXl3cIT=t3j+LtNXF%Bfg{bcb#GPNAd{2 zlS3!jrvYH}U=i#T+i4OP8FMBCd&XfZex8cok6tldO48*BmSk$sNs8+55NC1@;}m1g z*KsnjS2l9Q&@EQAFV9Kwd`e|LJ?zDkVO>SQd~%CVbf zYLrEy*mPHS_b&KUC=IDIwX z^b9n~Af4~>#~Sk{^52NmsN@WlJO=rLVGDEtTt20p%GBhDRT=X>fZq#%SCfU2VDqF< z9Z+}hd8zmp2Xd_K&;xY3M)%3Mg7b~}8nnI&XzhjO+kwg$nBw>k#(anTZz+tThg8wC zB4eY5i;yvc?&54Q|Mpxrw!Jwo0gkRR(UpNzqwO-SJVg9MDb=e@)ZdU@XQEA#e1!N% zGV>Y}-Ag1M-AfXo3o3H0i4O1+2T0=OOuWuSd;5vKCGlD&UO&_=u|R%`7k_5$-Uj+FaKx9K~PZfY#)-ZWaC zy#$Mr5ZU<-cNgG3Df}KMGa8L@EGhT=DTPi2suLWZ-N8xKNX~ecck{574R{#q8$L+j zQd0Egdx*oF;%_k+eUwX^1};8@d(jrny(^=ScMyBnoLN$ydlZ(clZ09_aLb7Hwl(!+ zLMjX0-Oc9!YVaokyIKmjw62jsz(~%u3`hSd;p;5G^&*pwpDkZgZwZ`zj+VMnqNu>* z7V}C;5hdL)iqAg6tpLUj2pB^(qo3!hnI99hPlQYEV@JPpc@fF`)V0rNE@-FesV`jG zmzI}*2;zq*5e0L#dJZ`KKM}3PJzrxj@_Gero+k^4yb@O_x1*TP9YvE@Ab!$8xINGOi9zxCH7>iFoa8(G z%0EmJW{6+F8sAQiOx|{EOS?;ep*ttz*q)Bs{({!niD3fnU|Zf2Fr|-lU`uVrVu9aR z{88c$5uZ=!f@NE|B;<3tF+qYUn-iQ*Q2B+D?opau+pTIi1g8z~@Tz`sYh&ADJgEvg zls?%JJwq@~CdMD+)QMEis7Y+keA%JNzf%Tp4oM0#3Jw%YW^$~;4p%LrSV*W5SbfM~ zR<;KLjM}~~lVQe?$ug>aJr&8dbx25H@E6FprwOUyy9>ZI!IDI6UyXc>gHLlE1NiBf z;ndVlWN~??%Ye8?Ze01!#20s&_#!*5JesLCs!>-th!0JCDIgj#M^Hs)tD^G=v0M*# z5YL!+6CjpHj!{KxRMAmV=s^(2LwFo40yD8AMM!5-40?>-0{rRW7+ir? zMvhWNBUDi>msRR`EUQZNc6!@7JuI_Vhfdg0^->c*1<)r)j#Nd1RS~9EMxCnjcFz@f ziiw{NfYTyJsPrc){TTsH2ep2B7qUDaZb$OFgC18~r?<__%weuH@$-OrZe)cjELVlS zhpi; zNl!#^)fvo_{iRwwW8zl=>552$^6-B#kuC>PfnL~!n$IEnOdlJoNj)_)&7$VDoA`}D zy&aPz% z6W8cvKx?FE_S0#g&T|vgywN6pFHrA^%vGsVRO&RM-VW5EdKD|Ul8%^-x)(4Ha5Lq+ zgo!@{%&y2Bg|Q|ziJ12Rb4z^$F%N@in)N_v)UwPZ%c|}AZFA< zI_?0V1y2LusmNmGy{NpuL4WaQ)H6`wTet4<$S~7sl#J-N*&So1Y|Y-E%{>{*C9U7G zhw%_lDnV8k_zRC>Sz%zYSvnMl$QCcp_yz$9B_{e8EIkFdtWLUm38uC+wM;SUuQKU1 z>M5p$>U)NX{{z+eGO|c{H!1Hn2xYjgnADNmd@u)?__u)gCQz1T)sVWW|{bp0R16ykSh386?|!B^AqZO`^embR93i-GPq+5E8KmqW7KZUx^oL;wbeJQ z!U-O3}D4rKs*9rHo08=rW1nSn?O#s|tRPnva5%a#}OiBt{{Bi^y_SaG5H&7WrH0 zJ}$q?B(_5SmXT$u;8ay`Ci1t@{at?AB(_2R7;HuqEK~*c$RDc*g<3&>ViMy3v3=0b zi_r?vv0TsSK>+R#`_L;>b571!=|@ZgEB3@Lku@s)tV+K^GaKCvGQ4M)9F+5irgcVP zKOe(zTKpo45mHQ1QX)AM+kyKTHB2_~HGvXcB1gw-|YbkqjApzkq> zd0=3l$SPI%CzUStmmo0?g;Lh8;_t@ZqpQHzy;XMlXVh%TD`Au0Kdg1>QcS~Sp2F!s ze4VA>56WW&b{oR}eq>AIq1|hDoaAmV{Vr0xYOL<4p_$X|5c7S5m)ljhx<+#QiQhY;w+&`9w@5;N@%yl89vF@@leu=p z_M?BU*Gj2bAe#vJ;LjWJ70F#8{((Uwp6)kdKE?{a?S}a+Srjy3hu)`7pQTU9)j#%y zNxX{M{Vk{+E#21I%ZWS&g?$70uVcR_JyxX`K!%?~ z2xb7-G%?XH_02UM`Z5bL!z8fkPkf~!7pl^$Rq4~zx2{3<$wI*tnIvP`wl0@6hnv_1 zn3>B&`adFWBw(otzZ|-WpEB{$2+2$DBl0|5kC)^Mw1(Bp#V@cKv z%4qS&i@!5l^U2UCm%~a_bE#lfTHO6@U_U|JQv6-S-<3q3s$3d$e_05v0CHlskT}p{ zHrT)cTsSP#!}+sR_s36S8$5X1U8wD?r~4IL=>P2N|19u-<_k=v_`8Wefu%p)?FnIs zk;HE3i+lUHc$y1|p&!8aQ>uyk%r8AM43nCw8+3z@xQ`I25WhzJT9W!>cyq*ml!&rC z0l-QcVQjc|iQ!t{FB*o@WMy?!CQjC6x?aje281~FtzFpUE$gtv@sZ?3vYD6n_Tc_ z7rezn-lihYszP_{weV`OJ|@YHz{fWCP<}&)F{eWf{M8#K!;#07w}PVk({TSFpVdXoY&N0f>vB{IuVq33wtrP*W49TJtyaOolsW|3n=>(vnQ^19 z<3tQ;Snfi|8B9ciJ{*0*B)cFm7*$_jF<64pI#uiDThTjA@=<_1q9PZo(w9`}tJN93 zwQMVLBo0ltqUW0=rlQHGEV03407iOeaQj>(Y_y(C#{XQ|fZ!Ac|5CXK!Kn;BU%42; zX;x;Wc; ziDvRkoVQbDN2{{ip(=Wn-xBE1Nw-5*_>_}BcDQWYJmP|ny5M6r`)L*Vt15iJq5fW! zMz2O)pZ$3khF!SZ*Mjy=oEi_5rcIi=+0XcGr#{e9UoROeEL@93@x(wyUg)7*R|QqF zm=Aa2$gm!jdl^6#J}#VgIZmMsVErCadvTLWR(NlqWSpytl4)axLBg9>vR#Zfq04x% zVZNx>LdkaMu4E&OR|k+<6}e26O;Tmk&~7-qfxYXV?Upd!G(b+Z#4Z;l(-Xn$OO;ft zJ;?XVqFA#Sd_@#%&&?~A%*l;0Go&cgsLm;r`owsRC~k=@4qFgZ z^mbPI)t|5YfX*Q@agkHjzqmGkUPb<<3jZqp3#9NG&xYoPgbnMln&5)tryNQeV+>GU z6dzL}g#Sjw*X?o9ZpfoeVq_Q@qY4mS75@$K-z4%IxdVvZu(!f`CXBteU|{bQG~N~e zJz~GPRrgb-j)qCdi7+f_xatX2Vy>$XCMO_=4N3SgAn-pS(YJm!&ydMWM-H)gEP;!+ z7L-rL|3dsPiT?JcW*o^MWOMQ!M`Ifo93#lsYXt|`ErtIL3B4mHFI|<;BI8VAyHI6{ z_YmlB#s9bX-xKrQV7>wyb16085*D7gC|6<{F9ZcTl%CHSN+TXzn8XqYEkr$yW4tDD z08ue?5}@8B7KQ=bDcv+q>6*m8u&7mz^elf1KQTAh!%YOQr-0I4Cb37D(loz--3=bl zh8oKrA5FWH^l3Z=ATQHQVsaRChMzpiBx=LSGyUWmlb8@rwujc!?m0<%5CGH+6pY z4gO9*i*HcZ%BWq}MNE^-3)Z|(aBhT+l)19@)t}aZMy=c8Qfo~LhARcbb*(C&t;)H+ z`WL1KczV|lcC`;2w)L>MtkC6kI_-A2)D)9i0Zgocu2JPn-R26qSQ)iTh#{F%RN7yl2{`uLybsCRKpyL~1ox1dw`eXV1P`@p|Z|Il# z`?KTY>-1j)>wSTGMn5LMf6({y*Lah376Dm$pbg)&3irMr&~92*%;!Ve9rr1o7PMrs zd(W(RGGR{5DMB%J{5R-RT%5Y5-JW{!OiRN(aVVZhc8iPrl~3{^hm3UvGJ0E-UQ#Xl z9HkJ?Q6L+8II8d~iGCIU7k(~Ldtj>&&tL%jw#|Jk@s*Mqifbb2j>CiT;V^ z;;YS$9mzLxV@HX5?WAN+75S$s*-LyJmr#+fe>QeJX%dfxI$X(_0t|}_L<|M+=MnLn zP1@S{%{g(E+$+F$h>ryl5EqKSAJMW+zGvsyBxVY1$lq*8^m8kLf`SU zv@^9PiDdz;%%4o+nQ%3nQk0w`*o(zqD*iH3`WKHDJ4&GOXOIcgcwT^)i+_;#%|!fn z&S)q5g8$?btVQxs$NJeWcouX%Sx63(1tysaQ$K@Q9#LPEDkPIIAz=X57fMbe>?zP? zXS7RB_KkKD4|UOaKu!=T6e z$?uuO+u`IB{N%T|8RABRk`pcAqaER+0BXF1OE}2_9ccqc*nl1LO3tw<=R)~a3Er_3 zTdU8ZP0i}d{X=qkzHhW|!)lhsdbw|%PxtNbQDGzPZS5QB=$F2cjvg&QCR*-W>D-Do za)-%3tIOo0JKU-&j!_lI@}U5B3A%J2-3unV3?^Ea>XKUQ_Sj`E&KTvd1Je0;POT~y zs*3$-psV;$Aj2CX-obSgBk{Wh9B&Gs+Xs&C>({{V>AWCq%T44FmiQCl_||?M9N}w& zUwfkfZw?q3r13V4Cb$)FydA*aQo!3G2Ep-$0Nx0|8wB`U4M!Z(C*2Gj|3<*^wilMq za&5l7d4RXP42B~=%x60BE!_;l#Alpg{)K7wOphXe({hW+tqi>Rhjq04u-v`j_{%>l z6Z>m#b6}g4!r9v@tUNME;~#Ivus1Rgwm;lrIEE>+aCsKa(qJ7}zP&AiVamkDDgSUh zhIl2MZ8uBLwjcRqTd-YtTLa~4VR;h+>$V)u(nnC}h0`eWL2$gqgZ#5R@hne3W(0977wR0- zEiLjk7>;~1Jp;!->J{q{)*tFh0**4Lu2O#}r*J>8^fO53AL$U@)`4-hf0!=get(XN zOeO~~Y#ZB-{!wpOFV>UwqU`80aD?YC|0px+o|U2PD;cEmkMyiOqmtru z+{t2iWH|D88_8U_{oz)_odI_d+|_WugL@oqBizSuU%{1vkx_6b!eLn(`3CMMxC9Cs z0k;iY25vT7J=}7*W8lt$>w3*Z*R;lId(a;Sx~?ap87 zXfa#@j(wJL4eK21Xyt~W*dEej-`e&6AZ=8;8|`5MZSqSVY@fD$jpg?bV5rlq2kS@s z!2U-2L4BhhSX;#Wo{nus8wOHRKEtG)7tkgh;*bvMk{`;0Y3w6|gE;f-ZEw^&I>J=L zkvH;fX@8FPVtJ%V7}B&j8H5Q(cz_8n@B9~d>TekS#ZAEfPurZffV9akDSag@9c9m7mc=$;Ssk0;hq4dz zb8-MfU1Ix?FSak+i#o-+Fr9kEzA_4qGPw%3B2hQU6MwCJVt5D~Y0xpwU+NzDVw~l( z9m(Uep!~3YSUK>QIJW-(tu{xME?(z1P)X_OoFf^{1NN1Y-MgiXNNI#^uRBg_x$ z$-H0UhkVeHPr^|io8p1ISUJ;{GrTFCCawQB$(g$P|FoRLJcQ+ZX&~qS6Mcn!J4~D7 zGTV?k&vvISvh4{&J)_PYxd|BRQy6Ad0Au^mrtAsnvyOHQVVwNfF~;iM0Hm=G4TiIN z$zQ@+d&08m*f+@|9*_U59;E?{t;e(gW^?*#%c=%mS%7PGedk}mWnW}J4cCiltPg3G z!;x3kiM);oXocI8@N^lt3OK^Uj0t?d06yGCy#g3y2~5c*Xj&VyfKgE z+q(Y{gny0PI97ylKMioLjiQ{WBh&-ZW1CVAm%coYq(#LHXY$epLwKj;7I=%xSsVL zh_rBh4+&s4RbNXx+$YFGxUXA2S^glnaQXF!v;1GOCt;bA?{IrFucu5|SL$1sCo3EB zW^GF)!sLbHCS|b;Tu)ihHic!e-6mj$^nlr76EIahU|4p~vWE76Vc#bV`wi<<3uk4) zU#nl#UFvjCIZy{#?+n~9IM##oSXTuX&PP<%kCg97IM#tMbjQMREl7LCIQbzi$9>9~ zf8>p6bkuLkjbZj5{x!q>`-PF^8Ak9o0*+-_*^(~PXbbtrGN@am%U{y048j@w@{jPW z5C2$qYb!{D^<`eqx=chGWn$|<`jq7;IR1Sa+)&CgSsv>^c;=JGmyvJFVV?ywSB)_LSV!__>%lhXpXHliv&R_5e~aO8va zvFSE$f5Wl^*w6O0*gporCE#p3uzr)^NOw~*W!bEYl@;}qvLZa4O=o?q49O4cIu*{= zhx!$k1(9^2K|X~(l{4!*3ZVL_sB2nk^ef@q2!CaTf0tN zmcRS=KmA16SX#6G?ZdL2m==Zm@n3!#X=LE|$GWlYy5Fwbg5je4Hq0=;i$wN%w-W%k zUALlryUA@0OK}HP__D38ak!|fXCiLb-CyZmN>^s8|NpymXW0j)|NmXO|KGVwcXZHK z{LAR%I3|uP-Zj*JL#Bog6%oJFUC)3dysA)RJ6p4Uu1jy+4@WK(-@DK1joHYwO8?c! z+}%admm*VD^bLAAcEz(Hpn12h$lwL-J~-=9!E+`!q2eF-JV%#X>Lc{~UHZL+D)zaG z{e;tO@A5R;zzm;QcIbWtVH@}5(9IBDshV)K3dO*S%hEalJRuLXV%lJ3!O>ELV{CIpVPh3;K-Sm-PODB6qJ^*4hwU@`1X9-!<^-Zyq7& zKk0o#?^_`4(etp^f4^NYPKKi2(fgj>4@lq)v6FyMQBLV9-^M?DTuON)yx_Ok%Uhx*cEl`#CEjf9|Zw7Di z40v1K{mh_Klw5kK+3?OE&~O+&(llgo6OJ6SNmvC@t)7<~#@7?N2GB=`CAmSn>xR7B z0peu=a!fZ6()_PF^d@odlk*1bt|NF5EUWjO)REN>;w%`F7EEIg&gwI37)2Mq-6&qa z!91My;t8&-9ykLCBd5bV)PL*b4*yWX8SKh|65*jEaeR#US_&`6Se$1qwqS3`oxD_%QFlS zoj2W4EC0$UoVHe9;;NY%m3O$j*lIv-8yrXL&l^Cdg~+{W6fV+H-}%6GB$v{8xpzLx zA2A9y>8S6Ud38_TE`04o&di?Gsares;#`ydirf3*8`!}1_+Gq@v76{k>OiTLau7uC z4(UvVk)$y3p3JVbdgqKijG@Z!H&NW86YcGDvopDolQODrryd4%B{dvUl%DTyuVX4T zCq7jGCNp?L#}uP>)%_f8+-`yQ@SnQ?54g?eYlV#Y*gA%72C z$@GmfTXh&Uj&Cg=;ERrTl$@&ZHsDeE$XfK8iS`U(`3Mu854?Fko+jO8I_~m&ndm~~ z@7t*KyGnnBeqq!>*~q*~zt7@Lu$f@kG|;P;9t17V=bI+_a+G&z7hX#{M|a?W<5{7` z(k6PVgP_E6sJ?gJ$_J|i2MzPYoIBPQ6Zc2SwbX@EaK`$DnLHH!BTBXj|3 z>4z>hs)ntvzsXrZPllL(*-`Z0q+qXEhD%F}RKebX4uob&jc{p?oABT?N%c0}rdW>L3EpnLK2;2|iNpEHy(bPa3_ZbQ|MQ4vQD`%B{ho2*wkuQh0#IV zrM7TsBYCMos+1H@=`I1_@?|!EdXd^v;K~ShsvGmrn;ghi0#Z(p)51~#p+X0R6YeOm zf>5W2s|u(O9Tbjp0%{JS&gcQG(+GQ7{}4_tL}i5-VK++5NU40qd4 z!vMEZ#zEbCCc;BF?9FGF=OB2MKlI_y9>=?Fry%d(-1ujrd&&TqvukCKnAnUi6Pu39 zl)UYgw-fBf3%W9N%Uv0A_k^1j!F5XCDQ_DNfq$bh7_KWhWro8<+nt~e-EmiTGw#*{ z?gAe-`2(oGtCOMewd{HmI{*;%k!qE^PbI%1^}mz)I6VfGw}QhR6QGV;Ch9Oh$9QXR z&?`IN#0~^*Q-J#bsQ*JJbN4Bftu!%MxmfctDtVwvV!{>-kjHiEm7Th&Q!lc*f#b$# zEIgrs-v@7r{^*-+yb7c1bgvq{E7;ft4&nhTJ332Rw%o*yLm9{VWuWH-!(R0GPQ3oj zw~axvUtmR++k`Qa+~3dbE0JLw^(sPdrLF0Ffm*&5xXI>r^-*L{8Y%m8?_BoeC@c<<))4G{s(RR8{28YqrWq% z45C5kL8FWxdKhAsq{sEwe&A{SDFQNWh=zK28_hs;XV(?i)aOeG{5wYf1yy&r?9_aBMcGw0sFB>D|I@L8K0AHdQEVeHl%AKrKuMDv`fQh108 z{}}PtlGNG54sF22^8PDDcsDY3lCK+4_q7oZ_WexUj^Joj3I2)1?-;p!%}QL!)V@4; zZE`d3b@Fo;!7QoAjnzFT_uc?hPe;~0v_n8|H13SpQMRJ#PYdpP#v`{;|;A3LDI$Aq0 z@c`;|QLDIEdWr4>sec0HtJMeuO4iMuq)7+x3^lID*i%LEc*E$)Jw{o9ay? zs7AAbt7d&X?+cQipc8In$^@6qMkZq?L3tYpPz|~neF$7TM5_IBjf^W{WqZ)B-AaOcX!8SE&Bdl)2NW1%G^qWis-RbyD_Vn)Q86j4Hdol2##G_*gdss;*bdNTpyA%pEqTV6k$@Nx zK#ZXvuxiWbG+^_?uc(&*Y-_l!BKxZRAC-qIinHWY`2jdBEjc7g56D{#~U?I zjGp#y0>q1VsNrO|Q9%zu*XNLTte9Dvy9J%-l6nt~%ZZHMQ-8^y+4{4fgJxZSlsgJz z?wv4?uRogD90y@veDtQ+?l{>7CfUG52VO^f1uKnPQ zUv~6nNv)2vl{{XeN7?An5Y)=3&0@?adJ%3kQVd zJ+LdP4r*%QRN=xmJ3H~EJbaoxtJs!#}Y994FRcPD41b6TL0lN7RE+xyqP2tu(jtRVCqO;On zHx&91oA(D1SiSi2{@axSAQbHd)LXmvi@k@aeSbq@>^DyOT}*tFi4m9hps%1h<2izGu)P(xLTCIn-^hs=N_cG` z2a??~6P@8LIp3K7Kr%n#&b9nCD*q-9B)fpjR6QBJoTDrz=D?bQSNC%RNy#ZDFWzPH z@&c@5U<~SX0v8NT3v7PLJd>9KgoopF`CF*`t?)GD6+O46L+@@Ob~Jf~fWRXESyk1c zs?KGj@DC$A+RI6j>94OA!(sSl|AlW_rPEhERGq2r=ztF~c6RD3 zdc-g99v|i_^h2D#ndsb3d;lxg9Qz9)NDkzndP459FuK!i%-q-Ma#5L<9yrULj5Uv2#Bz1EA)l@X@!>J=U{zKpgL}W;yoj(^M>Q~kCM>l5}vjC z@w5#*Wdl#zz!SpD;|}SuoEU%9KR|fj=&#{_u0MnSvVO_c_XXBSuwN4YPoWxal$6}p zR`AL;Dr_%T@b;Fdyw7@dcprmn>Hp0?+%$A?t|GmPc#BlUrQ&1FgzzNsv1xOaDt|`& zo5Yvg@);7wgzzd=_J#PDh>vM5QquHGzZL&l@nNr#a)|gavj}7F4L(*@@Dub)KA~T{ zNc_R{i~cVD+2S88K3;0MN~JHOkGT*1SH;Jg17T=2-WKovpzGJj2(oZCs#hUtRUA&g z-1o6*hVU@@Wl}2cnL@bqSn=D%$Mzahur~!?xG&9Pxa1@H#RrH#h(u4XcH(ii9_$-0h;k$AQU17Aux38Z^2el_ zL!^S9UqS4H`IWJ(qLpp$I8N`@cE zQ7jwG#J5v%Rth&1Vj?Ar z|G|^UuHJ!r*4r|#x4%b%lO3UDa|y0-#Ene}Sh}ZGRh6n*Slv;lx1`K4A1kQQwfKgC z-i0e>yBIIV?V@`D1%}T@8I2;xhHkwrM&?{NjA&1)A-`8cUWZ&vbP}qO3`+$Y65NTt zT2){SMMpbBd`$dV_Lnqnhnd70P(6&7ts+p98~i{RL2UvL&ZPX zr+Qk5>gjr$T75!@>Y(7>PZfDo4gOLM{uijqpNXCg($NrUv@cj~5x`cnn0qT}mu%7du8_Bt+_g;xA*K86IAh^;$$1J z7g|)f-P8&hQT6xoAQ1((Nfms4-F|Atxt2tSEBS1etlcF?73WzXOdKJHwbT(RNE5p~ zo?u91m48m9nwx(Mq2)ETuy4rW(G(cGrMv+ZVG(`Dn%DyvyeBS_a%pzLDYbHWoC+7HWs~Uk~;u(oJBnv)GrO) zepGa+Nsb2qo^w2;1{bKo*edk9L~Lt}`9HZX0nw^~f$mkz6x~}a{=U?%NH^`;pgX9s z(Om@qdo~F7lJEhd$IKZ))Qmc+%5=n#up>Cy%X5T7slV{%264Ztizfr}`I zeY%T?6}+4k{9Gzn%lK7{esW&st|z5o(#_ENDMOHH_MGgM4qLi|R@hMkyH z>}vVh#Rlw$X)7?L0EavHT@1F2edox@=sQ`xKOapTBIB!3cXZ*3d82M)#wb3EIM5$w zjoOe2DSgpJCix^3^9dE{Qk9RZ!5;h6*--jY+!+rV_s_BJIt6zK0ptbTiL5G5Qk4&r{H5%&_=*$g4nS`*>N(t)kLf%2*6o&l(UB(k zCNQy9^fAu@@vC)Wvfbk?nqrdg0N`!hnXM|*s&XtuVPemtJN>77cjDF|8>t*zK+6}1 zKZg=Tcm99^@&|OBNHFRwF!Gig%!*)hzCkHp;}&l<=yf&d{anZW7$tr0O41cV7b{DY zF%23N`C$Y$cj|N7I_R7aN#-o^F_Bb}AG>unbp2VWgMUIG*KDM%h3)dIfikp^^t!`ptSCmsPcEqh6Y?fP|l%GfZJj~L;BMQEc>RjF_i31$bD=em4 z5|m#iKtmkRl@{n+A#yh5Ft@wRW%&{Nw=6&MT16f>C1s+gNqrw>{g*R-s>B~*92cjW zsLTh-9}eX4v@5eqs_zz2s`W>_hwI+J9 ziEfFbd272FfL_MC5Vzl5pd!ChgU(ljUSSWtf<3fEr~RG})N@R92cVwTt^ea%RUDr1 zF1M(cqKn?pz5i?DT?3G-apSrgG+PboAoW{Gy%Gaz0VrQ)qIIBrVfevX`a9#@0yIqY ze6)Q*`A$4ovz<}@+P*>BF99jebT=EblabERVEg4h9ucfZdcG$S%Y_w}r^fo9prh|UtJPY3R zP~S$&WyCcmy0Hr%g~Eq8*>1&bFMnMGc|4m5+0QgCh3CjQUmW*1OLG}$@VbM z#U_gHxuAf~L0K>-WT{%g&Md}4O|08 z@u(6t|F*jX|7;~VS8DHDpYg08bnoks1&w}VqL-o)pF0bh9%ND)7eB`EsSGu6kQ#^+ zO8#;HYf}9K3j2pEO#2Ja?WLGeY=eIeUDCMHK4|1Y`02y&%|(2dD1(mI5x#;S28{av zL@nQ22#gbdG|7B5yuCFy-9dX|;2lE)q%o<kU8OcMy~v#ov;MUsu^l5}}7m#x~+_ z#q4i}HZ5sv$vtY(BStUa;`wxY z{H}1LN!VsEwaDD*g}wlgEc1h z8k=~lVA!hg^#F(OI9SEr!WVo|)mLzkGkCC8INGG}eccph+&8KIhpGN+gR0VEed?;J z{Z2eU%BmovpE*m7PW+K%_?D&@wReWg#zl|^fMvfcmVH9)E&ISXbXt+yzW)4LN4tzx zCiWxK(mWp&>|+@n32$T-jxhNZxOcG}A6iuXcUJw|shIexyiOa9r-WEr%4r{Y7Kvc^ z3`k+b?KhWaVLM6t8&VUp=Z}Nu#08cQkSN&dB{cvOyUpy;CjX!bXK+9|H9<$bE zH%i^X4NOrwsMm1TA(#SFpP#KYy3!f&f}2hLIFtgTe4XldmFkBtronXQjX*IUxnhDX ztpXt(r_?{LTxL}Y3uw#1Mgb@kKVj{Hlx}n#Iq4Nhc%q4Y3{G})=SK?;Gx@W@3Fg?> zs(uHnejKpyXYwYaxDP_SY$xP3{lXu}%ZJ_O$LI^!&`=wHwjPo2mV%=g*6&C-7Vw-l zLg+^l`g?bSj~5#R0h$8o-e4<pC$2@K~SGuLwG~fl~O0 zq0ui(ocFM%&Sm^1iJ$JzN4+mmOrW8s&_1W4EX8yPCfIwWzegR-}umbs-u*;xYQc9_cS-ci|c(v6Ps8{6nx(Q0}cdOKUY z(YNi@oC7tW<*_ZK?=X5nozb_1XF>(-CjSw%{llcyZ;a}N0; zSGpZikk%MOzwjU8%X6N0hv2lS)%fnujRawtfc{hbkEu)Vb+?~JRfr-ATv?+nXSpDJ zCH^N?hWsp<9*8|N%5bzVL(VNJg0GFf1S0s%Sxyi0=@=#(Q9hvR`RjkST3Ou~; zYNushQ~14<^fgP$;KSf7z~7a|=MId%2?hMe83*qX6LMu zON+b_qCZ(Ee<=PN6u_I^S8M2yZ%XF-;=f6dx14Q8_Lq|Jp7?Ju`|WQ13e9r}MVL24 zAl~i77>}sgAkhy3i5C7{qHhCVP3eX&{W7@^`(^$NB3??!QXH{2`Ix8~gQuj3f5`Y8 z#xIum2Y$ayQ8oO2S^BQ@OYS@b3GYb)C#XTf`!?{74ZLjw_NCX-Hy!vJ#7{1>{ql9H za_J|MSmU5RwIn`vX&(vDWS3yC0x$K6{Ec#$>cot?9nHEu%es|unU#MWxdO|QlHl&WF7pC5%i=bWX9LCtV7xK*Dl#{%yPC+NKEA6g z>XVqOfT8P*d78gB81n>wZ!+dlpRs)Rl(nos`N(&NTFV9qWA0FEnf-`Pnca&lvywG8%(nu}KA*!%KC2U<9eD3%<9z@S z^v}ywpBq)5cS!s%n9UU66XIa-bz@#Z8NGeRUJ38Od!1Nm0{3%^ixaE*Z{2p_y-SUU zuY-B8b-z`8npB@_N&ZdpJ{I3O>j%C+6TUy-HiUif=XDtGM_~P6u?_~|548JgoHxf5 zL;&y;Kk(B>sXo|r#D@UCg!y>gStqE5oVt)6eH;Bk^bhziv7It_0#C^Y)1*9@LRdl* zwuEC$0W4twEaAnf_tUEPM=T|wQOaws6kQ@TUljkjfO07*2R1gZ%$VQR;`CU^#wJX` z5KzW6?{rmOt;(m0jWvmK(0rA{-GGrU9@D%p3 z>d=$i{0nn^w^X`e$xptnX8k9*CT~1B9^_Bd@^;3f`tc@D9`D*&aNZ8#S+J)~!S1NR zOuQY zOl&?)MQm>?-VHXeUU0-#7CuVMSBJ@tKyFoJqSwig^eq8P`TC0lZWp|b;y=a)nCuvW zk>Xet3=~(2ssF9C0L4CXI{LlIJDuVFvXI6RQCJO>{k+szcA7x(7UR7LEnuqUAO{FW-n5`_f)-4W2?ktgDsq>eZg1dlwr^TI*wp)lbwO!2RLnZD70JcglP`x&)UM~f0$JWd0 zVUU^ZWaM3DC3c3$>VEOF8I31B+?I=D;fqcRGVs^40bUron)gij6EQ7|*1|g^djqpy z?AfxigByFm7Q-1Wp-cU~^MGJtqZOZu>e;ffLbhzYUcgVccpZY#CH`G(*@@wn_4WW< z(6VjPvMUHPDa16^prLufF#>dWuKBm&K8eZuo-H|41`XY!4?+{;_4d5)P2RWYR9Rih zHpVB9AyhpOdmRVLolwE1zG&Za6VJyJ>6D4bK}{E+ z?K~k6PlVqoOg(Q32Y^6-OW-#ET!NPh-24Cf*li z^fB>r&fbsr>6eE`q}0`>a5Ru{j?hP52>J(OM6ybh8f^-3G{0~wyhNocUQ`utSObu( zLW6B|1^}HmUTRy&HwJRLqp*`L`^c(<1ZM4_zU6o^)51npP~sq;Y&Q_ zZ>x&_A!C3?5b<|$f~AKscq?oSyk=AQEeL!Q5Gcp|r-w1{mYYIYDXuWjROQ$gem!Ii zzCs!QH1W?v#^Cd?G4OUVY13uWn2`9$xAZUu$yZG}0f0DOZC7P?sIvP-iA?f)G}q(Z zO#zojY?G3&rDaYM9~%@nv=yEvCH)`=S{OzB{fq|;bjfCj#$Hw-<@ z-zrQD3vU%BvnIU@aCf%2d~spB&{kox-K6n7#WeKsL{(O*u)qnP!WeIRRQus>@<|M} z^7)HY{Rr{fD4$1$wy#;~_IyqLJdVTsiqOoF%&A|svJnRg*%y*^L@Rj`YoX^YJxsA6 zrUz}*A6<_W@;p8jdDL|ebS5lCFsdIeemk=t>#<{^etJ!MB zqr>l9$jkt0$hWRGm^7aQVZVEHXEx}H#Yei}QMnc_h7hh%#qK0$G5A8lL|}v1`9fs8 z!`xHI;yX%?!ZJbF%O%W`glWP@AwJbP$YmWSS@s>S;u#X1WI3EH(K^;`La0GdoB1$c zdUlSDlE+-|@f`J%M_uq~k}A13XHsfqev#O~PpBT|KdzbWPa+dIQ3701Fd>DTcY?cx?yybg6R-bU!xAG&vgE{KU*RE!x26!Bp34+{GD zJM7QFdNA=WKA~P~60f;cTLRtrA1LI@$e~aYg%7;>d)40iDCa>}4qvPR?I!UXsN`Ke zwwMieaL}8imlX5VAwi2r3&MfoFCyAQ&NKlUHWpMH#a~Q4DGDv{3J=b;fAIiOrQW&r zFW{WgB+JkoT9}+K4s^V&z zupRvtNe)Geq;+A9Nmk)qOq1*%-lI)iZ;D|3ina|f@s_2|gtllC?WPD%A&Rz-w5y_v zRZ$n)EHxbUe!$5R-8oqi2&m{EQuhPIU*NYH&fvK=OYRH<12)En+H8g?nu#w7O!NnP&C zwMb-WpyrAHfRR1jla53`Q?wL}G)CG~(Uz)cdr=;fnvcTn3vq(60sS3MELH7F#Ms<>rLB=D4MT3oZ5Pz$Tw>)6z zSXVx#24Lu1mvEFMaK7Zv@d4ZtF-Wz> z!|e)g4IiIpiudU<#d}AZRpFmix{$lFC&8%mBZKJD*io)A-k!P;h||Ic#Nsnd@c}@r z_Yn(ULBBq$+xf8g6jR&?h$WGORN?8W@L7^R4@RTFc>967g~pqQ61blX;`71-Mtm1j z+yc}U0qS`meo1J+$ot9^AB_B!ktS7Gp$Z4uu9CkLLcY~?70BPS`+7xVMeT=)-;dgU zTaOiDd87hi!o~C*Ix0yPa7(au$d! zK<^HBE+y|~Q;dVf#ZN?*se(&X!2>`x`S*dfTb$^%U-iCHd>M<+81E^P40gl4r;T?o zN_)hO(RnABVm#m|ekrn46&$Jxu+pIc%zp-?ZwirKDnv`g$8#7Qk8xw)I+J={GScD~ zARBK+<*xQLMbjXkpg*HU(IW@@cG_-$d!LfY{y{(b46^vtczAI-_-K0@vO11~%V!-G+G*Vkp8mZx7X_y~O$*w@!B|yUJUXKY$!_=9Q4Du&L>Xo-lc}4#v4oU-AoF%mjQ=nEj2DvYj+z>zA2dwlxdM8 zR7sgC*@-G0!-*|b5?X`d^e`69SQujR0Uxt62nR6Nn&LC?@+l?d@m0PW_9~N>dx4<7 zr^vNICiP@3^TJm<>rYI{5)`|bSD2L+t5VFP(ayRbh?cr(MHCv1^3b8-&t)5yg+55^ zzmhz+t!ZXMOT)6pwrb`DZ&U#uYi0PW#BU{Tc~$$Gme!p8NGuTr0*q`&7q<)KO6jp# zT~*6!0qc5G{1`-x3h13!JzdK7M;O7O(phTtcsHBT&zq79P_uO^a-1riu1cShYuh@q zlZP}O){+T|EIEONm7EAV7#Mo#8G4%B+F+YSuQerCgUVHw$^j^HH*M;20BGv#0B~*O zXjO8BDtV6gdldVJdr+hOp?tUk2g3{(C=2ww8ojq`bgfOv1|YAG9HmMQR3&QwGehUq zo`XfUf6smFT~mTb9VK@Li_mYYGbXlLFUFM+`&f`WOv!x!xfi2?8gQB#aK7JF6L&#q zyXSf!rb3C;tZaEN@v$gVYL9M5G65m2RE`-Y;5b~US&jheH7eIx%d2=!svP5iv_*a` zM)-d67O5`hi=|98MGN@;D3-rTUjg%{`3hL;#{XE>l)MM--{q&<2TWH3PGWzRr+0Ya z3Tryta$1-{b?p<`*cqk-dx^Xwz(<&y$!I*dtFbK-Yc?fc007T|KTspKQzQKK4YZnn zc)kq7bk%m@J)8Q_EA~K)8V_$Hp|_Ug8E>Q?@=QLj$dfr;@oSyNn~;-4uPP3Io}pjt z*1o-lb&^DXlg}An$v~68oWGSOzcC==EMG6o5`oO8L;k?f3mZmA80-?Zv^iVYz(^Yy zVFSbc>uHSlXF0x*o-7>fV)74Q$-9~S{rH zZNT2r)yrO--fLS2&SMJ&kDG$W_={(8|5szz9~V`X#kugFIq1h<@WugMMU)vpg_o2+ zQ9-~op-{ACO~c2`119GO&I}0Zwr!aobumXxvow9`uBDj~m1$X0nN}ayFztt>rddH{ zX{N2Z+3xq=H$QR4@eeNZ-aGf)^Ul5ZoO91R_uPH-{~mmkqyM+?T{h=5dhulX!xwZJ z3g7tyKb90P%m^A?6x-^#jBR6=-k_G)v+VMu_vtBi$zo4tgv*oxuVUN_d|W1zQ|db> zbR*<`qC3jU!>l~O$~CMU!^&J%j-zv9X3$aU)KQ6at?hFBQILQpbh}vfX{^j+<#<-! zMG-#W6RJ&oH&|63lFtEZd(LC6fE^M}9a7PA`@C^{)Ht!rFAwhUl2-kxuEO4f37 zWsT&Lr&5<|?!eI5(RGa&2K2Q;R0*3MUH6i=*IxAZK>e};ma230%k_KGq!RX)=<==J!xpxc2>ondu9rgi1Oanre|1Q8M9QIJ;BH8q0Q*Cu~d2GHFA$a zfz#_W)j-x!A80aNQYlP&a`Tw*%m)Y`&r`t~=nsvl;st~a3j|Sj#BhbAW@5F&lOE7& zeGr<1)l@f_2KjLC!w2e@H#QTGU7=u zU`<87S)kT&J%Ls5`#)oncmbg*LJ!2x5yN<5c%127BtQcT8SB1h1Xv^1|(a6%o-v^p!-vi@qt#X}MY97Af33-weKm9L~B|7+W@Yr_M%p`2s69(Y$_> znHe!1I&lg&c^r4I-;9WM^Fk2_DfANZDkX&Js`z^pZh)8ZTNpijT$cC7s|@=;)o$6$ zE}nOf=SdaU(`T4Q*YSb`bXvug`uY7kB~oqp;Om|85XEgiH1{K;Gwt?Eu(@=n|50 zfTXlizP${?pWDmzAIH6vX{lsy!5H)8=fsPOUU@Z!L~pBp%i z+v8^fDdYt>9)(?qRv-i3Cj&mr!S2;&x|ZMd&M!@w@kF}#Z+JC+f}ZI`Z-y0J0lV~ORncM0 zLRF8ZQn)Hm3eyRw`ZLH}AJRkw=2en}^Q`=qmFcV;%*qUk1*dOVsS_6(qRVlleYaXA zn~8pF^i0SE#Ho9KuJB<_SdI~f0oGMreDzZoU$`++wRq!dsi0;{t~@U*F=GAzE3adR zE=g}8>7O!IHgec!K&-(_>#xxeB{4CH5qgr9h#4fr7G!&1bMJZ|O^MJwc-vvDJi*H2 zw91@7J~i?2Mt_Z-;37%vPN5t=#6Vi^2hlN*9;!maLJRJiflPm)j*}OvSo{Y*>vX4Q zg&5ePjr$Y!T#tip<8u8{GwKqr9ns8dhhq;jNq?H8A5w)CH-M(;R;`*u=vdIB#azi{ zQf~@IJN45sm*5nNak7849o5EbCjukZ#41JwLwq7jtXJ&edDISG3kgY+m0ct0BS`vK zmFJE4qDRPsK}_#LjabUHM4s{PQ&zT6-puwdhSV`8boMbQ;T(e-%F1J`JVNVOG9;6! z4CATV?!<9rzR*2)qyOv;3Z2-2)%lE-%mlIDnA%C0sBntE$!{o|627L*RQpLo*Pimj z{K#OwQ~M2H-Mo^pksHPQCycf{cjy!fO8< z2gfOHH++gH$HA?-UQt#wPS417I%S8etU@wdY8-MN+*)2FTpWY{mkLj+0MGS6*U)-7 z0}9PZ)<&YI23?(ISAzoRl5IwHv;xH@=(Y_TH0 zYbBWLsK?0#9IL76AELiAa@mr{j>ERhw(1%e62PdyhETu(U4r%s91gpKXo}Se`cM_7 z*~;xTHd7gk&^1?>Wx&s3M7HbR*xn4wkbpOm%Uo3mD_u4q38_PZws@8*@7r zJWw!wQtAJeW-Cf4;U@mH&N1kV)@gl4_UPR7*_pFE<$yG=UNpSEZTz~lMOzQOv88QF z&ADIbFp!*8u5ydm?_y%tGbbwMx3*2a?0ox?*AyjqdWpp^O3j;E{>XO!@a&8O?t|cJ zu(v~;Il{J}A-eAL$+ayTFSH)|1CAZiDVvP#?~%fuw3PvKOD1=h5glHF3bPe7GwNFP zH)L{U$iqA#BVga6G(t-&biUjulgV>ziVes>(q=+12QaCE&psnW6(9kF7Q(qRgA5pv zxQE$_+G&O6a);!or?NB};}W+*u^kT|_R^0?UP|g&l%+X1@(-1;3oiN+BW<+VTJA6# z;eRnDF)xKP$!2#YNfwKJu52PPRNUV{a}0*~szFA{YAJ(}U1qAOCNXy~z;sn2mDJme z&>u5c6Bl^Q1n+%B)R*Hp|hvAh%ctsLcP)C^S ziZT!~?H)VMrG&y1_nq!34c9L2J@e}M-uEqP{`W15smwgP&1JU1H3>A5#VOuKc6K{n zyL{e(l2>aFKPP;CGwl>K)Ix||v6y-U3v88Uo9g%!pYC0tt4(>M_2`h|-`+HxJP3v4 zpG%^7@ilRF&c=88JgGfcaqP;@o9Vw$ClZTW7L6$S?e(!;YdVfDUuw{D#;>#ym!Lo>-&qYkNIl;$i0S9UqsTb0eOVQ1j}FMXYVfB=l*16Qq#2e zzP_nqxHa_%>cVK_Fgh-bG7b>ZAuNlqdM&()_0My$_RZcKK9lw?yF97KDXy?DL{Aud ziR!ZQb;Ks(hoUhIo|su>x5}AL$tXKac2}m=Y_EbbnrWxqOk^T8^+B$MQl6irG5 z8mg?+u2e3-qr;9qi$s`2d&5IrWCl}UTI1FRn)*S+SS1^gI<7Ku zr&P-H(2>YgcvoQI8Cm6WVIcMk$4Q&)!U~Sk6t*j>jSe|7#TI)dLJ$;9a)d5nEQC+GhX1SM4f literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/grafite_parser.cmxa b/helm/ocaml/grafite_parser/grafite_parser.cmxa new file mode 100644 index 0000000000000000000000000000000000000000..cd3799fda09f3f618c31307b6597c0d860342ac9 GIT binary patch literal 3467 zcma)<2~ZPP7{?d92r`OC@uD1F2m*P47jhVmAPUha(&B+}SvJW^E_OE%#G)cHN>Q*5 zplIPy9a^nJDb;Ef#T#usP;0#fv~5uF!a~)G_C>Ib!m?(V$qf76e&73l|L^y{gy3qG zm#?qyJm3W~@=6b4m~{e%SuDe_p6fBJ$G~z3tuSmP<|Dybip4`I23N;X3O&whY1rLT z1mWmN(m-hxASkNef(eUrZbf}r;?!LC(-`zbN>dtE4i2WDJ7nnQkhXE++Q2pEvl<~B zHAkC3YQT0M=X{G;qc!C}tM{MU>vj;jgo_QVii!iihb^Bk&6r}D=pSH_eg9z-dRwqw zE+=Uq{!4x~tZBft--j7LyCRjz(35aU3X`Y;^Q^P0lskI*V8cpRmbY$DKpOZ)%#bi^`Z2o!Wzn|H@kc>uR$~V9_tBcQfl(7rpl#7KCBZeg0)@*O zX!&S|_tk%Dh-CSJRnt@ujtHR$(ECnt?!@@y`tX7^Uv16FtU>>l;5x8o{qO}d#ql@p z3+u{;zI<$pPBfLq)ue$1TgDHV-ngke6L&pq6<;|#9m0{36vKjfeY^*~9G`GLXHnJD z!FcUO^rk411tq19J&&C~Ueql}dNkWnJOM&4Gx5neDLQnfPtytl63U-Uz2vYxE2H^^ zFA5i;C21lw4!As2=iQvLGp0J$W_g^a%`^zz&G&=lveod+9Mpp0h5Ee34bvqLU<`3-mOUA)qLeYXcl_$ZbpaWyE6 z^hqItti%h&^CDtiXZb_enO(qx&9wV9W3+ke1DS$6Y0WSNthi!JvEIqw{ zYr|}P;}eq&a7M|-sep6S(7yFIt$RS$HG8Cn+ERjZM*Al6s2G~3cpcXMM+@nhrZSIDt#x-0YNNc^f^&nH$r zI=R=Wm^MXiH(yWhWfit~k=M%2o5N>&myLecNVHp|_ad(q!g1nq=XG9H2h2tPZJEQ} zp}7MKrxOPk_7g7bv}o298;o0u9*!$q=5VK^C?o(v&me{&X;vo3DV3fk0ruYK{o4Jo zZC}pne!e-^*^))CoKGirP{q19tna2o*QAR6nca0Q3-UxF7!I*la4N)JLaY@A!!QvH zMPFi(NCb{XI2rS+?4_yAC$8SUf86bD%OmH?DV8+1O;T=a1|^$vkxCgPki3(P~&q zgE)w6hN~FR%c9KoYEsUU6H&X9&VKXJm9Bur*NH$%YqfH*MnP%X8@hQ}MDwHr_C=TR%C*fA z{cm-TbPVOZLJ{7~^XSMb^Sf=8(o%PistBH9*Tt(o!b$O?>e?4f6Uz&{EHzn z*rqn7VEe=i)-B9>2+a<%+co{vg$d&>%^m8nsi=0v#~cmU5lQbd$9>qgUEQ7<9d|j~ z-Z;ky)cg!Z2n>N@1U-boU=jL5;PXEdboWZd_cIEr^Ll?C5ZH*;2wXg-36)wkDP(Yh zq~o=$P)%u-=*|&p2{bDS6>U)Th5|31l>|k|;{TtQ5GSBuG|wIuCs>MLpkO4=!eo?^ z4hlSZmYH(UYbZHIya5$|0%-O!S&m-^HOb=fIEzEUD4raYYSVNE1JE)(Lkm%ab}4;4 z!6Z)~VcTO~Y1)N{g0VdD2t;O5!^(6t$v}UusCpG?fPq|3O{Lb2g9106SbA1INv6gL zT8nDNml$rUMtgSr0-F|_c6^x8bfz0aMkq-l0S)8)MNyC}OVa#VydAW-g;cUEGNLn= zk{XglgPJKP&Qjl;n+Me2WZf6@NrDwIj1~8<#Zba2EP;oqP#} RbaCa$R!>vvwqF{ee*t^Kl&Js! literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.cmi b/helm/ocaml/grafite_parser/matitaDisambiguator.cmi new file mode 100644 index 0000000000000000000000000000000000000000..a50009c471d83f35f85bf5c5d95cadc5e20ff6fb GIT binary patch literal 2972 zcmbVOdr%c+6ko1aMzI<5G0mitiV%p8T*NdKbvM0;0ZO0~Y%vEQYP_vcFw|MbYnki=H+aOd(Q4uBI+S$FIA1gvR{;_j*&z|!;zw@1Q zzV92&c=+hp*w}GoG?}-!xQrm$hY&_TI zfwb{0`eZvNczp^*>1r{?WXXwwO_D^3Qnk_|jSk}kuqvV~Z5yiy;*p^o7tV9Cq8nI) zRc)c6ONW!CPKIN9!Gc;3M{XHXRsz-j*8oC|n& z#y<6$zZWRt5R<->Brcf|m<(2;!vMfU`v&%D0EdMCcesfiZXwc*Nd807I@7Enh$$>G zD|w&cY7K=zQy`Gl9$059jUoTm)i(TDi;yp4%@zDs2bO|vo`Y3a@!K`zcpWII8X>(U zvx>dN1ynV^m4>FUreNobdXL11`vlI^B$p6k4W$Fh!%Tq9^VA_zb;w~D@-N`o34c{1 ztP2K~GRPweVzavHiM@s$stiNlV8ig)aHZC+*tF6x&5m|8jR|XqI(VRm{p2XO#LAg4 zCbGf^PFB`4H8**YW(#+SBHz@byD{<}%^&7+K%eQ85Rs6aD`)Yvt}%7fUd2%}OvKhKUK_C!E61K#$=$hzgnO-qEH#f}NP_Wo5b_FybUp@UQ|*E_OWt zgr7u!@QEmV3jl*XK3?IxJZov^N{T{<>jg6fKZN!pyhrKV zleK+dd|J!HC3+Z6uyYD)hWf2_;scyw%RWa@zaGQPe@7@rd0Q%4h1sBaI!DmY=cwIb z6#6(0{RcQ(SK!ZIk--ThPa=5=$c?&{mwQqkg8#GJfd-U%)+O`x$-ijk{ z1Lw9u{qXljWU(E|9Z2p(vJA;xNcxd1r>MZ~$TE!}h;+CirNZ;F+T!(yyt-WKf4XK; zk71o(Dm_tE-Bwj2lGq%$gphPvrzu0GFF2pJVpXrk%B_7=HE_8hOJYKo1Wm08;o{!y za7jG#imFB?*m4w}bC9v+mbg%Y8V$q08wD-D^HPnPRuYpTN;UP7W#DmAN)JhUi}WiS}?&hN|{W zVWn(FhHYFXv+jIm8{RP@KmFDC5UE~S1pJH>hwQnj{g{HfJo)yXig_c`hVBQqrrQl! z(A9E%?VwZlE1WakJ3k%AtEygVvP1RCqM@#tRS8S;SFc$xw*u73jF-$`*n7$Zo9pbA zft4G&J*bCOj2tU59yq{I6tIJjl^&7l4bD@RwW+?k8+sWTIa6`)WN1UTj#X#fAJo)N gY?RCAY*y8$$CsQME6ggiOOu`us2_UD#B$<$bBoikSBnpUlA)*Eq zPgchZMNtR5{XC+s$Eu&=dMmDYtgs3y9xJ-8eE(P7H9ZMo*KfC>s;lZ9_1>#jXV=6R zsI3_~X3Ut`g@vOuZMuJ+rfIVrn$`(#55h?Z`3NZp^iVzr!Hv)zVE_WqwI7ZhJJ#1q zE7~5&=OPd;(J9=olW_Z?yg!0KpyvYfrE$C~5J(;!VI%@Q5K=yd^MiV(h!QRH>D|5 zBTPi#2=q`Jt2E&fEy+u73NC~J2=p9;oTr*esSo*rVdaSrwGTb*$w2xmJ5XAMwz7~t z==pcDeDOPEQSC=ODUdEb5vaY%M<^(JpXg2g(F=j-mCf^!CR)Xxe38Neg!xvQAv zB?Gky)lF}uGx3;)&>2DX1A0$Fpoe71Lm*pIxzds7$j{D4poicU2)}1cB|KF>l2RsW z7iDkqnSTXu3sbU^e4!*h#FO%*Z*sYTJUvv_mc}3e9)gh^?a>k66VVau-_a%OY5<=e zMb{pT#se1u^`8L<4ulIa=BRS@Rxm$cBp=B^?KcpC+A0O%r{9hp8;v(T)P_C;;!S;y z`0G|6IVewkl*R&ObLB56($w6y80o$UWM}fV_He21^h4;6K(bIEzoz;qO>&UTiYNII z$*cMs!AKVafgaT-sf=j*Adp>D9jR7c)j_cK>Y(yU1k#m);zwf=)kzPPO+z3ZNmhE= zmeJUu{7}iJ@RbhAF5Q5egFv#8oYZdge2;chG;R4Q9;%K}CP|{sws~rM;!E=GxBNln z-$tI=N%3l%R(LO1cq;#78$LVQK7Bf*NsNCPPRwc*OfnxHQh-zs&lRf-qM>{%*n#JDgm zve1Yx9_(#s2u7m*sz9iwF=A5l%otCLakq)J$cUd_SR7g%YJi^p@+SY;!ARI=#1{-G zsjKvdtNc|V)M~`%_bY2^@CPH2aKsnm-HiC6!BkLQ6RubVIYUGIyg3RU%hb zFj>{gdl~V$h12R*2Wmo<{y=0!V{Nc53O>D!_`<WOabd)!;=oe-7L?TIG#54e`qE z6K-tqhwADZqiBk=hbQ$a=w3pq!GqveyOc4R<55|#1u^H!^mWMX2Kzqq!mEOH-hPm} z0<9XZ(~czwQwG|}LJL2y6rSPDiE76r(^qYbsdlo|REMR^vCHP#$MaF%R3#dXxE35`Ns9&x zM(U4~m-j?X3sDnaVm1T!+AOc8@)A3Lt>S!xUAEm$-U95EL=v&f?y!?P74^N4t7=$n zxGvnrhOziI(}D`~&s5M0kyRk>)T)@+!I{e6gFJszp}$4BH^4nKLUM1bv*gb`32u85 zsRtCp2el9ryTM}RNPoNSOg#4N=C}2Z1gps5ARy17vSxc+ht6Q*`U;VL3gCSJml)Rg z`>z_72*0!#{EZmYQgkxUCYE{+8K0!BWa8tE66ntyj|_)2G>zOxIR3eKMhr zn-r`Il-C6P<&DuOm|;5h*WtZ75NRM5+)dSys|ogw&0r}pm`{;C`01xnekO74gQZZ7 zEz~k9>s{NhA|YlumC(qxjo(XDD=5!jMRq4;YxteYOm&p6R=E)6DpanLa%ZTVpK`NQ zZZ_qnsN7V_6{(z$aNxIH@WU zY^cVh+z<`aRRkNTmnK$Svd>z}&4f_y)9vH}I6!4NW-^+N^QX>iYB;mTOC?Fum3w}? zrJy2=X=P2+MC|PgRd`iVGUmK^OW#^FQbVwAbrNc#EE%^f-ZErT2HRk`06Nn(DEh833U| zk#HTYoRZnhfzYZFNHD{apdAh)Y8z{!p?Y-76R?_XTXvRQ4v;8=pbD0C(sSoTy?NAh z$@R}P7o=*k!HS-O`gvZX4qL?srh#3GegD5r~C zhqdzHXf+);$i+xvM3gIq6OAM%7|Jjs-O4-*DR$G6BWa8zc9NxVykVK-Kk>xNY(s37 zmCcZqJt*S`WW0td&Z(lforz934v?Oh@Y+ssX-g&fM!SZK?B2)6CMm=F##@8~D;)e& zcHJq7cga}kYQEvb7Lw;DXx=PRo=a4bW}OrNTRWPFXPOl`H? z*Qt{0RpJJTxsJ3SSQ!b|`_&AG0^#_E_uxGgs#(E}ggP!6)gQnvx1uH(i1;f*Rnm~c zag_JQxq-PNao;5?xs@n|;}Jd(i>Vx0bhpB|M`mwR+1q7yyUPASX4SgOjdd3srb$81 zmRYq?bvMdvgjPAv4Nr1gEX+*5#hKXdSiDbV7&Ds@zsqj46VHV0`)}Hxk{TJ^E~WTC z_tZ4|pdoFq^v8C+F=YYuZ^ua6Bi^!;@BJ65>}#XSs{cZjk8P1YLyM$VPyiWY)B?OI@=6*k*%6v=l4?kK@^Hu!r5 z{<}*2^luy-HLW66y(Fu%ZB|DWhkp>bK!VS+!M`f-F)QKL$UNupp@dEcP{Oe}f$mo4 z5^k>0RquDFsuHJ4=qlk-i5MRf(s2|9HX5=Erk1RU)`ZHv z30Ttnnw|)h4C`(F!Lfpc|1mS&VngGY4X(qR0Q&He6E-{RmTbsS=tbL*2FSZE&0@JQ! z+4r&RPrc1WfE9eT&%9xGIu5#zqWhs9e=V-95GfZ+D{T`gm(p?2+Z4S6OF&{5nSoT`*_5J#ZS#YG zYoOqNLp2A@YTOVegX=c9tKf$K{tCw|-!t(ez#X{924@QX4ZvUH=;&c44oe~VFQ$0> zT@vrsW-rF&P6-nIsNg??1lY|3g-onqols-f^uur$*^^7jfN5 z(cPwQSoqR;xXt3A5bhQsTy-opkEJd!g&IRbq0YxBdfY1nC&R=U>)fY45DC;u7Sck+ ztu3VQ6QVoVbu-xkCqQa^*lLUf924LMax_H(0f!V+YmiilW=16Awajns2wwTUiMpJZZTV^}jFpCK>0nElXG3Wctc>o>3 zdW4u5*UrKiq$HH*B*k>xP=eE=HM!wc3bKR>XHZlMNK>Ew_c=p&6 zpV1J7NGa3KV){Iwt`#XW6cc#@vYeO%09n@-5+q0!AnV&gRuW_tAm`@M*_q-uhl;}# z)x$vOVsYLdJ<}WKc~hyo@=is_6~%cE>iNi@D*HP(sQaV1ui44rlhmhyAb74c>{Qih z^y`GU42IpZhB>cd&L_|-X2_a&XC$+YB6O0hVtmAzlAzcm#MRtMLd=b8=k)2{5UoyF z@oKWlB8qSpPXhBiLQErRu`clz@m!u$j4vd%0QExL&R3xCRPoMsC3A$>0kQ5_%k*&! zof!Tt#4RG_8IkfdRv72yo2N#~Q0wH8&;}Ww*T$E4uQt9^D#Rn;{jla^u8Wv!r`fB% zK(CS~HCS)qT<2ElVZ6IYxkjX1jVjLg&=N&1jFJWp!h>sxYK1l%xZ6hn(AGe1m02Uo$_2 zXBP49hFx)*5I=&~4;HVvXui?pjMh->{8fmffd53s$a;oly(VoeSb;P$R?sc9T1;Y!!$Qpc2nlre zAbD)1b`MEnO|c0_fhm0`Q1qwTpwThmxJ#9fA-A9VR#_sQbk6|#_L1BQ z5Nx?67}RuplTb4)MUowoQqnoLF9&zIE=+u1BP~+9 zT5X;xHxQ}Wwo>+qVj7(&iqv!&yKD^m%rmXTsy?mA275`8G~2(@*2scV8K;xR50FG6 zbvU)9Iwio=ov?ArX*RbrBv~+qX#(L)RbM59;%jZRDg~&J_)BCwK*qggOke1%ZChtq zkVeamNiykC5bJ&dOUsbuZn9>}@P@!@+%~|+D}O~e7^%RQDyu{Bi*2S`B*n!<@vOXc zB9#+tGPP%#JfTT@NKW1~B{8fhXric`NplrWxO~WBBfE3}UR{tT>eihLzhUFxNBLY$qL zSB?s2MT>Bjt9j*l!z);j=h+wsg|iA6L97v2))g%4D#EDd1vbX3!WjZawRSGcYGPUI zWTmTMj%V;WSQ<>Etd&N(jLg6bd4I^q3oyCn^FBpB-ka3nxg>K&8DuWPnM zJ@|MMc`U-IB=2ZG%2&*X88Z`<^}=}-D6iCNSw?4;(UmB#q!k=U=0Wb$uo9fZ^L=~@ z_Z0K7Mrnd_p>W;^${VyGOHX6z=|p)w>eP8D5##0(pUg{8o!7uR+1#o*4dJ{MM7L-G z=EnaDBDxtw>3nGmG@nQ0GfisjCiygDx*|=D3g_J*-Km|<((+kaUn1QB($2iHg^vTh z!RK?GsOA{c5>)eqb2q5s+5+Zzhk4#3s$HNunXf_<7x5J!3zBJ;@l22|v=^wU1BLT3 zkUpx-XP!;WvzbUA0BIlIKnm7VAj%-`3d-g7N;y>*&SyZ`qRnHNYdn*Q@^MfO;^z?M z8knYr_k>5SFeWQW#a`ij2}CbyWz18+Jh&hx*fZQ|Bftw@0m92#1#`d4+#kY!@d)-R zT=>2rZ9W+qF~Q`Fe!n^~rjjAl`{Ri(V~L{OgW3!p5|x}F&eP3}M+dpXz-F^!A6z1< zs5Z<20R`E@@g}yO61h{c?CRNA+7|h!M6kEzqF1n&sVqs~EyDR7)H$M+Gxt5reLsv+ zz`IOtP8>dn<-++BF#c{i%L*?n@&he%I|3K}wv{_AzY=qV^PfQdRa?c<53}?m$~MQK z?*si3A5ux-VzR-5g`{xnwT@sD3G`5ZfFk}t18#5;{y-{x*cu`*4f5_N9BvKBo?qmM z2{Uz)<0Z_I!AIck98^czZEei0-5L%qq?LM@ChZOrT2^v6O)EKg8!H(?@7p5u0&Mxy zA7klHLh}KzQo?IS2z>zH{k3YAeiKXI0r+6v-G=80eK6pIv=uD<5|(}$;6wSzHat`4 zLjf*KX1miZdX{D6j8$3)oh(R_JP&YYUI35N50Ov9Nn<6yiXO6*w46v8P3IX!R4klL zmJ{75w@!jREiEej>r7lB^cHPx_F2Bb9~JsS2ynXAz%pKEnH|h6ND57bvaSg-o=Cli z=RvN=^3?KAurdkDrY3(PKU`IXWtd#2&~m`JO>rvi_ zv!!B|siJc?Jd>_;$x6+5T5}N}$-!P(XOqyc0qHiAG~<1=;ijA$G_j@uH zv5fPZ1-}P8#$otcz~}Lke0(l1P3+?Nc%jFDezS$X5$JnxTvo)LHcnrm-vON4agQjY zlx56El_lI=yp_*YLUk1SPGH=ntznrvSmsO62W>3XXlyQ`VU9;(=ErlZ)vlY}A)!5F z+|A&_tkulDvfyMHcc-R#ssMK;6YYrONAq5crfZvPCmhvT?2x`eEQ4(i&N2 z0n02z-4l6Q$yR=YW&4zBp&tRpx7G>(hbF>tgzqY9<~J#nQlVqlum8ZbYgxzJS;tq% z-&%U9FAM2YE%daFC40 z%Xk7Yc{!)b>i%*gR10FgOtM(1C<7|7oHhsZ7(Vh6#)yklbCavTz_bAhm)X*aS? zjCC5>OrI8#wvg~fYmUyi+fLqNCwJM&dllyWOnZ%G*wAMoudH-@{LyjP6(R5jzU2{qrD;F7U}3es`> z%e1|%RwPQT^fSroFlaYgiP4QY8osBBf&uK z@!9Jw$AiN4JW&3~v>RB*_gKe$UV{&j$BHx)CoQ)eR|^-GqOO+}vs@AYgY-B^`$i7N zXg-Am|8q_N$*GilGp8KMX_R~`rvl08%4gC|@4)FM`3&v?Nu@f=B@&d<1+ECwLICiR zBw_1?3tx3yUnvpNA?!jD*40+n<-&!9rt1jq+p$jTS*Hi!D!jpL33Oo+`f~I7w$pWTf#PG@O{~*o)@eH04VO1? zcHOq!bm5*3%xQ|*&C`PwZ_D@{ z;_wmO4NXi5dv;?tK^u-^36f0AF(7$Y##j;|{UH(lMO_zdMLbaG{gR0>tAJpij6as~ zej@%jaRIRv^PD>I0ofv&4Z(iCep+!aseRz^G9cD}HpJe=tjQ>HDpIhq{j4|8E18$_s_3IKf zX5t4ymJekvq7_OIA1;Jm38N)(&%`xep)V&=Or3<_7y8m<1pAh5CT{5peF;X?Je&0# z^9Wy`Z=K=l*3VPGX|B*`Cv%!^RxnH818q`csq3Se_D%Xsd<7s`rVD*aGHR(=JXz?z zoTagop`B^Rqp>zVdR6DPU*SSDAa&IUP9 z@?F>)&=~my?F!<2vAku$U!hADxU#{oFE+tD&69vSb3ol7XYJw^q7<%FYtQ=2>lvFE`w9TMDUz;IE%hBG1K&|#8+AD<;|H1j+Ct9wMrPH8 ztqgpF0rIB``kBmrq_TgJ+4ofTeVKhjW&bR*uhVex!wKgO*T;#uBisJjN%m<>`<`Xb zl`*bMFzv_V=8iuJ{e`3smwlN;#)u0-Oa+J+65-$59c!Jt66VT&Od>xhV{DK>xKzf= zi2SGa###@)8R3}5zM+@>u+8ovNqmNk12QfrMn~zkv^~@c7q$g7%DgW0SCiGSog#aa zq^^*0m5f&qr=RI+vCRoQ{tPzBJl>MX)iPcs;~FCTB{68bPJ;Zdmq-iO^S0<$*vZS` z^R5h%(3LJ+o@DM@2;?Txcclt07lx2z1iLR}ZzkML@MU|@&c4_jv|ae9i|zzAo6H0h zIU@A0lR2Gd+UT&*zf3OPXt`MS23z2BP1L^${flJO^UdPF3jNdM;tR~;Pv|hjo(-}u zRE*c#jMo8GxOKbWB89Y8CC*U^HRok-RV7!#`B^r8V=2d4zLmz*IKSDvB*zz-gZBN{ z&C+09ZH~^Dn&a=fp@h>LI-uss&rdi?LCaR);& z;n@=Z4ileM1D|(bte)tMyi)v5-OC*FTIKf3+`#1D@OW9uOR_ZiC(4+AP{!R1zih=@ zXB^U)qVox;PisO{YA{Zud_3cOC5r+deflge_cGC(z@JO_Wr(1Z_?GZbW8$d9Z|AB8 zOU*nnsPM#~QVFsJaBgW^(9*Wx5JYUgGRKb_a56R4{ObjS1C7xzZgnUAumL{hGW}Oc zJ!opMrWQYaUjgGrn!L=#C8eu3egxk3uOSR>^UH4LGEC%x_K=gB1og?Ed^6V^lOVr6 zg5!T`&0Nc+kZqdR-9vI|=ir37ArX8faTS)iVa6-t27lDcJbeMoFAc82&mIcBWm!u{ zt-RtdWq-J(*N^)j>kEka3--dNHoo4nCgqg%*Nwhx;w5ivhE2^MpBL^No^uUbcEBAP zf12lu@Q0maF;z|Bm}eY6uf1TB;k;0N6s$QG?UG@i`pLAf| zdvpALK+NCH6)tvfdAj=U)ZyAmJI;^)^QslGSdzaMo_Tar$+(RCOBQyU?2ddJy$Vvu zpWGGpeArdI`OpOoKRvhivWaD*UjW(s#P7!oH+OV=bN8_K|FO5?tg0t3oK_Qy(JxpE zJ)hm&Ji79%Po`db$*s3tanW8B&kWQTUa~cJ>FkoqeP0dPe_!`szlEO`Ou>y${Ccl& z`^fC+hpvxb6zKPiUin1sM*P(Y>VJic(}#8Wb>ylyu2}x`_gw=YzX?ud!D!(vJ9?)6 z@r~ziO7YHlZcERSQL)(ZJ)!XQ_18{V6+bfN?NfGczTn4S#-KW@dleRZUAyh0NxK%l zxGZf$`QWr^u~@4%FWlf?cKM)}AARF}lsuU>LS$>JFck8K_w zi?uhn6&}7ZGVp@~^G_MuA#KmQpL{0B0{Ei>g$0lAoP1-yi*~&FKerv6+j!^*xj~?z zI$B;+nDbrtj8FDeopa#eydN8$+4x8-*1CHY&bdF(a?9S|#y5X?=h7FNUxZa#|0=3* f*_gVuTO4cle{|j6o4-Bq>Tmc8#XRHLq~8Ar9u?zp literal 0 HcmV?d00001 diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.cmx b/helm/ocaml/grafite_parser/matitaDisambiguator.cmx new file mode 100644 index 0000000000000000000000000000000000000000..1f8b72b6c8f2d6fb0dcb31cf5f10929e82a18696 GIT binary patch literal 2318 zcma)72~ZPP7~WuX0GWDDZLx#g2*dG`a2NsI2nkU^so)eXxNMRQtRz|3-Eeq-2QtE- zgkit~g-3BHTE}MSj9Oa(Ydvad#c|qtS4&%{;)SKPtzzFMj14N5Oy0ho_ultk-}k?b zBaH@$TrOV$fV{M}r5(eZZ(x`x6T`-@z%cPZh zLjOdnkTzujMaq=)$kkOhQua1^4&MB9Hrh#MX%nvp?VHYb7LM~M-Wj!RUipQJehB?i znHaxVbj-UGe`T(|31NU*S;!k`4UnI3`fFY3e5bsaSW)GjdjrVY0<&IE zu|WB|{#(_+v@1W)>|K8;nIO=PI;n`uGk}$@l^xj!CdjavEt{=RYqB5=N~YL+lB4q} z4&*)Fs*IlGU!L~1%9VY<*Ptluuvv#);w$<~xj#>KZ=07AbsE8zvvd+^BD0XYis?@G z4@fWn)2%JgAK$Xj0HIGDtpyW%8ZA+}f?MhxF~9r0iTk+D7G+|e%{iGl|jV}EfHptN?miOvT{ zqL(aA`v^ae(KX8sw)bsB5iQlM27K}3&VbswzMk6`FNv$i-9?2@;aQ3_g58O-BCWz% zxk|ZmaoV$r7zke_7jUI2JKx;|^}TW0Qm zD9C{1vU!aGcn!Eux^+#zwzn^JkUO#I2!tVO%3vf|Dht()Edt3Olbuc7Lot@yAEuwS zoIzC$L1`>ucqCWGl+1$+xoKUcQ{m0)JG&bn^mYv)#oFthU6+~^-SO;w?Uwszk9sz; zg4bd3O^}wfO(q*8o9pY<%cO_=M+%7zN|a_wHim^OtzO$D9mgGu{(XtZZ|;`qyBBHO zS4|09^-9uQ+iH6EG~5f{UEWd36=MR2A1o)udf{f%$Dy%fz{Vq}SrrsEOmTY7373u+t?%i+cVQ9Ze7%#S_|W zhT$l}%+eg8B@G4*sm&oIl5mB>0-+V-y!1HUx(`>t)|!Q|)ndiPdlfhiEn-*n>~x75 zi*a-@P;9QF`N(1OW(V_&ka_Vmn{79n?XXd88yOSxV#q+M5CZFTk-Q%EQZOK57#KP# zQ1{-iH5t4fq7#}%T5GK*}M07a?&|=ZHTaq{`Mm{KJ3k=kZij*yZpdwJms2s0%c%e zv?Om6I3baN1w#EHDt&-}bi5=9;$@cQQBi8aU8jrx{~QF$c^Wy`RL6iLI%QBxX_j&>}&vOph=G65Qie{tJ!9Bms2b!a4f>kp{^3AR`Mak>!pl|$mAuPdwNa{nG@}HMKZn*0a8%aX1Hrr_TL#w`M z_@Lp9hL@lPPg~IfN6ltL5K<6{4Ji;UHqhujF# 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/ocaml/grafite_parser/matitaDisambiguator.mli b/helm/ocaml/grafite_parser/matitaDisambiguator.mli new file mode 100644 index 000000000..b7c85f6af --- /dev/null +++ b/helm/ocaml/grafite_parser/matitaDisambiguator.mli @@ -0,0 +1,51 @@ +(* 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/ + *) + +(** 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/ocaml/grafite_parser/matitaDisambiguator.o b/helm/ocaml/grafite_parser/matitaDisambiguator.o new file mode 100644 index 0000000000000000000000000000000000000000..5358eadfa47ec055d5ec3d7769fa5ddfd8ef3f1a GIT binary patch literal 11092 zcmb_i4{%(?dEb+s;cVT+2Pnyb?O2$@$N_AfWNcGRkSvQHws8zGi3A=$PSVM`_M|(X zPOjC`At1Z)%j2ekNhb~iZH!3bX=#TPm&mb8Y-}n*lMJ3ZjXmuI_fIA!b~+@KU=lU% z@3;HC)6*e6(RhkGKzn-<-I3@#09SxL6IJx123;@Y&i?;%&3|Tc|HJTjR|W z??#mxXN4MXwyFWH?ihC3!%i|XeB3&AmTJ!(F1<*h(s%fK?A)9Y|Kt3_zFJf}VHqgw zA83IYNLdhQa0?Ol-l)4i>^@*=dyV$-(t*WPTsnLM!Fky^<=$_(^M-#DDqiVc0~oAv zJLt{7(LcA{VoO-6M%<1lo19-s|Kamdw9nmj06}y%#KX?oxaEGva;s5@4F4J}f5}lc z$JN;s3rF1r9M%opdTOv$e2DmbnEU8U&{S%-##<*;7=kTfr+U2ALZxz{TRWixhr!P6 z8gX8AucyL4)uBE%a`6^2N7osfPdLZWG3q9xfLh((2qWUd$D_xl#^dZ?vAfU8xw{?K zY>2CAt-b8h)|QhZI>pbIp;r8iD76oBrkrY+sN81DX|c>^-g*Z>5IUN;|y#cK;~m4%E7z!9pl6T)%#A{jQHe?{*<|KI+bF5VJ{ zf!g!osq4#KKy~gs zZ-3$DQsdT~i-_34W<*My^6v|UMUzSCE~tYJC*~xrY2xy-Ot0DB%>Go2ImLJcyHFSl z*}~SO&fPgB{{ErnKKe7*FgaX#4b)by0i>BW_2voKGi7oA`J@IcZj+_h^%>pq<}jhO zDLTGpLb0_;)^-#hj`{l}-sQ_5Iw^q*v_U;oG%*7!r~ z6s++zCg^+LVxu`)oU35|K5*<#$x)&?ujfAc&nTPue;0>sdH#QcT@JHHNtbDqj5s@^ zrA;vmrsXi_9NFSggaOGQ7k1V~01;tEU`xW|O|Wyj|b^Ki+ozHr_pu&%@{Eb7;KN zSo%2M48x1@sPj-fhO?;-ZME+0%V`l$DoD{o7g8>y%-CBX!q*|R#)gm2*PDRveZg{$ z@{MVX6XN`%?&2JiY49(@!pA3Nk zBXQ7Erw`XL?Q>ef01GJu2s%Ud^uYdqEzud%Ka6wiTPu~=?&ap{|1&!6OY3)#-rU^r!jv(x+EZ6qtgV$*&cE5 zwt9&WSa8@J{3w(|fY6NzQ-_kWC0)ve+Xw{7($n4>K%wTHReu(G-rmCgbb zu{%f0wX1b)9cmAq$B(lB??md*8C~ScFC}B#-q6j}P0rPhK3ykI33mbISYHo3bW(Ta zj&kT#UBvOAzRhj*;B&0xhCFt;IGiX>QM|p3-h}FX{L#*gG7ZNb!_Vk)mKa{$ z;2ax^gYaF(IXZ?^6zBB|yZ*vqN@9z(=4dcG+xkeUwU#5o4JS6rn2kMzpV8GUWm#%w zX$wm+mNu|N_2!L4skJD72+z9_qlDJ+@%R;nmO1vti~jaXUfG{}zLwVxD}BIvy5~;U z=9inPEVjN^VN03&`b{7Qx-$c*zRt|H!BjDA7ke}P+f-LOu8_$tgmM#*WXqs5!QaP`2o}21h8kT)LGY*W2SclC1plQ*sanOigot`amwC5f;k_$@e3`8# zbe&SC(7#U0)v90WGAG)|MWI2<>Uzk|R_ITi)#_`yjNswfaJBW^>wJ7 z58J8zIDTs3g=Y;+Q9sailQ!01j8nP}TLm2U{QfSSq@Rx99fFI2#U%h2yxstHglx)oP^a9-Ph8-gwgwm) zraFPeg27&|R7hu+7SlV6YAH+IsbWek?Hm|D?+^Cy6_BHF7Wg#d?+-Bd-b0`G%)=jT z^q%>Pl!{)iV7uwh`Qbb-5zYwl8H28;*eH)zydK=I?%8&W@9+aQ*@llkY^Krf^ z@~k#bwK|Q$s~&~^cThg*<5$4ZGd_MZ_<0|{3;cqQr@{57kgls%kATPUXP#>HG|D{S zJ0NOaLY+VfrTy!c3cKcl>l*I?txQy351Z}K)G;dlEu^>u&~`B453E83k3{$vIJ z2KeW7Z`1$#744@h_)oxJ_sM?*8&p*CjpHxlh9wW}YOdhz6+BnLzX1NcFCP0V+7Ey; z2l#NjA6B&gw1U4~!9&=y&d9#S{)?nceYCd;JQ^W0`tPl1-&(YEHnm$voRo?jR8J12Kd0&ExR+l zEz>`9e7bVo>0lY%*X|lD6ovv~;`^9L+qur)vm2M22{SzdqB5mtFd2ltc&rRhMr$iZ?0o(XnWDx2+0b^X4bNCX7R*AIRU_ zGz6rz?oly9gG`8IOu%?OgZ*|>B48zIfrfyDr9k7VO9(VInSIVq<@4E~4A#Rn$yyo0 zrNlNnUo4nKXJ|Ilmnq6B#6;NJx@KO^#ln!CPYn#%iIqlWYc5^rTH9&5Yg+YXRq37m zcFO=Vv}pIFGTFg`Q8Vo+Y-Z26U_u*^C|X!H-DEo3XBV&+;>&c%jN6yPHX&unn}7{N zD{C+#Z-5rt?n~wERRQY(H%s17n6_NkMm?-QT((WEjSUTE87JFz7PFa7+s+qqJ(+CU zUKy}c=#4ww->sES8!Ns22TJr5QhnH7I#u&jsHmLeDIG4~6jIz6eM=8p(fGsg*?7+9r4p z5q5M4+C=o8oz9RS+MD+V65&aGl(eFEguK?NapQQa1c@p=K z!Y>HF0pDiqzeX@cguOjPjMpz%Bx1ZjAwvFfBF6i&;L|{kcY+-KP7A(4M89{4t;jDT z^jF~%@Cm`ag3kb}&~HCE`W=w^Bdmv?uL+(MoQ3ao#^n>hsy3z8k;Bh> z$k!{?P7ePb6zn0wk6mnsz9-2czmFX9`^h2yyx@yO$e(08Re}#A_?pleEJ1F>);A?_E0@AKu5NVg- z$MC&db+=NBfgJxvBJ|uQyhZpu!apZ`i||h2+l2QC|6{@3f`2CXwBR#DjJIF-UkiUh z_?Ym&7kpXpw6y&(4pD6UkI{CacmNxqAGvAOpQ)!}?2zroyla@{{mzQo*n zhCXTTJ3}|ZF4o^