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