From: Andrea Asperti Date: Fri, 5 Nov 2010 10:12:15 +0000 (+0000) Subject: - lexicon merged into ng_disambiguation X-Git-Tag: make_still_working~2720 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=791d52ba005e434be27cca1f8059d9f28da0183b;p=helm.git - lexicon merged into ng_disambiguation --- diff --git a/matita/components/METAS/meta.helm-grafite_parser.src b/matita/components/METAS/meta.helm-grafite_parser.src index bcde338d3..91bfdab4c 100644 --- a/matita/components/METAS/meta.helm-grafite_parser.src +++ b/matita/components/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation helm-ng_library" +requires="helm-grafite ulex08 helm-ng_disambiguation helm-ng_library helm-content_pres" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/matita/components/METAS/meta.helm-lexicon.src b/matita/components/METAS/meta.helm-lexicon.src deleted file mode 100644 index 0842312ec..000000000 --- a/matita/components/METAS/meta.helm-lexicon.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-content_pres helm-ng_library camlp5.gramlib" -version="0.0.1" -archive(byte)="lexicon.cma" -archive(native)="lexicon.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_cic_content.src b/matita/components/METAS/meta.helm-ng_cic_content.src index a2c08e135..1b45e784a 100644 --- a/matita/components/METAS/meta.helm-ng_cic_content.src +++ b/matita/components/METAS/meta.helm-ng_cic_content.src @@ -1,4 +1,4 @@ -requires="helm-library helm-content helm-ng_refiner" +requires="helm-library helm-ng_library helm-grafite helm-content helm-ng_refiner" version="0.0.1" archive(byte)="ng_cic_content.cma" archive(native)="ng_cic_content.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_library.src b/matita/components/METAS/meta.helm-ng_library.src index ebe2e340e..a40447075 100644 --- a/matita/components/METAS/meta.helm-ng_library.src +++ b/matita/components/METAS/meta.helm-ng_library.src @@ -1,4 +1,4 @@ -requires="helm-ng_refiner helm-ng_cic_content helm-ng_disambiguation helm-ng_paramodulation" +requires="helm-ng_refiner helm-registry helm-library" version="0.0.1" archive(byte)="ng_library.cma" archive(native)="ng_library.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_tactics.src b/matita/components/METAS/meta.helm-ng_tactics.src index 4a8eca4b1..f5d3a660d 100644 --- a/matita/components/METAS/meta.helm-ng_tactics.src +++ b/matita/components/METAS/meta.helm-ng_tactics.src @@ -1,4 +1,4 @@ -requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-ng_paramodulation" +requires="helm-ng_disambiguation helm-grafite_parser helm-ng_paramodulation" version="0.0.1" archive(byte)="ng_tactics.cma" archive(native)="ng_tactics.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index b1485c5cf..61ce8a364 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -18,13 +18,12 @@ MODULES = \ content \ grafite \ ng_refiner \ + ng_library \ ng_cic_content \ disambiguation \ ng_disambiguation \ ng_paramodulation \ - ng_library \ content_pres \ - lexicon \ grafite_parser \ ng_tactics \ grafite_engine \ diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index a964a1fca..34a327264 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,8 +1,7 @@ content.cmi: -notationUtil.cmi: -notationEnv.cmi: -notationPp.cmi: -interpretations.cmi: notationPt.cmx +notationUtil.cmi: notationPt.cmx +notationEnv.cmi: notationPt.cmx +notationPp.cmi: notationPt.cmx notationEnv.cmi notationPt.cmo: notationPt.cmx: content.cmo: content.cmi @@ -13,5 +12,3 @@ notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi -interpretations.cmo: notationUtil.cmi notationPt.cmx interpretations.cmi -interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 8d74439eb..7b0acd5dc 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -7,8 +7,8 @@ content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi -content2pres.cmi: cicNotationPres.cmi -sequent2pres.cmi: cicNotationPres.cmi +content2pres.cmi: termContentPres.cmi cicNotationPres.cmi +sequent2pres.cmi: termContentPres.cmi cicNotationPres.cmi renderingAttrs.cmo: renderingAttrs.cmi renderingAttrs.cmx: renderingAttrs.cmi cicNotationLexer.cmo: cicNotationLexer.cmi diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index dcc6377a0..f6168c1bc 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -6,7 +6,6 @@ hLog.cmi: trie.cmi: discrimination_tree.cmi: hTopoSort.cmi: -refCounter.cmi: graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi @@ -24,7 +23,5 @@ discrimination_tree.cmo: trie.cmi discrimination_tree.cmi discrimination_tree.cmx: trie.cmx discrimination_tree.cmi hTopoSort.cmo: hTopoSort.cmi hTopoSort.cmx: hTopoSort.cmi -refCounter.cmo: refCounter.cmi -refCounter.cmx: refCounter.cmi graphvizPp.cmo: graphvizPp.cmi graphvizPp.cmx: graphvizPp.cmi diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index e01d5bbfa..3a2590d84 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,8 +1,5 @@ grafiteAstPp.cmi: grafiteAst.cmx -grafiteMarshal.cmi: grafiteAst.cmx grafiteAst.cmo: grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi -grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi -grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 10236823a..d04ec9d2c 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,14 +1,11 @@ grafiteTypes.cmi: -grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi grafiteTypes.cmx: grafiteTypes.cmi -grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi -grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi -grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi grafiteSync.cmi \ +grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \ grafiteEngine.cmi -grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx grafiteSync.cmx \ +grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \ grafiteEngine.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e45f9bef8..b8b65a8c0 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,12 +1,9 @@ dependenciesParser.cmi: grafiteParser.cmi: -grafiteDisambiguate.cmi: print_grammar.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi print_grammar.cmx: print_grammar.cmi diff --git a/matita/components/lexicon/.depend b/matita/components/lexicon/.depend deleted file mode 100644 index 84cbde3e1..000000000 --- a/matita/components/lexicon/.depend +++ /dev/null @@ -1,6 +0,0 @@ -grafiteDisambiguate.cmi: -lexiconSync.cmi: grafiteDisambiguate.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi -lexiconSync.cmo: grafiteDisambiguate.cmi lexiconSync.cmi -lexiconSync.cmx: grafiteDisambiguate.cmx lexiconSync.cmi diff --git a/matita/components/lexicon/.depend.opt b/matita/components/lexicon/.depend.opt deleted file mode 100644 index 0fee4b18e..000000000 --- a/matita/components/lexicon/.depend.opt +++ /dev/null @@ -1,21 +0,0 @@ -lexiconAstPp.cmi: lexiconAst.cmx -lexiconMarshal.cmi: lexiconAst.cmx -cicNotation.cmi: lexiconAst.cmx -lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi -lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx -lexiconAst.cmo: -lexiconAst.cmx: -lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi -lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi -lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi -lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi -cicNotation.cmo: lexiconAst.cmx cicNotation.cmi -cicNotation.cmx: lexiconAst.cmx cicNotation.cmi -lexiconEngine.cmo: lexiconMarshal.cmi lexiconAstPp.cmi lexiconAst.cmx \ - cicNotation.cmi lexiconEngine.cmi -lexiconEngine.cmx: lexiconMarshal.cmx lexiconAstPp.cmx lexiconAst.cmx \ - cicNotation.cmx lexiconEngine.cmi -lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmx cicNotation.cmi \ - lexiconSync.cmi -lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \ - lexiconSync.cmi diff --git a/matita/components/lexicon/Makefile b/matita/components/lexicon/Makefile deleted file mode 100644 index 273aade43..000000000 --- a/matita/components/lexicon/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -PACKAGE = lexicon -PREDICATES = - -INTERFACE_FILES = \ - grafiteDisambiguate.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml deleted file mode 100644 index 88915c893..000000000 --- a/matita/components/lexicon/grafiteDisambiguate.ml +++ /dev/null @@ -1,332 +0,0 @@ -(* - * - * 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/ - *) - -(* $Id$ *) - -type db = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -} - -let initial_status = { - aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty; - new_aliases = [] -} - -class type g_status = - object - inherit Interpretations.g_status - method disambiguate_db: db - end - -class status = - object (self) - inherit Interpretations.status - val disambiguate_db = initial_status - method disambiguate_db = disambiguate_db - method set_disambiguate_db v = {< disambiguate_db = v >} - method set_disambiguate_status - : 'status. #g_status as 'status -> 'self - = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) - end - -let eval_with_new_aliases status f = - let status = - status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in - let res = f status in - let new_aliases = status#disambiguate_db.new_aliases in - new_aliases,res -;; - -let dump_aliases out msg status = - out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); - DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) - status#disambiguate_db.aliases - -let set_proof_aliases status ~implicit_aliases mode new_aliases = - if mode = GrafiteAst.WithoutPreferences then - status - else - (* MATITA 1.0 - let new_commands = - List.map - (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases - in *) - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status#disambiguate_db.aliases new_aliases in - let multi_aliases = - List.fold_left (fun acc (d,c) -> - DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias - d c acc) - status#disambiguate_db.multi_aliases new_aliases - in - let new_status = - {multi_aliases = multi_aliases ; - aliases = aliases; - new_aliases = - (if implicit_aliases then new_aliases else []) @ - status#disambiguate_db.new_aliases} - in - status#set_disambiguate_db new_status - -exception BaseUriNotSetYet - -let singleton msg = function - | [x], _ -> x - | l, _ -> - let debug = - Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" - msg (List.length l) - in - prerr_endline debug; assert false - -let __Implicit = "__Implicit__" -let __Closed_Implicit = "__Closed_Implicit__" - -let ncic_mk_choice status = function - | GrafiteAst.Symbol_alias (name, _, dsc) -> - if name = __Implicit then - dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) - else if name = __Closed_Implicit then - dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) - else - DisambiguateChoices.lookup_symbol_by_dsc status - ~mk_implicit:(function - | true -> NCic.Implicit `Closed - | false -> NCic.Implicit `Term) - ~mk_appl:(function - (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) - ~term_of_nref:(fun nref -> NCic.Const nref) - name dsc - | GrafiteAst.Number_alias (_, dsc) -> - let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in - desc, `Num_interp - (fun num -> match f with `Num_interp f -> f num | _ -> assert false) - | GrafiteAst.Ident_alias (name, uri) -> - uri, `Sym_interp - (fun l->assert(l = []); - let nref = NReference.reference_of_string uri in - NCic.Const nref) -;; - - -let mk_implicit b = - match b with - | false -> - GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") - | true -> - GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") -;; - -let nlookup_in_library - interactive_user_uri_choice input_or_locate_uri item -= - match item with - | DisambiguateTypes.Id id -> - (try - let references = NCicLibrary.resolve id in - List.map - (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) - ) references - with - NCicEnvironment.ObjectNotFound _ -> []) - | _ -> [] -;; - -let fix_instance item l = - match item with - DisambiguateTypes.Symbol (_,n) -> - List.map - (function - GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) - | _ -> assert false - ) l - | DisambiguateTypes.Num n -> - List.map - (function - GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d) - | _ -> assert false - ) l - | DisambiguateTypes.Id _ -> l -;; - - -let disambiguate_nterm estatus expty context metasenv subst thing -= - let diff, metasenv, subst, cic = - singleton "first" - (NCicDisambiguate.disambiguate_term - ~rdb:estatus - ~aliases:estatus#disambiguate_db.aliases - ~expty - ~universe:(Some estatus#disambiguate_db.multi_aliases) - ~lookup_in_library:nlookup_in_library - ~mk_choice:(ncic_mk_choice estatus) - ~mk_implicit ~fix_instance - ~description_of_alias:GrafiteAst.description_of_alias - ~context ~metasenv ~subst thing) - in - let estatus = - set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences - diff - in - metasenv, subst, estatus, cic -;; - - -type pattern = - NotationPt.term Disambiguate.disambiguator_input option * - (string * NCic.term) list * NCic.term option - -let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = - let interp path = NCicDisambiguate.disambiguate_path path in - let goal_path = HExtlib.map_option 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 x -> Some (text,prefix_len,x) - in - (wanted, hyp_paths, goal_path) -;; - -let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function - | `Unfold (Some t) -> assert false (* MATITA 1.0 *) - | `Normalize - | `Simpl - | `Unfold None - | `Whd as kind -> kind -;; - -let disambiguate_auto_params - disambiguate_term metasenv context (oterms, params) -= - match oterms with - | None -> metasenv, (None, params) - | Some terms -> - let metasenv, terms = - List.fold_right - (fun t (metasenv, terms) -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,t::terms) terms (metasenv, []) - in - metasenv, (Some terms, params) -;; - -let disambiguate_just disambiguate_term context metasenv = - function - `Term t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv, `Term t - | `Auto params -> - let metasenv,params = disambiguate_auto_params disambiguate_term metasenv - context params - in - metasenv, `Auto params -;; - -let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = - let uri = - let baseuri = - match baseuri with Some x -> x | None -> raise BaseUriNotSetYet - in - let name = - match obj with - | NotationPt.Inductive (_,(name,_,_,_)::_) - | NotationPt.Record (_,name,_,_) -> name ^ ".ind" - | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" - | NotationPt.Inductive _ -> assert false - in - NUri.uri_of_string (baseuri ^ "/" ^ name) - in - let diff, _, _, cic = - singleton "third" - (NCicDisambiguate.disambiguate_obj - ~lookup_in_library:nlookup_in_library - ~description_of_alias:GrafiteAst.description_of_alias - ~mk_choice:(ncic_mk_choice estatus) - ~mk_implicit ~fix_instance - ~uri - ~rdb:estatus - ~aliases:estatus#disambiguate_db.aliases - ~universe:(Some estatus#disambiguate_db.multi_aliases) - (text,prefix_len,obj)) in - let estatus = - set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences - diff - in - estatus, cic -;; - -let disambiguate_cic_appl_pattern status args = - let rec disambiguate = - function - NotationPt.ApplPattern l -> - NotationPt.ApplPattern (List.map disambiguate l) - | NotationPt.VarPattern id - when not - (List.exists - (function (NotationPt.IdentArg (_,id')) -> id'=id) args) - -> - let item = DisambiguateTypes.Id id in - begin - try - match - DisambiguateTypes.Environment.find item - status#disambiguate_db.aliases - with - GrafiteAst.Ident_alias (_, uri) -> - NotationPt.NRefPattern (NReference.reference_of_string uri) - | _ -> assert false - with Not_found -> - prerr_endline - ("LexiconEngine.eval_command: domain item not found: " ^ - (DisambiguateTypes.string_of_domain_item item)); - dump_aliases prerr_endline "" status; - raise - (Failure - ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) - end - | p -> p - in - disambiguate -;; - -let add_aliases_for_objs status = - List.fold_left - (fun status nref -> - let references = NCicLibrary.aliases_of nref in - let new_env = - List.map - (fun u -> - let name = NCicPp.r2s true u in - DisambiguateTypes.Id name, - GrafiteAst.Ident_alias (name,NReference.string_of_reference u) - ) references - in - set_proof_aliases status ~implicit_aliases:false - GrafiteAst.WithPreferences new_env - ) status diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli deleted file mode 100644 index 15dc42ae4..000000000 --- a/matita/components/lexicon/grafiteDisambiguate.mli +++ /dev/null @@ -1,80 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -type db - -class type g_status = - object - inherit Interpretations.g_status - method disambiguate_db: db - end - -class status : - object ('self) - inherit g_status - inherit Interpretations.status - method set_disambiguate_db: db -> 'self - method set_disambiguate_status: #g_status -> 'self - end - -val eval_with_new_aliases: - #status as 'status -> ('status -> 'a) -> - (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a - -val set_proof_aliases: - #status as 'status -> - implicit_aliases:bool -> (* implicit ones are made explicit *) - GrafiteAst.inclusion_mode -> - (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status - -val add_aliases_for_objs: #status as 'status -> NUri.uri list -> 'status - -(* args: print function, message (may be empty), status *) -val dump_aliases: (string -> unit) -> string -> #status -> unit - -exception BaseUriNotSetYet - -val disambiguate_nterm : - #status as 'status -> - NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution -> - NotationPt.term Disambiguate.disambiguator_input -> - NCic.metasenv * NCic.substitution * 'status * NCic.term - -val disambiguate_nobj : - #status as 'status -> ?baseuri:string -> - (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> - 'status * NCic.obj - -type pattern = - NotationPt.term Disambiguate.disambiguator_input option * - (string * NCic.term) list * NCic.term option - -val disambiguate_npattern: - GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern - -val disambiguate_cic_appl_pattern: - #status -> - NotationPt.argument_pattern list -> - NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index 1316c8eab..fd1b831b9 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,6 +1,6 @@ ncic2astMatcher.cmi: -nTermCicContent.cmi: +interpretations.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi -nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi -nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi +interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend index a520f2c39..df0847b17 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -1,7 +1,14 @@ +disambiguateChoices.cmi: nCicDisambiguate.cmi: +nnumber_notation.cmi: +grafiteDisambiguate.cmi: disambiguateChoices.cmo: disambiguateChoices.cmi disambiguateChoices.cmx: disambiguateChoices.cmi nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi -nnumber_notation.cmo: disambiguateChoices.cmi -nnumber_notation.cmx: disambiguateChoices.cmx +nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi +nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi +grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ + grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ + grafiteDisambiguate.cmi diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index f2694c199..df0847b17 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,5 +1,14 @@ +disambiguateChoices.cmi: nCicDisambiguate.cmi: +nnumber_notation.cmi: +grafiteDisambiguate.cmi: +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi -nnumber_notation.cmo: -nnumber_notation.cmx: +nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi +nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi +grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ + grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ + grafiteDisambiguate.cmi diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile index ad6a6de80..8c564325e 100644 --- a/matita/components/ng_disambiguation/Makefile +++ b/matita/components/ng_disambiguation/Makefile @@ -1,45 +1,15 @@ PACKAGE = ng_disambiguation PREDICATES = -INTERFACE_FILES = nCicDisambiguate.mli +INTERFACE_FILES = \ + disambiguateChoices.mli \ + nCicDisambiguate.mli \ + nnumber_notation.mli \ + grafiteDisambiguate.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) -IMPLEMENTATION_FILES = \ - disambiguateChoices.ml \ - $(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae - -all: -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - -depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) - ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot - tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot - cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot . - echo "NCicLibrary [ style=dashed ];" >> depend.dot - echo "NCicPp [ style=dashed ];" >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot . - -depend.png depend.eps: depend.dot - dot -Tpng > depend.png < depend.dot - dot -Tps > depend.eps < depend.dot include ../../Makefile.defs include ../Makefile.common - -OCAMLARCHIVEOPTIONS += -linkall diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml new file mode 100644 index 000000000..88915c893 --- /dev/null +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -0,0 +1,332 @@ +(* + * + * 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/ + *) + +(* $Id$ *) + +type db = { + aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; + new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list +} + +let initial_status = { + aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; + new_aliases = [] +} + +class type g_status = + object + inherit Interpretations.g_status + method disambiguate_db: db + end + +class status = + object (self) + inherit Interpretations.status + val disambiguate_db = initial_status + method disambiguate_db = disambiguate_db + method set_disambiguate_db v = {< disambiguate_db = v >} + method set_disambiguate_status + : 'status. #g_status as 'status -> 'self + = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) + end + +let eval_with_new_aliases status f = + let status = + status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in + let res = f status in + let new_aliases = status#disambiguate_db.new_aliases in + new_aliases,res +;; + +let dump_aliases out msg status = + out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); + DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) + status#disambiguate_db.aliases + +let set_proof_aliases status ~implicit_aliases mode new_aliases = + if mode = GrafiteAst.WithoutPreferences then + status + else + (* MATITA 1.0 + let new_commands = + List.map + (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases + in *) + let aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) + status#disambiguate_db.aliases new_aliases in + let multi_aliases = + List.fold_left (fun acc (d,c) -> + DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias + d c acc) + status#disambiguate_db.multi_aliases new_aliases + in + let new_status = + {multi_aliases = multi_aliases ; + aliases = aliases; + new_aliases = + (if implicit_aliases then new_aliases else []) @ + status#disambiguate_db.new_aliases} + in + status#set_disambiguate_db new_status + +exception BaseUriNotSetYet + +let singleton msg = function + | [x], _ -> x + | l, _ -> + let debug = + Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" + msg (List.length l) + in + prerr_endline debug; assert false + +let __Implicit = "__Implicit__" +let __Closed_Implicit = "__Closed_Implicit__" + +let ncic_mk_choice status = function + | GrafiteAst.Symbol_alias (name, _, dsc) -> + if name = __Implicit then + dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) + else if name = __Closed_Implicit then + dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) + else + DisambiguateChoices.lookup_symbol_by_dsc status + ~mk_implicit:(function + | true -> NCic.Implicit `Closed + | false -> NCic.Implicit `Term) + ~mk_appl:(function + (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) + ~term_of_nref:(fun nref -> NCic.Const nref) + name dsc + | GrafiteAst.Number_alias (_, dsc) -> + let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in + desc, `Num_interp + (fun num -> match f with `Num_interp f -> f num | _ -> assert false) + | GrafiteAst.Ident_alias (name, uri) -> + uri, `Sym_interp + (fun l->assert(l = []); + let nref = NReference.reference_of_string uri in + NCic.Const nref) +;; + + +let mk_implicit b = + match b with + | false -> + GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") + | true -> + GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") +;; + +let nlookup_in_library + interactive_user_uri_choice input_or_locate_uri item += + match item with + | DisambiguateTypes.Id id -> + (try + let references = NCicLibrary.resolve id in + List.map + (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) + ) references + with + NCicEnvironment.ObjectNotFound _ -> []) + | _ -> [] +;; + +let fix_instance item l = + match item with + DisambiguateTypes.Symbol (_,n) -> + List.map + (function + GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Num n -> + List.map + (function + GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Id _ -> l +;; + + +let disambiguate_nterm estatus expty context metasenv subst thing += + let diff, metasenv, subst, cic = + singleton "first" + (NCicDisambiguate.disambiguate_term + ~rdb:estatus + ~aliases:estatus#disambiguate_db.aliases + ~expty + ~universe:(Some estatus#disambiguate_db.multi_aliases) + ~lookup_in_library:nlookup_in_library + ~mk_choice:(ncic_mk_choice estatus) + ~mk_implicit ~fix_instance + ~description_of_alias:GrafiteAst.description_of_alias + ~context ~metasenv ~subst thing) + in + let estatus = + set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences + diff + in + metasenv, subst, estatus, cic +;; + + +type pattern = + NotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = + let interp path = NCicDisambiguate.disambiguate_path path in + let goal_path = HExtlib.map_option 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 x -> Some (text,prefix_len,x) + in + (wanted, hyp_paths, goal_path) +;; + +let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function + | `Unfold (Some t) -> assert false (* MATITA 1.0 *) + | `Normalize + | `Simpl + | `Unfold None + | `Whd as kind -> kind +;; + +let disambiguate_auto_params + disambiguate_term metasenv context (oterms, params) += + match oterms with + | None -> metasenv, (None, params) + | Some terms -> + let metasenv, terms = + List.fold_right + (fun t (metasenv, terms) -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,t::terms) terms (metasenv, []) + in + metasenv, (Some terms, params) +;; + +let disambiguate_just disambiguate_term context metasenv = + function + `Term t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv, `Term t + | `Auto params -> + let metasenv,params = disambiguate_auto_params disambiguate_term metasenv + context params + in + metasenv, `Auto params +;; + +let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = + let uri = + let baseuri = + match baseuri with Some x -> x | None -> raise BaseUriNotSetYet + in + let name = + match obj with + | NotationPt.Inductive (_,(name,_,_,_)::_) + | NotationPt.Record (_,name,_,_) -> name ^ ".ind" + | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" + | NotationPt.Inductive _ -> assert false + in + NUri.uri_of_string (baseuri ^ "/" ^ name) + in + let diff, _, _, cic = + singleton "third" + (NCicDisambiguate.disambiguate_obj + ~lookup_in_library:nlookup_in_library + ~description_of_alias:GrafiteAst.description_of_alias + ~mk_choice:(ncic_mk_choice estatus) + ~mk_implicit ~fix_instance + ~uri + ~rdb:estatus + ~aliases:estatus#disambiguate_db.aliases + ~universe:(Some estatus#disambiguate_db.multi_aliases) + (text,prefix_len,obj)) in + let estatus = + set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences + diff + in + estatus, cic +;; + +let disambiguate_cic_appl_pattern status args = + let rec disambiguate = + function + NotationPt.ApplPattern l -> + NotationPt.ApplPattern (List.map disambiguate l) + | NotationPt.VarPattern id + when not + (List.exists + (function (NotationPt.IdentArg (_,id')) -> id'=id) args) + -> + let item = DisambiguateTypes.Id id in + begin + try + match + DisambiguateTypes.Environment.find item + status#disambiguate_db.aliases + with + GrafiteAst.Ident_alias (_, uri) -> + NotationPt.NRefPattern (NReference.reference_of_string uri) + | _ -> assert false + with Not_found -> + prerr_endline + ("LexiconEngine.eval_command: domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + dump_aliases prerr_endline "" status; + raise + (Failure + ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) + end + | p -> p + in + disambiguate +;; + +let add_aliases_for_objs status = + List.fold_left + (fun status nref -> + let references = NCicLibrary.aliases_of nref in + let new_env = + List.map + (fun u -> + let name = NCicPp.r2s true u in + DisambiguateTypes.Id name, + GrafiteAst.Ident_alias (name,NReference.string_of_reference u) + ) references + in + set_proof_aliases status ~implicit_aliases:false + GrafiteAst.WithPreferences new_env + ) status diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.mli b/matita/components/ng_disambiguation/grafiteDisambiguate.mli new file mode 100644 index 000000000..15dc42ae4 --- /dev/null +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.mli @@ -0,0 +1,80 @@ +(* 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/ + *) + +type db + +class type g_status = + object + inherit Interpretations.g_status + method disambiguate_db: db + end + +class status : + object ('self) + inherit g_status + inherit Interpretations.status + method set_disambiguate_db: db -> 'self + method set_disambiguate_status: #g_status -> 'self + end + +val eval_with_new_aliases: + #status as 'status -> ('status -> 'a) -> + (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a + +val set_proof_aliases: + #status as 'status -> + implicit_aliases:bool -> (* implicit ones are made explicit *) + GrafiteAst.inclusion_mode -> + (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status + +val add_aliases_for_objs: #status as 'status -> NUri.uri list -> 'status + +(* args: print function, message (may be empty), status *) +val dump_aliases: (string -> unit) -> string -> #status -> unit + +exception BaseUriNotSetYet + +val disambiguate_nterm : + #status as 'status -> + NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution -> + NotationPt.term Disambiguate.disambiguator_input -> + NCic.metasenv * NCic.substitution * 'status * NCic.term + +val disambiguate_nobj : + #status as 'status -> ?baseuri:string -> + (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> + 'status * NCic.obj + +type pattern = + NotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +val disambiguate_npattern: + GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern + +val disambiguate_cic_appl_pattern: + #status -> + NotationPt.argument_pattern list -> + NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern diff --git a/matita/components/ng_disambiguation/nnumber_notation.mli b/matita/components/ng_disambiguation/nnumber_notation.mli new file mode 100644 index 000000000..91cba3b7c --- /dev/null +++ b/matita/components/ng_disambiguation/nnumber_notation.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2004, 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/ + *) + +(* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *) + +(* Works by side-effects only *) diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index da0ab80fc..2633e1aba 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -2,10 +2,9 @@ nDiscriminationTree.cmi: nCicMetaSubst.cmi: nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi -nRstatus.cmi: nCicCoercion.cmi nCicRefineUtil.cmi: -nCicUnification.cmi: nRstatus.cmi -nCicRefiner.cmi: nRstatus.cmi +nCicUnification.cmi: nCicCoercion.cmi +nCicRefiner.cmi: nCicCoercion.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi @@ -16,8 +15,6 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ nCicCoercion.cmi -nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi -nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index a90df82fa..47f203f0a 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -2,7 +2,7 @@ continuationals.cmi: nCicTacReduction.cmi: nTacStatus.cmi: continuationals.cmi nCicElim.cmi: -nTactics.cmi: nTacStatus.cmi continuationals.cmi +nTactics.cmi: nTacStatus.cmi nnAuto.cmi: nTacStatus.cmi nDestructTac.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi