From 551861bf1adbb1db5b0b9941b98ba54531157364 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 20:26:10 +0000 Subject: [PATCH] - content/interpretations.ml and ng_cic_content/nTermCicContent.ml where mutually recursive and part of the status was kept imperatively; the two files have been merged together into ng_cic_content/interpretations.ml --- .../METAS/meta.helm-ng_disambiguation.src | 2 +- matita/components/Makefile | 6 +- matita/components/content/.depend | 3 - matita/components/content/Makefile | 1 - matita/components/content/interpretations.ml | 177 --------------- .../components/content_pres/content2pres.mli | 2 +- .../components/content_pres/sequent2pres.mli | 2 +- matita/components/ng_cic_content/.depend | 8 +- matita/components/ng_cic_content/Makefile | 2 +- ...{nTermCicContent.ml => interpretations.ml} | 212 +++++++++++++----- .../interpretations.mli | 23 +- .../ng_cic_content/nTermCicContent.mli | 45 ---- matita/components/statuses.txt | 12 +- matita/matita/applyTransformation.ml | 6 +- matita/matita/applyTransformation.mli | 5 +- matita/matita/matitaGui.ml | 2 +- 16 files changed, 195 insertions(+), 313 deletions(-) delete mode 100644 matita/components/content/interpretations.ml rename matita/components/ng_cic_content/{nTermCicContent.ml => interpretations.ml} (81%) rename matita/components/{content => ng_cic_content}/interpretations.mli (82%) delete mode 100644 matita/components/ng_cic_content/nTermCicContent.mli diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src index 84eeab3fe..97a3c1346 100644 --- a/matita/components/METAS/meta.helm-ng_disambiguation.src +++ b/matita/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-content helm-ng_refiner helm-disambiguation" +requires="helm-ng_cic_content helm-ng_refiner helm-disambiguation" version="0.0.1" archive(byte)="ng_disambiguation.cma" archive(native)="ng_disambiguation.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 7d463f88c..b1485c5cf 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -15,12 +15,12 @@ MODULES = \ ng_kernel \ getter \ library \ - content \ + content \ grafite \ - disambiguation \ ng_refiner \ - ng_disambiguation \ ng_cic_content \ + disambiguation \ + ng_disambiguation \ ng_paramodulation \ ng_library \ content_pres \ diff --git a/matita/components/content/.depend b/matita/components/content/.depend index d5941b8ef..f4b4f3037 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -2,7 +2,6 @@ content.cmi: notationUtil.cmi: notationPt.cmo notationEnv.cmi: notationPt.cmo notationPp.cmi: notationPt.cmo notationEnv.cmi -interpretations.cmi: notationPt.cmo notationPt.cmo: notationPt.cmx: content.cmo: content.cmi @@ -13,5 +12,3 @@ notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi -interpretations.cmo: notationUtil.cmi notationPt.cmo interpretations.cmi -interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content/Makefile b/matita/components/content/Makefile index 5ea3ee796..8ea1cd33c 100644 --- a/matita/components/content/Makefile +++ b/matita/components/content/Makefile @@ -6,7 +6,6 @@ INTERFACE_FILES = \ notationUtil.mli \ notationEnv.mli \ notationPp.mli \ - interpretations.mli \ $(NULL) IMPLEMENTATION_FILES = \ notationPt.ml \ diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml deleted file mode 100644 index 28957074f..000000000 --- a/matita/components/content/interpretations.ml +++ /dev/null @@ -1,177 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -module Ast = NotationPt - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -let load_patterns32 = ref (fun _ -> assert false);; -let set_load_patterns32 f = load_patterns32 := f;; - -let idref id t = Ast.AttributedTerm (`IdRef id, t) - -type cic_id = string - -type term_info = - { sort: (cic_id, Ast.sort_kind) Hashtbl.t; - uri: (cic_id, NReference.reference) Hashtbl.t; - } - -module IntMap = Map.Make(struct type t = int let compare = compare end);; -module StringMap = Map.Make(String);; - -type db = { - counter: int; - pattern32_matrix: (bool * NotationPt.cic_appl_pattern * int) list; - level2_patterns32: - (string * string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern) IntMap.t; - interpretations: int list StringMap.t; (* symb -> id list *) -} - -let initial_db = { - counter = -1; - pattern32_matrix = []; - level2_patterns32 = IntMap.empty; - interpretations = StringMap.empty -} - -class type g_status = - object - method interp_db: db - end - -class status = - object - val interp_db = initial_db - method interp_db = interp_db - method set_interp_db v = {< interp_db = v >} - method set_interp_status - : 'status. #g_status as 'status -> 'self - = fun o -> {< interp_db = o#interp_db >} - end - -let find_level2_patterns32 status pid = - IntMap.find pid status#interp_db.level2_patterns32 - -let add_idrefs = - List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) - -let instantiate32 term_info idrefs env symbol args = - let rec instantiate_arg = function - | Ast.IdentArg (n, name) -> - let t = - try List.assoc name env - with Not_found -> prerr_endline ("name not found in env: "^name); - assert false - in - let rec count_lambda = function - | Ast.AttributedTerm (_, t) -> count_lambda t - | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body - | _ -> 0 - in - let rec add_lambda t n = - if n > 0 then - let name = NotationUtil.fresh_name () in - Ast.Binder (`Lambda, (Ast.Ident (name, None), None), - Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) - else - t - in - add_lambda t (n - count_lambda t) - in - let head = - let symbol = Ast.Symbol (symbol, 0) in - add_idrefs idrefs symbol - in - if args = [] then head - else Ast.Appl (head :: List.map instantiate_arg args) - -let fresh_id status = - let counter = status#interp_db.counter+1 in - status#set_interp_db ({ status#interp_db with counter = counter }), counter - -let add_interpretation (status : #status) dsc (symbol, args) appl_pattern = - let status,id = fresh_id status in - let ids = - try - id::StringMap.find symbol status#interp_db.interpretations - with Not_found -> [id] in - let status = - status#set_interp_db { status#interp_db with - level2_patterns32 = - IntMap.add id (dsc, symbol, args, appl_pattern) - status#interp_db.level2_patterns32; - pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix; - interpretations = StringMap.add symbol ids status#interp_db.interpretations - } - in - !load_patterns32 status#interp_db.pattern32_matrix; - status - -let toggle_active_interpretations status b = - status#set_interp_db { status#interp_db with - pattern32_matrix = - List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix } - -exception Interpretation_not_found - -let lookup_interpretations status ?(sorted=true) symbol = - try - let raw = - List.map ( - fun id -> - let (dsc, _, args, appl_pattern) = - try IntMap.find id status#interp_db.level2_patterns32 - with Not_found -> assert false - in - dsc, args, appl_pattern - ) (StringMap.find symbol status#interp_db.interpretations) - in - if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) - else raw - with Not_found -> raise Interpretation_not_found - -let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern -= - let lookup name = - try List.assoc name env - with Not_found -> - prerr_endline (sprintf "Name %s not found" name); - assert false - in - let rec aux = function - | Ast.NRefPattern nref -> term_of_nref nref - | Ast.ImplicitPattern -> mk_implicit false - | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> mk_appl (List.map aux terms) - in - aux appl_pattern diff --git a/matita/components/content_pres/content2pres.mli b/matita/components/content_pres/content2pres.mli index 1c5b410b2..87843815f 100644 --- a/matita/components/content_pres/content2pres.mli +++ b/matita/components/content_pres/content2pres.mli @@ -35,6 +35,6 @@ val ncontent2pres: #TermContentPres.status -> ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> - ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> + ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t -> NotationPt.term Content.cobj -> CicNotationPres.boxml_markup diff --git a/matita/components/content_pres/sequent2pres.mli b/matita/components/content_pres/sequent2pres.mli index cc3f27457..ae1051490 100644 --- a/matita/components/content_pres/sequent2pres.mli +++ b/matita/components/content_pres/sequent2pres.mli @@ -34,6 +34,6 @@ val nsequent2pres : #TermContentPres.status -> - ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> + ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t -> subst:NCic.substitution -> NotationPt.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/matita/components/ng_cic_content/.depend b/matita/components/ng_cic_content/.depend index 1316c8eab..dd8940e5a 100644 --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@ -1,6 +1,8 @@ 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.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmx \ + interpretations.cmi diff --git a/matita/components/ng_cic_content/Makefile b/matita/components/ng_cic_content/Makefile index c501a09e1..ac40a66f1 100644 --- a/matita/components/ng_cic_content/Makefile +++ b/matita/components/ng_cic_content/Makefile @@ -2,7 +2,7 @@ PACKAGE = ng_cic_content INTERFACE_FILES = \ ncic2astMatcher.mli \ - nTermCicContent.mli + interpretations.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/interpretations.ml similarity index 81% rename from matita/components/ng_cic_content/nTermCicContent.ml rename to matita/components/ng_cic_content/interpretations.ml index 61ff07689..7e175193b 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -23,24 +23,65 @@ * http://helm.cs.unibo.it/ *) -(* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *) +(* $Id$ *) open Printf module Ast = NotationPt + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () type id = string - let hide_coercions = ref true;; -class status = +type cic_id = string + +type term_info = + { sort: (cic_id, Ast.sort_kind) Hashtbl.t; + uri: (cic_id, NReference.reference) Hashtbl.t; + } + +module IntMap = Map.Make(struct type t = int let compare = compare end);; +module StringMap = Map.Make(String);; + +type db = { + counter: int; + pattern32_matrix: (bool * NotationPt.cic_appl_pattern * int) list; + level2_patterns32: + (string * string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) IntMap.t; + interpretations: int list StringMap.t; (* symb -> id list *) + compiled32: + (NCic.term -> ((string * NCic.term) list * NCic.term list * int) option) + Lazy.t +} + +let initial_db = { + counter = -1; + pattern32_matrix = []; + level2_patterns32 = IntMap.empty; + interpretations = StringMap.empty; + compiled32 = lazy (fun _ -> assert false) +} + +class type g_status = object - inherit NCicCoercion.status - inherit Interpretations.status + inherit NCicCoercion.g_status + method interp_db: db end + +class status = + object + inherit NCicCoercion.status + val interp_db = initial_db + method interp_db = interp_db + method set_interp_db v = {< interp_db = v >} + method set_interp_status + : 'status. #g_status as 'status -> 'self + = fun o -> {< interp_db = o#interp_db >}#set_coercion_status o + end let idref register_ref = let id = ref 0 in @@ -57,6 +98,112 @@ let level_of_uri u = String.sub name 4 (String.length name - 4) ;; +let find_level2_patterns32 status pid = + IntMap.find pid status#interp_db.level2_patterns32 + +let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) + +let instantiate32 idrefs env symbol args = + let rec instantiate_arg = function + | Ast.IdentArg (n, name) -> + let t = + try List.assoc name env + with Not_found -> prerr_endline ("name not found in env: "^name); + assert false + in + let rec count_lambda = function + | Ast.AttributedTerm (_, t) -> count_lambda t + | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body + | _ -> 0 + in + let rec add_lambda t n = + if n > 0 then + let name = NotationUtil.fresh_name () in + Ast.Binder (`Lambda, (Ast.Ident (name, None), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + else + t + in + add_lambda t (n - count_lambda t) + in + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol + in + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) + +let fresh_id status = + let counter = status#interp_db.counter+1 in + status#set_interp_db ({ status#interp_db with counter = counter }), counter + +let load_patterns32 status t = + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in + status#set_interp_db + {status#interp_db with + compiled32 = lazy (Ncic2astMatcher.Matcher32.compiler t) } +;; + +let add_interpretation status dsc (symbol, args) appl_pattern = + let status,id = fresh_id status in + let ids = + try + id::StringMap.find symbol status#interp_db.interpretations + with Not_found -> [id] in + let status = + status#set_interp_db { status#interp_db with + level2_patterns32 = + IntMap.add id (dsc, symbol, args, appl_pattern) + status#interp_db.level2_patterns32; + pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix; + interpretations = StringMap.add symbol ids status#interp_db.interpretations + } + in + load_patterns32 status status#interp_db.pattern32_matrix + +let toggle_active_interpretations status b = + status#set_interp_db { status#interp_db with + pattern32_matrix = + List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix } + +exception Interpretation_not_found + +let lookup_interpretations status ?(sorted=true) symbol = + try + let raw = + List.map ( + fun id -> + let (dsc, _, args, appl_pattern) = + try IntMap.find id status#interp_db.level2_patterns32 + with Not_found -> assert false + in + dsc, args, appl_pattern + ) (StringMap.find symbol status#interp_db.interpretations) + in + if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) + else raw + with Not_found -> raise Interpretation_not_found + +let instantiate_appl_pattern + ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern += + let lookup name = + try List.assoc name env + with Not_found -> + prerr_endline (sprintf "Name %s not found" name); + assert false + in + let rec aux = function + | Ast.NRefPattern nref -> term_of_nref nref + | Ast.ImplicitPattern -> mk_implicit false + | Ast.VarPattern name -> lookup name + | Ast.ApplPattern terms -> mk_appl (List.map aux terms) + in + aux appl_pattern + let destroy_nat = let is_nat_URI = NUri.eq (NUri.uri_of_string "cic:/matita/ng/arithmetics/nat/nat.ind") in @@ -204,50 +351,8 @@ let nast_of_cic0 status idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; -let compiled32 = ref None - -let get_compiled32 () = - match !compiled32 with - | None -> assert false - | Some f -> Lazy.force f - -let set_compiled32 f = compiled32 := Some f - -let add_idrefs = - List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) - -let instantiate32 idrefs env symbol args = - let rec instantiate_arg = function - | Ast.IdentArg (n, name) -> - let t = - try List.assoc name env - with Not_found -> prerr_endline ("name not found in env: "^name); - assert false - in - let rec count_lambda = function - | Ast.AttributedTerm (_, t) -> count_lambda t - | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body - | _ -> 0 - in - let rec add_lambda t n = - if n > 0 then - let name = NotationUtil.fresh_name () in - Ast.Binder (`Lambda, (Ast.Ident (name, None), None), - Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) - else - t - in - add_lambda t (n - count_lambda t) - in - let head = - let symbol = Ast.Symbol (symbol, 0) in - add_idrefs idrefs symbol - in - if args = [] then head - else Ast.Appl (head :: List.map instantiate_arg args) - let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = - match (get_compiled32 ()) term with + match Lazy.force status#interp_db.compiled32 term with | None -> nast_of_cic0 status ~idref ~output_type ~metasenv ~subst (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term @@ -276,20 +381,13 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = in let _, symbol, args, _ = try - Interpretations.find_level2_patterns32 status pid + find_level2_patterns32 status pid with Not_found -> assert false in let ast = instantiate32 idrefs env symbol args in idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) ;; -let load_patterns32 t = - let t = - HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t - in - set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) -;; - let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = let module K = Content in let nast_of_cic = @@ -487,5 +585,3 @@ in in res,ids_to_refs ;; - -Interpretations.set_load_patterns32 load_patterns32 diff --git a/matita/components/content/interpretations.mli b/matita/components/ng_cic_content/interpretations.mli similarity index 82% rename from matita/components/content/interpretations.mli rename to matita/components/ng_cic_content/interpretations.mli index 8ee3fc01f..a4a3fb9c0 100644 --- a/matita/components/content/interpretations.mli +++ b/matita/components/ng_cic_content/interpretations.mli @@ -26,15 +26,21 @@ (** {2 State handling} *) +type id = string + +val hide_coercions: bool ref + type db class type g_status = object + inherit NCicCoercion.g_status method interp_db: db end class status : object ('self) + inherit NCicCoercion.status method interp_db: db method set_interp_db: db -> 'self method set_interp_status: #g_status -> 'self @@ -49,9 +55,6 @@ val add_interpretation: NotationPt.cic_appl_pattern -> (* level 3 pattern *) 'status -val set_load_patterns32: - ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit - exception Interpretation_not_found (** @raise Interpretation_not_found *) @@ -76,7 +79,13 @@ val instantiate_appl_pattern: (string * 'term) list -> NotationPt.cic_appl_pattern -> 'term -val find_level2_patterns32: - #status -> int -> - string * string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern +val nmap_sequent: + #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + int * NCic.conjecture -> + NotationPt.term Content.conjecture * + (id, NReference.reference) Hashtbl.t (* id -> reference *) + +val nmap_obj: + #status -> NCic.obj -> + NotationPt.term Content.cobj * + (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli deleted file mode 100644 index 4a13a8956..000000000 --- a/matita/components/ng_cic_content/nTermCicContent.mli +++ /dev/null @@ -1,45 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -type id = string - -val hide_coercions: bool ref - -class status : - object ('self) - inherit NCicCoercion.status - inherit Interpretations.status - end - -val nmap_sequent: - #status as 'a -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - int * NCic.conjecture -> - NotationPt.term Content.conjecture * - (id, NReference.reference) Hashtbl.t (* id -> reference *) - -val nmap_obj: - #status -> NCic.obj -> - NotationPt.term Content.cobj * - (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index e2be9b49b..104a90938 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -7,8 +7,10 @@ grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion) |-> notation_parser -ntermciccontent = nciccoercion+interpretation - | - unif_hint - -applytransformation = ntermciccontent+termcontentpres +applytransformation + | + |-> ntermciccontent = nciccoercion+interpretation + | | + | unif_hint + | + |-> termcontentpres diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 8e09d9db4..442a7eb3c 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -37,7 +37,7 @@ class status = object - inherit NTermCicContent.status + inherit Interpretations.status inherit TermContentPres.status end @@ -47,7 +47,7 @@ let mpres_document pres_box = let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = let content_sequent,ids_to_refs = - NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in + Interpretations.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in @@ -55,7 +55,7 @@ let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = (function x::_ -> x | _ -> assert false) size pres_sequent let ntxt_of_cic_object ~map_unicode_to_tex size status obj = - let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in + let cobj,ids_to_nrefs = Interpretations.nmap_obj status obj in let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in BoxPp.render_to_string ~map_unicode_to_tex diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index 6d3e40810..4b95e5370 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -35,13 +35,12 @@ class status : object ('self) - inherit NTermCicContent.status + inherit Interpretations.status inherit TermContentPres.status end val ntxt_of_cic_sequent: - map_unicode_to_tex:bool -> int -> - #status -> + map_unicode_to_tex:bool -> int -> #status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index a42500bd6..d963cf6a2 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -859,7 +859,7 @@ class gui () = s#set_grafite_status status*) ); MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem - ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled); + ~callback:(fun enabled -> Interpretations.hide_coercions := enabled); MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem ~callback:(fun enabled -> Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled); -- 2.39.2