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