From aab0401db0bedd941da96a32acd600af3fbe42e7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 29 Oct 2010 16:42:43 +0000 Subject: [PATCH] WARNING: partial commit (does not compile) 1) major re-organization of statuses 2) major change to dumpability 3) partial functionalization of lexicon status --- matita/components/content/interpretations.ml | 161 ++++++++---------- matita/components/content/interpretations.mli | 50 +++--- .../grafite_engine/grafiteEngine.ml | 28 ++- .../components/grafite_engine/grafiteTypes.ml | 8 +- .../grafite_engine/grafiteTypes.mli | 7 +- .../grafite_engine/nCicCoercDeclaration.ml | 5 +- matita/components/grafite_parser/Makefile | 1 - .../grafite_parser/grafiteDisambiguate.ml | 30 ++-- .../grafite_parser/grafiteDisambiguate.mli | 20 ++- matita/components/grafite_parser/nEstatus.ml | 26 --- matita/components/grafite_parser/nEstatus.mli | 26 --- matita/components/lexicon/cicNotation.ml | 34 +--- matita/components/lexicon/cicNotation.mli | 13 +- matita/components/lexicon/lexiconEngine.ml | 6 +- matita/components/lexicon/lexiconEngine.mli | 2 + .../ng_cic_content/nTermCicContent.ml | 148 +--------------- .../ng_cic_content/nTermCicContent.mli | 10 +- .../ng_disambiguation/disambiguateChoices.ml | 5 +- .../ng_disambiguation/disambiguateChoices.mli | 1 + .../ng_disambiguation/nCicDisambiguate.mli | 4 +- matita/components/ng_library/nCicLibrary.ml | 104 ++++------- matita/components/ng_library/nCicLibrary.mli | 72 +++----- .../ng_paramodulation/nCicParamod.mli | 8 +- matita/components/ng_refiner/Makefile | 3 +- matita/components/ng_refiner/nCicRefiner.mli | 4 +- .../components/ng_refiner/nCicUnification.mli | 4 +- matita/components/ng_refiner/nRstatus.ml | 17 -- matita/components/ng_refiner/nRstatus.mli | 17 -- matita/components/ng_tactics/nTacStatus.ml | 44 ++++- matita/components/ng_tactics/nTacStatus.mli | 35 +++- matita/components/ng_tactics/nTactics.ml | 2 +- matita/components/ng_tactics/nTactics.mli | 16 +- matita/components/statuses.txt | 7 + matita/matita/applyTransformation.mli | 4 +- matita/matita/matitaMathView.ml | 10 +- 35 files changed, 340 insertions(+), 592 deletions(-) delete mode 100644 matita/components/grafite_parser/nEstatus.ml delete mode 100644 matita/components/grafite_parser/nEstatus.mli delete mode 100644 matita/components/ng_refiner/nRstatus.ml delete mode 100644 matita/components/ng_refiner/nRstatus.mli create mode 100644 matita/components/statuses.txt diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index 7e85d0fc1..e9166c20a 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -32,6 +32,9 @@ 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;; + type interpretation_id = int let idref id t = Ast.AttributedTerm (`IdRef id, t) @@ -43,38 +46,42 @@ type term_info = uri: (cic_id, NReference.reference) Hashtbl.t; } - (* persistent state *) - -let initial_level2_patterns32 () = Hashtbl.create 211 -let initial_interpretations () = Hashtbl.create 211 - -let level2_patterns32 = ref (initial_level2_patterns32 ()) -(* symb -> id list ref *) -let interpretations = ref (initial_interpretations ()) -let pattern32_matrix = ref [] -let counter = ref ~-1 -let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;; - -let stack = ref [] - -let push () = - stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack; - counter := ~-1; - level2_patterns32 := initial_level2_patterns32 (); - interpretations := initial_interpretations (); - pattern32_matrix := [] -;; - -let pop () = - match !stack with - [] -> assert false - | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old -> - stack := old; - counter := ocounter; - level2_patterns32 := olevel2_patterns32; - interpretations := ointerpretations; - pattern32_matrix := opattern32_matrix -;; +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 * interpretation_id) list; + level2_patterns32: + (string * string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) IntMap.t; + interpretations: interpretation_id 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)) @@ -109,84 +116,51 @@ let instantiate32 term_info idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let load_patterns32s = ref [];; - -let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;; -let fresh_id = - fun () -> - incr counter; - !counter - -let add_interpretation dsc (symbol, args) appl_pattern = - let id = fresh_id () in - Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern); - pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; - List.iter (fun f -> f !pattern32_matrix) !load_patterns32s; - (try - let ids = Hashtbl.find !interpretations symbol in - ids := id :: !ids - with Not_found -> Hashtbl.add !interpretations symbol (ref [id])); - id - -let get_all_interpretations () = - List.map - (function (_, _, id) -> - let (dsc, _, _, _) = - try - Hashtbl.find !level2_patterns32 id - with Not_found -> assert false - in - (id, dsc)) - !pattern32_matrix - -let get_active_interpretations () = - HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None) - !pattern32_matrix - -let set_active_interpretations ids = - let pattern32_matrix' = - List.map - (function - | (_, ap, id) when List.mem id ids -> (true, ap, id) - | (_, ap, id) -> (false, ap, id)) - !pattern32_matrix +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 + 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 - pattern32_matrix := pattern32_matrix'; - List.iter (fun f -> f !pattern32_matrix) !load_patterns32s + !load_patterns32 status#interp_db.pattern32_matrix; + status,id + +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 ?(sorted=true) symbol = +let lookup_interpretations status ?(sorted=true) symbol = try let raw = List.map ( fun id -> let (dsc, _, args, appl_pattern) = - try - Hashtbl.find !level2_patterns32 id + try IntMap.find id status#interp_db.level2_patterns32 with Not_found -> assert false in dsc, args, appl_pattern - ) - !(Hashtbl.find !interpretations symbol) + ) (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 remove_interpretation id = - (try - let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in - let ids = Hashtbl.find !interpretations symbol in - ids := List.filter ((<>) id) !ids; - Hashtbl.remove !level2_patterns32 id; - with Not_found -> raise Interpretation_not_found); - pattern32_matrix := - List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; - List.iter (fun f -> f !pattern32_matrix) !load_patterns32s - -let init () = List.iter (fun f -> f []) !load_patterns32s - let instantiate_appl_pattern ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern = @@ -203,4 +177,3 @@ let instantiate_appl_pattern | Ast.ApplPattern terms -> mk_appl (List.map aux terms) in aux appl_pattern - diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli index 50432801d..d04b56a8f 100644 --- a/matita/components/content/interpretations.mli +++ b/matita/components/content/interpretations.mli @@ -24,34 +24,48 @@ *) - (** {2 Persistant state handling} *) + (** {2 State handling} *) + +type db + +class type g_status = + object + method interp_db: db + end + +class status : + object ('self) + method interp_db: db + method set_interp_db: db -> 'self + method set_interp_status: #g_status -> 'self + end type interpretation_id type cic_id = string val add_interpretation: + #status as 'status -> string -> (* id / description *) string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) NotationPt.cic_appl_pattern -> (* level 3 pattern *) - interpretation_id + 'status * interpretation_id - (** @raise Interpretation_not_found *) -val lookup_interpretations: - ?sorted:bool -> string -> (* symbol *) - (string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern) list +val set_load_patterns32: + ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit exception Interpretation_not_found (** @raise Interpretation_not_found *) -val remove_interpretation: interpretation_id -> unit +val lookup_interpretations: + #status -> + ?sorted:bool -> string -> (* symbol *) + (string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) list (** {3 Interpretations toggling} *) -val get_all_interpretations: unit -> (interpretation_id * string) list -val get_active_interpretations: unit -> interpretation_id list -val set_active_interpretations: interpretation_id list -> unit +val toggle_active_interpretations: #status as 'status -> bool -> 'status (** {2 content -> cic} *) @@ -64,15 +78,7 @@ val instantiate_appl_pattern: (string * 'term) list -> NotationPt.cic_appl_pattern -> 'term -val push: unit -> unit -val pop: unit -> unit - -(* for Matita NG *) val find_level2_patterns32: - int -> - string * string * - NotationPt.argument_pattern list * NotationPt.cic_appl_pattern - -val add_load_patterns32: - ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit -val init: unit -> unit + #status -> int -> + string * string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 3a9e87eea..b12da3802 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -46,10 +46,8 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in - NCicLibrary.Serializer.register#run "unification_hints" - object(_ : 'a NCicLibrary.register_type) - method run = basic_eval_unification_hint - end + GrafiteTypes.Serializer.register#run "unification_hints" + basic_eval_unification_hint ;; let eval_unification_hint status t n = @@ -83,10 +81,7 @@ let record_index_obj = (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) l) in - NCicLibrary.Serializer.register#run "index_obj" - object(_ : 'a NCicLibrary.register_type) - method run = aux - end + GrafiteTypes.Serializer.register#run "index_obj" aux ;; let compute_keys status uri height kind = @@ -167,10 +162,7 @@ let record_index_eq = ~refresh_uri_in_term = index_eq (NCicLibrary.refresh_uri uri) in - NCicLibrary.Serializer.register#run "index_eq" - object(_ : 'a NCicLibrary.register_type) - method run = basic_index_eq - end + GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq ;; let index_eq_for_auto status uri = @@ -199,10 +191,7 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) in - NCicLibrary.Serializer.register#run "constraints" - object(_:'a NCicLibrary.register_type) - method run = basic_eval_add_constraint - end + GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint ;; let eval_add_constraint status u1 u2 = @@ -568,8 +557,11 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = let status,uris = match cmd with | GrafiteAst.Include (loc, baseuri) -> - NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status, [] + let status,obj = + GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = status#set_dump (obj::status#dump) in + status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Set (loc, name, value) -> status, [] in diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index b99b15eaa..d36998181 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -37,12 +37,16 @@ class status = fun (b : string) -> NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular)) in object + (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) + inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty)) + inherit NCicLibrary.dumpable_status val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) method baseuri = baseuri method set_baseuri v = {< baseuri = v >} method ng_mode = ng_mode; method set_ng_mode v = {< ng_mode = v >} - (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) - inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty)) end + +module Serializer = + NCicLibrary.Serializer(struct type dumpable_status = status end) diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index e59e5375a..f407cc49b 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -34,10 +34,13 @@ val command_error: string -> 'a (** @raise Command_error *) class status : string -> object ('self) + (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) + inherit NTacStatus.tac_status + inherit NCicLibrary.dumpable_status method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] method set_ng_mode: [`ProofMode | `CommandMode] -> 'self - (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) - inherit NTacStatus.tac_status end + +module Serializer: NCicLibrary.SerializerType with type dumpable_status = status diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index 3cf076265..8ba2f92f8 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -291,10 +291,7 @@ let record_ncoercion = let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term = List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l in - NCicLibrary.Serializer.register#run "ncoercion" - object(self : 'a NCicLibrary.register_type) - method run = aux_l - end + GrafiteTypes.Serializer.register#run "ncoercion" aux_l ;; let basic_eval_and_record_ncoercion infos status = diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 5583ecb8a..c1288b4ab 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -5,7 +5,6 @@ INTERFACE_FILES = \ dependenciesParser.mli \ grafiteParser.mli \ cicNotation2.mli \ - nEstatus.mli \ grafiteDisambiguate.mli \ print_grammar.mli \ $(NULL) diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index c465fe1d8..f12a97372 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -25,6 +25,21 @@ (* $Id$ *) +class g_status = + object + inherit LexiconEngine.g_status + inherit NCicCoercion.g_status + end + +class status = + object (self) + inherit LexiconEngine.status + inherit NCicCoercion.status + method set_grafite_disambiguate_status + : 'status. #g_status as 'status -> 'self + = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o + end + exception BaseUriNotSetYet let singleton msg = function @@ -39,14 +54,14 @@ let singleton msg = function let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let ncic_mk_choice = function +let ncic_mk_choice status = function | LexiconAst.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 + DisambiguateChoices.lookup_symbol_by_dsc status ~mk_implicit:(function | true -> NCic.Implicit `Closed | false -> NCic.Implicit `Term) @@ -117,7 +132,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing ~expty ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) ~lookup_in_library:nlookup_in_library - ~mk_choice:ncic_mk_choice + ~mk_choice:(ncic_mk_choice estatus) ~mk_implicit ~fix_instance ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst thing) @@ -195,7 +210,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = (NCicDisambiguate.disambiguate_obj ~lookup_in_library:nlookup_in_library ~description_of_alias:LexiconAst.description_of_alias - ~mk_choice:ncic_mk_choice + ~mk_choice:(ncic_mk_choice estatus) ~mk_implicit ~fix_instance ~uri ~rdb:estatus @@ -205,10 +220,3 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = let estatus = LexiconEngine.set_proof_aliases estatus diff in estatus, cic ;; - -let disambiguate_command estatus (text,prefix_len,cmd)= - match cmd with - | GrafiteAst.Include _ - | GrafiteAst.Print _ - | GrafiteAst.Set _ as cmd -> - estatus,cmd diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 2de3a1b6d..97ff55874 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -25,20 +25,28 @@ exception BaseUriNotSetYet -val disambiguate_command: - LexiconEngine.status as 'status -> - GrafiteAst.command Disambiguate.disambiguator_input -> - 'status * GrafiteAst.command +class g_status : + object + inherit LexiconEngine.g_status + inherit NCicCoercion.g_status + end + +class status : + object + inherit LexiconEngine.status + inherit NCicCoercion.status + method set_grafite_disambiguate_status: #g_status -> 'self + end val disambiguate_nterm : NCic.term option -> - (#NEstatus.status as 'status) -> + (#status as 'status) -> NCic.context -> NCic.metasenv -> NCic.substitution -> NotationPt.term Disambiguate.disambiguator_input -> NCic.metasenv * NCic.substitution * 'status * NCic.term val disambiguate_nobj : - #NEstatus.status as 'status -> + #status as 'status -> ?baseuri:string -> (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> 'status * NCic.obj diff --git a/matita/components/grafite_parser/nEstatus.ml b/matita/components/grafite_parser/nEstatus.ml deleted file mode 100644 index ebfd686cd..000000000 --- a/matita/components/grafite_parser/nEstatus.ml +++ /dev/null @@ -1,26 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -class type g_status = - object - inherit LexiconEngine.g_status - inherit NCicLibrary.g_dumpable_status - end - -class status = - object (self) - inherit LexiconEngine.status - inherit NCicLibrary.dumpable_status - method set_estatus : 'status. #g_status as 'status -> 'self - = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o - end diff --git a/matita/components/grafite_parser/nEstatus.mli b/matita/components/grafite_parser/nEstatus.mli deleted file mode 100644 index cc356aa46..000000000 --- a/matita/components/grafite_parser/nEstatus.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -class type g_status = - object - inherit LexiconEngine.g_status - inherit NCicLibrary.g_dumpable_status - end - -class status : - object ('self) - inherit LexiconEngine.status - inherit NCicLibrary.dumpable_status - inherit g_status - method set_estatus: #g_status -> 'self - end diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml index 28cab9458..e25ca3e57 100644 --- a/matita/components/lexicon/cicNotation.ml +++ b/matita/components/lexicon/cicNotation.ml @@ -45,7 +45,7 @@ let initial_rule_ids_to_items ()= Hashtbl.create 113 let parser_ref_counter = ref (initial_parser_ref_counter ());; let rule_ids_to_items = ref (initial_rule_ids_to_items ());; -let process_notation st = +let process_notation status st = match st with | Notation (loc, dir, l1, associativity, precedence, l2) -> let l1 = @@ -75,11 +75,13 @@ let process_notation st = else [] in - !rule_id @ pp_id + status,!rule_id @ pp_id | Interpretation (loc, dsc, l2, l3) -> - let interp_id = Interpretations.add_interpretation dsc l2 l3 in - [InterpretationId interp_id] - | st -> [] + let status,interp_id = + Interpretations.add_interpretation status dsc l2 l3 + in + status,[InterpretationId interp_id] + | st -> status,[] let remove_notation = function | RuleId id -> @@ -90,25 +92,7 @@ let remove_notation = function RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id) !parser_ref_counter item | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id - | InterpretationId id -> Interpretations.remove_interpretation id - -let get_all_notations () = - List.map - (fun (interp_id, dsc) -> - InterpretationId interp_id, "interpretation: " ^ dsc) - (Interpretations.get_all_interpretations ()) - -let get_active_notations () = - List.map (fun id -> InterpretationId id) - (Interpretations.get_active_interpretations ()) - -let set_active_notations ids = - let interp_ids = - HExtlib.filter_map - (function InterpretationId interp_id -> Some interp_id | _ -> None) - ids - in - Interpretations.set_active_interpretations interp_ids + | InterpretationId id -> () let history = ref [];; @@ -117,13 +101,11 @@ let push () = parser_ref_counter := initial_parser_ref_counter (); rule_ids_to_items := initial_rule_ids_to_items (); TermContentPres.push (); - Interpretations.push (); CicNotationParser.push () ;; let pop () = TermContentPres.pop (); - Interpretations.pop (); CicNotationParser.pop (); match !history with | [] -> assert false diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli index 9e231e331..085feda0d 100644 --- a/matita/components/lexicon/cicNotation.mli +++ b/matita/components/lexicon/cicNotation.mli @@ -27,18 +27,11 @@ type notation_id val compare_notation_id : notation_id -> notation_id -> int -val process_notation: LexiconAst.command -> notation_id list +val process_notation: + #Interpretations.status as 'status -> LexiconAst.command + -> 'status * notation_id list val remove_notation: notation_id -> unit -(** {2 Notation enabling/disabling} - * Right now, only disabling of notation during pretty printing is supported. - * If it is useful to disable it also for the input phase is still to be - * understood ... *) - -val get_all_notations: unit -> (notation_id * string) list (* id, dsc *) -val get_active_notations: unit -> notation_id list -val set_active_notations: notation_id list -> unit - val push: unit -> unit val pop: unit -> unit diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index a0dfb87cf..4aba86187 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -49,16 +49,18 @@ let initial_status = { class type g_status = object + inherit Interpretations.g_status method lstatus: lexicon_status end class status = object(self) + inherit Interpretations.status val lstatus = initial_status method lstatus = lstatus method set_lstatus v = {< lstatus = v >} method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self - = fun o -> self#set_lstatus o#lstatus + = fun o -> (self#set_lstatus o#lstatus)#set_interp_status o end let dump_aliases out msg status = @@ -151,7 +153,7 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd = (loc, dsc, (symbol, args), disambiguate cic_appl_pattern) | _-> cmd in - let notation_ids' = CicNotation.process_notation cmd in + let sstatus,notation_ids' = CicNotation.process_notation sstatus cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in let sstatus = sstatus#set_lstatus status in diff --git a/matita/components/lexicon/lexiconEngine.mli b/matita/components/lexicon/lexiconEngine.mli index f08891b5a..c4fcac0a8 100644 --- a/matita/components/lexicon/lexiconEngine.mli +++ b/matita/components/lexicon/lexiconEngine.mli @@ -34,12 +34,14 @@ type lexicon_status = { class type g_status = object + inherit Interpretations.g_status method lstatus: lexicon_status end class status : object ('self) inherit g_status + inherit Interpretations.status method set_lstatus: lexicon_status -> 'self method set_lexicon_engine_status: #g_status -> 'self end diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index 5d91cee28..61ff07689 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -36,14 +36,11 @@ type id = string let hide_coercions = ref true;; -(* -type interpretation_id = int - -type term_info = - { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, UriManager.uri) Hashtbl.t; - } -*) +class status = + object + inherit NCicCoercion.status + inherit Interpretations.status + end let idref register_ref = let id = ref 0 in @@ -207,44 +204,7 @@ let nast_of_cic0 status idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; - (* persistent state *) - -(* -let initial_level2_patterns32 () = Hashtbl.create 211 -let initial_interpretations () = Hashtbl.create 211 - -let level2_patterns32 = ref (initial_level2_patterns32 ()) -(* symb -> id list ref *) -let interpretations = ref (initial_interpretations ()) -*) let compiled32 = ref None -(* -let pattern32_matrix = ref [] -let counter = ref ~-1 - -let stack = ref [] - -let push () = - stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack; - counter := ~-1; - level2_patterns32 := initial_level2_patterns32 (); - interpretations := initial_interpretations (); - compiled32 := None; - pattern32_matrix := [] -;; - -let pop () = - match !stack with - [] -> assert false - | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old -> - stack := old; - counter := ocounter; - level2_patterns32 := olevel2_patterns32; - interpretations := ointerpretations; - compiled32 := ocompiled32; - pattern32_matrix := opattern32_matrix -;; -*) let get_compiled32 () = match !compiled32 with @@ -316,7 +276,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = in let _, symbol, args, _ = try - Interpretations.find_level2_patterns32 pid + Interpretations.find_level2_patterns32 status pid with Not_found -> assert false in let ast = instantiate32 idrefs env symbol args in @@ -328,102 +288,8 @@ let load_patterns32 t = HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t in set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) -in - Interpretations.add_load_patterns32 load_patterns32; - Interpretations.init () ;; -(* -let fresh_id = - fun () -> - incr counter; - !counter - -let add_interpretation dsc (symbol, args) appl_pattern = - let id = fresh_id () in - Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern); - pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; - load_patterns32 !pattern32_matrix; - (try - let ids = Hashtbl.find !interpretations symbol in - ids := id :: !ids - with Not_found -> Hashtbl.add !interpretations symbol (ref [id])); - id - -let get_all_interpretations () = - List.map - (function (_, _, id) -> - let (dsc, _, _, _) = - try - Hashtbl.find !level2_patterns32 id - with Not_found -> assert false - in - (id, dsc)) - !pattern32_matrix - -let get_active_interpretations () = - HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None) - !pattern32_matrix - -let set_active_interpretations ids = - let pattern32_matrix' = - List.map - (function - | (_, ap, id) when List.mem id ids -> (true, ap, id) - | (_, ap, id) -> (false, ap, id)) - !pattern32_matrix - in - pattern32_matrix := pattern32_matrix'; - load_patterns32 !pattern32_matrix - -exception Interpretation_not_found - -let lookup_interpretations symbol = - try - HExtlib.list_uniq - (List.sort Pervasives.compare - (List.map - (fun id -> - let (dsc, _, args, appl_pattern) = - try - Hashtbl.find !level2_patterns32 id - with Not_found -> assert false - in - dsc, args, appl_pattern) - !(Hashtbl.find !interpretations symbol))) - with Not_found -> raise Interpretation_not_found - -let remove_interpretation id = - (try - let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in - let ids = Hashtbl.find !interpretations symbol in - ids := List.filter ((<>) id) !ids; - Hashtbl.remove !level2_patterns32 id; - with Not_found -> raise Interpretation_not_found); - pattern32_matrix := - List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; - load_patterns32 !pattern32_matrix - -let _ = load_patterns32 [] - -let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_uri 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.UriPattern uri -> term_of_uri uri - | Ast.ImplicitPattern -> mk_implicit false - | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> mk_appl (List.map aux terms) - in - aux appl_pattern -*) - let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = let module K = Content in let nast_of_cic = @@ -621,3 +487,5 @@ in in res,ids_to_refs ;; + +Interpretations.set_load_patterns32 load_patterns32 diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli index d691acdec..f06ea2e91 100644 --- a/matita/components/ng_cic_content/nTermCicContent.mli +++ b/matita/components/ng_cic_content/nTermCicContent.mli @@ -87,13 +87,19 @@ type id = string val hide_coercions: bool ref +class status : + object ('self) + inherit NCicCoercion.status + inherit Interpretations.status + end + val nmap_sequent: - #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + #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: - #NCicCoercion.status -> NCic.obj -> + #status -> NCic.obj -> NotationPt.term Content.cobj * (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 94643b3b0..3a79d1bfa 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -72,8 +72,9 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_nref (dsc, args, appl_pattern)= [] -> combined | _::_ -> mk_appl (combined::rest)) -let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_nref symbol dsc = - let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in +let lookup_symbol_by_dsc status ~mk_appl ~mk_implicit ~term_of_nref symbol dsc = + let interpretations = + Interpretations.lookup_interpretations status ~sorted:false symbol in try mk_choice ~mk_appl ~mk_implicit ~term_of_nref (List.find (fun (dsc', _, _) -> dsc = dsc') interpretations) diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli index 1d98fa3a6..60a938a80 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.mli +++ b/matita/components/ng_disambiguation/disambiguateChoices.mli @@ -43,6 +43,7 @@ val nlookup_num_by_dsc: string -> NCic.term codomain_item * @param dsc description (1st component of codomain_item) *) val lookup_symbol_by_dsc: + #Interpretations.status -> mk_appl: ('term list -> 'term) -> mk_implicit: (bool -> 'term) -> term_of_nref: (NReference.reference -> 'term) -> diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index b02ce3cc8..d2ae7f566 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -22,7 +22,7 @@ val disambiguate_term : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - rdb:#NRstatus.status -> + rdb:#NCicCoercion.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> @@ -42,7 +42,7 @@ val disambiguate_obj : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - rdb:#NRstatus.status -> + rdb:#NCicCoercion.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index 1ed016e77..d4ea77a31 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -146,48 +146,13 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; -type automation_cache = NDiscriminationTree.DiscriminationTree.t -type unit_eq_cache = NCicParamod.state - -class type g_eq_status = - object - method eq_cache : unit_eq_cache - end - -class eq_status = - object(self) - val eq_cache = NCicParamod.empty_state - method eq_cache = eq_cache - method set_eq_cache v = {< eq_cache = v >} - method set_eq_status - : 'status. #g_eq_status as 'status -> 'self - = fun o -> self#set_eq_cache o#eq_cache - end - -class type g_auto_status = - object - method auto_cache : automation_cache - end - -class auto_status = - object(self) - val auto_cache = NDiscriminationTree.DiscriminationTree.empty - method auto_cache = auto_cache - method set_auto_cache v = {< auto_cache = v >} - method set_auto_status - : 'status. #g_auto_status as 'status -> 'self - = fun o -> self#set_auto_cache o#auto_cache - end - class type g_status = object - inherit NRstatus.g_status method timestamp: timestamp end class status = object(self) - inherit NRstatus.status val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} @@ -224,37 +189,39 @@ let serialize ~baseuri dump = type obj = string * Obj.t - -class type g_dumpable_status = - object - inherit g_status - inherit g_auto_status - inherit g_eq_status - method dump: obj list - end - class dumpable_status = object(self) - inherit status - inherit auto_status - inherit eq_status val dump = ([] : obj list) method dump = dump method set_dump v = {< dump = v >} - method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self - = fun o -> - (((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o)#set_eq_status o end -type 'a register_type = - < run: 'status. - 'a -> refresh_uri_in_universe:(NCic.universe -> - NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> - (#dumpable_status as 'status) -> 'status > +module type SerializerType = + sig + type dumpable_status + + type 'a register_type = + 'a -> + refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> + refresh_uri_in_term:(NCic.term -> NCic.term) -> + dumpable_status -> dumpable_status + + val register: < run: 'a. string -> 'a register_type -> ('a -> obj) > + val serialize: baseuri:NUri.uri -> obj list -> unit + (* the obj is the "include" command to be added to the dump list *) + val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj + end -module Serializer = +module Serializer(D: sig type dumpable_status end) = struct - let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status = fun _ -> assert false end (* unknown data*)) + type dumpable_status = D.dumpable_status + type 'a register_type = + 'a -> + refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> + refresh_uri_in_term:(NCic.term -> NCic.term) -> + dumpable_status -> dumpable_status + + let require1 = ref (fun _ -> assert false) (* unknown data*) let already_registered = ref [] let register = @@ -265,14 +232,11 @@ module Serializer = already_registered := tag :: !already_registered; let old_require1 = !require1 in require1 := - object - method run : 'status. obj -> (#dumpable_status as 'status) -> 'status = - fun ((tag',data) as x) -> - if tag=tag' then - require#run (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term - else - old_require1#run x - end; + (fun ((tag',data) as x) -> + if tag=tag' then + require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term + else + old_require1 x); (fun x -> tag,Obj.repr x) end @@ -282,7 +246,7 @@ module Serializer = try includes := baseuri::!includes; let dump = require0 ~baseuri in - List.fold_right !require1#run dump status + List.fold_right !require1 dump status with Sys_error _ -> raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri)) @@ -292,15 +256,11 @@ module Serializer = (* memorizzo baseuri in una tabella; *) require2 ~baseuri in - register#run "include" - object(self : 'a register_type) - method run = aux - end + register#run "include" aux let require ~baseuri status = let status = require2 ~baseuri status in - let dump = record_include baseuri :: status#dump in - status#set_dump dump + status,record_include baseuri end diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index 03b844397..de53755f4 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -13,39 +13,11 @@ exception LibraryOutOfSync of string Lazy.t -type automation_cache = NDiscriminationTree.DiscriminationTree.t -type unit_eq_cache = NCicParamod.state - -class type g_eq_status = - object - method eq_cache : unit_eq_cache - end - -class eq_status : - object('self) - inherit g_eq_status - method set_eq_cache: unit_eq_cache -> 'self - method set_eq_status: #g_eq_status -> 'self - end - -class type g_auto_status = - object - method auto_cache : automation_cache - end - -class auto_status : - object('self) - inherit g_auto_status - method set_auto_cache: automation_cache -> 'self - method set_auto_status: #g_auto_status -> 'self - end - type timestamp class type g_status = object method timestamp: timestamp - inherit NRstatus.g_status end class status : @@ -73,35 +45,29 @@ val init: unit -> unit type obj -class type g_dumpable_status = - object - inherit g_status - inherit g_auto_status - inherit g_eq_status - method dump: obj list - end - -class dumpable_status : - object ('self) - inherit status - inherit auto_status - inherit eq_status - inherit g_dumpable_status - method set_dump: obj list -> 'self - method set_dumpable_status: #g_dumpable_status -> 'self - end +module type SerializerType = + sig + type dumpable_status -type 'a register_type = - < run: 'status. - 'a -> refresh_uri_in_universe:(NCic.universe -> - NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> - (#dumpable_status as 'status) -> 'status > + type 'a register_type = + 'a -> + refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> + refresh_uri_in_term:(NCic.term -> NCic.term) -> + dumpable_status -> dumpable_status -module Serializer: - sig val register: < run: 'a. string -> 'a register_type -> ('a -> obj) > val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> (#dumpable_status as 'status) -> 'status + (* the obj is the "include" command to be added to the dump list *) + val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj + end + +module Serializer(D: sig type dumpable_status end) : + SerializerType with type dumpable_status = D.dumpable_status + +class dumpable_status : + object ('self) + method dump: obj list + method set_dump: obj list -> 'self end (* CSC: only required during old-to-NG phase, to be deleted *) diff --git a/matita/components/ng_paramodulation/nCicParamod.mli b/matita/components/ng_paramodulation/nCicParamod.mli index 96eeb71ae..86a104073 100644 --- a/matita/components/ng_paramodulation/nCicParamod.mli +++ b/matita/components/ng_paramodulation/nCicParamod.mli @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) val nparamod : - #NRstatus.status -> + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> (NCic.term * NCic.term) -> (NCic.term * NCic.term) list -> (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list @@ -24,19 +24,19 @@ val index_obj: state -> NUri.uri -> state val is_equation: NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> bool val paramod : - #NRstatus.status -> + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> state -> (NCic.term * NCic.term) -> (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list val fast_eq_check : - #NRstatus.status -> + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> state -> (NCic.term * NCic.term) -> (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list val demod : - #NRstatus.status -> + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> state -> (NCic.term * NCic.term) -> diff --git a/matita/components/ng_refiner/Makefile b/matita/components/ng_refiner/Makefile index bf1fe3be5..79871a567 100644 --- a/matita/components/ng_refiner/Makefile +++ b/matita/components/ng_refiner/Makefile @@ -6,8 +6,7 @@ INTERFACE_FILES = \ nCicMetaSubst.mli \ nCicUnifHint.mli \ nCicCoercion.mli \ - nRstatus.mli \ - nCicRefineUtil.mli \ + nCicRefineUtil.mli \ nCicUnification.mli \ nCicRefiner.mli diff --git a/matita/components/ng_refiner/nCicRefiner.mli b/matita/components/ng_refiner/nCicRefiner.mli index 1a04d2abd..6ec18e365 100644 --- a/matita/components/ng_refiner/nCicRefiner.mli +++ b/matita/components/ng_refiner/nCicRefiner.mli @@ -16,7 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; val typeof : - #NRstatus.status -> + #NCicCoercion.status -> ?localise:(NCic.term -> Stdpp.location) -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term option -> (* term, expected type *) @@ -24,7 +24,7 @@ val typeof : (* menv, subst,refined term, type *) val typeof_obj : - #NRstatus.status -> + #NCicCoercion.status -> ?localise:(NCic.term -> Stdpp.location) -> NCic.obj -> NCic.obj diff --git a/matita/components/ng_refiner/nCicUnification.mli b/matita/components/ng_refiner/nCicUnification.mli index 429610218..159d24c10 100644 --- a/matita/components/ng_refiner/nCicUnification.mli +++ b/matita/components/ng_refiner/nCicUnification.mli @@ -16,7 +16,7 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; val unify : - #NRstatus.status -> + #NCicCoercion.status -> ?test_eq_only:bool -> (* default: false *) ?swap:bool -> (* default: false *) NCic.metasenv -> NCic.substitution -> NCic.context -> @@ -33,7 +33,7 @@ val fix_sorts: * [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ] *) val delift_type_wrt_terms: - #NRstatus.status -> + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term list -> NCic.metasenv * NCic.substitution * NCic.term diff --git a/matita/components/ng_refiner/nRstatus.ml b/matita/components/ng_refiner/nRstatus.ml deleted file mode 100644 index 9a6fd4ef2..000000000 --- a/matita/components/ng_refiner/nRstatus.ml +++ /dev/null @@ -1,17 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) - -class type g_status = NCicCoercion.status - -class status = NCicCoercion.status - diff --git a/matita/components/ng_refiner/nRstatus.mli b/matita/components/ng_refiner/nRstatus.mli deleted file mode 100644 index 631e629e5..000000000 --- a/matita/components/ng_refiner/nRstatus.mli +++ /dev/null @@ -1,17 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) - -class type g_status = NCicCoercion.status - -class status : NCicCoercion.status - diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 9f653abd5..9504e64ba 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -16,6 +16,9 @@ let pp x = if !debug then prerr_endline (Lazy.force x) else () ;; +type automation_cache = NDiscriminationTree.DiscriminationTree.t +type unit_eq_cache = NCicParamod.state + exception Error of string lazy_t * exn option let fail ?exn msg = raise (Error (msg,exn)) @@ -31,21 +34,56 @@ let wrap fname f x = | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname) ;; +class type g_eq_status = + object + method eq_cache : unit_eq_cache + end + +class eq_status = + object(self) + val eq_cache = NCicParamod.empty_state + method eq_cache = eq_cache + method set_eq_cache v = {< eq_cache = v >} + method set_eq_status + : 'status. #g_eq_status as 'status -> 'self + = fun o -> self#set_eq_cache o#eq_cache + end + +class type g_auto_status = + object + method auto_cache : automation_cache + end + +class auto_status = + object(self) + val auto_cache = NDiscriminationTree.DiscriminationTree.empty + method auto_cache = auto_cache + method set_auto_cache v = {< auto_cache = v >} + method set_auto_status + : 'status. #g_auto_status as 'status -> 'self + = fun o -> self#set_auto_cache o#auto_cache + end + class type g_pstatus = object - inherit NEstatus.g_status + inherit GrafiteDisambiguate.g_status + inherit g_auto_status + inherit g_eq_status method obj: NCic.obj end class pstatus = fun (o: NCic.obj) -> object (self) - inherit NEstatus.status + inherit GrafiteDisambiguate.status + inherit auto_status + inherit eq_status val obj = o method obj = obj method set_obj o = {< obj = o >} method set_pstatus : 'status. #g_pstatus as 'status -> 'self - = fun o -> (self#set_estatus o)#set_obj o#obj + = fun o -> + (((self#set_lexicon_engine_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o end type tactic_term = NotationPt.term Disambiguate.disambiguator_input diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index a51435e24..cfb7123bb 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -14,16 +14,47 @@ exception Error of string lazy_t * exn option val fail: ?exn:exn -> string lazy_t -> 'a +type automation_cache = NDiscriminationTree.DiscriminationTree.t +type unit_eq_cache = NCicParamod.state + +class type g_eq_status = + object + method eq_cache : unit_eq_cache + end + +class eq_status : + object('self) + inherit g_eq_status + method set_eq_cache: unit_eq_cache -> 'self + method set_eq_status: #g_eq_status -> 'self + end + +class type g_auto_status = + object + method auto_cache : automation_cache + end + +class auto_status : + object('self) + inherit g_auto_status + method set_auto_cache: automation_cache -> 'self + method set_auto_status: #g_auto_status -> 'self + end + class type g_pstatus = object - inherit NEstatus.g_status + inherit GrafiteDisambiguate.g_status + inherit g_auto_status + inherit g_eq_status method obj: NCic.obj end class pstatus : NCic.obj -> object ('self) - inherit NEstatus.status + inherit GrafiteDisambiguate.status + inherit auto_status + inherit eq_status method obj: NCic.obj method set_obj: NCic.obj -> 'self method set_pstatus: #g_pstatus -> 'self diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 09427a315..ac3dd00b7 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -249,7 +249,7 @@ let distribute_tac tac (status : #tac_status) = ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn ;; -let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; +let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; let repeat_tac t s = let rec repeat t (status : #tac_status as 'a) : 'a = diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index 822421a24..bfa965391 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -71,20 +71,8 @@ val constructor_tac : ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic val atomic_tac : - (((int * Continuationals.Stack.switch) list * 'a list * 'b list * - [> `NoTag ]) - list NTacStatus.status -> - (< auto_cache : NCicLibrary.automation_cache; - eq_cache : NCicLibrary.unit_eq_cache; - coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list; - lstatus : LexiconEngine.lexicon_status; obj : NCic.obj; - set_coerc_db : NCicCoercion.db -> 'c; - set_coercion_status : 'd. (#NCicCoercion.g_status as 'd) -> 'c; - set_uhint_db : NCicUnifHint.db -> 'c; - set_unifhint_status : 'e. (#NCicUnifHint.g_status as 'e) -> 'c; - timestamp : NCicLibrary.timestamp; uhint_db : NCicUnifHint.db; .. > - as 'c)) -> - (#NTacStatus.tac_status as 'f) -> 'f + (NTacStatus.tac_status -> 'c #NTacStatus.status) -> + (#NTacStatus.tac_status as 'f) -> 'f type indtyinfo diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt new file mode 100644 index 000000000..8e47b67f0 --- /dev/null +++ b/matita/components/statuses.txt @@ -0,0 +1,7 @@ +grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon +nciccoercion) + |--> dumpable | + |--> nciclibrary interpretation + +ntermciccontent -> nciccoercion+interpretation + | + unif_hint diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index 93d8afc19..e67a88ee3 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -35,10 +35,10 @@ val ntxt_of_cic_sequent: map_unicode_to_tex:bool -> int -> - #NCicCoercion.status -> + #NTermCicContent.status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) val ntxt_of_cic_object: - map_unicode_to_tex:bool -> int -> #NCicCoercion.status -> NCic.obj -> string + map_unicode_to_tex:bool -> int -> #NTermCicContent.status -> NCic.obj -> string diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index f418abe6f..d0710ab4e 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -620,7 +620,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #NCicCoercion.status as 'status -> NCic.metasenv -> + 'status. #NTermCicContent.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -637,7 +637,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + 'status. #NTermCicContent.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -728,7 +728,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal None method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit - = fun status -> + = fun (status : #NTacStatus.tac_status) -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #NCicCoercion.status as 'status -> page:int -> + 'status. #NTermCicContent.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with @@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit + method goto_sequent: 'status. #NTermCicContent.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try -- 2.39.2