1structure NDatatype :> NDatatype = 2struct 3 4open NDDB Witness; 5open lcsymtacs; 6open combinSyntax; 7open ParseDatatype; 8open oneSyntax; 9open combinSyntax; 10 11val ERR = Feedback.mk_HOL_ERR "MyDatatype"; 12 13(*****************************************************************) 14 15fun gen_tyvar _ = Type.gen_tyvar (); 16 17(* get type variables in a pretype *) 18fun pty_get_tyvars pty = 19 case pty of 20 dAQ _ => [ ] 21 | dVartype s => [s] 22 | dTyop {Args, ...} => Lib.U (map pty_get_tyvars Args); 23 24(* fromType : hol_type -> ParseDatatype.pretype *) 25fun fromType ty = 26 if is_vartype ty 27 then dVartype (dest_vartype ty) 28 else let val {Args, Thy, Tyop} = dest_thy_type ty 29 val thy = if Thy = "" then NONE else SOME Thy 30 in dTyop {Args=(map fromType Args), Thy=thy, Tyop=Tyop} 31 end; 32 33(* interleave two lists *) 34fun interleave [] y = y 35 | interleave x [] = x 36 | interleave (x::xs) (y::ys) = x::y::(interleave xs ys); 37 38(* functions to access dictionaries *) 39fun lookup tyvar (tyvar'::tyvars, h::dict) = 40 if tyvar = tyvar' then SOME h 41 else lookup tyvar (tyvars, dict) 42 | lookup _ _ = NONE; 43fun insert (tyvar, value) ([], []) = ([tyvar], [value]) 44 | insert (tyvar, value) (tyvar'::tyvars, h::dict) = 45 if tyvar = tyvar' then (tyvar::tyvars, value::dict) 46 else let 47 val (x, y) = (insert (tyvar,value) (tyvars, dict)) 48 in (tyvar'::x, h::y) end; 49 50(* Constructs a 0-ary type, caring for the theory *) 51fun make_type tyop NONE = mk_type(tyop, []) 52 | make_type tyop (SOME thy) = 53 mk_thy_type {Thy =thy, Tyop=tyop, Args=[]}; 54 55(* Replaces occurrences of defining types with type variables *) 56fun fix_mutual_vars dict pty = 57 case pty of 58 dTyop {Args=[], Thy=NONE, Tyop} => ( 59 case lookup Tyop dict of 60 SOME v => dVartype (dest_vartype v) 61 | NONE => dTyop {Args=[], Thy=NONE, Tyop=Tyop} 62 ) 63 | dTyop {Args, Thy, Tyop} => dTyop { 64 Args = map (fix_mutual_vars dict) Args, 65 Thy = Thy, Tyop = Tyop } 66 | _ => pty; 67 68(* Generates a new rich type variable *) 69fun gen_rich_tyvar tyvar ret (map, map') (all, all') = { 70 inj_pair = ASSUME(list_mk_icomb(inj_pair_tm, [map, ret])), 71 ret_map = REFL (combinSyntax.mk_o(ret, map')), 72 all_tm = all, 73 all_thm = REFL (mk_comb(all, mk_var("x", tyvar))), 74 all_map = REFL (combinSyntax.mk_o(all, map')), 75 all_T = REFL all, 76 all_mono = ASSUME (list_mk_icomb(pred_setSyntax.subset_tm, [all, all'])) 77}: rich_type; 78 79(* Generates richness for a constant type *) 80fun gen_rich_const ty self = let 81 val func = INST_TYPE[alpha|->ty, beta|->self] 82 in { 83 inj_pair = func (#inj_pair constantly_rich), 84 ret_map = func (#ret_map constantly_rich), 85 all_tm = #all_tm constantly_rich, 86 all_thm = func (#all_thm constantly_rich), 87 all_map = func (#all_map constantly_rich), 88 all_T = func (#all_T constantly_rich), 89 all_mono = func (#all_mono constantly_rich) 90}: rich_type 91end; 92 93(* A version of list_mk_icomb for theorems *) 94local 95 val mk_aty = list_mk_rbinop (Lib.curry Type.-->) 96 val args = fst o strip_fun o Term.type_of o lhs o concl 97 val LIST_MK_COMB = List.foldl (MK_COMB o swap) 98in 99fun LIST_MK_ICOMB fth aths = 100 let 101 val tyl = mk_aty (List.take (args fth, List.length aths)) 102 and tyr = mk_aty (List.map (Term.type_of o lhs o concl) aths) 103 in 104 LIST_MK_COMB (INST_TYPE (Type.match_type tyl tyr) fth) aths 105 end 106end; 107 108(* Makes generalizes nesting of type constructors *) 109fun nest_tyop tyop [] = 110 dTyop {Args=[], Thy=SOME"one", Tyop="one"} 111 | nest_tyop tyop (C::[]) = C 112 | nest_tyop tyop (C::Cs) = let 113 val args = [C, nest_tyop tyop Cs] 114 in dTyop {Args=args, Thy=NONE, Tyop=tyop} 115 end; 116 117(* Moltiplies and sums the components of a type description 118 to get just one constructor *) 119fun type_descriptions ([]: ParseDatatype.AST list) = [] 120 | type_descriptions ((_, ParseDatatype.Constructors clist)::tl) 121 = (nest_tyop "sum" 122 (map ((nest_tyop "prod") o snd) clist) 123 )::(type_descriptions tl) 124 | type_descriptions ((_, ParseDatatype.Record _)::_) 125 = raise ERR "MyDatatype" 126 ("Cannot handle records for now."); 127 128(********************* Composition Functions *********************) 129 130(* These functions combine the theorem of the current type op 131 with theorems of the parameter types to get theorems for the 132 composed type *) 133local 134fun compose_inj_pair thm thms = 135 foldl ((uncurry o C) MATCH_MP) thm thms; 136fun compose_ret_map thm thms = 137 let val retrieve_tm = ( fst o strip_comb o snd o dest_eq 138 o snd o strip_forall o concl) thm 139 in SYM (RIGHT_CONV_RULE ((REWR_CONV o DEEP_SYM) thm) 140 (SYM (LIST_MK_ICOMB (REFL retrieve_tm) thms ))) 141end; 142fun compose_all_tm tm tms = list_mk_icomb(tm, tms); 143fun compose_all_mono thm thms = 144 if List.length thms = 1 then MATCH_MP thm (hd thms) 145 else if List.length thms = 2 then MATCH_MP thm 146 ((uncurry CONJ) (pair_of_list(thms))) 147 else MATCH_MP thm (foldl (uncurry CONJ) (hd (rev thms)) (tl (rev thms))); 148in 149val compose_funs = { 150 inj_pair = compose_inj_pair , 151 ret_map = compose_ret_map , 152 all_tm = compose_all_tm , 153 all_thm = (fn x=> fn y=> TRUTH), (* fixme *) 154 all_map = compose_ret_map , 155 all_T = (fn x=> fn y=> TRUTH), (* fixme *) 156 all_mono = compose_all_mono 157} 158end; 159 160(**** Main composition function! The magic occurs down here! *****) 161fun compose dict self pty = 162 case pty of 163 dAQ ty => gen_rich_const ty self 164 | dVartype s => valOf (lookup s dict) 165 | dTyop {Args, Thy, Tyop} => 166 case lookup Tyop (!types) of 167 NONE => if Args = [] then 168 compose dict self (dAQ (pretypeToType pty)) 169 else raise ERR "compose" 170 ("Type '"^Tyop^"' not supported.") 171 | SOME this => let 172 val args = map (compose dict self) Args 173 in { 174 inj_pair = (#inj_pair compose_funs) 175 (#inj_pair this) 176 (map #inj_pair args), 177 ret_map = (#ret_map compose_funs) 178 (#ret_map this) 179 (map #ret_map args), 180 all_thm = TRUTH, (* FIXME *) 181 all_tm = (#all_tm compose_funs) 182 (#all_tm this) 183 (map #all_tm args), 184 all_map = (#all_map compose_funs) 185 (#all_map this) 186 (map #all_map args), 187 all_T = (#all_T compose_funs) 188 (#all_T this) 189 (map #all_T args), 190 all_mono= (#all_mono compose_funs) 191 (#all_mono this) 192 (map #all_mono args) 193 } : rich_type 194 end; 195 196(* After the composition, we have to do some lambda abstractions 197 in order to get the theorems in the right form *) 198local 199fun gen_inj_pair_thm thm maps rets = 200 GENL (interleave maps rets) (DISCH_ALL thm) 201fun gen_ret_map_thm thm maps rets = let 202 val eq = concl thm 203 val (O, [r, m]) = strip_comb (lhs eq) 204 val func = fn (x,l) => RIGHT_LIST_BETA (REFL (list_mk_comb(list_mk_abs(l, x), l))) 205 val r' = func(r, rets) 206 val m' = func(m, maps) 207 val left = MK_COMB (AP_TERM O r', m') 208 val os = map combinSyntax.mk_o (zip rets maps) 209 val func2 = fst o dom_rng o type_of 210 val subst = map op|-> (zip (map func2 rets) (map func2 maps)) 211 val r'' = INST_TYPE subst r' 212 val rets' = map (inst subst) rets 213 val repl = map op|-> (zip rets' os) 214 val right = INST repl r'' 215 val trans = TRANS (TRANS left thm) (SYM right) 216in GENL (interleave maps rets) trans 217end; 218fun gen_all_mono_thm thm rtcs = 219 GEN_ALL (foldl (uncurry DISCH) thm 220 (map (concl o #all_mono) rtcs)) 221 |> REWRITE_RULE [AND_IMP_INTRO]; 222(* DISCH ((concl o #all_mono o hd) rtcs) thm;*) 223in 224fun compose_pretype pty = let 225 (* 'self' type variable *) 226 val self = gen_tyvar () 227 val oself = optionSyntax.mk_option self 228 (* variables *) 229 val vnames = pty_get_tyvars pty 230 val vars = map mk_vartype vnames 231 (* generate map/retrieve functions for the base case *) 232 val indices = map gen_tyvar vars 233 val rets = map (fn (x,y) => genvar (x --> y --> oself)) 234 (zip vars indices) 235 val map_rngs = map gen_tyvar vars 236 val maps = map (genvar o op-->) (zip vars map_rngs) 237 (* reverse maps: for retrieve_map theorems *) 238 val maps' = map (genvar o op-->) (zip map_rngs vars) 239 val alls = map (fn v => genvar (v --> bool)) vars 240 val alls' = map (fn v => genvar (v --> bool)) vars 241 val func = fn (w, (x, (y, z))) => gen_rich_tyvar w x y z 242 val rtcs = map func 243 (zip vars (zip rets (zip (zip maps maps') (zip alls alls')))) 244 val dict = (vnames, rtcs) 245 val comp = compose dict self pty 246 in {inj_pair = gen_inj_pair_thm (#inj_pair comp) maps rets, 247 ret_map = gen_ret_map_thm (#ret_map comp) maps' rets, 248 all_tm = list_mk_abs(alls, #all_tm comp), 249 all_thm = TRUTH, 250 all_map = gen_ret_map_thm (#all_map comp) maps' alls, 251 all_T = #all_T comp, 252 all_mono = gen_all_mono_thm (#all_mono comp) rtcs 253 } : rich_type 254end 255end; 256 257 258(*****************************************************************) 259(* mk_constructor: takes a rich type - a composition of other *) 260(* types - and returns the fixpoint of that type *) 261(* constructor with respect to the type vars *) 262(* that have been created by gen_tyvar. *) 263(*****************************************************************) 264local 265 val x = mk_var("x", alpha); 266 val Jsome_tm = mk_abs(x, mk_abs(mk_var("u", one_ty), 267 optionSyntax.mk_some x)); 268 val Iu_tm = mk_abs(x, oneSyntax.one_tm) 269 fun helper thm = 270 if (is_forall o concl) thm then let 271 val c = concl thm 272 val (f, c') = dest_forall c 273 val (g, _ ) = dest_forall c' 274 val (a, a') = (dom_rng o type_of) f 275 val (i, os) = (dom_rng o snd o dom_rng o type_of) g 276 val self = optionSyntax.dest_option os 277 val x = genvar self 278 val b = is_gen_tyvar a 279 val f' = if b then inst [alpha|->self] Iu_tm 280 else inst [alpha|->a ] combinSyntax.I_tm 281 val g' = if b then inst [alpha|->self] Jsome_tm 282 else inst [alpha|->a, beta|->self] J_tm 283 val thm = INST_TYPE [a |-> (if b then self else a), 284 a'|-> (if b then one_ty else a), 285 i |-> one_ty] thm 286 val thm = ((SPEC g') o (SPEC f')) thm 287 val t = if b then INST_TYPE [alpha|->self] some_inj_thm 288 else INST_TYPE [alpha|->a, beta|->self] k_inj_thm 289 in PROVE_HYP t (helper thm) 290 end else UNDISCH_ALL thm 291in 292fun mk_constructor (ty:rich_type) = 293 let 294 val thm = helper (#inj_pair ty) 295 val (r, R) = (dest_comb o concl) thm 296 val (_, M) = dest_comb r 297 val (_, L) = (dom_rng o type_of) M 298 val (B, O) = (dom_rng o snd o dom_rng o type_of) R 299 val self = optionSyntax.dest_option O 300 val tree_ty = (listSyntax.mk_list_type B) 301 --> pairSyntax.mk_prod(L, numSyntax.num) 302 val thm = INST_TYPE[self|->tree_ty] thm 303 in MATCH_MP inj_constr_thm thm 304 end 305end; 306 307(* mk_all *) 308local 309 val KT = mk_abs(mk_var("x", alpha), T); 310 fun helper tm dict self = if is_abs tm then 311 let 312 val (x, t) = dest_abs tm 313 val ty = (fst o dom_rng o type_of) x 314 in helper (case lookup ty dict of 315 NONE => subst [x |-> (inst [alpha|->ty] KT)] t 316 | SOME s => subst [(inst [ty|->self] x) 317 |-> mk_var("ok_"^s, self-->bool)] 318 (inst [ty|->self] t) 319 ) dict self 320 end else tm; 321 fun div_sum tm 1 = [tm] 322 | div_sum tm n = let 323 val (a, b) = dest_comb tm 324 val (_,ab) = dest_comb a 325 in b::(div_sum ab (n-1)) 326 end; 327in 328fun mk_all tm dict self = 329 let 330 val a = helper tm (swap dict) self 331 val b = div_sum a (List.length (fst dict)) 332in b end; 333end; 334 335 336fun div_sum_vars ty f 1 = let 337 val var = genvar ty 338 in [(var, f var)] 339 end 340 | div_sum_vars ty f n = let 341 val (a, b) = sumSyntax.dest_sum ty 342 val var = genvar a 343 val inv = sumSyntax.mk_inl(var, b) 344 val f' = f o (fn x => sumSyntax.mk_inr(x, a)) 345 in (var, inv)::(div_sum_vars b f' (n-1)) 346 end; 347 348(*****************************************************************) 349(*****************************************************************) 350 351fun Datatype q = let 352 val df = ParseDatatype.hparse q 353 (* sum all the types and the constructors *) 354 val ty_descrs = type_descriptions df 355 val pty = nest_tyop "sum" ty_descrs 356 (* fixpoint variables *) 357 val ty_names = map fst df 358 val mut_no = List.length df 359 val ty_vars = map gen_tyvar df 360 (* replace fixpoint vars *) 361 val dict = (ty_names, ty_vars) 362 val pty = fix_mutual_vars dict pty 363 (* old: my_wit *) 364 val rich_comp = compose_pretype pty 365 val ty_names = fst dict 366 val inj_Co = mk_constructor rich_comp 367 val Co = (snd o dest_comb o concl) inj_Co; 368 val (dom, rng) = (dom_rng o type_of) Co; 369 (* predicate names for representation predicates *) 370 val no = List.length ty_names 371 val oks = map (fn s=>mk_var("ok_"^s, rng-->bool)) ty_names 372 val vars = div_sum_vars dom I no 373 (**) 374 val all_tm = #all_tm rich_comp 375 val tmp = gen_tyvar () 376 val alls = rev (map (inst [tmp|->rng]) (mk_all all_tm dict tmp)) 377 (**) 378 val Hyps = map mk_comb (zip alls (map fst vars)) 379 val Cs = map (curry mk_comb Co) (map snd vars) 380 val Cons = map mk_comb (zip oks Cs) 381 val rules = map mk_imp (zip Hyps Cons) 382 val genl = map mk_forall (zip (map fst vars) rules) 383 val def_tm = list_mk_conj genl 384 (**) 385 val mythm = prove(``!P Q. (P SUBSET Q) = (!x. P x ==> Q x)``, 386 simp[pred_setTheory.SUBSET_DEF, boolTheory.IN_DEF]) 387 val mono = PURE_REWRITE_RULE [mythm] (#all_mono rich_comp) 388 val func = fn x => (PURE_REWRITE_RULE [mythm] x 389 |> SIMP_RULE bool_ss [PULL_FORALL] 390 |> SPEC_ALL) 391 val monoset = map (fn x => 392 ((fst o dest_const o #all_tm) x, func (#all_mono x))) 393 (snd (!NDDB.types)) 394 val (rules, ind, cases) = 395 InductiveDefinition.new_inductive_definition 396 ((!IndDefLib.the_monoset)@monoset) "stem" (def_tm, []) 397 (* witnesses *) 398 val ws = List.tabulate(no, K (NONE:Thm.thm option)) 399 val constrs = map GEN_ALL (BODY_CONJUNCTS rules) (* fixme *) 400 val goal = map 401 (fst o dest_imp o snd o strip_forall o concl) constrs 402 val gthms = map ASSUME goal 403 val wits = Witness.find_inductive_witnesses gthms ws constrs 404 (**) 405 val tyaxs = map new_type_definition (zip ty_names wits) 406 val func = fn (s,ax) => define_new_type_bijections 407 {name = s^"_absrep", ABS = s^"_abs", REP = s^"_rep", tyax = ax} 408in map func (zip ty_names tyaxs) 409end; 410 411(* tests: *) 412val q = `X = C Y | C X ; Y = C ('b option option option) | C 'a` 413val it = Datatype q 414(*val repabss = map extract_abs_rep it*) 415 416end; 417 418(* 419fun extract_abs_rep thm = let 420 val tmp = thm |> concl |> dest_conj |> fst |> dest_forall |> snd |> dest_eq |> fst |> dest_comb 421 in ((fst o dest_comb o snd) tmp, fst tmp) 422end; 423 424 425fun mk_constructors absreps = let 426 (* Ci' = absi o C o INi o (map rep1 .. repn) *) 427 Hyps 428Cs 429val abs = map snd repabss 430val reps = map fst repabss 431val map_tm = (hd o tl o snd o strip_comb o fst o dest_eq 432 o snd o strip_forall o concl o #all_map) rich_comp 433list_mk_icomb(map_tm, ) 434free_vars map_tm 435val map_reps_tm = list_mk_comb(map_tm, 436list_mk_icomb(combinSyntax.o_tm, [Co, ] 437 val 438 439(* RUBBISH *) 440(* 441 MyDatatype.wit_test `X = C X 'a X 'b | C 'a ; Y = C Y | C 'a` 442 test2 `X = C (X+(X#X))` 443*)(* 444val xxx = mk_thm([], ``(!x. sette x ==> nove x) ==> 445 (sum_all sette 446 (prod_all sette otto )) x ==> 447 (sum_all nove 448 (prod_all nove zero )) x``); 449*) 450 451 452*) 453