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"
--- /dev/null
+<?xml version="1.0"?>
+<b:box xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:b="http://helm.cs.unibo.it/2003/BoxML">
+ <b:h>
+ <b:space width="2em"/>
+ <b:v>
+ <b:space height="2ex"/>
+ <b:v>
+ <b:decor style="box">
+ <b:space width="1ex" height="1ex"/>
+ </b:decor>
+ <b:space height="1ex"/>
+ <b:text>This goal has already been closed.</b:text>
+ <b:text>Use the "skip" command to throw it away.</b:text>
+ </b:v>
+ </b:v>
+ </b:h>
+</b:box>
lablgtkmathview \
lablgtksourceview \
helm-xmldiff \
+helm-tactics \
"
for r in $FINDLIB_REQUIRES
do
<accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image552">
+ <widget class="GtkImage" id="image680">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image553">
+ <widget class="GtkImage" id="image681">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image554">
+ <widget class="GtkImage" id="image682">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image555">
+ <widget class="GtkImage" id="image683">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image556">
+ <widget class="GtkImage" id="image684">
<property name="visible">True</property>
<property name="stock">gtk-execute</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image557">
+ <widget class="GtkImage" id="image685">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image558">
+ <widget class="GtkImage" id="image686">
<property name="visible">True</property>
<property name="stock">gtk-undo</property>
<property name="icon_size">1</property>
<accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image559">
+ <widget class="GtkImage" id="image687">
<property name="visible">True</property>
<property name="stock">gtk-redo</property>
<property name="icon_size">1</property>
<accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image560">
+ <widget class="GtkImage" id="image688">
<property name="visible">True</property>
<property name="stock">gtk-cut</property>
<property name="icon_size">1</property>
<accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image561">
+ <widget class="GtkImage" id="image689">
<property name="visible">True</property>
<property name="stock">gtk-copy</property>
<property name="icon_size">1</property>
<accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image562">
+ <widget class="GtkImage" id="image690">
<property name="visible">True</property>
<property name="stock">gtk-paste</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image563">
+ <widget class="GtkImage" id="image691">
<property name="visible">True</property>
<property name="stock">gtk-delete</property>
<property name="icon_size">1</property>
<child>
<widget class="GtkImageMenuItem" id="findReplMenuItem">
<property name="visible">True</property>
- <property name="label" translatable="yes">_Find & Replace</property>
+ <property name="label" translatable="yes">_Find & Replace ...</property>
<property name="use_underline">True</property>
<accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image564">
+ <widget class="GtkImage" id="image692">
<property name="visible">True</property>
<property name="stock">gtk-find-and-replace</property>
<property name="icon_size">1</property>
</child>
</widget>
</child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator8">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="externalEditorMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Edit with E_xternal Editor</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
<accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image565">
+ <widget class="GtkImage" id="image693">
<property name="visible">True</property>
<property name="stock">gtk-zoom-in</property>
<property name="icon_size">1</property>
<accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image566">
+ <widget class="GtkImage" id="image694">
<property name="visible">True</property>
<property name="stock">gtk-zoom-out</property>
<property name="icon_size">1</property>
<accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image567">
+ <widget class="GtkImage" id="image695">
<property name="visible">True</property>
<property name="stock">gtk-zoom-100</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image568">
+ <widget class="GtkImage" id="image696">
<property name="visible">True</property>
<property name="stock">gtk-about</property>
<property name="icon_size">1</property>
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 *)
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
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 *)
| [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
| `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) ->
| 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)
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
| 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
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
| 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
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
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:");
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 *)
| 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 =
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
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
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 (
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"
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 () =
(*
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:
?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:
?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:
?include_paths:string list ->
?clean_baseuri:bool ->
MatitaTypes.status ->
- statement ->
+ GrafiteParser.statement ->
MatitaTypes.status
val initial_status: MatitaTypes.status lazy_t
(".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
| 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;
~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))
* 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
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
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 =
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 *)
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 =
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 *)
| 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 _ =
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)
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
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
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
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
~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 *)
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 =
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
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 =
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 []
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 =
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 ());
current_mathml <- Some mathml);
end
+let tab_label meta_markup =
+ let rec aux =
+ function
+ | `Current m -> sprintf "<b>%s</b>" (aux m)
+ | `Closed m -> sprintf "<s>%s</s>" (aux m)
+ | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %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
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 ->
_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 ()
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
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);
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";
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
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
end
-let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
+let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
+ MatitaGuiTypes.sequentsViewer
+=
new sequentsViewer ~notebook ~cicMathView ()
let cicBrowser () =
:: (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
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
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
(** 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
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
open Printf
open MatitaTypes
+module TA = GrafiteAst
+
let debug = false
let debug_print = if debug then prerr_endline else ignore
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;
}
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
(* 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
| _ -> 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
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
| 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
| [_,_,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
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:"."
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;
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
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
[], 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";
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
| 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 -> ()
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
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
method private getFilename =
match guistuff.filenamedata with Some f,_ -> f | _ -> assert false
+
+ method filename = self#getFilename
method private ppFilename =
match guistuff.filenamedata with
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;
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
| 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
_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
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
* 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
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
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
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
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
| 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
module Ast = CicNotationPt
-let tactical_terminator = "."
+let tactical_terminator = ""
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
| 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
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
]
];
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 ]
];
| 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)
| 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)
| 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
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
]];
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)
]
];
* 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
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
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 \
introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
autoTactic.cmx tactics.cmi
-continuationals.cmo: continuationals.cmi
-continuationals.cmx: continuationals.cmi
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:
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
| 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
| 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 <abs>"
- 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
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
| 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
(* 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 ****************************************************************)
* http://cs.unibo.it/helm/.
*)
-open CicReduction
+(* open CicReduction
open ProofEngineTypes
-open UriManager
+open UriManager *)
(** DEBUGGING *)
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) =
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 <tactic> 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 <tactic> 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
+
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
+
projects / helm.git / commitdiff