1 module Auto where 2 3 import Core_datatype 4 import Edlib 5 import Lookup 6 import Tree 7 import X_interface 8 9 import Vtslib 10 11 import Tactics 12 13 import Parse 14 15 import Type_defs 16 17 import Goals 18 import Globals -- partain 19 import Tags -- partain 20 21 import Kernel 22 23 24 auto_tac = Tactic "Auto" null_arg_fn auto 25 26 --split_tac = OrdTactic ("Split",null_arg_fn,split) 27 28 29 30 31 auto _ sg lt _ (TrmSpec tm) = auto_tm sg lt tm 32 33 auto _ sg lt _ (ThmSpec _) = Bad "Not Applicable" 34 35 auto _ sg lt _ (DecSpec dc) = auto_dc sg lt dc 36 37 auto _ sg1 lt _ (SgnSpec sg2) = auto_sg sg1 lt sg2 38 39 40 41 auto_tm sg lt tm = Ok ([], tm_valid (trm_to_Trm sg tm)) 42 43 44 auto_dc sg lt dc = Ok ([], dc_valid (dec_to_Dec sg dc)) 45 46 47 auto_sg sg0 lt sg = Ok ([], sg_valid (sgn_to_Sgn sg)) 48 49 50 51 tm_valid tm [] = SOME (TrmDone tm) 52 53 tm_valid _ _ = NONE 54 55 56 dc_valid dc [] = SOME (DecDone dc) 57 58 dc_valid _ _ = NONE 59 60 61 sg_valid sg [] = SOME (SgnDone sg) 62 63 sg_valid _ _ = NONE 64 65 {- 66 67 split _ Sg lt _ (TrmSpec tm) = split_tm Sg lt tm 68 69 split _ Sg lt _ (DecSpec dc) = split_dc Sg lt dc 70 71 split _ Sg lt _ (SgnSpec sg) = split_sg Sg lt sg 72 73 split _ Sg lt _ (ThmSpec _) = Bad "Not Applicable" 74 75 76 77 split_tm Sg lt tm@(Sym _ _ _ _) 78 = ([], [], [], lift_null_update Sg lt (tm_valid (trm_to_Trm Sg tm))) 79 80 split_tm Sg lt tm@(Constant _ _ _) = 81 ([], [], [], lift_null_update Sg lt (tm_valid (trm_to_Trm Sg tm))) 82 83 split_tm Sg lt tm@(Const _ _ _ _ _) 84 = ([], [], [], lift_null_update Sg lt (tm_valid (trm_to_Trm Sg tm))) 85 86 split_tm Sg lt tm@(App tm1 tm2 _ _) 87 = ([TrmSpec tm1,TrmSpec tm2],[lt,lt],[True,True], 88 lift_null_update Sg lt app_valid) 89 90 split_tm Sg lt tm@(Pair tm1 tm2 tm3 _ _) 91 = ([TrmSpec tm1,TrmSpec tm2,TrmSpec tm3],[lt,lt,lt],[True,True,True], 92 lift_null_update Sg lt pair_valid) 93 94 split_tm Sg lt tm@(Binder q dc tm1 _ _) 95 = ([DecSpec dc,TrmSpec tm1],[error "no lt"], [True,False], 96 binder_valid (binder_fn q) Sg) 97 98 split_tm Sg lt tm@(Cond dc tm1 tm2 _ _) 99 = ([DecSpec dc,TrmSpec tm1,TrmSpec tm2],[error "no lt"], 100 [True,False,False], cond_valid Sg) 101 102 split_tm Sg lt tm@(Unary u tm1 _ _) 103 = 104 ([TrmSpec tm1],[lt],[true], 105 lift_null_update Sg lt (unary_valid (unary_fn u))) 106 | split_tm Sg lt (tm as Binary (b,tm1,tm2,_,_)) = 107 ([TrmSpec tm1,TrmSpec tm2],[lt,lt],[true,true], 108 lift_null_update Sg lt (binary_valid (binary_fn b))) 109 | split_tm Sg lt (tm as Recurse (tmL,ty,_,_)) = 110 let val tmL1 = tmL @ [ty] 111 in (map TrmSpec tmL1, 112 map (fn x => lt) tmL1, 113 map (fn x => true) tmL1, 114 lift_null_update Sg lt recurse_valid) 115 end 116 117 and split_dc Sg lt (dc as Symbol_dec (tm,_)) = 118 ([TrmSpec tm],[lt],[true], 119 lift_null_update Sg lt (symbol_dec_valid symbol_dec)) 120 | split_dc Sg lt (dc as Axiom_dec (tm,_)) = 121 ([TrmSpec tm],[lt],[true], 122 lift_null_update Sg lt (symbol_dec_valid axiom_dec)) 123 | split_dc Sg lt (dc as Def (tm,_,_)) = 124 ([TrmSpec tm],[lt],[true], 125 lift_null_update Sg lt (symbol_dec_valid def)) 126 | split_dc Sg lt (dc as Decpair (dc1,dc2,_)) = 127 ([DecSpec dc1, DecSpec dc2],[lt,extend_lookup_table true dc1 lt], 128 [true,false], decpair_valid Sg) 129 | split_dc Sg lt (dc as Data (dcL, tmLL,_)) = 130 fail "Can't split datatypes yet!" 131 132 and split_sg Sg lt (Empty _) = ( [], [],[], 133 lift_null_update Sg lt (empty_valid) ) 134 | split_sg Sg lt (Extend (dc,sg,_)) = 135 ([SgnSpec sg, DecSpec dc],[lt,extend_lookup_table true dc lt], 136 [true,false], extend_valid Sg) 137 | split_sg Sg lt (Combine _) = 138 fail "Can't split combine yet!" 139 | split_sg Sg lt (Share _) = 140 fail "Can't split combine yet!" 141 142 and empty_valid [] = SOME (SgnDone empty) 143 144 and extend_valid Sg dnL rwL = 145 case (dnL, rwL) 146 of ([SOME (SgnDone Sg), SOME (DecDone dc)],_) => 147 (rwL,[Sg,Sg],SOME (SgnDone (extend dc Sg))) 148 | ([SOME (SgnDone Sg), NONE], [true,false]) => 149 ([true,true],[Sg,Sg],NONE) 150 | _ => (rwL,[Sg,Sg],NONE) 151 152 and symbol_dec_valid f [SOME (TrmDone tm)] = 153 SOME (DecDone (f tm)) 154 155 and decpair_valid Sg dnL rwL = 156 case (dnL, rwL) 157 of ([SOME (DecDone dc1), SOME (DecDone dc2)],_) => 158 (rwL,[Sg,extend dc1 Sg],SOME (DecDone (decpair dc2))) 159 | ([SOME (DecDone dc1), NONE], [true,false]) => 160 ([true,true],[Sg,extend dc1 Sg],NONE) 161 | _ => (rwL,[Sg,Sg],NONE) 162 163 and app_valid [SOME (TrmDone tm1), SOME (TrmDone tm2)] = 164 SOME (TrmDone (appl tm1 tm2)) 165 166 and pair_valid [SOME (TrmDone tm1),SOME (TrmDone tm2),SOME (TrmDone tm3)] = 167 SOME (TrmDone (pair tm1 tm2 tm3)) 168 169 and binder_valid binder Sg dnL rwL = 170 case (dnL, rwL) 171 of ([SOME (DecDone dc), SOME (TrmDone tm)],_) => 172 (rwL,[Sg,extend dc Sg],SOME (TrmDone (binder tm))) 173 | ([SOME (DecDone dc), NONE], [true,false]) => 174 ([true,true],[Sg,extend dc Sg],NONE) 175 | _ => (rwL,[Sg,Sg],NONE) 176 177 and cond_valid Sg dnL rwL = 178 case (dnL, rwL) 179 of ([SOME (DecDone dc), 180 SOME (TrmDone tm1), 181 SOME (TrmDone tm2)],_) => 182 (rwL, 183 [Sg,extend dc Sg], 184 SOME (TrmDone (conditional tm1 tm2))) 185 | ([SOME (DecDone dc), NONE,NONE],[true,false,false]) => 186 ([true,true,true],[Sg,extend dc Sg,extend dc Sg],NONE) 187 | _ => (rwL,[Sg,Sg,Sg],NONE) 188 189 and unary_valid unary [SOME (TrmDone tm1)] = 190 SOME (TrmDone (unary tm1)) 191 192 and binary_valid binary [SOME (TrmDone tm1), SOME (TrmDone tm2)] = 193 SOME (TrmDone (binary tm1 tm2)) 194 195 and recurse_valid tmL = 196 if forall (fn SOME _ => true | NONE => false) tmL 197 then let val (rec_tmL, rec_ty) = split_list tmL 198 in SOME (TrmDone (recurse rec_tmL rec_ty)) end 199 else NONE 200 201 and split_list [SOME (TrmDone tm)] = ([],tm) 202 | split_list (SOME (TrmDone x)::l) = 203 let val (l1,l2) = split_list l in (x::l1,l2) end 204 205 and lift_null_update Sg lt vf dnL rwL = 206 let val dn = vf dnL 207 in (rwL,for (length rwL) (rep Sg) [], dn) end 208 209 and rep Sg l = Sg :: l 210 211 and binder_fn Forall = universal 212 | binder_fn Exists = existential 213 | binder_fn Lambda = lambda 214 | binder_fn Imp = implication 215 | binder_fn Subtype = subtype 216 | binder_fn Pi = pi 217 | binder_fn Sigma = sigma 218 219 and unary_fn Not = negation 220 221 and binary_fn And = conjunction 222 | binary_fn Or = disjunction 223 | binary_fn Issubtype = issubtype 224 | binary_fn Eq' = equal 225 226 in 227 228 229 end 230 end 231 end 232 -}