X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.mli;h=88fafc1f8bf5e91be97802e7fcfea51bc44c5d75;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d7cc2754575375a55b1a7467289527a2f11af931;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli index d7cc27545..88fafc1f8 100644 --- a/helm/ocaml/tactics/tacticals.mli +++ b/helm/ocaml/tactics/tacticals.mli @@ -23,39 +23,70 @@ * http://cs.unibo.it/helm/. *) - val id_tac : ProofEngineTypes.tactic +val fail_tac: ProofEngineTypes.tactic + +(* 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 mk_tactic : (input_status -> output_status) -> tactic + val apply_tactic : tactic -> input_status -> output_status - (* tacticals *) -val try_tactics: - tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic + val id_tac : tactic -val thens: - start: ProofEngineTypes.tactic -> - continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic + val goals : output_status -> ProofEngineTypes.goal list + val get_stack : input_status -> stack + val set_stack : stack -> output_status -> output_status -val then_: - start: ProofEngineTypes.tactic -> - continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + val inject : input_status -> output_status + val focus : goal -> output_status -> input_status + end *) - (** "folding" of then_ *) -val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic +module type T = +sig + type tactic -val repeat_tactic: - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + val first: tactics: (string * tactic) list -> tactic + val thens: start: tactic -> continuations: tactic list -> tactic + val then_: start: tactic -> continuation: tactic -> 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 -val do_tactic: - n: int -> - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.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 -val try_tactic: - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic +module Make (S: Continuationals.Status) : T with type tactic = S.tactic -val solve_tactics: - tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic +include T with type tactic = ProofEngineTypes.tactic -val fail: 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 -(* -val prova_tac : ProofEngineTypes.tactic -*)