Istari

Tactic

signature TACTIC =
   sig
      
      type goal = Judgement.judgement * Directory.directory
      type validation = Refine.validation
      type validator = validation list -> validation * validation list
      type answer = exn

      (* The success continuation takes the failure continuation as an argument.
         It can be used to backtrack.
      *)

      type 'a tacticm = 
         goal
         -> (string -> answer)                                              (* failure continuation *)
         -> (('a * goal) list * validator * (string -> answer) -> answer)   (* success continuation *)
         -> answer

      type tactic = Message.label tacticm

      datatype priority = Primary | Secondary



      (* control flow *)

      val idtac : tactic
      val idtacM : 'a -> 'a tacticm
      val fail : string -> 'a tacticm
      val cut : 'a tacticm -> 'a tacticm
      val lift : (unit -> 'a tacticm) -> 'a tacticm
      val done : 'a tacticm  (* Like fail, but without the stigma. *)


      (* combination *)

      val andthen : 'a tacticm -> 'b tacticm -> 'b tacticm
      val andthenl : 'a tacticm -> 'b tacticm list -> 'b tacticm
      val andthenlPad : 'a tacticm -> 'b tacticm list -> 'b tacticm -> 'b tacticm
      val andthenOn : int -> 'a tacticm -> 'a tacticm -> 'a tacticm
      val andthen1 : 'a tacticm -> 'b tacticm -> 'b tacticm

      val andthenM : 'a tacticm -> ('a -> 'b tacticm) -> 'b tacticm
      val andthenlM : 'a tacticm -> ('a -> 'b tacticm) list -> 'b tacticm
      val andthenlPadM : 'a tacticm -> ('a -> 'b tacticm) list -> ('a -> 'b tacticm) -> 'b tacticm
      val andthenOnM : int -> 'a tacticm -> ('a -> 'a tacticm) -> 'a tacticm

      val andthenFoldM :
         'a tacticm 
         -> ('a -> 'b -> 'c tacticm * 'b)
         -> ('b -> string option)
         -> 'b
         -> 'c tacticm

      val andthenPri : priority tacticm -> priority tacticm -> priority tacticm
      val andthenlPri : priority tacticm -> priority tacticm list -> priority tacticm
      val andthenlPadPri : priority tacticm -> priority tacticm list -> priority tacticm -> priority tacticm

      val attempt : tactic -> tactic
      val first : 'a tacticm list -> 'a tacticm
      val repeat : tactic -> tactic
      val repeatCount : tactic -> int tacticm
      val repeatn : int -> tactic -> tactic
      val orthen : 'a tacticm -> (unit -> 'a tacticm) -> 'a tacticm

      val ifthen : 'a tacticm -> 'b tacticm -> 'b tacticm -> 'b tacticm
      val ifthenM : 'a tacticm -> ('a -> 'b tacticm) -> 'b tacticm -> 'b tacticm


      (* direct computation *)

      val replaceJudgement : Judgement.judgement -> tactic
      val replaceHyp : int -> Judgement.hyp -> tactic
      val replaceConcl : Term.term -> tactic


      (* miscellaneous *)

      val withgoal : (goal -> 'a tacticm) -> 'a tacticm
      val withidir : (Directory.idirectory -> 'a tacticm) -> 'a tacticm
      val withterm : ETerm.eterm -> (Term.term -> 'a tacticm) -> 'a tacticm
      val withHeadConst : string -> (Constant.constant -> 'a tacticm) -> 'a tacticm

      val setFailure : string -> 'a tacticm -> 'a tacticm
      val transformFailure : (string -> string) -> 'a tacticm -> 'a tacticm

      exception Tryf of string
      val tryf : (unit -> 'a) -> ('a -> 'b tacticm) -> 'b tacticm

      val displayTac : string -> tactic


      (* primitive actions *)

      val refine : Rule.rule -> tactic
      val chdir : Directory.directory -> tactic
      val cast : Judgement.judgement -> Refine.validation -> tactic
      val execute : goal -> tactic -> (Refine.validation, string) Sum.sum


      val >> : 'a tacticm -> 'b tacticm -> 'b tacticm                           (* andthen *)
      val >>> : 'a tacticm -> 'b tacticm list -> 'b tacticm                     (* andthenl *)
      val >>+ : 'a tacticm -> 'b tacticm -> 'b tacticm                          (* andthen1 *)
      val >>= : 'a tacticm -> ('a -> 'b tacticm) -> 'b tacticm                  (* andthenM *)
      val >>>= : 'a tacticm -> ('a -> 'b tacticm) list -> 'b tacticm            (* andthenlM *)
      val >>! : priority tacticm -> priority tacticm -> priority tacticm        (* andthenPri *)
      val >>>! : priority tacticm -> priority tacticm list -> priority tacticm  (* andthenlPri *)

   end

This site is open source. Improve this page.