From: Stefano Zacchiroli Date: Tue, 25 Oct 2005 13:49:08 +0000 (+0000) Subject: new tacticals X-Git-Tag: V_0_7_2_3~192 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git new tacticals --- diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index d8daa1fd7..85418121f 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -43,6 +43,7 @@ let script_template = runtime_base_dir ^ "/matita.ma.templ" let core_notation_script = runtime_base_dir ^ "/core_notation.moo" let coq_notation_script = runtime_base_dir ^ "/coq.moo" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" +let closed_xml = runtime_base_dir ^ "/closed.xml" let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml" let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in" diff --git a/helm/matita/closed.xml b/helm/matita/closed.xml new file mode 100644 index 000000000..d3125efb7 --- /dev/null +++ b/helm/matita/closed.xml @@ -0,0 +1,17 @@ + + + + + + + + + + + + This goal has already been closed. + Use the "skip" command to throw it away. + + + + diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index bad92774b..6f154dded 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -49,6 +49,7 @@ lablgtk2.glade \ lablgtkmathview \ lablgtksourceview \ helm-xmldiff \ +helm-tactics \ " for r in $FINDLIB_REQUIRES do diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 9c40b8efa..ecb2e4061 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -877,7 +877,7 @@ - + True gtk-new 1 @@ -898,7 +898,7 @@ - + True gtk-open 1 @@ -919,7 +919,7 @@ - + True gtk-save 1 @@ -940,7 +940,7 @@ - + True gtk-save-as 1 @@ -961,7 +961,7 @@ - + True gtk-execute 1 @@ -988,7 +988,7 @@ - + True gtk-quit 1 @@ -1023,7 +1023,7 @@ - + True gtk-undo 1 @@ -1045,7 +1045,7 @@ - + True gtk-redo 1 @@ -1072,7 +1072,7 @@ - + True gtk-cut 1 @@ -1093,7 +1093,7 @@ - + True gtk-copy 1 @@ -1114,7 +1114,7 @@ - + True gtk-paste 1 @@ -1134,7 +1134,7 @@ True - + True gtk-delete 1 @@ -1170,12 +1170,12 @@ True - _Find & Replace + _Find & Replace ... True - + True gtk-find-and-replace 1 @@ -1187,6 +1187,20 @@ + + + + True + + + + + + True + Edit with E_xternal Editor + True + + @@ -1251,7 +1265,7 @@ - + True gtk-zoom-in 1 @@ -1273,7 +1287,7 @@ - + True gtk-zoom-out 1 @@ -1294,7 +1308,7 @@ - + True gtk-zoom-100 1 @@ -1346,7 +1360,7 @@ True - + True gtk-about 1 diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 5e2526748..b9e09f24d 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -77,9 +77,12 @@ let _ = let sequents_observer status = sequents_viewer#reset; match status.proof_status with - | Incomplete_proof ((proof, goal) as status) -> - sequents_viewer#load_sequents status; - sequents_viewer#goto_sequent goal + | Incomplete_proof ({ stack = stack } as incomplete_proof) -> + sequents_viewer#load_sequents incomplete_proof; + (try + script#setGoal (Continuationals.Stack.find_goal stack); + sequents_viewer#goto_sequent script#goal + with Failure _ -> script#setGoal ~-1); | Proof proof -> sequents_viewer#load_logo_with_qed | No_proof -> sequents_viewer#load_logo | Intermediate _ -> assert false (* only the engine may be in this state *) @@ -138,12 +141,19 @@ let _ = addDebugItem "print top-level grammar entries" CicNotationParser.print_l2_pattern; addDebugItem "dump moo to stderr" (fun _ -> - let status = (MatitaScript.instance ())#status in + let status = (MatitaScript.current ())#status in let moo, metadata = status.moo_content_rev in List.iter (fun cmd -> prerr_endline (GrafiteAstPp.pp_command cmd)) (List.rev moo); List.iter (fun m -> prerr_endline (GrafiteAstPp.pp_metadata m)) metadata); + addDebugItem "print metasenv goals and stack to stderr" + (fun _ -> + prerr_endline ("metasenv goals: " ^ String.concat " " + (List.map (fun (g, _, _) -> string_of_int g) + (MatitaScript.current ())#proofMetasenv)); + prerr_endline ("stack: " ^ Continuationals.Stack.pp + (MatitaMisc.get_stack (MatitaScript.current ())#status))); addDebugItem "rotate light bulbs" (fun _ -> let nb = gui#main#hintNotebook in diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index cffb9cf44..9595df931 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -40,11 +40,6 @@ type options = { clean_baseuri: bool } -type statement = - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, - string) - GrafiteAst.statement - (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) @@ -160,14 +155,19 @@ let singleton = function | [x], _ -> x | _ -> assert false -let disambiguate_term status_ref term = + (** @param term not meaningful when context is given *) +let disambiguate_term ?context status_ref goal term = let status = !status_ref in + let context = + match context with + | Some c -> c + | None -> MatitaMisc.get_proof_context status goal + in let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) - ~context:(MatitaMisc.get_proof_context status) - ~metasenv:(MatitaMisc.get_proof_metasenv status) term) + ~context ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status diff in @@ -216,15 +216,15 @@ let disambiguate_reduction_kind aliases_ref = function | `Unfold None | `Whd as kind -> kind -let disambiguate_tactic status tactic = +let disambiguate_tactic status goal tactic = let status_ref = ref status in let tactic = match tactic with | GrafiteAst.Absurd (loc, term) -> - let cic = disambiguate_term status_ref term in + let cic = disambiguate_term status_ref goal term in GrafiteAst.Absurd (loc, cic) | GrafiteAst.Apply (loc, term) -> - let cic = disambiguate_term status_ref term in + let cic = disambiguate_term status_ref goal term in GrafiteAst.Apply (loc, cic) | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> @@ -236,19 +236,21 @@ let disambiguate_tactic status tactic = | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id) | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id) | GrafiteAst.Compare (loc,term) -> - let term = disambiguate_term status_ref term in + let term = disambiguate_term status_ref goal term in GrafiteAst.Compare (loc,term) | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n) | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc | GrafiteAst.Cut (loc, ident, term) -> - let cic = disambiguate_term status_ref term in + let cic = disambiguate_term status_ref goal term in GrafiteAst.Cut (loc, ident, cic) | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc | GrafiteAst.Decompose (loc, types, what, names) -> let disambiguate types = function | GrafiteAst.Type _ -> assert false | GrafiteAst.Ident id -> - (match disambiguate_term status_ref (CicNotationPt.Ident (id, None)) with + (match disambiguate_term status_ref goal + (CicNotationPt.Ident (id, None)) + with | Cic.MutInd (uri, tyno, _) -> (GrafiteAst.Type (uri, tyno) :: types) | _ -> raise Disambiguate.NoWellTypedInterpretation) @@ -256,24 +258,24 @@ let disambiguate_tactic status tactic = let types = List.fold_left disambiguate [] types in GrafiteAst.Decompose (loc, types, what, names) | GrafiteAst.Discriminate (loc,term) -> - let term = disambiguate_term status_ref term in + let term = disambiguate_term status_ref goal term in GrafiteAst.Discriminate(loc,term) | GrafiteAst.Exact (loc, term) -> - let cic = disambiguate_term status_ref term in + let cic = disambiguate_term status_ref goal term in GrafiteAst.Exact (loc, cic) | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref what in - let using = disambiguate_term status_ref using in + let what = disambiguate_term status_ref goal what in + let using = disambiguate_term status_ref goal using in GrafiteAst.Elim (loc, what, Some using, depth, idents) | GrafiteAst.Elim (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref what in + let what = disambiguate_term status_ref goal what in GrafiteAst.Elim (loc, what, None, depth, idents) | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> - let what = disambiguate_term status_ref what in - let using = disambiguate_term status_ref using in + let what = disambiguate_term status_ref goal what in + let using = disambiguate_term status_ref goal using in GrafiteAst.ElimType (loc, what, Some using, depth, idents) | GrafiteAst.ElimType (loc, what, None, depth, idents) -> - let what = disambiguate_term status_ref what in + let what = disambiguate_term status_ref goal what in GrafiteAst.ElimType (loc, what, None, depth, idents) | GrafiteAst.Exists loc -> GrafiteAst.Exists loc | GrafiteAst.Fail loc -> GrafiteAst.Fail loc @@ -291,20 +293,20 @@ let disambiguate_tactic status tactic = | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g) | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc | GrafiteAst.Injection (loc, term) -> - let term = disambiguate_term status_ref term in + let term = disambiguate_term status_ref goal term in GrafiteAst.Injection (loc,term) | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> let f term to_what = - let term = disambiguate_term status_ref term in + let term = disambiguate_term status_ref goal term in term :: to_what in let to_what = List.fold_right f to_what [] in - let what = disambiguate_term status_ref what in + let what = disambiguate_term status_ref goal what in GrafiteAst.LApply (loc, depth, to_what, what, ident) | GrafiteAst.Left loc -> GrafiteAst.Left loc | GrafiteAst.LetIn (loc, term, name) -> - let term = disambiguate_term status_ref term in + let term = disambiguate_term status_ref goal term in GrafiteAst.LetIn (loc,term,name) | GrafiteAst.Reduce (loc, red_kind, pattern) -> let pattern = disambiguate_pattern status_ref pattern in @@ -316,7 +318,7 @@ let disambiguate_tactic status tactic = let with_what = disambiguate_lazy_term status_ref with_what in GrafiteAst.Replace (loc, pattern, with_what) | GrafiteAst.Rewrite (loc, dir, t, pattern) -> - let term = disambiguate_term status_ref t in + let term = disambiguate_term status_ref goal t in let pattern = disambiguate_pattern status_ref pattern in GrafiteAst.Rewrite (loc, dir, term, pattern) | GrafiteAst.Right loc -> GrafiteAst.Right loc @@ -324,13 +326,17 @@ let disambiguate_tactic status tactic = | GrafiteAst.Split loc -> GrafiteAst.Split loc | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc | GrafiteAst.Transitivity (loc, term) -> - let cic = disambiguate_term status_ref term in + let cic = disambiguate_term status_ref goal term in GrafiteAst.Transitivity (loc, cic) in status_ref, tactic let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= let module PEH = ProofEngineHelpers in +(* let print_m name metasenv = + prerr_endline (">>>>> " ^ name); + prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) + in *) (* phase one calculates: * new_goals_from_refine: goals added by refine * head_goal: the first goal opened by ythe tactic @@ -370,9 +376,13 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= if always_opens_a_goal then metas_for_tactic_head @ metas_for_refine_goals @ metas_for_tactic_goals - else + else begin +(* print_m "metas_for_refine_goals" metas_for_refine_goals; + print_m "metas_for_tactic_head" metas_for_tactic_head; + print_m "metas_for_tactic_goals" metas_for_tactic_goals; *) metas_for_refine_goals @ metas_for_tactic_head @ metas_for_tactic_goals + end in let goals = List.map (fun (metano, _, _) -> metano) produced_metas in produced_metas, goals @@ -407,11 +417,7 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= let after = extract after_l in before, after in - (* DEBUG CODE - let print_m name metasenv = - prerr_endline (">>>>> " ^ name); - prerr_endline (CicMetaSubst.ppmetasenv metasenv []) - in +(* |+ DEBUG CODE +| print_m "BEGIN" start; prerr_endline ("goal was: " ^ string_of_int current_goal); prerr_endline ("and metas from refine are:"); @@ -423,8 +429,9 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= print_m "metas_for_tactic_head" metas_for_tactic_head; print_m "metas_for_refine_goals" metas_for_refine_goals; print_m "metas_for_tactic_goals" metas_for_tactic_goals; + print_m "produced_metas" produced_metas; print_m "after" after; - FINE DEBUG CODE *) +|+ FINE DEBUG CODE +| *) before @ produced_metas @ after, goals (* maybe we only need special cases for apply and goal *) @@ -439,96 +446,130 @@ let classify_tactic tactic = | GrafiteAst.IdTac _ | GrafiteAst.Generalize _ | GrafiteAst.Elim _ + | GrafiteAst.Cut _ | GrafiteAst.Decompose _ -> true, true (* tactics we don't want to reorder goals. I think only Goal needs this. *) | GrafiteAst.Goal _ -> false, true (* tactics like apply *) | _ -> true, false -let apply_tactic tactic status = +let apply_tactic tactic (status, goal) = +(* prerr_endline "apply_tactic"; *) +(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *) let starting_metasenv = MatitaMisc.get_proof_metasenv status in - let status_ref, tactic = disambiguate_tactic status tactic in + let before = List.map (fun g, _, _ -> g) starting_metasenv in +(* prerr_endline "disambiguate"; *) + let status_ref, tactic = disambiguate_tactic status goal tactic in let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in - let proof_status = MatitaMisc.get_proof_status !status_ref in + let proof = MatitaMisc.get_current_proof !status_ref in + let proof_status = proof, goal in let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in (* apply tactic will change the status pointed by status_ref ... *) - let current_goal = let _, g = proof_status in g in - let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in - let proof, goals = - if needs_reordering then +(* prerr_endline "apply_tactic bassa"; *) + let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in + let after = ProofEngineTypes.goals_of_proof proof in + let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in +(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before)); +prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after)); +prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *) +(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals)); +prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) + let proof, opened_goals = + if needs_reordering then begin let uri, metasenv_after_tactic, t, ty = proof in - let reordered_metasenv, goals = - reorder_metasenv starting_metasenv metasenv_after_refinement - metasenv_after_tactic goals current_goal always_opens_a_goal in - (uri, reordered_metasenv, t, ty), goals - else - proof, goals +(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) + let reordered_metasenv, opened_goals = + reorder_metasenv + starting_metasenv + metasenv_after_refinement metasenv_after_tactic + opened goal always_opens_a_goal + in + let proof' = uri, reordered_metasenv, t, ty in +(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) + proof', opened_goals + end + else + proof, opened_goals in - let dummy = -1 in - { !status_ref with - proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, - goals + let incomplete_proof = + match !status_ref.proof_status with + | Incomplete_proof p -> p + | _ -> assert false + in + { !status_ref with proof_status = + Incomplete_proof { incomplete_proof with proof = proof } }, + opened_goals, closed_goals module MatitaStatus = - struct - type input_status = MatitaTypes.status - type output_status = MatitaTypes.status * ProofEngineTypes.goal list - type tactic = input_status -> output_status +struct + type input_status = MatitaTypes.status * ProofEngineTypes.goal - let focus (status,_) goal = - let proof,_ = MatitaMisc.get_proof_status status in - {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)} + type output_status = + MatitaTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list - let goals (_,goals) = goals - - let set_goals (status,_) goals = status,goals - - let id_tac status = - apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status + type tactic = input_status -> output_status + let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) let mk_tactic tac = tac - let apply_tactic tac = tac + let goals (_, opened, closed) = opened, closed + let set_goals (opened, closed) (status, _, _) = (status, opened, closed) + let get_stack (status, _) = MatitaMisc.get_stack status - end + let set_stack stack (status, opened, closed) = + MatitaMisc.set_stack stack status, opened, closed -module MatitaTacticals = Tacticals.Make(MatitaStatus) + let inject (status, _) = (status, [], []) + let focus goal (status, _, _) = (status, goal) +end + +module MatitaTacticals = Tacticals.Make (MatitaStatus) let eval_tactical status tac = - let rec tactical_of_ast tac = - match tac with - | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic + let rec tactical_of_ast l tac = + match tac with + | GrafiteAst.Tactic (loc, tactic) -> + MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic)) | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals) - | GrafiteAst.Do (loc, num, tactical) -> - MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical) + assert (l > 0); + MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals) + | GrafiteAst.Do (loc, n, tactical) -> + MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical) | GrafiteAst.Repeat (loc, tactical) -> - MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical) + MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical) | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - MatitaTacticals.thens ~start:(tactical_of_ast tactical) - ~continuations:(List.map tactical_of_ast tacticals) + assert (l > 0); + MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical) + ~continuations:(List.map (tactical_of_ast (l+1)) tacticals) | GrafiteAst.First (loc, tacticals) -> MatitaTacticals.first - ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals) + ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) | GrafiteAst.Try (loc, tactical) -> - MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical) + MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical) | GrafiteAst.Solve (loc, tacticals) -> MatitaTacticals.solve_tactics - ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals) - in - let status,goals = tactical_of_ast tac status in - let proof,_ = MatitaMisc.get_proof_status status in - let new_status = - match goals with - | [] -> - let (_,metasenv,_,_) = proof in - (match metasenv with - | [] -> Proof proof - | (ng,_,_)::_ -> Incomplete_proof (proof,ng)) - | ng::_ -> Incomplete_proof (proof, ng) + ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals) + + | GrafiteAst.Skip loc -> MatitaTacticals.skip + | GrafiteAst.Dot loc -> MatitaTacticals.dot + | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon + | GrafiteAst.Branch loc -> MatitaTacticals.branch + | GrafiteAst.Shift loc -> MatitaTacticals.shift + | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i + | GrafiteAst.Merge loc -> MatitaTacticals.merge + | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals + | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus + in + let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in + let status = (* is proof completed? *) + match status.proof_status with + | Incomplete_proof { stack = stack; proof = proof } + when Continuationals.Stack.is_empty stack -> + { status with proof_status = Proof proof } + | _ -> status in - { status with proof_status = new_status } + status let eval_coercion status coercion = let coer_uri,coer_ty = @@ -669,7 +710,7 @@ let disambiguate_command status = status,cmd | GrafiteAst.Coercion (loc, term) -> let status_ref = ref status in - let term = disambiguate_term status_ref term in + let term = disambiguate_term ~context:[] status_ref ~-1 term in !status_ref, GrafiteAst.Coercion (loc,term) | GrafiteAst.Obj (loc,obj) -> let status,obj = disambiguate_obj status obj in @@ -743,7 +784,7 @@ let eval_command opts status cmd = command_error ("Someone allows to start a thm without giving the "^ "name/uri. This should be fixed!") - | _-> command_error "You can't qed an uncomplete theorem" + | _-> command_error "You can't Qed an incomplete theorem" in let suri = UriManager.string_of_uri uri in if metasenv <> [] then @@ -836,7 +877,9 @@ let eval_command opts status cmd = match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in let initial_proof = (Some uri, metasenv, bo, ty) in - { status with proof_status = Incomplete_proof (initial_proof,goalno)} + let initial_stack = Continuationals.Stack.of_metasenv metasenv in + { status with proof_status = + Incomplete_proof { proof = initial_proof; stack = initial_stack } } | _ -> if metasenv <> [] then command_error ( @@ -868,7 +911,10 @@ let eval_command opts status cmd = let eval_executable opts status ex = match ex with - | GrafiteAst.Tactical (_, tac) -> eval_tactical status tac + | GrafiteAst.Tactical (_, tac, None) -> eval_tactical status tac + | GrafiteAst.Tactical (_, tac, Some punct) -> + let status = eval_tactical status tac in + eval_tactical status punct | GrafiteAst.Command (_, cmd) -> eval_command opts status cmd | GrafiteAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" @@ -943,7 +989,7 @@ let eval_from_stream_greedy let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = eval_from_stream ?do_heavy_checks ?include_paths ?clean_baseuri status - (Ulexing.from_utf8_string str) (fun _ _ ->()) + (Ulexing.from_utf8_string str) (fun _ _ -> ()) let default_options () = (* diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 2253748d9..e8cdbad0e 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -27,11 +27,6 @@ exception Drop exception UnableToInclude of string exception IncludedFileNotCompiled of string -type statement = - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, - string) - GrafiteAst.statement - (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) val eval_string: @@ -45,7 +40,7 @@ val eval_from_stream: ?include_paths:string list -> ?clean_baseuri:bool -> MatitaTypes.status ref -> Ulexing.lexbuf -> - (MatitaTypes.status -> statement -> unit) -> + (MatitaTypes.status -> GrafiteParser.statement -> unit) -> unit val eval_from_stream_greedy: @@ -53,7 +48,7 @@ val eval_from_stream_greedy: ?include_paths:string list -> ?clean_baseuri:bool -> MatitaTypes.status ref-> Ulexing.lexbuf -> - (MatitaTypes.status -> statement -> unit) -> + (MatitaTypes.status -> GrafiteParser.statement -> unit) -> unit val eval_ast: @@ -61,7 +56,7 @@ val eval_ast: ?include_paths:string list -> ?clean_baseuri:bool -> MatitaTypes.status -> - statement -> + GrafiteParser.statement -> MatitaTypes.status val initial_status: MatitaTypes.status lazy_t diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index fce5cf6d9..d6cddfaab 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -49,5 +49,6 @@ let to_string = (".moo file '%s' has been compiled by a different version of matita, " ^^ "please recompile it") fname + | Continuationals.Error s -> "Tactical error: " ^ Lazy.force s | exn -> "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 686f54399..0ad36dfee 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -307,7 +307,9 @@ let report_error ~title ~message ?parent () = | PopupClosed -> () -let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = +let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) + ?default () += let dialog = gui#newEmptyDialog () in dialog#emptyDialog#set_title title; dialog#emptyDialogLabel#set_label msg; @@ -324,11 +326,22 @@ let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add () in let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in + let buffer = view#buffer in + (match default with + | None -> () + | Some text -> + buffer#set_text text; + buffer#select_range buffer#start_iter buffer#end_iter); view#misc#grab_focus (); connect_button dialog#emptyDialogOkButton (fun _ -> - return (Some (view#buffer#get_text ()))) + return (Some (buffer#get_text ()))) end else begin (* monoline input required: use a TextEntry widget *) let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in + (match default with + | None -> () + | Some text -> + entry#set_text text; + entry#select_region ~start:0 ~stop:max_int); entry#misc#grab_focus (); connect_button dialog#emptyDialogOkButton (fun _ -> return (Some entry#text)) diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 91a3e495b..e5d0e9be9 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -137,5 +137,7 @@ val report_error: * for prompting the user otherwise a TextEntry widget will be * @return the string given by the user *) val ask_text: - gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string + gui:#gui -> + ?title:string -> ?msg:string -> ?multiline:bool -> ?default:string -> unit -> + string diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5c5b24c4d..bf25a5493 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -69,7 +69,7 @@ let ask_and_save_moo_if_needed parent fname status = let save () = let moo_fname = MatitaMisc.obj_file_of_script fname in MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in - if (MatitaScript.instance ())#eos && + if (MatitaScript.current ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then begin @@ -218,7 +218,7 @@ class gui () = let safe_undo = fun () -> (* phase 1: we save the actual status of the marks and we undo *) - let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in + let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in let locked_iter_offset = locked_iter#offset in let mark2 = @@ -246,7 +246,7 @@ class gui () = if mark_iter#offset < locked_iter_offset then begin source_view#buffer#move_mark `INSERT ~where:mark_iter; - (MatitaScript.instance ())#goto `Cursor (); + (MatitaScript.current ())#goto `Cursor (); end; (* phase 4: we perform again the undo. This time we are sure that the text to undo is not locked *) @@ -256,7 +256,7 @@ class gui () = fun () -> (* phase 1: we save the actual status of the marks, we redo and we undo *) - let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in + let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in let locked_iter_offset = locked_iter#offset in let mark2 = @@ -284,7 +284,7 @@ class gui () = if mark_iter#offset < locked_iter_offset then begin source_view#buffer#move_mark `INSERT ~where:mark_iter; - (MatitaScript.instance ())#goto `Cursor (); + (MatitaScript.current ())#goto `Cursor (); end; (* phase 4: we perform again the redo. This time we are sure that the text to redo is not locked *) @@ -352,13 +352,14 @@ class gui () = | Some (s :: _) -> clipboard#set_text s); connect_menu_item main#pasteMenuItem (fun () -> source_view#buffer#paste_clipboard clipboard; - (MatitaScript.instance ())#clean_dirty_lock); + (MatitaScript.current ())#clean_dirty_lock); connect_menu_item main#deleteMenuItem (fun () -> ignore (source_view#buffer#delete_selection ())); connect_menu_item main#selectAllMenuItem (fun () -> source_buffer#move_mark `INSERT source_buffer#start_iter; source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); connect_menu_item main#findReplMenuItem show_find_Repl; + connect_menu_item main#externalEditorMenuItem self#externalEditor; ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = @@ -520,13 +521,13 @@ class gui () = let hole = CicNotationPt.UserInput in let loc = DisambiguateTypes.dummy_floc in let tac ast _ = - if (MatitaScript.instance ())#onGoingProof () then - (MatitaScript.instance ())#advance + if (MatitaScript.current ())#onGoingProof () then + (MatitaScript.current ())#advance ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) () in let tac_w_term ast _ = - if (MatitaScript.instance ())#onGoingProof () then + if (MatitaScript.current ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ GrafiteAstPp.pp_tactic ast) @@ -581,7 +582,7 @@ class gui () = source_buffer#set_language matita_lang; source_buffer#set_highlight true in - let s () = MatitaScript.instance () in + let s () = MatitaScript.current () in let disableSave () = script_fname <- None; main#saveMenuItem#misc#set_sensitive false @@ -642,11 +643,11 @@ class gui () = let cursor () = source_buffer#place_cursor (source_buffer#get_iter_at_mark (`NAME "locked")) in - let advance _ = (MatitaScript.instance ())#advance (); cursor () in - let retract _ = (MatitaScript.instance ())#retract (); cursor () in - let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in - let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in - let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in + let advance _ = (MatitaScript.current ())#advance (); cursor () in + let retract _ = (MatitaScript.current ())#retract (); cursor () in + let top _ = (MatitaScript.current ())#goto `Top (); cursor () in + let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in + let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in let advance = locker (keep_focus advance) in let retract = locker (keep_focus retract) in let top = locker (keep_focus top) in @@ -660,7 +661,7 @@ class gui () = in (* quit *) self#setQuitCallback (fun () -> - let status = (MatitaScript.instance ())#status in + let status = (MatitaScript.current ())#status in if source_view#buffer#modified then begin let rc = ask_unsaved main#toplevel in @@ -733,7 +734,7 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* source_view *) ignore(source_view#connect#after#paste_clipboard - ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock)); + ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock)); (* clean_locked is set to true only "during" a PRIMARY paste operation (i.e. by clicking with the second mouse button) *) let clean_locked = ref false in @@ -750,11 +751,11 @@ class gui () = ~callback:( fun tag ~start:_ ~stop:_ -> if !clean_locked && - tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid + tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid then begin clean_locked := false; - (MatitaScript.instance ())#clean_dirty_lock; + (MatitaScript.current ())#clean_dirty_lock; clean_locked := true end)); (* math view handling *) @@ -774,8 +775,64 @@ class gui () = MatitaMathView.update_font_sizes ()); MatitaMathView.reset_font_size (); + method private externalEditor () = + let cmd = Helm_registry.get "matita.external_editor" in +(* ZACK uncomment to enable interactive ask of external editor command *) +(* let cmd = + let msg = + "External editor command: +%f will be substitute for the script name, +%p for the cursor position in bytes, +%l for the execution point in bytes." + in + ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false + ~default:(Helm_registry.get "matita.external_editor") () + in *) + let fname = (MatitaScript.current ())#filename in + let slice mark = + source_buffer#start_iter#get_slice + ~stop:(source_buffer#get_iter_at_mark mark) + in + let script = MatitaScript.current () in + let locked = `MARK script#locked_mark in + let string_pos mark = string_of_int (String.length (slice mark)) in + let cursor_pos = string_pos `INSERT in + let locked_pos = string_pos locked in + let cmd = + Pcre.replace ~pat:"%f" ~templ:fname + (Pcre.replace ~pat:"%p" ~templ:cursor_pos + (Pcre.replace ~pat:"%l" ~templ:locked_pos + cmd)) + in + let locked_before = slice locked in + let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in + ignore (Unix.system cmd); + source_buffer#set_text (HExtlib.input_file fname); + let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in + source_buffer#move_mark locked locked_iter; + source_buffer#apply_tag script#locked_tag + ~start:source_buffer#start_iter ~stop:locked_iter; + let locked_after = slice locked in + let line = ref 0 in + let col = ref 0 in + try + for i = 0 to String.length locked_before - 1 do + if locked_before.[i] <> locked_after.[i] then begin + source_buffer#place_cursor + ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col))); + script#goto `Cursor (); + raise Exit + end else if locked_before.[i] = '\n' then begin + incr line; + col := 0 + end + done + with + | Exit -> () + | Invalid_argument _ -> script#goto `Bottom () + method loadScript file = - let script = MatitaScript.instance () in + let script = MatitaScript.current () in script#reset (); script#assignFileName file; let content = diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index 963bb4698..cf738cd85 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -117,7 +117,7 @@ object method reset: unit method load_logo: unit method load_logo_with_qed: unit - method load_sequents: ProofEngineTypes.status -> unit + method load_sequents: MatitaTypes.incomplete_proof -> unit method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 84dff49e9..e69c22cf8 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -149,10 +149,12 @@ let usage () = try Hashtbl.find usages usage_key with Not_found -> default_usage let registry_defaults = - [ "matita.debug", "false"; - "matita.quiet", "false"; - "matita.preserve", "false"; - "db.nodb", "false"; + [ + "db.nodb", "false"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.quiet", "false"; ] let set_registry_values = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 7d2a47a94..1ad4b2cd1 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -28,10 +28,12 @@ open Printf open MatitaTypes open MatitaGtkMisc +module Stack = Continuationals.Stack + (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) - method private script = MatitaScript.instance () + method private script = MatitaScript.current () end let cicBrowsers = ref [] @@ -284,7 +286,7 @@ object (self) List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) in let id = get_id node in - let script = MatitaScript.instance () in + let script = MatitaScript.current () in let metasenv = script#proofMetasenv in let context = script#proofContext in let metasenv, context, conclusion = @@ -363,7 +365,8 @@ object (self) ApplyTransformation.mml_of_cic_sequent metasenv sequent in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, + Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); @@ -391,6 +394,19 @@ object (self) current_mathml <- Some mathml); end +let tab_label meta_markup = + let rec aux = + function + | `Current m -> sprintf "%s" (aux m) + | `Closed m -> sprintf "%s" (aux m) + | `Shift (pos, m) -> sprintf "|%d: %s" pos (aux m) + | `Meta n -> sprintf "?%d" n + in + let markup = aux meta_markup in + (GMisc.label ~markup ~show:true ())#coerce + +let goal_of_switch = function Stack.Open g | Stack.Closed g -> g + class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = object (self) inherit scriptAccessor @@ -419,9 +435,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = notebook#set_show_tabs false; notebook#append_page logo_with_qed - method private tab_label metano = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - method reset = (match scrolledWin with | Some w -> @@ -444,13 +457,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- []; self#script#setGoal ~-1; - method load_sequents (status: ProofEngineTypes.status) = - let ((_, metasenv, _, _), goal) = status in + method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } = let sequents_no = List.length metasenv in _metasenv <- metasenv; - pages <- sequents_no; - self#script#setGoal goal; - let win metano = + pages <- 0; + let win goal_switch = let w = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS ~shadow_type:`IN ~show:true () @@ -468,42 +479,82 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = parent#remove cicMathView#coerce; w#add cicMathView#coerce in - goal2win <- (metano, reparent) :: goal2win; + goal2win <- (goal_switch, reparent) :: goal2win; w#coerce in + assert ( + let stack_goals = Stack.open_goals stack in + let proof_goals = ProofEngineTypes.goals_of_proof proof in + if + HExtlib.list_uniq (List.sort Pervasives.compare stack_goals) + <> List.sort Pervasives.compare proof_goals + then begin + prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals)); + prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals)); + false + end + else true + ); + let render_switch = + function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i) + in let page = ref 0 in - List.iter - (fun (metano, _, _) -> - page2goal <- (!page, metano) :: page2goal; - goal2page <- (metano, !page) :: goal2page; + let added_goals = ref [] in + (* goals can be duplicated on the tack due to focus, but we should avoid + * multiple labels in the user interface *) + let add_tab markup goal_switch = + let goal = Stack.goal_of_switch goal_switch in + if not (List.mem goal !added_goals) then begin + notebook#append_page ~tab_label:(tab_label markup) (win goal_switch); + page2goal <- (!page, goal_switch) :: page2goal; + goal2page <- (goal_switch, !page) :: goal2page; incr page; - notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) - metasenv; + pages <- pages + 1; + added_goals := goal :: !added_goals + end + in + let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in + Stack.iter (** populate notebook with tabs *) + ~env:(fun depth tag (pos, sw) -> + let markup = + match depth, pos with + | 0, _ -> `Current (render_switch sw) + | 1, pos when Stack.head_tag stack = Stack.BranchTag -> + `Shift (pos, render_switch sw) + | _ -> render_switch sw + in + add_tab markup sw) + ~cont:add_switch ~todo:add_switch + stack; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> - let goal = - try - List.assoc page page2goal - with Not_found -> assert false + let goal_switch = + try List.assoc page page2goal with Not_found -> assert false in - self#script#setGoal goal; - self#render_page ~page ~goal)) - - method private render_page ~page ~goal = - cicMathView#load_sequent _metasenv goal; - try - List.assoc goal goal2win (); - cicMathView#set_selection None - with Not_found -> assert false + self#script#setGoal (goal_of_switch goal_switch); + self#render_page ~page ~goal_switch)) + + method private render_page ~page ~goal_switch = + (match goal_switch with + | Stack.Open goal -> cicMathView#load_sequent _metasenv goal + | Stack.Closed goal -> + let doc = Lazy.force MatitaMisc.closed_goal_mathml in + cicMathView#load_root ~root:doc#get_documentElement); + (try + cicMathView#set_selection None; + List.assoc goal_switch goal2win () + with Not_found -> assert false) method goto_sequent goal = - let page = + let goal_switch, page = try - List.assoc goal goal2page + List.find + (function Stack.Open g, _ | Stack.Closed g, _ -> g = goal) + goal2page with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal + self#render_page page goal_switch end @@ -611,7 +662,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let query = String.lowercase (List.nth queries combo#active) in let input = win#queryInputText#text in let statement = "whelp " ^ query ^ " " ^ input ^ "." in - (MatitaScript.instance ())#advance ~statement () + (MatitaScript.current ())#advance ~statement () in ignore(win#queryInputText#connect#activate ~callback:start_query); ignore(combo#connect#changed ~callback:start_query); @@ -724,7 +775,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private blank () = self#_showMath; - mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement + mathView#load_root + (Lazy.force MatitaMisc.empty_mathml)#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck"; @@ -741,7 +793,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj - | Incomplete_proof ((uri, metasenv, bo, ty), _) -> + | Incomplete_proof { proof = (uri, metasenv, bo, ty) } -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj @@ -805,7 +857,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in if is_whelp txt then begin set_whelp_query txt; - (MatitaScript.instance ())#advance ~statement:(txt ^ ".") () + (MatitaScript.current ())#advance ~statement:(txt ^ ".") () end else begin let entry = match txt with @@ -834,7 +886,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) end -let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = +let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) (): + MatitaGuiTypes.sequentsViewer += new sequentsViewer ~notebook ~cicMathView () let cicBrowser () = @@ -897,7 +951,7 @@ let get_math_views () = :: (List.map (fun b -> b#mathView) !cicBrowsers) let get_selections () = - if (MatitaScript.instance ())#onGoingProof () then + if (MatitaScript.current ())#onGoingProof () then let rec aux = function | [] -> None diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 8f97b25a9..17473f38b 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -115,13 +115,16 @@ let append_phrase_sep s = else s -let empty_mathml () = +let empty_mathml = lazy ( DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) - ~qualifiedName:(Gdome.domString "math") ~doctype:None + ~qualifiedName:(Gdome.domString "math") ~doctype:None) -let empty_boxml () = +let empty_boxml = lazy ( DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) - ~qualifiedName:(Gdome.domString "box") ~doctype:None + ~qualifiedName:(Gdome.domString "box") ~doctype:None) + +let closed_goal_mathml = lazy ( + DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ()) exception History_failure @@ -217,31 +220,47 @@ let singleton f = let instance = lazy (f ()) in fun () -> Lazy.force instance -let get_proof_status status = +let get_current_proof status = match status.proof_status with - | Incomplete_proof s -> s + | Incomplete_proof { proof = p } -> p | _ -> statement_error "no ongoing proof" let get_proof_metasenv status = match status.proof_status with | No_proof -> [] - | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv - | Proof (_, metasenv, _, _) -> metasenv - | Intermediate m -> m + | Proof (_, metasenv, _, _) + | Incomplete_proof { proof = (_, metasenv, _, _) } + | Intermediate metasenv -> + metasenv -let get_proof_context status = +let get_proof_context status goal = match status.proof_status with - | Incomplete_proof ((_, metasenv, _, _), goal) -> + | Incomplete_proof { proof = (_, metasenv, _, _) } -> let (_, context, _) = CicUtil.lookup_meta goal metasenv in context | _ -> [] -let get_proof_conclusion status = +let get_proof_conclusion status goal = match status.proof_status with - | Incomplete_proof ((_, metasenv, _, _), goal) -> + | Incomplete_proof { proof = (_, metasenv, _, _) } -> let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in conclusion | _ -> statement_error "no ongoing proof" + +let get_stack status = + 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 + | Incomplete_proof p -> + { status with proof_status = Incomplete_proof { p with stack = stack } } + | Proof _ -> + assert (Continuationals.Stack.is_empty stack); + status + | _ -> assert false let qualify status name = get_string_option status "baseuri" ^ "/" ^ name diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 1f72dbddd..8dbde7fd9 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -63,8 +63,11 @@ val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list (** Gdome.element of a MathML document whose rendering should be blank. Used * by cicBrowser to render "about:blank" document *) -val empty_mathml: unit -> Gdome.document -val empty_boxml: unit -> Gdome.document +val empty_mathml: Gdome.document lazy_t +val empty_boxml: Gdome.document lazy_t + + (** shown for goals closed by side effects *) +val closed_goal_mathml: Gdome.document lazy_t exception History_failure @@ -96,10 +99,16 @@ val singleton: (unit -> 'a) -> (unit -> 'a) val qualify: MatitaTypes.status -> string -> string -val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status +val get_current_proof: MatitaTypes.status -> ProofEngineTypes.proof +val get_stack: MatitaTypes.status -> Continuationals.Stack.t +val set_stack: Continuationals.Stack.t ->MatitaTypes.status ->MatitaTypes.status val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv -val get_proof_context: MatitaTypes.status -> Cic.context -val get_proof_conclusion: MatitaTypes.status -> Cic.term + +val get_proof_context: + MatitaTypes.status -> ProofEngineTypes.goal -> Cic.context + +val get_proof_conclusion: + MatitaTypes.status -> ProofEngineTypes.goal -> Cic.term (** given the base name of an image, returns its full path *) val image_path: string -> string diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index dcb0baebf..080450416 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -26,6 +26,8 @@ open Printf open MatitaTypes +module TA = GrafiteAst + let debug = false let debug_print = if debug then prerr_endline else ignore @@ -58,7 +60,9 @@ let first_line s = let goal_ast n = let module A = GrafiteAst in let loc = DisambiguateTypes.dummy_floc in - A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))) + A.Executable (loc, A.Tactical (loc, + A.Tactic (loc, A.Goal (loc, n)), + Some (A.Dot loc))) type guistuff = { mathviewer:MatitaTypes.mathViewer; @@ -69,7 +73,6 @@ type guistuff = { } let eval_with_engine guistuff status user_goal parsed_text st = - let module TA = GrafiteAst in let module TAPp = GrafiteAstPp in let include_ = match guistuff.filenamedata with @@ -92,15 +95,17 @@ let eval_with_engine guistuff status user_goal parsed_text st = (* we add the goal command if needed *) let inital_space,new_status,new_status_and_text_list' = match status.proof_status with - | Incomplete_proof (_, goal) when goal <> user_goal -> - let status = +(* | Incomplete_proof { stack = stack } + when not (List.mem user_goal (Continuationals.head_goals stack)) -> + let status = MatitaEngine.eval_ast ~include_paths:include_ - ~do_heavy_checks:true status (goal_ast user_goal) in - let initial_space = - if initial_space = "" then "\n" else initial_space - in - "\n", status, - [status, initial_space ^ TAPp.pp_tactic (TA.Goal (loc, user_goal))] + ~do_heavy_checks:true status (goal_ast user_goal) + in + let initial_space = if initial_space = "" then "\n" else initial_space + in + "\n", status, + [ status, + initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *) | _ -> initial_space,status,[] in let new_status = MatitaEngine.eval_ast @@ -114,6 +119,10 @@ let eval_with_engine guistuff status user_goal parsed_text st = | _ -> MatitaSync.alias_diff ~from:status new_status in (* we remove the defined object since we consider them "automatic aliases" *) + let dummy_st = + TA.Comment (DisambiguateTypes.dummy_floc, + TA.Note (DisambiguateTypes.dummy_floc, "")) + in let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in @@ -138,12 +147,12 @@ let eval_with_engine guistuff status user_goal parsed_text st = let new_status = MatitaSync.set_proof_aliases status [k,value] in - "\n",new_status,((new_status, new_text)::acc) + "\n",new_status,((new_status, (new_text, dummy_st))::acc) ) (initial_space,status,[]) new_aliases in let parsed_text = initial_space ^ parsed_text in let res = List.rev new_status_and_text_list_rev @ new_status_and_text_list' @ - [new_status, parsed_text] + [new_status, (parsed_text, st)] in res,parsed_text_length @@ -202,11 +211,11 @@ let eval_with_engine guistuff status user_goal parsed_text st = | Some d -> handle_with_devel d ;; -let disambiguate term status = +let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in let dbd = MatitaDb.instance () in let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in + let context = MatitaMisc.get_proof_context status user_goal in let interps = MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in @@ -214,8 +223,7 @@ let disambiguate term status = | [_,_,x,_], _ -> x | _ -> assert false -let eval_macro guistuff status unparsed_text parsed_text script mac = - let module TA = GrafiteAst in +let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = MatitaDb in @@ -228,7 +236,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> - let term = disambiguate term status in + let term = disambiguate_macro_term term status user_goal in let l = MQ.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." @@ -238,7 +246,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WInstance (loc, term) -> - let term = disambiguate term status in + let term = disambiguate_macro_term term status user_goal in let l = MQ.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; @@ -249,7 +257,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WElim (loc, term) -> - let term = disambiguate term status in + let term = disambiguate_macro_term term status user_goal in let uri = match term with | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None @@ -260,7 +268,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WHint (loc, term) -> - let term = disambiguate term status in + let term = disambiguate_macro_term term status user_goal in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in @@ -268,24 +276,26 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let s = MatitaMisc.get_proof_status status in - let l = List.map fst (MQ.experimental_hint ~dbd s) in + let proof = MatitaMisc.get_current_proof status 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 | [] -> [], parsed_text_length | [uri] -> - let ast = - TA.Executable (loc, - (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None)))))) - in + let suri = UriManager.string_of_uri uri in + let ast = + TA.Executable (loc, (TA.Tactical (loc, + TA.Tactic (loc, + TA.Apply (loc, CicNotationPt.Uri (suri, None))), + Some (TA.Dot loc)))) + in let new_status = MatitaEngine.eval_ast status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in - [ new_status , extra_text ], parsed_text_length + [ new_status , (extra_text, ast) ], parsed_text_length | _ -> MatitaLog.error "The result of the urichooser should be only 1 uri, not:\n"; @@ -295,7 +305,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = assert false) | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in + let context = MatitaMisc.get_proof_context status user_goal in let interps = MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term @@ -330,18 +340,16 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = | TA.Print (_,kind) -> failwith "not implemented" | TA.Search_pat (_, search_kind, str) -> failwith "not implemented" | TA.Search_term (_, search_kind, term) -> failwith "not implemented" - let eval_executable guistuff status user_goal unparsed_text parsed_text script ex = - let module TA = GrafiteAst in let module TAPp = GrafiteAstPp in let module MD = MatitaDisambiguator in let module ML = MatitacleanLib in let parsed_text_length = String.length parsed_text in match ex with - | TA.Command (loc, _) | TA.Tactical (loc, _) -> + | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () @@ -362,41 +370,48 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script guistuff status user_goal parsed_text (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> - eval_macro guistuff status unparsed_text parsed_text script mac + eval_macro guistuff status user_goal unparsed_text parsed_text script mac + +let parse_statement baseoffset parsedlen ?error_tag (buffer: GText.buffer) text += + try + GrafiteParser.parse_statement (Ulexing.from_utf8_string text) + with CicNotationParser.Parse_error (floc, err) as exn -> + match error_tag with + | None -> raise exn + | Some error_tag -> + let (x, y) = CicNotationPt.loc_of_floc floc in + let x = parsedlen + x in + let y = parsedlen + y in + let x' = baseoffset + x in + let y' = baseoffset + y in + let x_iter = buffer#get_iter (`OFFSET x') in + let y_iter = buffer#get_iter (`OFFSET y') in + buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; + let id = ref None in + id := Some (buffer#connect#changed ~callback:(fun () -> + buffer#remove_tag error_tag ~start:buffer#start_iter + ~stop:buffer#end_iter; + match !id with + | None -> assert false (* a race condition occurred *) + | Some id -> + (new GObj.gobject_ops buffer#as_buffer)#disconnect id)); + let flocb,floce = floc in + let floc = + { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } + in + buffer#place_cursor (buffer#get_iter (`OFFSET x')); + raise (CicNotationParser.Parse_error (floc, err)) let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) - guistuff status user_goal script unparsed_text + guistuff status user_goal script statement = - if Pcre.pmatch ~rex:only_dust_RE unparsed_text then raise Margin; - let st = - try - GrafiteParser.parse_statement (Ulexing.from_utf8_string unparsed_text) - with - CicNotationParser.Parse_error (floc,err) as exc -> - let (x, y) = CicNotationPt.loc_of_floc floc in - let x = parsedlen + x in - let y = parsedlen + y in - let x' = baseoffset + x in - let y' = baseoffset + y in - let x_iter = buffer#get_iter (`OFFSET x') in - let y_iter = buffer#get_iter (`OFFSET y') in - buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; - let id = ref None in - id := - Some - (buffer#connect#changed - ~callback:( - fun () -> - buffer#remove_tag error_tag ~start:buffer#start_iter - ~stop:buffer#end_iter; - match !id with - None -> assert false (* a race condition occurred *) - | Some id -> - (new GObj.gobject_ops buffer#as_buffer)#disconnect id)); - let flocb,floce = floc in - let floc = - {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y } in - raise (CicNotationParser.Parse_error (floc,err)) + let st, unparsed_text = + match statement with + | `Raw text -> + if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; + parse_statement baseoffset parsedlen ~error_tag buffer text, text + | `Ast (st, text) -> st, text in let text_of_loc loc = let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in @@ -410,11 +425,11 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) let s = String.sub unparsed_text parsed_text_length remain_len in let s,len = eval_statement baseoffset (parsedlen + parsed_text_length) error_tag - buffer guistuff status user_goal script s + buffer guistuff status user_goal script (`Raw s) in (match s with - | (status, text) :: tl -> - ((status, parsed_text ^ text)::tl), (parsed_text_length + len) + | (status, (text, ast)) :: tl -> + ((status, (parsed_text ^ text, ast))::tl), (parsed_text_length + len) | [] -> [], 0) | GrafiteAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in @@ -447,6 +462,8 @@ object (self) method private getFilename = match guistuff.filenamedata with Some f,_ -> f | _ -> assert false + + method filename = self#getFilename method private ppFilename = match guistuff.filenamedata with @@ -483,30 +500,56 @@ object (self) method status = match history with hd :: _ -> hd | _ -> assert false method private _advance ?statement () = + let rec aux st = + let baseoffset = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in + let (entries, parsed_len) = + eval_statement baseoffset 0 error_tag buffer guistuff self#status + userGoal self st + in + let (new_statuses, new_statements, new_asts) = + let statuses, statements = List.split entries in + let texts, asts = List.split statements in + statuses, texts, asts + in + history <- List.rev new_statuses @ history; + statements <- List.rev new_statements @ statements; + let start = buffer#get_iter_at_mark (`MARK locked_mark) in + let new_text = String.concat "" new_statements in + if statement <> None then + buffer#insert ~iter:start new_text + else + let s = match st with `Raw s | `Ast (_, s) -> s in + if new_text <> String.sub s 0 parsed_len then + begin + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; + end; + self#moveMark (String.length new_text); + (* + (match List.rev new_asts with (* advance again on punctuation *) + | TA.Executable (_, TA.Tactical (_, tac, _)) :: _ -> + let baseoffset = + (buffer#get_iter_at_mark (`MARK locked_mark))#offset + in + let text = self#getFuture in + (try + (match parse_statement baseoffset 0 ?error_tag:None buffer text with + | TA.Executable (loc, TA.Tactical (_, tac, None)) as st + when GrafiteAst.is_punctuation tac -> + let len = snd (CicNotationPt.loc_of_floc loc) in + aux (`Ast (st, String.sub text 0 len)) + | _ -> ()) + with CicNotationParser.Parse_error _ | End_of_file -> ()) + | _ -> ()) + *) + in let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len) = - eval_statement (buffer#get_iter_at_mark (`MARK locked_mark))#offset 0 - error_tag buffer guistuff self#status userGoal self s - in - let (new_statuses, new_statements) = List.split entries in - history <- List.rev new_statuses @ history; - statements <- List.rev new_statements @ statements; - let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" new_statements in - if statement <> None then - buffer#insert ~iter:start new_text - else - if new_text <> String.sub s 0 parsed_len then - begin - let stop = start#copy#forward_chars parsed_len in - buffer#delete ~start ~stop; - buffer#insert ~iter:start new_text; - end; - self#moveMark (String.length new_text) + aux (`Raw s) method private _retract offset status new_statements new_history = - let cur_status = match history with s::_ -> s | [] -> assert false in + let cur_status = match history with s::_ -> s | [] -> assert false in MatitaSync.time_travel ~present:cur_status ~past:status; statements <- new_statements; history <- new_history; @@ -555,11 +598,6 @@ object (self) buffer#move_mark mark ~where:new_mark_pos; buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; buffer#move_mark `INSERT old_insert; - begin - match self#status.proof_status with - Incomplete_proof (_,goal) -> self#setGoal goal - | _ -> () - end ; let mark_position = buffer#get_iter_at_mark mark in if source_view#move_mark_onscreen mark then begin @@ -721,11 +759,13 @@ object (self) | Incomplete_proof _ -> true | Intermediate _ -> assert false - method proofStatus = MatitaMisc.get_proof_status self#status +(* method proofStatus = MatitaMisc.get_proof_status self#status *) method proofMetasenv = MatitaMisc.get_proof_metasenv self#status - method proofContext = MatitaMisc.get_proof_context self#status - method proofConclusion = MatitaMisc.get_proof_conclusion self#status + method proofContext = MatitaMisc.get_proof_context self#status userGoal + method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal + method stack = MatitaMisc.get_stack self#status method setGoal n = userGoal <- n + method goal = userGoal method eos = let s = self#getFuture in @@ -771,6 +811,5 @@ let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirm _script := Some s; s -let instance () = match !_script with None -> assert false | Some s -> s - +let current () = match !_script with None -> assert false | Some s -> s diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index a44d615d2..35ae43ebb 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -49,18 +49,21 @@ object method assignFileName : string -> unit (* to the current active file *) method loadFromFile : string -> unit method saveToFile : unit -> unit + method filename : string (** {2 Current proof} (if any) *) (** @return true if there is an ongoing proof, false otherise *) method onGoingProof: unit -> bool - method proofStatus: ProofEngineTypes.status (** @raise Statement_error *) +(* method proofStatus: ProofEngineTypes.status |+* @raise Statement_error +| *) method proofMetasenv: Cic.metasenv (** @raise Statement_error *) method proofContext: Cic.context (** @raise Statement_error *) method proofConclusion: Cic.term (** @raise Statement_error *) + method stack: Continuationals.Stack.t (** @raise Statement_error *) method setGoal: int -> unit + method goal: int (** end of script, true if the whole script has been executed *) method eos: bool @@ -91,5 +94,5 @@ val script: * the value of this ref *) (* TODO Zack: orrible solution until we found a better one for having a single * access point for the script *) -val instance: unit -> script +val current: unit -> script diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 8b4cb1f9d..29fefca03 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -41,9 +41,14 @@ exception Option_error of string * string exception Unbound_identifier of string +type incomplete_proof = { + proof: ProofEngineTypes.proof; + stack: Continuationals.Stack.t; +} + type proof_status = | No_proof - | Incomplete_proof of ProofEngineTypes.status + | Incomplete_proof of incomplete_proof | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv (* Status in which the proof could be while it is being processed by the @@ -74,8 +79,9 @@ let set_metasenv metasenv status = let proof_status = match status.proof_status with | No_proof -> Intermediate metasenv - | Incomplete_proof ((uri, _, proof, ty), goal) -> - Incomplete_proof ((uri, metasenv, proof, ty), goal) + | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) -> + Incomplete_proof + { incomplete_proof with proof = (uri, metasenv, proof, ty) } | Intermediate _ -> Intermediate metasenv | Proof _ -> assert false in diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index 144c0c1f2..e425519c6 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -33,9 +33,14 @@ val command_error : string -> 'a exception Option_error of string * string exception Unbound_identifier of string +type incomplete_proof = { + proof: ProofEngineTypes.proof; + stack: Continuationals.Stack.t; +} + type proof_status = No_proof - | Incomplete_proof of ProofEngineTypes.status + | Incomplete_proof of incomplete_proof | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 8ee8eca78..13a8b3883 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -95,8 +95,8 @@ let level2_meta_keywords = let level2_ast_keywords = Hashtbl.create 23 let _ = List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) - [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; - "with"; "in"; "and"; "to"; "as"; "on"; "names" ] + [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; + "with"; "in"; "and"; "to"; "as"; "on" ] let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index d3c9d0e95..cba5acd1f 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -207,16 +207,31 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactical = | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical * ('term, 'lazy_term, 'reduction, 'ident) tactical list | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list - (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) + (* try a sequence of loc * tactical until one succeeds, fail otherwise *) | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical (* try a tactical and mask failures *) | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list + | Dot of loc + | Semicolon of loc + | Branch of loc + | Shift of loc + | Pos of loc * int + | Merge of loc + | Focus of loc * int list + | Unfocus of loc + | Skip of loc + +let is_punctuation = + function + | Dot _ | Semicolon _ | Branch _ | Shift _ | Merge _ | Pos _ -> true + | _ -> false type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term,'obj) command | Macro of loc * 'term macro | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical + * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *) type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = | Note of loc * string diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index 9e4d63271..3e19ed281 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -29,7 +29,7 @@ open GrafiteAst module Ast = CicNotationPt -let tactical_terminator = "." +let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator @@ -313,16 +313,27 @@ let rec pp_tactical = function | Try (_, tac) -> "try " ^ pp_tactical tac | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) -and pp_tacticals ~sep tacs = - String.concat sep (List.map pp_tactical tacs) + | Dot _ -> "." + | Semicolon _ -> ";" + | Branch _ -> "[" + | Shift _ -> "|" + | Pos (_, i) -> sprintf "%d:" i + | Merge _ -> "]" + | Focus (_, goals) -> + sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) + | Unfocus _ -> "unfocus" + | Skip _ -> "skip" -let pp_tactical tac = pp_tactical tac ^ tactical_terminator -let pp_tactic tac = pp_tactic tac ^ tactic_terminator -let pp_command tac = pp_command tac ^ command_terminator +and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs) + +let pp_tactical tac = pp_tactical tac +let pp_tactic tac = pp_tactic tac +let pp_command tac = pp_command tac let pp_executable = function | Macro (_,x) -> pp_macro_ast x - | Tactical (_,x) -> pp_tactical x + | Tactical (_, tac, Some punct) -> pp_tactical tac ^ pp_tactical punct + | Tactical (_, tac, None) -> pp_tactical tac | Command (_,x) -> pp_command x let pp_comment = function diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 3438e2c33..2863d5374 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -27,6 +27,11 @@ open Printf module Ast = CicNotationPt +type statement = + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + GrafiteAst.obj, string) + GrafiteAst.statement + let grammar = CicNotationParser.level2_ast_grammar let term = CicNotationParser.term @@ -46,10 +51,8 @@ EXTEND ] ]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; - tactic_term: [ [ t = term -> t ] ]; - ident_list0: [ - [ SYMBOL "["; idents = LIST0 IDENT SEP SYMBOL ";"; SYMBOL "]" -> idents ] - ]; + tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; + ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ]; tactic_term_list1: [ [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; @@ -102,6 +105,13 @@ EXTEND | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; + intros_spec: [ + [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + num, idents + ] + ]; + using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; tactic: [ [ IDENT "absurd"; t = tactic_term -> GrafiteAst.Absurd (loc, t) @@ -132,24 +142,17 @@ EXTEND | IDENT "decide"; IDENT "equality" -> GrafiteAst.DecideEquality loc | IDENT "decompose"; types = OPT ident_list0; what = IDENT; - OPT "names"; num = OPT [num = int -> num]; - idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + (num, idents) = intros_spec -> let types = match types with None -> [] | Some types -> types in let to_spec id = GrafiteAst.Ident id in GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) | IDENT "discriminate"; t = tactic_term -> GrafiteAst.Discriminate (loc, t) - | IDENT "elim"; what = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ]; - OPT "names"; num = OPT [num = int -> num]; - idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + | IDENT "elim"; what = tactic_term; using = using; + (num, idents) = intros_spec -> GrafiteAst.Elim (loc, what, using, num, idents) - | IDENT "elimType"; what = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ]; - OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + | IDENT "elimType"; what = tactic_term; using = using; + (num, idents) = intros_spec -> GrafiteAst.ElimType (loc, what, using, num, idents) | IDENT "exact"; t = tactic_term -> GrafiteAst.Exact (loc, t) @@ -179,14 +182,13 @@ EXTEND | IDENT "intro"; ident = OPT IDENT -> let idents = match ident with None -> [] | Some id -> [id] in GrafiteAst.Intros (loc, Some 1, idents) - | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + | IDENT "intros"; (num, idents) = intros_spec -> GrafiteAst.Intros (loc, num, idents) | IDENT "lapply"; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; - ident = OPT [ "using" ; ident = IDENT -> ident ] -> + ident = OPT [ IDENT "using" ; ident = IDENT -> ident ] -> let to_what = match to_what with None -> [] | Some to_what -> to_what in GrafiteAst.LApply (loc, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc @@ -218,38 +220,56 @@ EXTEND GrafiteAst.Transitivity (loc, t) ] ]; - tactical: + atomic_tactical: [ "sequence" LEFTA - [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> - match tacticals with - [] -> assert false - | [tac] -> tac - | l -> GrafiteAst.Seq (loc, l) + [ t1 = SELF; SYMBOL ";"; t2 = SELF -> + let ts = + match t1 with + | GrafiteAst.Seq (_, l) -> l @ [ t2 ] + | _ -> [ t1; t2 ] + in + GrafiteAst.Seq (loc, ts) ] | "then" NONA - [ tac = tactical; SYMBOL ";"; - SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + [ tac = SELF; SYMBOL ";"; + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> (GrafiteAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ IDENT "do"; count = int; tac = tactical -> + [ IDENT "do"; count = int; tac = SELF; IDENT "end" -> GrafiteAst.Do (loc, count, tac) - | IDENT "repeat"; tac = tactical -> - GrafiteAst.Repeat (loc, tac) + | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac) ] | "simple" NONA [ IDENT "first"; - SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> GrafiteAst.First (loc, tacs) - | IDENT "try"; tac = NEXT -> - GrafiteAst.Try (loc, tac) + | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac) | IDENT "solve"; - SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> GrafiteAst.Solve (loc, tacs) - | LPAREN; tac = tactical; RPAREN -> tac + | LPAREN; tac = SELF; RPAREN -> tac | tac = tactic -> GrafiteAst.Tactic (loc, tac) ] ]; + punctuation_tactical: + [ + [ SYMBOL "[" -> GrafiteAst.Branch loc + | SYMBOL "|" -> GrafiteAst.Shift loc + | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i) + | SYMBOL "]" -> GrafiteAst.Merge loc + | SYMBOL ";" -> GrafiteAst.Semicolon loc + | SYMBOL "." -> GrafiteAst.Dot loc + ] + ]; + tactical: + [ "simple" NONA + [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals) + | IDENT "unfocus" -> GrafiteAst.Unfocus loc + | IDENT "skip" -> GrafiteAst.Skip loc + | tac = atomic_tactical LEVEL "loops" -> tac + ] + ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact @@ -483,7 +503,9 @@ EXTEND ]]; executable: [ [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) - | tac = tactical; SYMBOL "." -> GrafiteAst.Tactical (loc, tac) + | tac = tactical; punct = punctuation_tactical -> + GrafiteAst.Tactical (loc, tac, Some punct) + | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) ] ]; diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli index 36f1db49b..5cd6c2622 100644 --- a/helm/ocaml/cic_notation/grafiteParser.mli +++ b/helm/ocaml/cic_notation/grafiteParser.mli @@ -23,13 +23,13 @@ * http://helm.cs.unibo.it/ *) - (** @raise End_of_file *) -val parse_statement: - Ulexing.lexbuf -> - (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, - GrafiteAst.obj, string) +type statement = + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + GrafiteAst.obj, string) GrafiteAst.statement +val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) + (** @raise End_of_file *) val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 7c915b4c5..d667574fa 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -1,5 +1,6 @@ proofEngineHelpers.cmi: proofEngineTypes.cmi -tacticals.cmi: proofEngineTypes.cmi +continuationals.cmi: proofEngineTypes.cmi +tacticals.cmi: proofEngineTypes.cmi continuationals.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi @@ -24,8 +25,10 @@ proofEngineReduction.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ proofEngineReduction.cmi -tacticals.cmo: proofEngineTypes.cmi tacticals.cmi -tacticals.cmx: proofEngineTypes.cmx tacticals.cmi +continuationals.cmo: proofEngineTypes.cmi continuationals.cmi +continuationals.cmx: proofEngineTypes.cmx continuationals.cmi +tacticals.cmo: proofEngineTypes.cmi continuationals.cmi tacticals.cmi +tacticals.cmx: proofEngineTypes.cmx continuationals.cmx tacticals.cmi reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ proofEngineHelpers.cmi reductionTactics.cmi reductionTactics.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ @@ -116,5 +119,3 @@ tactics.cmx: variousTactics.cmx tacticals.cmx ring.cmx reductionTactics.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi -continuationals.cmo: continuationals.cmi -continuationals.cmx: continuationals.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 1b27678fb..7f48873a0 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -9,13 +9,14 @@ REQUIRES = \ INTERFACE_FILES = \ proofEngineTypes.mli \ proofEngineHelpers.mli proofEngineReduction.mli \ + continuationals.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ fourierR.mli fwdSimplTactic.mli history.mli statefulProofEngine.mli \ - tactics.mli continuationals.mli + tactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index f4f9e34f6..345502d5b 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -25,42 +25,174 @@ open Printf -exception Error of string Lazy.t +let debug = true +let debug_print s = if debug then prerr_endline (Lazy.force s) else () -module type Engine = +exception Error of string lazy_t +let fail msg = raise (Error msg) + +type goal = ProofEngineTypes.goal + +module Stack = +struct + type switch = Open of goal | Closed of goal + type locator = int * switch + type tag = BranchTag | FocusTag | NoTag + type entry = locator list * locator list * locator list * tag + type t = entry list + + let empty = [ [], [], [], NoTag ] + + let fold ~env ~cont ~todo init stack = + let rec aux acc depth = + function + | [] -> acc + | (locs, todos, conts, tag) :: tl -> + let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in + let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in + let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in + aux acc (depth + 1) tl + in + assert (stack <> []); + aux init 0 stack + + let iter ~env ~cont ~todo = + fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) () + + let map ~env ~cont ~todo = + let depth = ref ~-1 in + List.map + (fun (s, t, c, tag) -> + incr depth; + let d = !depth in + env d tag s, todo d tag t, cont d tag c, tag) + + let is_open = function _, Open _ -> true | _ -> false + let close = function n, Open g -> n, Closed g | l -> l + let filter_open = List.filter is_open + let is_fresh = function n, Open _ when n > 0 -> true | _ -> false + let goal_of_loc = function _, Open g | _, Closed g -> g + let goal_of_switch = function Open g | Closed g -> g + let switch_of_loc = snd + + let zero_pos = List.map (fun g -> 0, Open g) + + let init_pos locs = + let pos = ref 0 in (* positions are 1-based *) + List.map (function _, sw -> incr pos; !pos, sw) locs + + let extract_pos i = + let rec aux acc = + function + | [] -> fail (lazy (sprintf "relative position %d not found" i)) + | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl + | hd :: tl -> aux (hd :: acc) tl + in + aux [] + + let deep_close gs = + let close _ _ = + List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l) + in + let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in + map ~env:close ~cont:rm ~todo:rm + + let rec find_goal = + function + | [] -> raise (Failure "Continuationals.find_goal") + | (l :: _, _ , _ , _) :: _ -> goal_of_loc l + | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l + | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l + | _ :: tl -> find_goal tl + + let is_empty = + function + | [] -> assert false + | [ [], [], [], NoTag ] -> true + | _ -> false + + let of_metasenv metasenv = + let goals = List.map (fun (g, _, _) -> g) metasenv in + [ zero_pos goals, [], [], NoTag ] + + let head_switches = + function + | (locs, _, _, _) :: _ -> List.map switch_of_loc locs + | [] -> assert false + + let head_goals = + function + | (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | [] -> assert false + + let head_tag = + function + | (_, _, _, tag) :: _ -> tag + | [] -> assert false + + let shift_goals = + function + | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | [] -> assert false + | _ -> [] + + let open_goals stack = + let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in + List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack) + + let (@+) = (@) (* union *) + + let (@-) s1 s2 = (* difference *) + List.fold_right + (fun e acc -> if List.mem e s2 then acc else e :: acc) + s1 [] + + let (@~-) locs gs = (* remove some goals from a locators list *) + List.fold_right + (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc) + locs [] + + let pp stack = + let pp_goal = string_of_int in + let pp_switch = + function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g + in + let pp_loc (i, s) = string_of_int i ^ pp_switch s in + let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in + let pp_tag = function BranchTag -> "B" | FocusTag -> "F" | NoTag -> "N" in + let pp_stack_entry (env, todo, cont, tag) = + sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont) + (pp_tag tag) + in + String.concat " :: " (List.map pp_stack_entry stack) +end + +module type Status = sig - type goal - type proof + type input_status + type output_status + type tactic - val is_goal_closed: goal -> proof -> bool - val goals_of_proof: proof -> goal list + val id_tactic : tactic + val mk_tactic : (input_status -> output_status) -> tactic + val apply_tactic : tactic -> input_status -> output_status - val apply_tactic: - tactic -> proof -> goal -> - proof * goal list * goal list -end + val goals : output_status -> goal list * goal list (** opened, closed goals *) + val set_goals: goal list * goal list -> output_status -> output_status + val get_stack : input_status -> Stack.t + val set_stack : Stack.t -> output_status -> output_status -(** like List.assoc returning a pair: binding matching the given key, - * associative list without the returned binding - * @raise Not_found *) -let list_assoc_extract key = - let rec aux acc = - function - | [] -> raise Not_found - | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl) - | hd :: tl -> aux (hd :: acc) tl - in - aux [] + val inject : input_status -> output_status + val focus : goal -> output_status -> input_status +end module type C = sig - type goal - type proof + type input_status + type output_status type tactic - type status - type tactical = | Tactic of tactic | Skip @@ -70,43 +202,25 @@ sig | Semicolon | Branch - | Shift of int option - | Select of goal list - | End + | Shift + | Pos of int + | Merge - | Tactical of tactical - - val eval: t -> status -> status - val init: proof -> status - - val get_proof: status -> proof - val set_proof: proof -> status -> status + | Focus of goal list + | Unfocus - type goal_switch = Open of goal | Closed of goal - val get_goals: status -> goal_switch list + | Tactical of tactical - val is_completed: status -> bool + val eval: t -> input_status -> output_status end -module Make (E:Engine) = +module Make (S: Status) = struct - type goal = E.goal - type proof = E.proof - type tactic = E.tactic - - type goal_switch = Open of goal | Closed of goal - type 'a stack = 'a list - type stack_tag = BranchTag | SelectTag | NoTag - type stack_entry = - (int * goal_switch) list * goal list * goal list * stack_tag - type status = proof * stack_entry stack - - let get_proof = fst - let set_proof p (_, s) = p, s - let get_goals (_, stack) = - match stack with - | (goals, _, _, _) :: _ -> List.map snd goals - | [] -> assert false + open Stack + + type input_status = S.input_status + type output_status = S.output_status + type tactic = S.tactic type tactical = | Tactic of tactic @@ -116,130 +230,125 @@ struct | Dot | Semicolon | Branch - | Shift of int option - | Select of goal list - | End + | Shift + | Pos of int + | Merge + | Focus of goal list + | Unfocus | Tactical of tactical - let goal_of = function _, Open g -> g | _, Closed g -> g - let is_open = function _, Open _ -> true | _, Closed _ -> false - let open_all = List.map (fun p, g -> p, Open g) - - let union a b = a @ b - - let complementary part full = (* not really efficient *) - List.fold_left (fun acc g -> if List.mem g part then acc else g::acc) - full [] - - let close to_close = - List.map - (function - | p, Open g when List.mem g to_close -> p, Closed g - | g -> g) - - let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag) - - let dummy_pos = ~-1 - let add_dummy_pos g = dummy_pos, g - let map_dummy_pos = List.map add_dummy_pos - - let map_open_pos = - let rec aux pos = - function - | [] -> [] - | g :: tl -> (pos, Open g) :: aux (pos + 1) tl - in - aux 1 + let pp_t = + function + | Dot -> "Dot" + | Semicolon -> "Semicolon" + | Branch -> "Branch" + | Shift -> "Shift" + | Pos i -> "Pos " ^ string_of_int i + | Merge -> "Merge" + | Focus gs -> + sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs)) + | Unfocus -> "Unfocus" + | Tactical _ -> "Tactical " - let eval_tactical tactical proof switch = + let eval_tactical tactical ostatus switch = match tactical, switch with - | Tactic tac, Open n -> E.apply_tactic tac proof n - | Skip, Closed n -> proof, [], [n] - | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal")) - | Skip, Open _ -> raise (Error (lazy "can't skip an open goal")) - - let eval continuational status = - match continuational, status with - | _, (_, []) -> assert false - | Tactical t, (proof, (env, todo, left,tag)::tail) -> - assert (List.length env > 1); - let proof, opened, closed = - List.fold_left - (fun (proof, opened, closed) cur_goal -> - if List.exists ((=) (goal_of cur_goal)) closed then - proof, opened, closed - else - let proof, newopened, newclosed = - eval_tactical t proof (snd cur_goal) + | Tactic tac, Open n -> + let ostatus = S.apply_tactic tac (S.focus n ostatus) in + let opened, closed = S.goals ostatus in + ostatus, opened, closed + | Skip, Closed n -> ostatus, [], [n] + | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal") + | Skip, Open _ -> fail (lazy "can't skip an open goal") + + let eval cmd istatus = + let stack = S.get_stack istatus in + debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack))); + let new_stack stack = S.inject istatus, stack in + let ostatus, stack = + match cmd, stack with + | _, [] -> assert false + | Tactical tac, (g, t, k, tag) :: s -> + debug_print (lazy ("context length " ^string_of_int (List.length g))); + let rec aux s go gc = + function + | [] -> s, go, gc + | loc :: loc_tl -> + debug_print (lazy "inner eval tactical"); + let s, go, gc = + if List.exists ((=) (goal_of_loc loc)) gc then + s, go, gc + else + let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in + s, (go @- gc') @+ go', gc @+ gc' in - proof, - union (complementary newclosed opened) newopened, - union closed newclosed - ) (proof, [],[]) env - in - let pos = ref 0 in - let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in - proof, - (open_all stack_opened, - complementary closed todo, - complementary opened left, tag) - :: map_stack - (close closed) (complementary closed) (complementary opened) tail - | Semicolon, (proof, stack) -> proof, stack - | Dot, (proof, (env, todo, left, tag)::tail) -> - let env, left = - match List.filter is_open env, left with - | [], [] -> raise (Error (lazy "There is nothig to do for '.'")) - | g::env,left -> [g], union (List.map goal_of env) left - | [], g::left -> [dummy_pos, Open g], left - in - proof, (env, todo, left, tag)::tail - | Branch, (proof, (g1::tl, todo, left, tag)::tail) -> - assert (List.length tl >= 1); - proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail - | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context")) - | Shift opt_pos, (proof, (leftopen, t, l,BranchTag):: - (goals, todo, left,tag)::tail) -> - let next_goal, rem_goals = - match opt_pos, goals with - | None, g1 :: tl -> g1, tl - | Some pos, _ -> - (try - list_assoc_extract pos goals - with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos)))) - | None, [] -> raise (Error (lazy "no more goals to shift")) - in - let t = - union t (union (List.map goal_of (List.filter is_open leftopen)) l) - in - proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail - | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift")) - | Select gl, (proof, stack) -> - List.iter - (fun g -> - if E.is_goal_closed g proof then - raise (Error (lazy "you can't select a closed goal"))) - gl; - (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack) - | End, (proof, stack) -> - (match stack with - | ([], [], [], SelectTag)::tail -> proof, tail - | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail -> - let env = - (union (open_all (map_dummy_pos t)) - (union (open_all (map_dummy_pos l)) - (union not_processed (List.filter is_open leftopen)))) - in - proof, (env,todo,left,tag)::tail - | _ -> raise (Error (lazy "can't end here"))) - - let init proof = - proof, - [ map_open_pos (E.goals_of_proof proof), [], [], NoTag ] - - let is_completed = - function - | (_, [[],[],[],NoTag]) -> true - | _ -> false + aux s go gc loc_tl + in + let s0, go0, gc0 = S.inject istatus, [], [] in + let sn, gon, gcn = aux s0 go0 gc0 g in + debug_print (lazy ("opened: " + ^ String.concat " " (List.map string_of_int gon))); + debug_print (lazy ("closed: " + ^ String.concat " " (List.map string_of_int gcn))); + let stack = + (zero_pos gon, t @~- gcn, k @~- gon, tag) :: deep_close gcn s + in + sn, stack + | Dot, ([], _, [], _) :: _ -> + (* backward compatibility: do-nothing-dot *) + new_stack stack + | Dot, (g, t, k, tag) :: s -> + (match filter_open g, k with + | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s) + | [], loc :: k -> + assert (is_open loc); + new_stack (([ loc ], t, k, tag) :: s) + | _ -> fail (lazy "can't use \".\" here")) + | Semicolon, _ -> new_stack stack + | Branch, (g, t, k, tag) :: s -> + (match init_pos g with + | [] | [ _ ] -> fail (lazy "too few goals to branch"); + | loc :: loc_tl -> + new_stack + (([ loc ], [], [], BranchTag) :: (loc_tl, t, k, tag) :: s)) + | Shift, (g, t, k, BranchTag) :: (g', t', k', tag) :: s -> + (match g' with + | [] -> fail (lazy "no more goals to shift") + | loc :: loc_tl -> + new_stack + (([ loc ], t @+ filter_open g, [], BranchTag) + :: (loc_tl, t', k', tag) :: s)) + | Shift, _ -> fail (lazy "can't shift goals here") + | Pos i, ([ loc ], [], [], BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let loc_i, g' = extract_pos i g' in + new_stack + (([ loc_i ], [], [], BranchTag) + :: ([ loc ] @+ g', t', k', tag) :: s) + | Pos i, (g, t, k, BranchTag) :: (g', t', k', tag) :: s -> + let loc_i, g' = extract_pos i g' in + new_stack + (([ loc_i ], [], [], BranchTag) + :: (g', t' @+ filter_open g, k', tag) :: s) + | Pos _, _ -> fail (lazy "can't use relative positioning here") + | Merge, (g, t, k, BranchTag) :: (g', t', k', tag) :: s -> + new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | Merge, _ -> fail (lazy "can't merge goals here") + | Focus [], _ -> assert false + | Focus gs, s -> + let stack_locs = + let add_l acc _ _ l = if is_open l then l :: acc else acc in + Stack.fold ~env:add_l ~cont:add_l ~todo:add_l [] s + in + List.iter + (fun g -> + if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then + fail (lazy (sprintf "goal %d not found (or closed)" g))) + gs; + new_stack ((zero_pos gs, [], [], FocusTag) :: deep_close gs s) + | Unfocus, ([], [], [], FocusTag) :: s -> new_stack s + | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open") + in + debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack))); + S.set_stack stack ostatus end diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli index 109dbaf99..176fd58b2 100644 --- a/helm/ocaml/tactics/continuationals.mli +++ b/helm/ocaml/tactics/continuationals.mli @@ -25,28 +25,80 @@ exception Error of string Lazy.t -module type Engine = +type goal = ProofEngineTypes.goal + +(** {2 Goal stack} *) + +module Stack: sig - type goal - type proof + type switch = Open of goal | Closed of goal + type locator = int * switch + type tag = BranchTag | FocusTag | NoTag + type entry = locator list * locator list * locator list * tag + type t = entry list + + val empty: t + + val find_goal: t -> goal (** find "next" goal *) + val is_empty: t -> bool (** a singleton empty level *) + val of_metasenv: Cic.metasenv -> t + val head_switches: t -> switch list (** top level switches *) + val head_goals: t -> goal list (** top level goals *) + val head_tag: t -> tag (** top level tag *) + val shift_goals: t -> goal list (** second level goals *) + val open_goals: t -> goal list (** all (Open) goals *) + val goal_of_switch: switch -> goal + + (** @param int depth, depth 0 is the top of the stack *) + val fold: + env: ('a -> int -> tag -> locator -> 'a) -> + cont:('a -> int -> tag -> locator -> 'a) -> + todo:('a -> int -> tag -> locator -> 'a) -> + 'a -> t -> 'a + + val iter: (** @param depth as above *) + env: (int -> tag -> locator -> unit) -> + cont:(int -> tag -> locator -> unit) -> + todo:(int -> tag -> locator -> unit) -> + t -> unit + + val map: (** @param depth as above *) + env: (int -> tag -> locator list -> locator list) -> + cont:(int -> tag -> locator list -> locator list) -> + todo:(int -> tag -> locator list -> locator list) -> + t -> t + + val pp: t -> string +end + +(** {2 Functorial interface} *) + +module type Status = +sig + type input_status + type output_status + type tactic - val is_goal_closed: goal -> proof -> bool - val goals_of_proof: proof -> goal list + val id_tactic : tactic + val mk_tactic : (input_status -> output_status) -> tactic + val apply_tactic : tactic -> input_status -> output_status - val apply_tactic: - tactic -> proof -> goal -> - proof * goal list * goal list (** new proof, opened goals, closed goals *) + val goals : output_status -> goal list * goal list (** opened, closed goals *) + val set_goals: goal list * goal list -> output_status -> output_status + val get_stack : input_status -> Stack.t + val set_stack : Stack.t -> output_status -> output_status + + val inject : input_status -> output_status + val focus : goal -> output_status -> input_status end module type C = sig - type goal - type proof + type input_status + type output_status type tactic - type status - type tactical = | Tactic of tactic | Skip @@ -56,28 +108,19 @@ sig | Semicolon | Branch - | Shift of int option - | Select of goal list - | End + | Shift + | Pos of int + | Merge + | Focus of goal list + | Unfocus | Tactical of tactical - val eval: t -> status -> status - val init: proof -> status - - (** {2 Status accessors} *) - - val get_proof: status -> proof - val set_proof: proof -> status -> status - - type goal_switch = Open of goal | Closed of goal - val get_goals: status -> goal_switch list - - val is_completed: status -> bool + val eval: t -> input_status -> output_status end -module Make (E:Engine) : C - with type goal = E.goal - and type proof = E.proof - and type tactic = E.tactic +module Make (S: Status) : C + with type tactic = S.tactic + and type input_status = S.input_status + and type output_status = S.output_status diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index bb269411e..27cb1cc33 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -103,16 +103,19 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what = (* elim type ****************************************************************) -let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) - ?depth ?using what = - let elim what = P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what in - let elim_type_tac status = - let tac = T.thens ~start: (P.cut_tac what) - ~continuations:[elim (C.Rel 1); T.id_tac] - in - E.apply_tactic tac status - in - E.mk_tactic elim_type_tac +let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth + ?using what += + let elim what = + P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what + in + let elim_type_tac status = + let tac = + T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] + in + E.apply_tactic tac status + in + E.mk_tactic elim_type_tac (* decompose ****************************************************************) diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 3d5626afa..827d58bbc 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -23,9 +23,9 @@ * http://cs.unibo.it/helm/. *) -open CicReduction +(* open CicReduction open ProofEngineTypes -open UriManager +open UriManager *) (** DEBUGGING *) @@ -34,7 +34,7 @@ let debug = false let debug_print = fun _ -> () (** debugging print *) -let warn s = debug_print (lazy ("TACTICALS WARNING: " ^ (Lazy.force s))) +let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s))) let id_tac = let id_tac (proof,goal) = @@ -42,255 +42,373 @@ let id_tac = let _, _, _ = CicUtil.lookup_meta goal metasenv in (proof,[goal]) in - mk_tactic id_tac + ProofEngineTypes.mk_tactic id_tac let fail_tac = let fail_tac (proof,goal) = let _, metasenv, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in - raise (Fail (lazy "fail tactical")) + raise (ProofEngineTypes.Fail (lazy "fail tactical")) in - mk_tactic fail_tac - -module type Status = - sig - type input_status - type output_status - type tactic - val id_tac : tactic - val mk_tactic : (input_status -> output_status) -> tactic - val apply_tactic : tactic -> input_status -> output_status - val goals : output_status -> ProofEngineTypes.goal list - val set_goals: output_status -> ProofEngineTypes.goal list -> output_status - val focus : output_status -> ProofEngineTypes.goal -> input_status - end + ProofEngineTypes.mk_tactic fail_tac + +type goal = ProofEngineTypes.goal + + (** TODO needed until tactics start returning both opened and closed goals + * First part of the function performs a diff among goals ~before tactic + * application and ~after it. Second part will add as both opened and closed + * the goals which are returned as opened by the tactic *) +let goals_diff ~before ~after ~opened = + let sort_opened opened add = + opened @ (List.filter (fun g -> not (List.mem g opened)) add) + in + let remove = + List.fold_left + (fun remove e -> if List.mem e after then remove else e :: remove) + [] before + in + let add = + List.fold_left + (fun add e -> if List.mem e before then add else e :: add) + [] + after + in + let add, remove = (* adds goals which have been both opened _and_ closed *) + List.fold_left + (fun (add, remove) opened_goal -> + if List.mem opened_goal before + then opened_goal :: add, opened_goal :: remove + else add, remove) + (add, remove) + opened + in + sort_opened opened add, remove module type T = - sig +sig type tactic - val first: tactics: (string * tactic) list -> tactic - val thens: start: tactic -> continuations: tactic list -> tactic - val then_: start: tactic -> continuation: tactic -> tactic - - (** "folding" of then_ *) val seq: tactics: tactic list -> tactic - val repeat_tactic: tactic: tactic -> tactic - val do_tactic: n: int -> tactic: tactic -> tactic - val try_tactic: tactic: tactic -> tactic - val solve_tactics: tactics: (string * tactic) list -> tactic - end -module Make (S:Status) : T with type tactic = S.tactic = + val tactic: tactic -> tactic + val skip: tactic + val dot: tactic + val semicolon: tactic + val branch: tactic + val shift: tactic + val pos: int -> tactic + val merge: tactic + val focus: int list -> tactic + val unfocus: tactic +end + +module Make (S: Continuationals.Status) : T with type tactic = S.tactic = struct -type tactic = S.tactic + module C = Continuationals.Make (S) + + type tactic = S.tactic + + let fold_eval status ts = + let istatus = + List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts + in + S.inject istatus (** naive implementation of ORELSE tactical, try a sequence of tactics in turn: if one fails pass to the next one and so on, eventually raises (failure "no tactics left") *) -let first ~tactics = - let rec first ~(tactics: (string * tactic) list) status = - warn (lazy "in Tacticals.first"); - match tactics with - | (descr, tac)::tactics -> - warn (lazy ("Tacticals.first IS TRYING " ^ descr)); - (try - let res = S.apply_tactic tac status in - warn (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!")); - res - with - e -> - match e with - (Fail _) - | (CicTypeChecker.TypeCheckerFailure _) - | (CicUnification.UnificationFailure _) -> - warn (lazy ( - "Tacticals.first failed with exn: " ^ - Printexc.to_string e)); - first ~tactics status - | _ -> raise e (* [e] must not be caught ; let's re-raise it *) - ) - | [] -> raise (Fail (lazy "first: no tactics left")) - in - S.mk_tactic (first ~tactics) - - -let thens ~start ~continuations = - let thens ~start ~continuations status = - let output_status = S.apply_tactic start status in - let new_goals = S.goals output_status in - try - let output_status,goals = - List.fold_left2 - (fun (output_status,goals) goal tactic -> - let status = S.focus output_status goal in - let output_status' = S.apply_tactic tactic status in - let new_goals' = S.goals output_status' in - (output_status',goals@new_goals') - ) (output_status,[]) new_goals continuations - in - S.set_goals output_status goals - with - Invalid_argument _ -> - let debug = lazy (Printf.sprintf "thens: expected %i new goals, found %i" - (List.length continuations) (List.length new_goals)) + let first ~tactics = + let rec first ~(tactics: (string * tactic) list) istatus = + info (lazy "in Tacticals.first"); + match tactics with + | (descr, tac)::tactics -> + info (lazy ("Tacticals.first IS TRYING " ^ descr)); + (try + let res = S.apply_tactic tac istatus in + info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!")); + res + with + e -> + match e with + | (ProofEngineTypes.Fail _) + | (CicTypeChecker.TypeCheckerFailure _) + | (CicUnification.UnificationFailure _) -> + info (lazy ( + "Tacticals.first failed with exn: " ^ + Printexc.to_string e)); + first ~tactics istatus + | _ -> raise e) (* [e] must not be caught ; let's re-raise it *) + | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left")) in - raise (Fail debug) - in - S.mk_tactic (thens ~start ~continuations ) - - -let then_ ~start ~continuation = - let then_ ~start ~continuation status = - let output_status = S.apply_tactic start status in - let new_goals = S.goals output_status in - let output_status,goals = - List.fold_left - (fun (output_status,goals) goal -> - let status = S.focus output_status goal in - let output_status' = S.apply_tactic continuation status in - let new_goals' = S.goals output_status' in - (output_status',goals@new_goals') - ) (output_status,[]) new_goals - in - S.set_goals output_status goals - in - S.mk_tactic (then_ ~start ~continuation) - -let rec seq ~tactics = - match tactics with - | [] -> assert false - | [tac] -> tac - | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) - -(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) - -(* This keep on appling tactic until it fails *) -(* When generates more than one goal, you have a tree of - application on the tactic, repeat_tactic works in depth on this tree *) - -let repeat_tactic ~tactic = - let rec repeat_tactic ~tactic status = - warn (lazy "in repeat_tactic"); - try - let output_status = S.apply_tactic tactic status in - let goallist = S.goals output_status in - let rec step output_status goallist = - match goallist with - [] -> output_status,[] - | head::tail -> - let status = S.focus output_status head in - let output_status' = repeat_tactic ~tactic status in - let goallist' = S.goals output_status' in - let output_status'',goallist'' = step output_status' tail in - output_status'',goallist'@goallist'' + S.mk_tactic (first ~tactics) + + let thens ~start ~continuations = + S.mk_tactic + (fun istatus -> + fold_eval istatus + ([ C.Tactical (C.Tactic start); C.Branch ] + @ (HExtlib.list_concat ~sep:[ C.Shift ] + (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations)) + @ [ C.Merge ])) + +(* let thens ~start ~continuations = + let thens ~start ~continuations status = + let output_status = S.apply_tactic start status in + let new_goals = S.goals output_status in + try + let output_status,goals = + List.fold_left2 + (fun (output_status,goals) goal tactic -> + let status = S.focus goal output_status in + let output_status' = S.apply_tactic tactic status in + let new_goals' = S.goals output_status' in + (output_status',goals@new_goals') + ) (output_status,[]) new_goals continuations + in + S.set_goals output_status goals + with + Invalid_argument _ -> + let debug = Printf.sprintf "thens: expected %i new goals, found %i" + (List.length continuations) (List.length new_goals) + in + raise (Fail debug) in - let output_status,goallist = step output_status goallist in - S.set_goals output_status goallist - with - (Fail _) as e -> - warn (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ; - S.apply_tactic S.id_tac status - in - S.mk_tactic (repeat_tactic ~tactic) - - -(* This tries to apply tactic n times *) -let do_tactic ~n ~tactic = - let rec do_tactic ~n ~tactic status = - if n = 0 then - S.apply_tactic S.id_tac status - else - try - let output_status = S.apply_tactic tactic status in - let goallist = S.goals output_status in - let rec step output_status goallist = - match goallist with - [] -> output_status, [] - | head::tail -> - let status = S.focus output_status head in - let output_status' = do_tactic ~n:(n-1) ~tactic status in - let goallist' = S.goals output_status' in - let (output_status'', goallist'') = step output_status' tail in - output_status'', goallist'@goallist'' + S.mk_tactic (thens ~start ~continuations ) *) + + let then_ ~start ~continuation = + S.mk_tactic + (fun istatus -> + fold_eval istatus + [ C.Tactical (C.Tactic start); + C.Semicolon; + C.Tactical (C.Tactic continuation) ]) + +(* let then_ ~start ~continuation = + let then_ ~start ~continuation status = + let output_status = S.apply_tactic start status in + let new_goals = S.goals output_status in + let output_status,goals = + List.fold_left + (fun (output_status,goals) goal -> + let status = S.focus goal output_status in + let output_status' = S.apply_tactic continuation status in + let new_goals' = S.goals output_status' in + (output_status',goals@new_goals') + ) (output_status,[]) new_goals in - let output_status,goals = step output_status goallist in - S.set_goals output_status goals - with - (Fail _) as e -> - warn (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ; - S.apply_tactic S.id_tac status - in - S.mk_tactic (do_tactic ~n ~tactic) - - - -(* This applies tactic and catches its possible failure *) -let try_tactic ~tactic = - let rec try_tactic ~tactic status = - warn (lazy "in Tacticals.try_tactic"); - try - S.apply_tactic tactic status - with - (Fail _) as e -> - warn (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); - S.apply_tactic S.id_tac status - in - S.mk_tactic (try_tactic ~tactic) - -(* This tries tactics until one of them doesn't _solve_ the goal *) -(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) -let solve_tactics ~tactics = - let rec solve_tactics ~(tactics: (string * tactic) list) status = - warn (lazy "in Tacticals.solve_tactics"); - match tactics with - | (descr, currenttactic)::moretactics -> - warn (lazy ("Tacticals.solve_tactics is trying " ^ descr)); - (try - let output_status = S.apply_tactic currenttactic status in - let goallist = S.goals output_status in - match goallist with - [] -> warn (lazy ("Tacticals.solve_tactics: " ^ descr ^ - " solved the goal!!!")); -(* questo significa che non ci sono piu' goal, o che current_tactic non ne - ha aperti di nuovi? (la 2a!) ##### - nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) - output_status - | _ -> warn (lazy ("Tacticals.solve_tactics: try the next tactic")); - solve_tactics ~tactics:(moretactics) status - with - (Fail _) as e -> - warn (lazy ("Tacticals.solve_tactics: current tactic failed with exn: " ^ - Printexc.to_string e)); - solve_tactics ~tactics status - ) - | [] -> raise (Fail (lazy "solve_tactics cannot solve the goal")); - S.apply_tactic S.id_tac status - in - S.mk_tactic (solve_tactics ~tactics) + S.set_goals output_status goals + in + S.mk_tactic (then_ ~start ~continuation) *) + + let seq ~tactics = + S.mk_tactic + (fun istatus -> + fold_eval istatus + (HExtlib.list_concat ~sep:[ C.Semicolon ] + (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics))) + +(* let rec seq ~tactics = + match tactics with + | [] -> assert false + | [tac] -> tac + | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) *) + + (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno + * applicato la tattica *) + + let rec step f output_status opened closed = + match opened with + | [] -> output_status, [], closed + | head :: tail -> + let status = S.focus head output_status in + let output_status' = f status in + let opened', closed' = S.goals output_status' in + let output_status'', opened'', closed'' = + step f output_status' tail [] + in + output_status'', opened' @ opened'', closed' @ closed'' + + (* This keep on appling tactic until it fails. When generates more + * than one goal, you have a tree of application on the tactic, repeat_tactic + * works in depth on this tree *) + let repeat_tactic ~tactic = + let rec repeat_tactic ~tactic status = + info (lazy "in repeat_tactic"); + try +(* let rec step output_status opened closed = + match opened with + | [] -> output_status, [], closed + | head :: tail -> + let status = S.focus head output_status in + let output_status' = repeat_tactic ~tactic status in + let opened', closed' = S.goals output_status' in + let output_status'', opened'', closed'' = + step output_status' tail [] + in + output_status'', opened' @ opened'', closed' @ closed'' + in *) + let output_status = S.apply_tactic tactic status in + let opened, closed = S.goals output_status in + let output_status, opened', closed' = + step (repeat_tactic ~tactic) output_status opened closed + in + S.set_goals (opened', closed') output_status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy + ("Tacticals.repeat_tactic failed after nth time with exception: " + ^ Printexc.to_string e)); + S.apply_tactic S.id_tactic status + in + S.mk_tactic (repeat_tactic ~tactic) + + (* This tries to apply tactic n times *) + let do_tactic ~n ~tactic = + let rec do_tactic ~n ~tactic status = + if n = 0 then + S.apply_tactic S.id_tactic status + else + try + let output_status = S.apply_tactic tactic status in + let opened, closed = S.goals output_status in +(* let rec step output_status goallist = + match goallist with + [] -> output_status, [] + | head::tail -> + let status = S.focus head output_status in + let output_status' = do_tactic ~n:(n-1) ~tactic status in + let goallist' = S.goals output_status' in + let (output_status'', goallist'') = step output_status' tail in + output_status'', goallist'@goallist'' + in *) + let output_status, opened', closed' = + step (do_tactic ~n:(n-1) ~tactic) output_status opened closed + in + S.set_goals (opened', closed') output_status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy + ("Tacticals.do_tactic failed after nth time with exception: " + ^ Printexc.to_string e)) ; + S.apply_tactic S.id_tactic status + in + S.mk_tactic (do_tactic ~n ~tactic) + + (* This applies tactic and catches its possible failure *) + let try_tactic ~tactic = + let rec try_tactic ~tactic status = + info (lazy "in Tacticals.try_tactic"); + try + S.apply_tactic tactic status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy ( + "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); + S.apply_tactic S.id_tactic status + in + S.mk_tactic (try_tactic ~tactic) + + (* This tries tactics until one of them doesn't _solve_ the goal *) + (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) + let solve_tactics ~tactics = + let rec solve_tactics ~(tactics: (string * tactic) list) status = + info (lazy "in Tacticals.solve_tactics"); + match tactics with + | (descr, currenttactic)::moretactics -> + info (lazy ("Tacticals.solve_tactics is trying " ^ descr)); + (try + let output_status = S.apply_tactic currenttactic status in + let opened, closed = S.goals output_status in + match opened with + | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ + " solved the goal!!!")); + (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha + * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che + * solve_tactics has solved the goal? (si!) *) + output_status + | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic")); + solve_tactics ~tactics:(moretactics) status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy ( + "Tacticals.solve_tactics: current tactic failed with exn: " + ^ Printexc.to_string e)); + solve_tactics ~tactics status + ) + | [] -> + raise (ProofEngineTypes.Fail + (lazy "solve_tactics cannot solve the goal")) + in + S.mk_tactic (solve_tactics ~tactics) + + let cont_proxy cont = S.mk_tactic (C.eval cont) + + let tactic t = cont_proxy (C.Tactical (C.Tactic t)) + let skip = cont_proxy (C.Tactical C.Skip) + let dot = cont_proxy C.Dot + let semicolon = cont_proxy C.Semicolon + let branch = cont_proxy C.Branch + let shift = cont_proxy C.Shift + let pos i = cont_proxy (C.Pos i) + let merge = cont_proxy C.Merge + let focus goals = cont_proxy (C.Focus goals) + let unfocus = cont_proxy C.Unfocus end module ProofEngineStatus = - struct - type input_status = ProofEngineTypes.status - type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list - type tactic = ProofEngineTypes.tactic - let id_tac = id_tac - let mk_tactic = ProofEngineTypes.mk_tactic - let apply_tactic = ProofEngineTypes.apply_tactic - let goals (_,goals) = goals - let set_goals (proof,_) goals = proof,goals - let focus (proof,_) goal = proof,goal - end - -module ProofEngineTacticals = Make(ProofEngineStatus) +struct + module Stack = Continuationals.Stack + + type input_status = + ProofEngineTypes.status (* (proof, goal) *) * Stack.t + + type output_status = + (ProofEngineTypes.proof * goal list * goal list) * Stack.t + + type tactic = ProofEngineTypes.tactic + + let id_tactic = id_tac + + let mk_tactic f = + ProofEngineTypes.mk_tactic + (fun (proof, goal) as pstatus -> + let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in + let istatus = pstatus, stack in +(* let ostatus = f istatus in + let ((proof, opened, _), _) = ostatus in *) + let (proof, _, _), stack = f istatus in + let opened = Continuationals.Stack.open_goals stack in + proof, opened) + + let apply_tactic tac ((proof, _) as pstatus, stack) = + let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in +(* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *) + let before = ProofEngineTypes.goals_of_proof proof in + let after = ProofEngineTypes.goals_of_proof proof' in + let opened_goals, closed_goals = goals_diff ~before ~after ~opened in +(* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *) + (proof', opened_goals, closed_goals), stack + + let goals ((_, opened, closed), _) = opened, closed + let set_goals (opened, closed) ((proof, _, _), stack) = + (proof, opened, closed), stack + + let get_stack = snd + let set_stack stack (opstatus, _) = opstatus, stack + + let inject ((proof, _), stack) = ((proof, [], []), stack) + let focus goal ((proof, _, _), stack) = (proof, goal), stack +end + +module ProofEngineTacticals = Make (ProofEngineStatus) include ProofEngineTacticals + diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli index 06afc21dc..88fafc1f8 100644 --- a/helm/ocaml/tactics/tacticals.mli +++ b/helm/ocaml/tactics/tacticals.mli @@ -26,41 +26,67 @@ val id_tac : ProofEngineTypes.tactic val fail_tac: ProofEngineTypes.tactic -module type Status = +(* module type Status = sig +|+ type external_input_status +| type input_status type output_status +|+ type external_output_status +| + +|+ val internalize: external_input_status -> input_status + val externalize: output_status -> external_output_status +| + type tactic - val id_tac : tactic + val mk_tactic : (input_status -> output_status) -> tactic val apply_tactic : tactic -> input_status -> output_status + + val id_tac : tactic + val goals : output_status -> ProofEngineTypes.goal list - val set_goals: output_status -> ProofEngineTypes.goal list -> output_status - val focus : output_status -> ProofEngineTypes.goal -> input_status - end + val get_stack : input_status -> stack + val set_stack : stack -> output_status -> output_status + + val inject : input_status -> output_status + val focus : goal -> output_status -> input_status + end *) module type T = - sig +sig type tactic val first: tactics: (string * tactic) list -> tactic - val thens: start: tactic -> continuations: tactic list -> tactic - val then_: start: tactic -> continuation: tactic -> tactic - - (** "folding" of then_ *) - val seq: tactics: tactic list -> tactic - + val seq: tactics: tactic list -> tactic (** "folding" of then_ *) val repeat_tactic: tactic: tactic -> tactic - val do_tactic: n: int -> tactic: tactic -> tactic - val try_tactic: tactic: tactic -> tactic - val solve_tactics: tactics: (string * tactic) list -> tactic - end -module Make (S:Status) : T with type tactic = S.tactic +(* module C: + sig *) + val tactic: tactic -> tactic (** apply tactic to all goal in env *) + val skip: tactic + val dot: tactic + val semicolon: tactic + val branch: tactic + val shift: tactic + val pos: int -> tactic + val merge: tactic + val focus: int list -> tactic + val unfocus: tactic +(* end *) +end + +module Make (S: Continuationals.Status) : T with type tactic = S.tactic include T with type tactic = ProofEngineTypes.tactic + +(* TODO temporary *) +val goals_diff: + before:ProofEngineTypes.goal list -> + after:ProofEngineTypes.goal list -> + opened:ProofEngineTypes.goal list -> + ProofEngineTypes.goal list * ProofEngineTypes.goal list +