From e66e67d2f9f2772d63a7457e386f9616f62a2f39 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jan 2006 18:45:58 +0000 Subject: [PATCH] Bug fixed: macros in the middle of a goto cursor or goto end-of-script were not executed. Explanation: the current goal was set only externally, but it is used by macro disambiguation. To fix the bug I have finally changed the type of a "lazy_macro" so that its input is now a context. it used to be an integer, the selected goal; however, the integer does not make sense since a macro can be invoked also when there is no current proof. --- helm/matita/matita.ml | 7 +- helm/matita/matitaEngine.ml | 5 +- helm/matita/matitaScript.ml | 96 +++++++++++++-------- helm/matita/matitaScript.mli | 4 +- helm/ocaml/grafite_engine/grafiteEngine.ml | 8 +- helm/ocaml/grafite_engine/grafiteEngine.mli | 6 +- 6 files changed, 79 insertions(+), 47 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 9e96651fe..69b14b819 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -81,9 +81,14 @@ let _ = match grafite_status.proof_status with | Incomplete_proof ({ stack = stack } as incomplete_proof) -> sequents_viewer#load_sequents incomplete_proof; + let goal = + match script#goal with + None -> assert false + | Some n -> n + in (try script#setGoal (Continuationals.Stack.find_goal stack); - sequents_viewer#goto_sequent script#goal + sequents_viewer#goto_sequent goal with Failure _ -> script#setGoal ~-1); | Proof proof -> sequents_viewer#load_logo_with_qed | No_proof -> sequents_viewer#load_logo diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 6fca24b13..f0d8ee46c 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -53,13 +53,12 @@ let disambiguate_command lexicon_status_ref grafite_status cmd = lexicon_status_ref := lexicon_status; GrafiteTypes.set_metasenv metasenv grafite_status,cmd -let disambiguate_macro lexicon_status_ref grafite_status macro goal = +let disambiguate_macro lexicon_status_ref grafite_status macro context = let metasenv,macro = GrafiteDisambiguate.disambiguate_macro lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) - (GrafiteTypes.get_proof_context grafite_status goal) - macro + context macro in GrafiteTypes.set_metasenv metasenv grafite_status,macro diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 469676fa7..a0d0944ca 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -35,6 +35,7 @@ let debug_print = if debug then prerr_endline else ignore (** raised when one of the script margins (top or bottom) is reached *) exception Margin +exception NoUnfinishedProof let safe_substring s i j = try String.sub s i j with Invalid_argument _ -> assert false @@ -264,8 +265,13 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu [], parsed_text_length (* REAL macro *) | TA.Hint loc -> + let user_goal' = + match user_goal with + Some n -> n + | None -> raise NoUnfinishedProof + in let proof = GrafiteTypes.get_current_proof grafite_status in - let proof_status = proof,user_goal in + let proof_status = proof,user_goal' in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in (match selected with @@ -298,7 +304,10 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu assert false) | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = GrafiteTypes.get_proof_context grafite_status user_goal in + let context = + match user_goal with + None -> [] + | Some n -> GrafiteTypes.get_proof_context grafite_status n in let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); @@ -340,7 +349,11 @@ and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_stat with MatitaTypes.Cancel -> [], 0 | GrafiteEngine.Macro (_loc,lazy_macro) -> - let grafite_status,macro = lazy_macro user_goal in + let context = + match user_goal with + None -> [] + | Some n -> GrafiteTypes.get_proof_context grafite_status n in + let grafite_status,macro = lazy_macro context in eval_macro buffer guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script macro @@ -449,7 +462,7 @@ object (self) * Invariant: this list length is 1 + length of statements *) (** goal as seen by the user (i.e. metano corresponding to current tab) *) - val mutable userGoal = ~-1 + val mutable userGoal = None (** text mark and tag representing locked part of a script *) val locked_mark = @@ -467,33 +480,37 @@ object (self) method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false method private _advance ?statement () = - let rec aux st = - let (entries, parsed_len) = - eval_statement buffer guistuff self#lexicon_status self#grafite_status - userGoal self st - in - let new_statuses, new_statements = - let statuses, texts = List.split entries in - statuses, texts - in - history <- new_statuses @ history; - statements <- new_statements @ statements; - let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" (List.rev new_statements) in - if statement <> None then - buffer#insert ~iter:start new_text - else begin - let s = match st with `Raw s | `Ast (_, s) -> s in - if new_text <> String.sub s 0 parsed_len then begin - buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len); - buffer#insert ~iter:start new_text; - end; - end; - self#moveMark (String.length new_text) - in - let s = match statement with Some s -> s | None -> self#getFuture in - HLog.debug ("evaluating: " ^ first_line s ^ " ..."); - (try aux (`Raw s) with End_of_file -> raise Margin) + let s = match statement with Some s -> s | None -> self#getFuture in + HLog.debug ("evaluating: " ^ first_line s ^ " ..."); + let (entries, parsed_len) = + try + eval_statement buffer guistuff self#lexicon_status self#grafite_status + userGoal self (`Raw s) + with End_of_file -> raise Margin + in + let new_statuses, new_statements = + let statuses, texts = List.split entries in + statuses, texts + in + history <- new_statuses @ history; + statements <- new_statements @ statements; + let start = buffer#get_iter_at_mark (`MARK locked_mark) in + let new_text = String.concat "" (List.rev new_statements) in + if statement <> None then + buffer#insert ~iter:start new_text + else begin + if new_text <> String.sub s 0 parsed_len then begin + buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len); + buffer#insert ~iter:start new_text; + end; + end; + self#moveMark (String.length new_text); + (* 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 + Incomplete_proof p -> + userGoal <- Some (Continuationals.Stack.find_goal p.stack) + | _ -> userGoal <- None method private _retract offset lexicon_status grafite_status new_statements new_history @@ -618,7 +635,7 @@ object (self) method private reset_buffer = statements <- []; history <- [ initial_statuses ]; - userGoal <- ~-1; + userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter @@ -727,12 +744,21 @@ object (self) (* method proofStatus = MatitaTypes.get_proof_status self#status *) method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status + method proofContext = - GrafiteTypes.get_proof_context self#grafite_status userGoal + match userGoal with + None -> assert false + | Some n -> + GrafiteTypes.get_proof_context self#grafite_status n + method proofConclusion = - GrafiteTypes.get_proof_conclusion self#grafite_status userGoal + match userGoal with + None -> assert false + | Some n -> + GrafiteTypes.get_proof_conclusion self#grafite_status n + method stack = GrafiteTypes.get_stack self#grafite_status - method setGoal n = userGoal <- n + method setGoal n = userGoal <- Some n method goal = userGoal method eos = diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index c9e60943b..edebcf322 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +exception NoUnfinishedProof + class type script = object @@ -66,7 +68,7 @@ object method stack: Continuationals.Stack.t (** @raise Statement_error *) method setGoal: int -> unit - method goal: int + method goal: int option (** end of script, true if the whole script has been executed *) method eos: bool diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml index 5614ff23a..26d7712d3 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -27,9 +27,9 @@ exception Drop exception IncludedFileNotCompiled of string (* file name *) -(* the integer is expected to be the goal the user is currently seeing *) exception Macro of - GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) + GrafiteAst.loc * + (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) type options = { do_heavy_checks: bool ; @@ -338,7 +338,7 @@ type eval_ast = disambiguate_macro: (GrafiteTypes.status -> 'term GrafiteAst.macro -> - int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> @@ -374,7 +374,7 @@ type 'a eval_executable = disambiguate_macro: (GrafiteTypes.status -> 'term GrafiteAst.macro -> - int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> options -> GrafiteTypes.status -> diff --git a/helm/ocaml/grafite_engine/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli index a87bb5a95..ee5f3a157 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.mli +++ b/helm/ocaml/grafite_engine/grafiteEngine.mli @@ -25,9 +25,9 @@ exception Drop exception IncludedFileNotCompiled of string -(* the integer is expected to be the goal the user is currently seeing *) exception Macro of - GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) + GrafiteAst.loc * + (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) val eval_ast : disambiguate_tactic: @@ -45,7 +45,7 @@ val eval_ast : disambiguate_macro: (GrafiteTypes.status -> 'term GrafiteAst.macro -> - int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> -- 2.39.2