From 53a5acbe28212706be9c684d612aee1ccb165587 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 29 Oct 2010 20:57:21 +0000 Subject: [PATCH] WARNING: partial commit. - matita is compiling again, but totally untested - major re-organization of the statuses --- .../components/grafite_engine/grafiteEngine.ml | 18 +++++++----------- .../grafite_engine/grafiteEngine.mli | 5 ----- .../components/grafite_engine/grafiteTypes.ml | 1 + .../components/grafite_engine/grafiteTypes.mli | 1 + .../grafite_engine/nCicCoercDeclaration.ml | 4 +--- .../grafite_parser/grafiteDisambiguate.ml | 2 +- .../grafite_parser/grafiteDisambiguate.mli | 8 ++++---- matita/components/ng_library/nCicLibrary.ml | 8 -------- matita/components/ng_library/nCicLibrary.mli | 8 +------- matita/components/ng_tactics/nTactics.ml | 8 ++++---- matita/components/statuses.txt | 8 ++++---- matita/matita/matitaEngine.ml | 11 +---------- matita/matita/matitaGui.ml | 16 +++++++++------- matita/matita/matitaGuiTypes.mli | 6 +++--- matita/matita/matitacLib.ml | 2 +- 15 files changed, 38 insertions(+), 68 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index b12da3802..8eb438e18 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -549,11 +549,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = eval_add_constraint status [`Type,u1] [`Type,u2] ;; -let eval_comment ~disambiguate_command opts status (text,prefix_len,c) = - status, [] +let eval_comment opts status (text,prefix_len,c) = status, [] -let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = - let status,cmd = disambiguate_command status (text,prefix_len,cmd) in +let rec eval_command opts status (text,prefix_len,cmd) = let status,uris = match cmd with | GrafiteAst.Include (loc, baseuri) -> @@ -567,7 +565,7 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = in status,uris -and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = +and eval_executable opts status (text,prefix_len,ex) = match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then @@ -582,19 +580,17 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = in status,[] | GrafiteAst.Command (_, cmd) -> - eval_command ~disambiguate_command opts status (text,prefix_len,cmd) + eval_command opts status (text,prefix_len,cmd) | GrafiteAst.NCommand (_, cmd) -> eval_ncommand opts status (text,prefix_len,cmd) | GrafiteAst.NMacro (loc, macro) -> raise (NMacro (loc,macro)) -and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status -(text,prefix_len,st) -= +and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) = let opts = { do_heavy_checks = do_heavy_checks ; } in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable ~disambiguate_command opts status (text,prefix_len,ex) + eval_executable opts status (text,prefix_len,ex) | GrafiteAst.Comment (_,c) -> - eval_comment ~disambiguate_command opts status (text,prefix_len,c) + eval_comment opts status (text,prefix_len,c) ;; diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index ad88d5dfd..10bc4d36d 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -29,11 +29,6 @@ exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a val eval_ast : - disambiguate_command: - (GrafiteTypes.status -> - GrafiteAst.command disambiguator_input -> - GrafiteTypes.status * GrafiteAst.command) -> - ?do_heavy_checks:bool -> GrafiteTypes.status -> GrafiteAst.statement disambiguator_input -> diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index d36998181..82fc6d605 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -40,6 +40,7 @@ class status = fun (b : string) -> (* 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 + inherit NCicLibrary.status val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) method baseuri = baseuri diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index f407cc49b..92af84bab 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -37,6 +37,7 @@ class status : (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) inherit NTacStatus.tac_status inherit NCicLibrary.dumpable_status + inherit NCicLibrary.status method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index 8ba2f92f8..ca56a3aee 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -311,8 +311,7 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity status,uris ;; -let eval_ncoercion status name t ty (id,src) tgt = - +let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = let metasenv,subst,status,ty = GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in assert (metasenv=[]); @@ -321,7 +320,6 @@ let eval_ncoercion status name t ty (id,src) tgt = GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in - let status, src, tgt, cpos, arity = src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in let status, uris = diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index f12a97372..143ac5e11 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -25,7 +25,7 @@ (* $Id$ *) -class g_status = +class type g_status = object inherit LexiconEngine.g_status inherit NCicCoercion.g_status diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 97ff55874..200d507a8 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -25,14 +25,14 @@ exception BaseUriNotSetYet -class g_status : - object +class type g_status = + object inherit LexiconEngine.g_status inherit NCicCoercion.g_status - end + end class status : - object + object ('self) inherit LexiconEngine.status inherit NCicCoercion.status method set_grafite_disambiguate_status: #g_status -> 'self diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index d4ea77a31..70be8ae57 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -146,19 +146,11 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; -class type g_status = - object - method timestamp: timestamp - end - class status = object(self) val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} - method set_library_status - : 'status. #g_status as 'status -> 'self - = fun o -> self#set_timestamp o#timestamp end let time_travel status = diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index de53755f4..bad0d8975 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -15,16 +15,10 @@ exception LibraryOutOfSync of string Lazy.t type timestamp -class type g_status = - object - method timestamp: timestamp - end - class status : object ('self) - inherit g_status + method timestamp: timestamp method set_timestamp: timestamp -> 'self - method set_library_status: #g_status -> 'self end (* it also checks it and add it to the environment *) diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index ac3dd00b7..331945819 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -205,10 +205,10 @@ let compare_statuses ~past ~present = let exec tac (low_status : #lowtac_status) g = let stack = [ [0,Open g], [], [], `NoTag ] in let status = - (new NTacStatus.status low_status#obj stack)#set_estatus low_status + (new NTacStatus.status low_status#obj stack)#set_pstatus low_status in let status = tac status in - (low_status#set_estatus status)#set_obj status#obj + (low_status#set_pstatus status)#set_obj status#obj ;; let distribute_tac tac (status : #tac_status) = @@ -236,7 +236,7 @@ let distribute_tac tac (status : #tac_status) = in aux s go gc loc_tl in - let s0 = (new NTacStatus.status status#obj ())#set_estatus status in + let s0 = (new NTacStatus.status status#obj ())#set_pstatus status in let s0, go0, gc0 = s0, [], [] in let sn, gon, gcn = aux s0 go0 gc0 g in debug_print (lazy ("opened: " @@ -246,7 +246,7 @@ let distribute_tac tac (status : #tac_status) = let stack = (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s in - ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn + ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn ;; let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index 8e47b67f0..cb454ba5c 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -1,7 +1,7 @@ -grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon +nciccoercion) - |--> dumpable | - |--> nciclibrary interpretation +grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion) + |--> dumpable | | + |--> nciclibrary interpretation unif_hint -ntermciccontent -> nciccoercion+interpretation +ntermciccontent = nciccoercion+interpretation | unif_hint diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index ef685c595..5cf0ad95d 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -30,13 +30,6 @@ module G = GrafiteAst let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -let disambiguate_command lexicon_status_ref grafite_status cmd = - let lexicon_status,cmd = - GrafiteDisambiguate.disambiguate_command !lexicon_status_ref cmd - in - lexicon_status_ref := lexicon_status; - grafite_status,cmd - let eval_macro_screenshot (status : GrafiteTypes.status) name = assert false (* MATITA 1.0 let _,_,metasenv,subst,_ = status#obj in @@ -63,9 +56,7 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = let lexicon_status_ref = ref (status :> LexiconEngine.status) in let baseuri = status#baseuri in let new_status,new_objs = - GrafiteEngine.eval_ast - ~disambiguate_command:(disambiguate_command lexicon_status_ref) - ?do_heavy_checks status (text,prefix_len,ast) + GrafiteEngine.eval_ast ?do_heavy_checks status (text,prefix_len,ast) in let new_status = if !lexicon_status_ref#lstatus != status#lstatus then diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 6d4c8c0f5..7f2cb952c 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -81,7 +81,7 @@ let save_moo grafite_status = in LexiconMarshal.save_lexicon lexicon_fname grafite_status#lstatus.LexiconEngine.lexicon_content_rev; - NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; @@ -856,12 +856,14 @@ class gui () = | false -> main#toplevel#unfullscreen ()); main#fullscreenMenuItem#set_active false; MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem - ~callback:(function - | true -> - CicNotation.set_active_notations - (List.map fst (CicNotation.get_all_notations ())) - | false -> - CicNotation.set_active_notations []); + ~callback:( + let s = s () in + let status = + Interpretations.toggle_active_interpretations s#grafite_status + in + assert false (* MATITA1.0 ??? + s#set_grafite_status status*) + ); MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled); MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 7fc6f9ae5..64dd3cd6f 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -131,9 +131,9 @@ object (** load a sequent and render it into parent widget *) method nload_sequent: - #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> int -> unit + #NTermCicContent.status -> NCic.metasenv -> NCic.substitution -> int -> unit - method load_nobject: #NCicCoercion.status -> NCic.obj -> unit + method load_nobject: #NTermCicContent.status -> NCic.obj -> unit end class type sequentsViewer = @@ -143,7 +143,7 @@ object method load_logo_with_qed: unit method nload_sequents: #NTacStatus.tac_status -> unit method goto_sequent: - #NCicCoercion.status -> int -> unit (* to be called _after_ load_sequents *) + #NTermCicContent.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 8ab5d407f..cc0793c96 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -231,7 +231,7 @@ let compile atstart options fname = (if Helm_registry.get_bool "matita.moo" then begin (* FG: we do not generate .moo when dumping .mma files *) LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump end; let tm = Unix.gmtime elapsed in -- 2.39.2