1 module Tactics where
    2 
    3 import Core_datatype
    4 import X_interface
    5 
    6 import Vtslib
    7 
    8 import Globals
    9 
   10 import Lookup
   11 
   12 import Kernel
   13 
   14 import Edlib
   15 
   16 import Goals
   17 
   18 import Tags     -- partain
   19 
   20 import Tree
   21 
   22 import Type_defs
   23 
   24 data TACTIC 
   25         = Tactic String               
   26                 ( Global_state -> Lookup_table -> Obj -> Xin ->
   27                           Xst ( MayBe ( Option [String] ) String ) )
   28                 ( Global_state -> Sgn -> Lookup_table -> Option [String] -> Obj
   29                    -> MayBe ([Obj] , ( [Option Done] -> Option Done )) String )
   30 
   31 data Ordered_tactic 
   32         = OrdTactic String
   33                    ( Global_state -> Lookup_table -> Obj -> Xin ->
   34                           Xst ( MayBe ( Option [String] ) String ) )
   35                    ( Global_state -> Sgn -> Lookup_table -> 
   36                      Option [String] -> Obj -> 
   37                       MayBe ( [Obj] , [Lookup_table] , [Bool] ,
   38                          ([Option Done] -> [Bool] -> 
   39                           ( [Bool] , [Sgn] , Option Done ))) String )
   40 
   41 
   42 
   43 
   44 lift_tactic (Tactic name arg_fn subgoal_fn) 
   45     = ( name , lift )
   46       where
   47       lift (TreeSt t@(Tree g [] dn vf u) spine gst ) 
   48           = arg_fn gst lt obj /./
   49             exp
   50             where
   51             (Goal NONE NONE com uid obj rw sg lt) = g
   52             exp args 
   53                 = return_val ( subgoal_fn gst sg lt args obj ) /./
   54                   exp'
   55                   where
   56                   exp' ( subgoals , valid_fn ) 
   57                         = make_goal1 sg lt subgoals [] /./
   58                           exp'' 
   59                           where
   60                           exp'' subtrees
   61                                = reTurn ( TreeSt (vf' gst t1) spine gst )
   62                                  where
   63                                  vf' = lift_tactic_valid valid_fn
   64                                  g1 =Goal (SOME name) args com uid obj rw sg lt
   65                                  t1 = Tree g1 subtrees NONE vf' (SOME t)
   66       lift _ = return_err "cannot apply tactic" 
   67 
   68 
   69 
   70 lift_ordtactic (OrdTactic name arg_fn subgoal_fn) 
   71     = ( name , lift )
   72       where
   73       lift (TreeSt t@(Tree g [] dn vf u) spine gst ) 
   74           = arg_fn gst lt obj /./
   75             exp
   76             where
   77             (Goal NONE NONE com uid obj rw sg lt) = g
   78             exp args 
   79                 = return_val ( subgoal_fn gst sg lt args obj ) /./
   80                   exp'
   81                   where
   82                   exp' ( subgoals , ltL , rwL , valid_fn )
   83                        = make_goal2 sg (zip ltL (zip rwL subgoals)) [] /./
   84                          exp''
   85                          where
   86                          exp'' subtrees
   87                                 = reTurn ( TreeSt (vf' gst t1) spine gst )
   88                                   where
   89                                   vf' = lift_ordtactic_valid valid_fn
   90                                   g1 =Goal (SOME name) args com uid obj rw sg lt
   91                                   t1 = Tree g1 subtrees NONE vf' (SOME t)
   92       lift _ = return_err "cannot apply tactic" 
   93 
   94 
   95 
   96 lift_tactic_valid vf gst t@(Tree g tl NONE vf' u) 
   97         = Tree g tl dn vf' u
   98 --        `handle`
   99 --         _ -> t
  100           where
  101           dnL = map get_done tl
  102           dn  = vf dnL 
  103 
  104 lift_tactic_valid _ _ t = t
  105 
  106 
  107 
  108 
  109 lift_ordtactic_valid vf gst t @(Tree g tl NONE vf' u) 
  110         = Tree g tl' dn vf' u
  111 --          handle _ => t
  112           where
  113           dnL = map get_done tl
  114           bL  = map get_rw tl
  115           (bL',sgL,dn) = vf dnL bL
  116           tl' = map set_info (zip tl (zip bL' sgL))
  117 
  118 lift_ordtactic_valid _ _ t = t
  119 
  120 
  121 
  122 
  123 make_goal1 sg lt ( obj : objL ) glL
  124         = make_goal1' sg lt obj /./
  125           ( \ gl -> make_goal1  sg lt objL ( glL <: gl ))
  126 
  127 make_goal1 _ _ [] glL 
  128         = reTurn glL 
  129 
  130 
  131 
  132 
  133 make_goal1' sg lt obj
  134         = genuid /./
  135           ( \ uid -> reTurn ( Tree (Goal NONE NONE NONE uid obj True sg lt)
  136                                                          [] NONE id' NONE ))
  137 
  138 
  139 
  140 make_goal2 sg ((lt, (rw, obj)) : pL ) glL 
  141         = make_goal2' sg lt rw obj /./
  142           ( \ gl -> make_goal2  sg pL ( glL <: gl ))
  143 
  144 make_goal2 _ [] glL 
  145         = reTurn glL 
  146 
  147 
  148 
  149 
  150 make_goal2' sg lt rw obj
  151         = genuid /./
  152           ( \ uid -> reTurn ( Tree (Goal NONE NONE NONE uid 
  153                                         obj rw sg lt) [] NONE id' NONE ))
  154 
  155 
  156 get_done (Tree _ _ dn _ _) = dn
  157 
  158 get_rw (Tree (Goal _ _ _ _ _ rw _ _) _ _ _ _) = rw
  159 
  160 set_info (Tree (Goal cmd arg com uid obj _ _ lt) tl dn vf u , (rw,sg)) 
  161         = Tree (Goal cmd arg com uid obj rw sg lt) tl dn vf u
  162 
  163 id' x y = y
  164 
  165 null_arg_fn gst lt spc = reTurn NONE