From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 08:34:19 +0000 (+0000) Subject: More statuses converted to objects. X-Git-Tag: make_still_working~3841 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git More statuses converted to objects. --- diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 4abfc933e..b1cc9d671 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -86,11 +86,11 @@ let rec tactic_of_ast status ast = | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term | GrafiteAst.ApplyS (_, term, params) -> Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ()) - ~automation_cache:status.GrafiteTypes.automation_cache + ~automation_cache:status#automation_cache | GrafiteAst.Assumption _ -> Tactics.assumption | GrafiteAst.AutoBatch (_,params) -> Tactics.auto ~params ~dbd:(LibraryDb.instance ()) - ~automation_cache:status.GrafiteTypes.automation_cache + ~automation_cache:status#automation_cache | GrafiteAst.Cases (_, what, pattern, (howmany, names)) -> Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names) ~pattern what @@ -112,7 +112,7 @@ let rec tactic_of_ast status ast = | GrafiteAst.Demodulate (_, params) -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~params - ~automation_cache:status.GrafiteTypes.automation_cache + ~automation_cache:status#automation_cache | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) @@ -183,12 +183,12 @@ let rec tactic_of_ast status ast = | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1 | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) -> Declarative.by_just_we_proved ~dbd:(LibraryDb.instance()) - ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1 + ~automation_cache:status#automation_cache just ty id t1 | GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove t id t2 | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) - ~automation_cache:status.GrafiteTypes.automation_cache t + ~automation_cache:status#automation_cache t | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> Declarative.we_proceed_by_cases_on t t1 | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> @@ -197,14 +197,14 @@ let rec tactic_of_ast status ast = | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) -> Declarative.existselim ~dbd:(LibraryDb.instance()) - ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2 + ~automation_cache:status#automation_cache just id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.AndElim(_,just,id1,t1,id2,t2) -> Declarative.andelim ~dbd:(LibraryDb.instance ()) - ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2 + ~automation_cache:status#automation_cache just id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) - ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont + ~automation_cache:status#automation_cache termine t1 t2 cont let classify_tactic tactic = match tactic with @@ -347,13 +347,13 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = proof', opened_goals in let incomplete_proof = - match status.GrafiteTypes.proof_status with + match status#proof_status with | GrafiteTypes.Incomplete_proof p -> p | _ -> assert false in - { status with GrafiteTypes.proof_status = - GrafiteTypes.Incomplete_proof - { incomplete_proof with GrafiteTypes.proof = proof } }, + status#set_proof_status + (GrafiteTypes.Incomplete_proof + { incomplete_proof with GrafiteTypes.proof = proof }), opened_goals, closed_goals let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (status, goal) = @@ -381,13 +381,13 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) ( proof', opened_goals in let incomplete_proof = - match status.GrafiteTypes.proof_status with + match status#proof_status with | GrafiteTypes.Incomplete_proof p -> p | _ -> assert false in - { status with GrafiteTypes.proof_status = - GrafiteTypes.Incomplete_proof - { incomplete_proof with GrafiteTypes.proof = proof } }, + status#set_proof_status + (GrafiteTypes.Incomplete_proof + { incomplete_proof with GrafiteTypes.proof = proof }), opened_goals, closed_goals type eval_ast = {ea_go: @@ -508,7 +508,7 @@ let add_coercions_of_lemmas lemmas status = lemmas in let status = GrafiteTypes.add_moo_content moo_content status in - {status with GrafiteTypes.coercions = CoercDb.dump () }, + status#set_coercions (CoercDb.dump ()), lemmas let eval_coercion status ~add_composites uri arity saturations = @@ -581,11 +581,11 @@ let non_punctuation_tactical_of_ast (text,prefix_len,punct) = let eval_tactical status tac = let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in let status = (* is proof completed? *) - match status.GrafiteTypes.proof_status with + match status#proof_status with | GrafiteTypes.Incomplete_proof { GrafiteTypes.stack = stack; proof = proof } when Continuationals.Stack.is_empty stack -> - { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof } + status#set_proof_status (GrafiteTypes.Proof proof) | _ -> status in status @@ -672,7 +672,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = match cmd with | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NQed loc -> - (match status.GrafiteTypes.ng_status with + (match status#ng_status with | GrafiteTypes.ProofMode estatus -> let uri,height,menv,subst,obj_kind = estatus#obj in if menv <> [] then @@ -713,13 +713,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = estatus,uri::uris_rev ) (estatus,[]) objs in let uris = uri::List.rev uris_rev in - {status with - GrafiteTypes.ng_status = - GrafiteTypes.CommandMode (estatus :> NEstatus.status)},`New uris + status#set_ng_status + (GrafiteTypes.CommandMode (estatus :> NEstatus.status)),`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.NObj (loc,obj) -> let estatus = - match status.GrafiteTypes.ng_status with + match status#ng_status with | GrafiteTypes.ProofMode _ -> assert false | GrafiteTypes.CommandMode es -> es in @@ -729,12 +728,10 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let uri,height,nmenv,nsubst,nobj = obj in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = - { status with - GrafiteTypes.ng_status = - GrafiteTypes.ProofMode - (subst_metasenv_and_fix_names - ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus)) - } + status#set_ng_status + (GrafiteTypes.ProofMode + (subst_metasenv_and_fix_names + ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))) in (match nmenv with [] -> @@ -754,13 +751,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status assert false (* TODO: for user input *) | GrafiteAst.Index (loc,Some key,uri) -> let universe = - status.GrafiteTypes.automation_cache.AutomationCache.univ + status#automation_cache.AutomationCache.univ in let universe = Universe.index universe key (CicUtil.term_of_uri uri) in let cache = { - status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } + status#automation_cache with AutomationCache.univ = universe } in - let status = { status with GrafiteTypes.automation_cache = cache } in + let status = status#set_automation_cache cache in (* debug let msg = let candidates = Universe.get_candidates status.GrafiteTypes.universe key in @@ -772,20 +769,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status = GrafiteTypes.add_moo_content [cmd] status in status,`Old [] | GrafiteAst.Select (_,uri) as cmd -> - if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old [] + if List.mem cmd status#moo_content_rev then status, `Old [] else let cache = - AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache + AutomationCache.add_term_to_active status#automation_cache [] [] [] (CicUtil.term_of_uri uri) None in - let status = { status with GrafiteTypes.automation_cache = cache } in + let status = status#set_automation_cache cache in let status = GrafiteTypes.add_moo_content [cmd] status in status, `Old [] | GrafiteAst.Pump (_,steps) -> let cache = - AutomationCache.pump status.GrafiteTypes.automation_cache steps + AutomationCache.pump status#automation_cache steps in - let status = { status with GrafiteTypes.automation_cache = cache } in + let status = status#set_automation_cache cache in status, `Old [] | GrafiteAst.PreferCoercion (loc, coercion) -> eval_prefer_coercion status coercion @@ -849,7 +846,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Print (_,_) -> status,`Old [] | GrafiteAst.Qed loc -> let uri, metasenv, _subst, bo, ty, attrs = - match status.GrafiteTypes.proof_status with + match status#proof_status with | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) -> uri, metasenv, subst, body, ty, attrs | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) -> @@ -867,7 +864,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in let status, lemmas = add_obj uri obj status in - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + status#set_proof_status GrafiteTypes.No_proof, (*CSC: I throw away the arities *) `Old (uri::lemmas) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> @@ -924,10 +921,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let _subst = [] in let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in - { status with GrafiteTypes.proof_status = - GrafiteTypes.Incomplete_proof - { GrafiteTypes.proof = initial_proof; stack = initial_stack } ; - }, + status#set_proof_status + (GrafiteTypes.Incomplete_proof + { GrafiteTypes.proof = initial_proof; stack = initial_stack }), `Old [] | _ -> if metasenv <> [] then @@ -936,12 +932,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status CicMetaSubst.ppmetasenv [] metasenv)); let status, lemmas = add_obj uri obj status in let status,new_lemmas = add_coercions_of_lemmas lemmas status in - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + status#set_proof_status GrafiteTypes.No_proof, `Old (uri::new_lemmas@lemmas) in - match status.GrafiteTypes.proof_status with + match status#proof_status with GrafiteTypes.Intermediate _ -> - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris + status#set_proof_status GrafiteTypes.No_proof,uris | _ -> status,uris } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command @@ -965,7 +961,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.NTactic (_(*loc*), tacl) -> - (match status.GrafiteTypes.ng_status with + (match status#ng_status with | GrafiteTypes.CommandMode _ -> assert false | GrafiteTypes.ProofMode nstatus -> let nstatus = @@ -975,7 +971,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status subst_metasenv_and_fix_names nstatus) nstatus tacl in - { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus }, + status#set_ng_status (GrafiteTypes.ProofMode nstatus), `New []) | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 74e2cf2e2..5cf9dc360 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -128,13 +128,13 @@ let add_obj ~pack_coercion_obj uri obj status = in let automation_cache,status = List.fold_left add_to_universe - (status.GrafiteTypes.automation_cache,status) + (status#automation_cache,status) uris_to_index in - {status with - GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects; - GrafiteTypes.automation_cache = automation_cache}, - lemmas + (status + #set_objects (uri :: lemmas @ status#objects)) + #set_automation_cache automation_cache, + lemmas let add_coercion ~pack_coercion_obj ~add_composites status uri arity saturations baseuri @@ -143,9 +143,9 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity LibrarySync.add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri in let status = - { status with GrafiteTypes.coercions = CoercDb.dump () ; - objects = lemmas @ status.GrafiteTypes.objects; - } + (status + #set_coercions (CoercDb.dump ())) ; + #set_objects (lemmas @ status#objects) in let estatus = NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status) @@ -153,9 +153,9 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity let status = GrafiteTypes.set_estatus estatus status in status, lemmas -let prefer_coercion s u = +let prefer_coercion status u = CoercDb.prefer u; - { s with GrafiteTypes.coercions = CoercDb.dump () } + status#set_coercions (CoercDb.dump ()) (** @return l2 \ l1 *) let uri_list_diff l2 l1 = @@ -167,22 +167,17 @@ let uri_list_diff l2 l1 = let time_travel ~present ~past = let objs_to_remove = - uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in + uri_list_diff present#objects past#objects in List.iter LibrarySync.remove_obj objs_to_remove; - CoercDb.restore past.GrafiteTypes.coercions; + CoercDb.restore past#coercions; NCicLibrary.time_travel (GrafiteTypes.get_estatus past) ;; -let initial_status lexicon_status baseuri = { - GrafiteTypes.moo_content_rev = []; - proof_status = GrafiteTypes.No_proof; - objects = []; - coercions = CoercDb.empty_coerc_db; - automation_cache = AutomationCache.empty (); - baseuri = baseuri; - ng_status = GrafiteTypes.CommandMode (new NEstatus.status) -} - +let initial_status lexicon_status baseuri = + new GrafiteTypes.status [] GrafiteTypes.No_proof [] + CoercDb.empty_coerc_db (AutomationCache.empty ()) + baseuri (GrafiteTypes.CommandMode (new NEstatus.status)) +;; let init baseuri = CoercDb.restore CoercDb.empty_coerc_db; diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 5d0ce025d..9fd40b1c4 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -48,37 +48,56 @@ type ng_status = | ProofMode of NTacStatus.tac_status | CommandMode of NEstatus.status -type status = { - moo_content_rev: GrafiteMarshal.moo; - proof_status: proof_status; - objects: UriManager.uri list; - coercions: CoercDb.coerc_db; - automation_cache:AutomationCache.cache; - baseuri: string; - ng_status: ng_status; -} +class status = + fun (mcr : GrafiteMarshal.moo) (ps : proof_status) (o : UriManager.uri list) + (c : CoercDb.coerc_db) (ac : AutomationCache.cache) (b : string) + (ns : ng_status) + -> + object + val moo_content_rev = mcr + val proof_status = ps + val objects = o + val coercions = c + val automation_cache = ac + val baseuri = b + val ng_status = ns + method moo_content_rev = moo_content_rev + method set_moo_content_rev v = {< moo_content_rev = v >} + method proof_status = proof_status + method set_proof_status v = {< proof_status = v >} + method objects = objects + method set_objects v = {< objects = v >} + method coercions = coercions + method set_coercions v = {< coercions = v >} + method automation_cache = automation_cache + method set_automation_cache v = {< automation_cache = v >} + method baseuri = baseuri + method set_baseuri v = {< baseuri = v >} + method ng_status = ng_status; + method set_ng_status v = {< ng_status = v >} + end let get_estatus x = - match x.ng_status with + match x#ng_status with | ProofMode t -> (t :> NEstatus.status) | CommandMode e -> e ;; let set_estatus e x = - { x with ng_status = - match x.ng_status with + x#set_ng_status + (match x#ng_status with ProofMode t -> ProofMode t#set_estatus e - | CommandMode _ -> CommandMode e} + | CommandMode _ -> CommandMode e) ;; let get_current_proof status = - match status.proof_status with + match status#proof_status with | Incomplete_proof { proof = p } -> p | Proof p -> p | _ -> raise (Statement_error "no ongoing proof") let get_proof_metasenv status = - match status.proof_status with + match status#proof_status with | No_proof -> [] | Proof (_, metasenv, _, _, _, _) | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } @@ -86,15 +105,15 @@ let get_proof_metasenv status = metasenv let get_stack status = - match status.proof_status with + match status#proof_status with | Incomplete_proof p -> p.stack | Proof _ -> Continuationals.Stack.empty | _ -> assert false let set_stack stack status = - match status.proof_status with + match status#proof_status with | Incomplete_proof p -> - { status with proof_status = Incomplete_proof { p with stack = stack } } + status#set_proof_status (Incomplete_proof { p with stack = stack }) | Proof _ -> assert (Continuationals.Stack.is_empty stack); status @@ -102,7 +121,7 @@ let set_stack stack status = let set_metasenv metasenv status = let proof_status = - match status.proof_status with + match status#proof_status with | No_proof -> Intermediate metasenv | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) -> Incomplete_proof @@ -110,26 +129,26 @@ let set_metasenv metasenv status = | Intermediate _ -> Intermediate metasenv | Proof (_, metasenv', _, _, _, _) -> assert (metasenv = metasenv'); - status.proof_status + status#proof_status in - { status with proof_status = proof_status } + status#set_proof_status proof_status let get_proof_context status goal = - match status.proof_status with + match status#proof_status with | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } -> let (_, context, _) = CicUtil.lookup_meta goal metasenv in context | _ -> [] let get_proof_conclusion status goal = - match status.proof_status with + match status#proof_status with | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } -> let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in conclusion | _ -> raise (Statement_error "no ongoing proof") let add_moo_content cmds status = - let content = status.moo_content_rev in + let content = status#moo_content_rev in let content' = List.fold_right (fun cmd acc -> @@ -145,61 +164,21 @@ let add_moo_content cmds status = in (* prerr_endline ("new moo content: " ^ String.concat " " (List.map GrafiteAstPp.pp_command content')); *) - { status with moo_content_rev = content' } - -let get_baseuri status = status.baseuri;; - -(* -let get_option status name = - try - StringMap.find name status.options - with Not_found -> raise (Option_error (name, "not found")) - -let set_option status name value = - let types = [ (* no set options defined! *) ] in - let ty_and_mangler = - try List.assoc name types - with Not_found -> - command_error (Printf.sprintf "Unknown option \"%s\"" name) - in - let value = - match ty_and_mangler with - | `String, f -> String (f value) - | `Int, f -> - (try - Int (int_of_string (f value)) - with Failure _ -> - command_error (Printf.sprintf "Not an integer value \"%s\"" value)) - in - { status with options = StringMap.add name value status.options } - + status#set_moo_content_rev content' -let get_string_option status name = - match get_option status name with - | String s -> s - | _ -> raise (Option_error (name, "not a string value")) -*) +let get_baseuri status = status#baseuri;; let dump_status status = HLog.message "status.aliases:\n"; HLog.message "status.proof_status:"; HLog.message - (match status.proof_status with + (match status#proof_status with | No_proof -> "no proof\n" | Incomplete_proof _ -> "incomplete proof\n" | Proof _ -> "proof\n" | Intermediate _ -> "Intermediate\n"); HLog.message "status.options\n"; -(* REMOVEME - StringMap.iter (fun k v -> - let v = - match v with - | String s -> s - | Int i -> string_of_int i - in - HLog.message (k ^ "::=" ^ v)) status.options; -*) HLog.message "status.coercions\n"; HLog.message "status.objects:\n"; List.iter - (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects + (fun u -> HLog.message (UriManager.string_of_uri u)) status#objects diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 867e5299e..c30beead0 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -46,15 +46,30 @@ type ng_status = | ProofMode of NTacStatus.tac_status | CommandMode of NEstatus.status -type status = { - moo_content_rev: GrafiteMarshal.moo; - proof_status: proof_status; - objects: UriManager.uri list; - coercions: CoercDb.coerc_db; - automation_cache:AutomationCache.cache; - baseuri: string; - ng_status: ng_status; -} +class status : + GrafiteMarshal.moo -> + proof_status -> + UriManager.uri list -> + CoercDb.coerc_db -> + AutomationCache.cache -> + string -> + ng_status -> + object ('self) + method moo_content_rev: GrafiteMarshal.moo + method set_moo_content_rev: GrafiteMarshal.moo -> 'self + method proof_status: proof_status + method set_proof_status: proof_status -> 'self + method objects: UriManager.uri list + method set_objects: UriManager.uri list -> 'self + method coercions: CoercDb.coerc_db + method set_coercions: CoercDb.coerc_db -> 'self + method automation_cache:AutomationCache.cache + method set_automation_cache:AutomationCache.cache -> 'self + method baseuri: string + method set_baseuri: string -> 'self + method ng_status: ng_status + method set_ng_status: ng_status -> 'self + end val dump_status : status -> unit diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 4bd7390f9..e9965c4ca 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -93,7 +93,7 @@ let _ = let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer grafite_status = sequents_viewer#reset; - match grafite_status.proof_status with + match grafite_status#proof_status with | Incomplete_proof ({ stack = stack } as incomplete_proof) -> sequents_viewer#load_sequents incomplete_proof; (try @@ -107,7 +107,7 @@ let _ = with Failure _ -> script#setGoal None); | Proof proof -> sequents_viewer#load_logo_with_qed | No_proof -> - (match grafite_status.ng_status with + (match grafite_status#ng_status with ProofMode nstatus -> sequents_viewer#nload_sequents nstatus; (try @@ -182,7 +182,7 @@ let _ = CicNotationParser.print_l2_pattern; addDebugItem "dump moo to stderr" (fun _ -> let grafite_status = (MatitaScript.current ())#grafite_status in - let moo = grafite_status.moo_content_rev in + let moo = grafite_status#moo_content_rev in List.iter (fun cmd -> prerr_endline @@ -203,7 +203,7 @@ let _ = HLog.debug (CicPp.ppterm (match - (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status + (MatitaScript.current ())#grafite_status#proof_status with | GrafiteTypes.No_proof -> (Cic.Implicit None) | Incomplete_proof i -> @@ -218,7 +218,7 @@ let _ = ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") (match - (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status + (MatitaScript.current ())#grafite_status#proof_status with | GrafiteTypes.No_proof -> assert false | Incomplete_proof i -> diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index c5906e16a..7b5a929cb 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -73,7 +73,7 @@ let save_moo grafite_status = let script = MatitaScript.current () in let baseuri = GrafiteTypes.get_baseuri grafite_status in let no_pstatus = - grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof + grafite_status#proof_status = GrafiteTypes.No_proof in match script#bos, script#eos, no_pstatus with | true, _, _ -> () @@ -85,8 +85,7 @@ let save_moo grafite_status = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in - GrafiteMarshal.save_moo moo_fname - grafite_status.GrafiteTypes.moo_content_rev; + GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index e93ac4f3c..22ad1e4cf 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1334,7 +1334,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; - match self#script#grafite_status.proof_status with + match self#script#grafite_status#proof_status with | Proof (uri, metasenv, _subst, bo, ty, attrs) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = @@ -1348,7 +1348,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_loadObj obj | _ -> - match self#script#grafite_status.ng_status with + match self#script#grafite_status#ng_status with ProofMode tstatus -> self#_loadNObj tstatus#obj | _ -> self#blank () diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 8de5ccebc..108b23237 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -485,7 +485,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [({grafite_status with proof_status = No_proof}), parsed_text ],"", + [(grafite_status#set_proof_status No_proof), parsed_text ],"", parsed_text_length | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in @@ -512,7 +512,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status let (_,menv,subst,_,_,_), _ = ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params - ~automation_cache:grafite_status.GrafiteTypes.automation_cache) + ~automation_cache:grafite_status#automation_cache) proof_status in let proof_term = @@ -802,7 +802,7 @@ object (self) buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext; (* here we need to set the Goal in case we are going to cursor (or to bottom) and we will face a macro *) - match self#grafite_status.proof_status with + match self#grafite_status#proof_status with Incomplete_proof p -> userGoal <- (try Some (Continuationals.Stack.find_goal p.stack) @@ -1094,7 +1094,7 @@ object (self) HLog.error "The script is too big!\n" method onGoingProof () = - match self#grafite_status.proof_status with + match self#grafite_status#proof_status with | No_proof | Proof _ -> false | Incomplete_proof _ -> true | Intermediate _ -> assert false diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 268da7e51..b52e75741 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -149,7 +149,7 @@ let rec interactive_loop () = | `Do command -> let str = Ulexing.from_utf8_string command in let watch_statuses grafite_status = - match grafite_status.GrafiteTypes.proof_status with + match grafite_status#proof_status with GrafiteTypes.Incomplete_proof {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; GrafiteTypes.stack = stack } -> @@ -225,7 +225,7 @@ let main () = let proof_status,moo_content_rev,lexicon_content_rev,dump = match !grafite_status with | s::_ -> - s.proof_status, s.moo_content_rev, + s#proof_status, s#moo_content_rev, (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev, (GrafiteTypes.get_estatus s)#dump | _ -> assert false diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index baac2409c..18b406708 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -99,7 +99,7 @@ let dump f = ;; let get_macro_context = function - | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> [] + | Some status when status#proof_status = GrafiteTypes.No_proof -> [] | Some status -> let stack = GrafiteTypes.get_stack status in let goal = Continuationals.Stack.find_goal stack in @@ -257,7 +257,7 @@ let compile atstart options fname = in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = - grafite_status.proof_status, grafite_status.moo_content_rev, + grafite_status#proof_status, grafite_status#moo_content_rev, (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev in if proof_status <> GrafiteTypes.No_proof then