1 module Tacticals where
    2 
    3 import Core_datatype
    4 import Kernel
    5 import Lookup
    6 import X_interface
    7 
    8 import Tactics
    9 
   10 import Goals
   11 import Globals   -- partain
   12 import Tags         -- partain
   13 
   14 import Tree
   15 
   16 import Edlib
   17 
   18 import Type_defs
   19 
   20 import Vtslib
   21 
   22 
   23 
   24 infixr 5 `orelse`
   25 
   26 infixr 4 `andthen`
   27 
   28 
   29 
   30 orelse f1 f2 trst 
   31         = f1 trst
   32           `handle` 
   33           ( \ _ -> f2 trst )
   34 
   35 
   36 
   37 andthen f1 f2 trst 
   38         = f1 trst     /./
   39           subtrst f2 
   40 
   41 
   42 repeat_tac f trst 
   43         = f trst /./
   44           ( \ trst' -> subtrst (repeat_tac f) trst' 
   45                        `handle` 
   46                        ( \ _ -> reTurn trst ))
   47 
   48 
   49 
   50 for' 0 f trst = reTurn trst
   51 
   52 for' i f trst 
   53         = f trst                  /./
   54           subtrst (for' (i-1) f) 
   55 
   56 
   57 
   58 subtrst f trst@(TreeSt (Tree _ trL _ _ _) _ _) 
   59         = subtrst' 0 (length trL) f trst
   60 
   61 
   62 subtrst' i j f trst 
   63         | i >= j    = reTurn trst
   64         | otherwise = tree_down i trst   /./
   65                       f                  /./
   66                       tree_up            /./
   67                       subtrst' (i+1) j f