1structure lisp_extractLib :> lisp_extractLib = 2struct 3 4open HolKernel boolLib bossLib; 5open lisp_extractTheory lisp_semanticsTheory; 6 7open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 8open optionTheory arithmeticTheory relationTheory; 9open stringLib pairSyntax; 10 11infix \\ 12val op \\ = op THEN; 13val RW = REWRITE_RULE; 14val RW1 = ONCE_REWRITE_RULE; 15 16 17(* definitions *) 18 19fun remove_let_and_conv tm = let 20 val (xs,b) = pairSyntax.dest_anylet tm 21 val _ = 1 < length xs orelse fail() 22 fun mk_tuple [] = fail() 23 | mk_tuple [x] = x 24 | mk_tuple (x::xs) = pairSyntax.mk_pair(x,mk_tuple xs) 25 val vs = mk_tuple (map fst xs) 26 val ys = mk_tuple (map snd xs) 27 val result = pairSyntax.mk_anylet([(vs,ys)],b) 28 val th1 = pairLib.let_CONV tm 29 val th2 = pairLib.let_CONV result 30 in TRANS th1 (SYM th2) end handle HOL_ERR _ => NO_CONV tm 31 32fun new_def def_tm term_tac = let 33 val name = def_tm |> dest_eq |> fst |> repeat rator |> dest_var |> fst 34 val def_rw = QCONV (DEPTH_CONV remove_let_and_conv) def_tm 35 val new_def_tm = def_rw |> concl |> rand 36 val def = case term_tac of 37 NONE => Define [ANTIQUOTE new_def_tm] 38 | SOME x => tDefine name [ANTIQUOTE new_def_tm] x 39 val def = def |> SPEC_ALL |> CONV_RULE (REWR_CONV (SYM def_rw)) 40 val ind = (SOME (fetch "-" (name^"_ind") |> PURE_REWRITE_RULE [pairTheory.PAIR_EQ]) 41 handle HOL_ERR _ => NONE) 42 in (def,ind) end 43 44 45(* ML equivalent of term datatype defined in lisp_semanticsTheory *) 46 47datatype 48 primitive_op = op_CONS | op_EQUAL | op_LESS | op_SYMBOL_LESS | op_ADD | op_SUB | 49 op_ATOMP | op_CONSP | op_NATP | op_SYMBOLP | op_CAR | op_CDR 50 51datatype 52 mfunc = PrimitiveFun of primitive_op 53 | mDefine | Print | Error | Funcall | Fun of string; 54 55datatype 56 mterm = Const of term 57 | Var of string 58 | App of mfunc * mterm list 59 | If of mterm * mterm * mterm 60 | LamApp of string list * mterm * mterm list 61 | Or of mterm list 62 (* only macros below *) 63 | And of mterm list 64 | Cond of (mterm * mterm) list 65 | Let of (string * mterm) list * mterm 66 | LetStar of (string * mterm) list * mterm 67 | First of mterm | Second of mterm | Third of mterm 68 | Fourth of mterm | Fifth of mterm | List of mterm list 69 | Defun of string * string list * term; 70 71 72(* a mapping: term -> mterm *) 73 74fun dest_primitive_op tm = 75 if tm ~~ ``opCONS`` then op_CONS else 76 if tm ~~ ``opEQUAL`` then op_EQUAL else 77 if tm ~~ ``opLESS`` then op_LESS else 78 if tm ~~ ``opSYMBOL_LESS`` then op_SYMBOL_LESS else 79 if tm ~~ ``opADD`` then op_ADD else 80 if tm ~~ ``opSUB`` then op_SUB else 81 if tm ~~ ``opCONSP`` then op_CONSP else 82 if tm ~~ ``opSYMBOLP`` then op_SYMBOLP else 83 if tm ~~ ``opNATP`` then op_NATP else 84 if tm ~~ ``opCAR`` then op_CAR else 85 if tm ~~ ``opCDR`` then op_CDR else fail() 86 87fun dest_func tm = let 88 val p = repeat rator tm 89 in if p ~~ ``PrimitiveFun`` then PrimitiveFun (dest_primitive_op (rand tm)) else 90 if p ~~ ``Define`` then mDefine else 91 if p ~~ ``Print`` then Print else 92 if p ~~ ``Error`` then Error else 93 if p ~~ ``Funcall`` then Funcall else 94 if p ~~ ``Fun`` then Fun (stringSyntax.fromHOLstring (rand tm)) else fail() 95 end 96 97fun dest_term tm = let 98 fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ [y] end 99 handle HOL_ERR _ => [tm]; 100 val xs = list_dest dest_comb tm 101 val p = repeat rator tm 102 in if p ~~ ``Const`` then Const (rand tm) else 103 if p ~~ ``Var`` then Var (stringSyntax.fromHOLstring (rand tm)) else 104 if p ~~ ``App`` then App ((dest_func (tm |> rator |> rand)), 105 map (dest_term) (fst (listSyntax.dest_list (rand tm)))) else 106 if p ~~ ``If`` then If (dest_term (el 2 xs),dest_term (el 3 xs),dest_term (el 4 xs)) else 107 if p ~~ ``LamApp`` then 108 LamApp (map stringSyntax.fromHOLstring 109 (fst (listSyntax.dest_list (el 2 xs))), 110 dest_term (el 3 xs), 111 map (dest_term) (fst (listSyntax.dest_list (el 4 xs)))) else 112 if p ~~ ``First`` then First (dest_term (rand tm)) else 113 if p ~~ ``Second`` then Second (dest_term (rand tm)) else 114 if p ~~ ``Third`` then Third (dest_term (rand tm)) else 115 if p ~~ ``Fourth`` then Fourth (dest_term (rand tm)) else 116 if p ~~ ``Fifth`` then Fifth (dest_term (rand tm)) else 117 if p ~~ ``Or`` then Or (map (dest_term) (fst (listSyntax.dest_list (rand tm)))) else 118 if p ~~ ``And`` then And (map (dest_term) (fst (listSyntax.dest_list (rand tm)))) else 119 if p ~~ ``List`` then List (map (dest_term) (fst (listSyntax.dest_list (rand tm)))) else 120 if p ~~ ``Let`` then 121 Let (map 122 ((fn (x,y) => (stringSyntax.fromHOLstring x, dest_term y)) o 123 pairSyntax.dest_pair) 124 (fst (listSyntax.dest_list (el 2 xs))), 125 dest_term (el 3 xs)) else 126 if p ~~ ``LetStar`` then 127 LetStar (map 128 ((fn (x,y) => (stringSyntax.fromHOLstring x, dest_term y)) o 129 pairSyntax.dest_pair) 130 (fst (listSyntax.dest_list (el 2 xs))), 131 dest_term (el 3 xs)) else 132 if p ~~ ``Cond`` then 133 Cond (map 134 ((fn (x,y) => (dest_term x, dest_term y)) o pairSyntax.dest_pair) 135 (fst (listSyntax.dest_list (el 2 xs)))) else 136 if p ~~ ``Defun`` then Defun (stringSyntax.fromHOLstring (el 2 xs), 137 map stringSyntax.fromHOLstring (fst (listSyntax.dest_list (el 3 xs))), 138 el 4 xs) else fail() 139 end 140 141 142(* mapping from shallow embeddings to deep embeddings *) 143 144infix $$ 145val op $$ = mk_comb 146 147val string_uppercase = let 148 fun uppercase_char c = 149 if #"a" <= c andalso c <= #"z" then chr (ord c - (ord #"a" - ord #"A")) else c 150 in String.translate (fn c => implode [uppercase_char c]) end 151 152fun shallow_to_deep tm = let 153 fun fromHOLstring s = string_uppercase (stringSyntax.fromHOLstring s) 154 fun fromMLstring s = stringSyntax.fromMLstring (string_uppercase s) 155 fun is_const tm = 156 (if rator tm ~~ ``Sym`` then can fromHOLstring (rand tm) else 157 if rator tm ~~ ``Val`` then can numSyntax.int_of_term (rand tm) else 158 if rator (rator tm) ~~ ``Dot`` then is_const (rand (rator tm)) andalso 159 is_const (rand tm) 160 else false) handle HOL_ERR _ => false 161 val lisp_primitives = 162 [(``Dot``,``opCONS``), 163 (``LISP_CONS``,``opCONS``), 164 (``LISP_EQUAL:SExp->SExp->SExp``,``opEQUAL``), 165 (``LISP_LESS``,``opLESS``), 166 (``LISP_SYMBOL_LESS``,``opSYMBOL_LESS``), 167 (``LISP_ADD``,``opADD``), 168 (``LISP_SUB``,``opSUB``), 169 (``LISP_CONSP``,``opCONSP``), 170 (``LISP_SYMBOLP``,``opSYMBOLP``), 171 (``LISP_NUMBERP``,``opNATP``), 172 (``CAR``,``opCAR``), 173 (``CDR``,``opCDR``)] 174 fun aux_fail tm = 175 failwith("Unable to translate: \n\n" ^ term_to_string tm ^ "\n\n") 176 fun aux tm = 177 if is_const tm then ``Const`` $$ tm else 178 if can (match_term ``Val n``) tm then aux_fail tm else 179 if can (match_term ``Sym s``) tm then aux_fail tm else 180 if is_var tm then let 181 val (s,ty) = dest_var tm 182 val _ = ty = ``:SExp`` orelse failwith("Variable of wrong type: " ^ s) 183 in ``Var`` $$ fromMLstring s end 184 else if is_cond tm then let 185 val (x1,x2,x3) = dest_cond tm 186 val _ = if rator x1 ~~ ``isTrue`` then () else aux_fail x1 187 in ``If`` $$ aux (rand x1) $$ aux x2 $$ aux x3 end 188 else if can pairSyntax.dest_anylet tm then let 189 val (xs,x) = pairSyntax.dest_anylet tm 190 val ys = map (fn (x,y) => pairSyntax.mk_pair(x |> dest_var |> fst |> fromMLstring, aux y)) xs 191 val y = listSyntax.mk_list(ys,``:string # term``) 192 in ``Let`` $$ y $$ (aux x) end 193 else (* general function application *) let 194 fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ [y] end 195 handle HOL_ERR _ => [tm]; 196 val xs = list_dest dest_comb tm 197 val (x,xs) = (hd xs, tl xs) 198 fun lookup x [] = fail() 199 | lookup x ((y,z)::zs) = if x ~~ y then z else lookup x zs 200 val f = ``PrimitiveFun`` $$ lookup x lisp_primitives handle HOL_ERR _ => 201 ``Fun`` $$ fromMLstring (fst (dest_const x)) 202 handle HOL_ERR _ => aux_fail x 203 val ys = map aux xs 204 in ``App`` $$ f $$ listSyntax.mk_list(ys,``:term``) end 205 fun preprocess tm = QCONV (REWRITE_CONV [isTrue_INTRO]) tm 206 val th = preprocess tm 207 val tm2 = rand (concl th) 208 in (aux tm2, th) end 209 210(* 211val tm = ``let x = LISP_ADD x y in let z = y in LISP_SUB x y`` 212dest_term (fst (shallow_to_deep tm)) 213 214 plan: provide a method which, given a list of definition and 215 induction thm pairs, produces deep embeddings and correspondence 216 proofs. 217 218*) 219 220 221(* state of extraction function *) 222 223local 224 val lookup_thm = ref TRUTH; 225 val assum_rw = ref TRUTH; 226 val assum_clauses = ref (tl [TRUTH]); 227 val atbl = ref (fn (name:string) => (fail():thm)); 228 fun set_assum_rw th = let 229 val (x,y) = th |> SPEC_ALL |> concl |> dest_eq 230 val name = (repeat rator x |> dest_const |> fst) ^ "_abbrev" 231 val z = rand y 232 val rw = Define `^(mk_eq(mk_var(name,type_of z),z))` 233 val _ = assum_rw := (RW [GSYM rw] th) 234 in th end 235 fun fupdate x y f i = if x = i then y else f i; 236 val lemma = prove(``(x = (y:bool)) ==> (x ==> y)``,SIMP_TAC std_ss []) 237in 238 fun set_lookup_thm th = (lookup_thm := th) 239 fun get_lookup_thm () = !lookup_thm 240 fun atbl_install name th = (atbl := fupdate name th (!atbl)) 241 fun atbl_lookup name = (!atbl) name 242 fun install_assum_eq th = 243 th |> SPEC_ALL |> concl |> rator |> rand 244 |> (REWRITE_CONV [GSYM CONJ_ASSOC,set_assum_rw th,fns_assum_def,EVERY_DEF] 245 THENC DEPTH_CONV (PairRules.PBETA_CONV)) 246 |> MATCH_MP lemma |> UNDISCH 247 |> set_lookup_thm 248 fun get_assum_rw () = !assum_rw 249 fun add_assum_clause th = (assum_clauses := th::(!assum_clauses)) 250 fun get_assum_clauses () = !assum_clauses 251end 252 253 254(* R_ev a function which evaluates the semantics of pure functions *) 255 256val PRW1 = PURE_ONCE_REWRITE_RULE 257 258val mk_string = stringSyntax.fromMLstring 259 260val simplify_name = let 261 val normal_chars = explode "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789" 262 fun to_lower c = 263 if #"A" <= c andalso c <= #"Z" 264 then chr (ord c + (ord #"a" - ord #"A")) else c 265 in fn s => 266 if s = "<=" then "less_eq" else 267 String.translate (fn c => if mem c normal_chars then implode [to_lower c] else "_") s end 268 269fun prim2term op_CONS = ``opCONS`` 270 | prim2term op_EQUAL = ``opEQUAL`` 271 | prim2term op_LESS = ``opLESS`` 272 | prim2term op_SYMBOL_LESS = ``opSYMBOL_LESS`` 273 | prim2term op_ADD = ``opADD`` 274 | prim2term op_SUB = ``opSUB`` 275 | prim2term op_ATOMP = ``opATOMP`` 276 | prim2term op_CONSP = ``opCONSP`` 277 | prim2term op_NATP = ``opNATP`` 278 | prim2term op_SYMBOLP = ``opSYMBOLP`` 279 | prim2term op_CAR = ``opCAR`` 280 | prim2term op_CDR = ``opCDR`` 281 282fun R_ap (PrimitiveFun p) = SIMP_RULE std_ss [EVAL_DATA_OP_def] (SPEC (prim2term p) R_ap_PrimiveFun) 283 | R_ap (Fun name) = atbl_lookup name 284 | R_ap mDefine = R_ap_Define 285 | R_ap Error = R_ap_Error 286 | R_ap Print = R_ap_Print 287 | R_ap (Funcall) = R_ap_Funcall 288 289fun R_ev (Const c) = SPEC c R_ev_Const 290 | R_ev (Var v) = SPEC (mk_string v) R_ev_Var 291 | R_ev (If (x,y,z)) = MATCH_MP (MATCH_MP R_ev_If (LIST_CONJ [R_ev y,R_ev z])) (R_ev x) 292 | R_ev (Or []) = R_ev_Or_NIL 293 | R_ev (Or [x]) = MATCH_MP R_ev_Or_SING (R_ev x) 294 | R_ev (Or (x::y::xs)) = MATCH_MP (MATCH_MP R_ev_Or_CONS_CONS (R_ev (Or (y::xs)))) (R_ev x) 295 | R_ev (App (f,args)) = let 296 fun R_evl [] = R_evl_NIL 297 | R_evl (x::xs) = MATCH_MP (MATCH_MP R_evl_CONS (R_evl xs)) x 298 val th = DISCH_ALL (R_evl (map (UNDISCH o R_ev) args)) 299 |> PURE_REWRITE_RULE [AND_IMP_INTRO] 300 val th = if is_imp (concl th) then th else DISCH T th 301 val th = MATCH_MP (MATCH_MP R_ev_App (R_ap f)) th 302 val c = SIMP_CONV std_ss [TL,HD,EL_simp_restricted,LENGTH,EL] 303 val th = CONV_RULE (BINOP_CONV c) th 304 in th end 305 | R_ev (LamApp (vs,body,args)) = let 306 val th = MATCH_MP R_ev_LamApp (R_ev (Let (zip vs args,body))) 307 val th = CONV_RULE ((RAND_CONV o RATOR_CONV o RAND_CONV o 308 RATOR_CONV o RAND_CONV) EVAL) th 309 in th end 310 | R_ev (Let (xs,x)) = let 311 fun R_evl [] = R_evl_NIL 312 | R_evl (x::xs) = MATCH_MP (MATCH_MP R_evl_CONS (R_evl xs)) x 313 val th = DISCH_ALL (R_evl (map (UNDISCH o R_ev o snd) xs)) 314 |> PURE_REWRITE_RULE [AND_IMP_INTRO] 315 val exps = th |> concl |> rand |> rand |> rator |> rand 316 val xs1 = listSyntax.mk_list(map mk_string (map fst xs),``:string``) 317 val th = MATCH_MP (SPEC xs1 R_ev_Let) th 318 val th1 = R_ev x 319 val tm1 = th1 |> concl |> rand |> rator |> rand |> rand 320 val tm2 = th |> concl |> dest_imp |> fst |> rand |> rator |> rand |> rand 321 val th = MATCH_MP th (INST (fst (match_term tm1 tm2)) th1) 322 val c = SIMP_CONV std_ss [TL,HD,EL_simp_restricted,LENGTH,EL,ZIP] 323 val th = CONV_RULE (BINOP_CONV c) th 324 val tm = th |> concl |> rand |> rand |> rator |> rand 325 val xs3 = map (fn x => mk_var(simplify_name(fst x),``:SExp``)) xs 326 val xs4 = fst (listSyntax.dest_list exps) 327 val tm2 = subst [``VarBind ^xs1 ^exps`` |-> ``VarBind ^xs1 ^(listSyntax.mk_list(xs3,``:SExp``))``] tm 328 val tm3 = pairSyntax.mk_anylet(zip xs3 xs4,tm2) 329 val rw = GSYM (pairLib.let_CONV tm3) 330 val _ = ((fst o dest_eq o concl) rw ~~ tm) orelse 331 failwith("R_ev (Let ...) failed.") 332 val th = CONV_RULE ((RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) (REWR_CONV rw)) th 333 in th end 334 | R_ev (LetStar ([],x)) = PRW1 [R_ev_LetStar_NIL] (R_ev x) 335 | R_ev (LetStar ((v::vs),x)) = PRW1 [R_ev_LetStar_CONS] (R_ev (Let ([v],LetStar (vs,x)))) 336 | R_ev (First x) = MATCH_MP R_ev_FIRST (R_ev x) 337 | R_ev (Second x) = MATCH_MP R_ev_SECOND (R_ev x) 338 | R_ev (Third x) = MATCH_MP R_ev_THIRD (R_ev x) 339 | R_ev (Fourth x) = MATCH_MP R_ev_FOURTH (R_ev x) 340 | R_ev (Fifth x) = MATCH_MP R_ev_FIFTH (R_ev x) 341 | R_ev (And []) = PRW1 [R_ev_And_NIL] (R_ev (Const ``Sym "T"``)) 342 | R_ev (And [x]) = PRW1 [R_ev_And_SING] (R_ev x) 343 | R_ev (And (x::y::xs)) = PRW1 [R_ev_And_CONS] (R_ev (If (x,And (y::xs),Const ``Sym "NIL"``))) 344 | R_ev (List []) = PRW1 [R_ev_List_NIL] (R_ev (Const ``Sym "NIL"``)) 345 | R_ev (List (x::xs)) = PRW1 [R_ev_List_CONS] (R_ev (App (PrimitiveFun op_CONS,[x,List xs]))) 346 | R_ev (Cond []) = PRW1 [R_ev_Cond_NIL] (R_ev (Const ``Sym "NIL"``)) 347 | R_ev (Cond ((x1,x2)::xs)) = PRW1 [R_ev_Cond_CONS] (R_ev (If (x1,x2,Cond xs))) 348 | R_ev _ = failwith("Unsupported construct.") 349 350 351(* extraction of pure functions *) 352 353fun remove_primes th = let 354 fun last s = substring(s,size s-1,1) 355 fun delete_last_prime s = if last s = "'" then substring(s,0,size(s)-1) else fail() 356 fun foo [] ys i = i 357 | foo (x::xs) ys i = let 358 val name = (fst o dest_var) x 359 val new_name = repeat delete_last_prime name 360 in if name = new_name then foo xs (x::ys) i else let 361 val new_var = mk_var(new_name,type_of x) 362 in foo xs (new_var::ys) ((x |-> new_var) :: i) end end 363 val i = foo (free_varsl (concl th :: hyp th)) [] [] 364 in INST i th end 365 366local 367 val tm1 = ``(f:'a |-> 'b) ' z`` 368 val tm2 = ``x IN FDOM (f:'a |-> 'b)`` 369in 370 fun is_fapply_or_in_fdom tm = 371 can (match_term tm1) tm orelse can (match_term tm2) tm 372end 373 374fun eval_fappy_conv tm = 375 if not (is_fapply_or_in_fdom tm) then NO_CONV tm else 376 (REWRITE_CONV [VarBind_def,VarBindAux_def,FDOM_FUPDATE,FDOM_FEMPTY,IN_INSERT, 377 IN_UNION,REVERSE_DEF,APPEND,FAPPLY_FUPDATE_THM,FUNION_DEF,NOT_IN_EMPTY] THENC 378 DEPTH_CONV stringLib.string_EQ_CONV THENC 379 REWRITE_CONV []) tm 380 381fun diff xs ys = filter (fn x => not (mem x ys)) xs 382fun mk_sexp_fun_ty x = mk_type("fun",[``:SExp``,x]) 383fun CS rw = ConseqConv.CONSEQ_REWRITE_CONV ([], rw, []) 384 ConseqConv.CONSEQ_CONV_STRENGTHEN_direction 385 386fun pure_extract name term_tac = let 387 val _ = print ("extracting: "^name^"\n") 388 (* evaluate semantics *) 389 val name_tm = stringSyntax.fromMLstring name 390 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` 391 |> REWRITE_CONV [get_lookup_thm()] 392 |> concl |> rand |> pairSyntax.dest_pair 393 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring 394 |> map (fn s => mk_var(simplify_name s,``:SExp``)) 395 |> (fn xs => listSyntax.mk_list(xs,``:SExp``)) 396 val v = mk_var("__result__",``:SExp list -> SExp``) 397 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``) 398 val _ = atbl_install name lemma 399 fun FORCE_UNDISCH th = UNDISCH th handle HOL_ERR _ => th 400 val mt = dest_term t 401 val th1 = FORCE_UNDISCH (SIMP_RULE std_ss [] (R_ev mt)) |> remove_primes 402 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 403 |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH] 404 val tm2 = th2 |> concl |> rator |> rand 405 val tm1 = th1 |> concl 406 val s = fst (match_term (rator tm1) (rator tm2)) 407 val c = DEPTH_CONV eval_fappy_conv 408 val th4 = MATCH_MP th2 (INST s th1) |> DISCH_ALL |> RW [AND_IMP_INTRO] 409 |> CONV_RULE (BINOP_CONV c) 410 (* invent function *) 411 val good_name = simplify_name name 412 val params = listSyntax.dest_list args |> fst 413 val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` params 414 val new_fun = mk_var(good_name,ty) 415 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params 416 fun mk_els [] access = [] 417 | mk_els (x::xs) access = ((x:term) |-> ``HD ^access``) :: mk_els xs ``TL ^access`` 418 val args_var = ``args:SExp list`` 419 val tm = mk_abs(args_var,subst (mk_els params args_var) lhs) 420 val th5 = INST [v|->tm] th4 |> SIMP_RULE std_ss [HD,TL,isTrue_if] 421 val rhs = th5 |> concl |> rand |> rand |> rator |> rand 422 val def_tm = mk_eq(lhs,rhs) 423 val (def,ind) = new_def def_tm term_tac 424 val const_tm = def |> SPEC_ALL |> concl |> rator |> rand |> repeat rator 425 (* prove certificate theorem *) 426 val th6 = INST [new_fun |-> const_tm] th5 |> RW1 [GSYM def] 427 val goal = mk_imp(hd (hyp (get_lookup_thm())),th6 |> concl |> rand) 428 val f = foldr mk_abs goal params 429 val forall_goal = foldr mk_forall goal params 430 val result = case ind of 431 NONE => RW [] th6 432 | SOME i => let 433 val i = ISPEC f i |> CONV_RULE (DEPTH_CONV BETA_CONV) 434 val result = prove(i |> concl |> rand, 435 PURE_ONCE_REWRITE_TAC [R_ap_SET_ENV] 436 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] i) \\ REPEAT STRIP_TAC 437 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] th6) \\ ASM_REWRITE_TAC [] 438 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [] \\ RES_TAC 439 \\ METIS_TAC []) |> SPECL params 440 in result end 441 (* install for future use *) 442 val _ = atbl_install name result 443 val _ = save_thm(good_name ^ "_def[compute]",def) 444 val _ = save_thm("R_ev_" ^ good_name,result) 445 in def end; 446 447fun pure_extract_mutual_rec names term_tac = let 448 val _ = print "extracting:" 449 val _ = map (fn name => print (" " ^ name)) names 450 val _ = print "\n" 451 (* evaluate semantics *) 452 fun gen_data name = let 453 val name_tm = stringSyntax.fromMLstring name 454 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` 455 |> REWRITE_CONV [get_lookup_thm()] 456 |> concl |> rand |> pairSyntax.dest_pair 457 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring 458 |> map (fn s => mk_var(simplify_name s,``:SExp``)) 459 |> (fn xs => listSyntax.mk_list(xs,``:SExp``)) 460 val v = mk_var("__" ^ name ^ "__result__",``:SExp list -> SExp``) 461 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``) 462 val _ = atbl_install name lemma 463 in (name,name_tm,t,args,v,lemma) end 464 val data = map gen_data names 465 fun FORCE_UNDISCH th = UNDISCH th handle HOL_ERR _ => th 466 fun derive_thm (name,name_tm,t,args,v,lemma) = let 467 val mt = dest_term t 468 val th1 = FORCE_UNDISCH (SIMP_RULE std_ss [] (R_ev mt)) |> remove_primes 469 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 470 |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH] 471 val tm2 = th2 |> concl |> rator |> rand 472 val tm1 = th1 |> concl 473 val s = fst (match_term (rator tm1) (rator tm2)) 474 val c = DEPTH_CONV eval_fappy_conv 475 val th4 = MATCH_MP th2 (INST s th1) |> DISCH_ALL |> RW [AND_IMP_INTRO] 476 |> CONV_RULE (BINOP_CONV c) 477 in th4 end; 478 val thms = map derive_thm data 479 (* invent function *) 480 fun common_name [] = "" 481 | common_name [name] = name 482 | common_name (x::xs) = x ^ "_" ^ common_name xs 483 val good_name = simplify_name (common_name names) 484 fun mk_tuple [] = mk_var("()",``:unit``) 485 | mk_tuple [x] = x 486 | mk_tuple (x::xs) = pairSyntax.mk_pair(x,mk_tuple xs) 487 val xs = map (fn (name,name_tm,t,args,v,lemma) => 488 mk_tuple (listSyntax.dest_list args |> fst)) data 489 fun list_mk_sum_ty [] = fail() 490 | list_mk_sum_ty [x] = x 491 | list_mk_sum_ty (x::xs) = mk_type("sum",[x,list_mk_sum_ty xs]) 492 val input_ty = list_mk_sum_ty (map type_of xs) 493 val new_fun = mk_var(good_name,mk_type("fun",[input_ty,``:SExp``])) 494 fun params [] ty = [] 495 | params [v] ty = [v] 496 | params (v::vs) ty = let 497 val ts = snd (dest_type ty) 498 val t1 = el 1 ts 499 val t2 = el 2 ts 500 in sumSyntax.mk_inl(v,t2) :: 501 map (fn x => sumSyntax.mk_inr(x,t1)) (params vs t2) end 502 val ps = params xs input_ty 503 val lhs = map (fn x => mk_comb(new_fun,x)) ps 504 fun mk_els [] access = [] 505 | mk_els (x::xs) access = ((x:term) |-> ``HD ^access``) :: mk_els xs ``TL ^access`` 506 val args_var = ``args:SExp list`` 507 fun make_subs ((name,name_tm,t,args,v,lemma),(input,l)) = 508 v |-> mk_abs(args_var,subst (mk_els (fst (listSyntax.dest_list args)) args_var) l) 509 val ss = map make_subs (zip data (zip ps lhs)) 510 val ys = map (SIMP_RULE std_ss [HD,TL,isTrue_if] o INST ss) thms 511 val rhs = map (fst o pairSyntax.dest_pair o 512 snd o dest_comb o snd o dest_comb o concl) ys 513 val def_tm = list_mk_conj (map mk_eq (zip lhs rhs)) 514 val def = case term_tac of 515 NONE => Define [ANTIQUOTE def_tm] 516 | SOME t => tDefine good_name [ANTIQUOTE def_tm] t 517 val ind = fetch "-" (good_name ^ "_ind") 518 val const_tm = def |> SPEC_ALL |> CONJUNCTS |> last 519 |> concl |> rator |> rand |> repeat rator 520 (* prove certificate theorem *) 521 val zs = map (RW1 [R_ap_SET_ENV] o RW1 [GSYM def] o INST [new_fun|->const_tm]) ys 522 val aps = map (snd o dest_comb o concl) zs 523 val extra = hd aps |> rand |> rand 524 val new_prop = mk_var(good_name ^ "_prop",mk_type("fun",[type_of extra,mk_type("fun",[input_ty,``:bool``])])) 525 val ind_hyp_tm = map (fn (x,y) => mk_eq(mk_comb(mk_comb(new_prop,extra),x),y)) (zip ps aps) 526 |> list_mk_conj 527 val ind_hyp = Define [ANTIQUOTE ind_hyp_tm] |> SPEC_ALL 528 val tm = ind_hyp |> CONJUNCTS |> hd |> concl |> rator |> rand |> rator 529 val input_var = mk_var("input",input_ty) 530 val tt = mk_comb(tm,input_var) 531 val tt = mk_imp(hd (hyp (get_lookup_thm())),tt) 532 val goal = mk_forall(input_var,tt) 533 val i = ISPEC (mk_abs(input_var,tt)) ind |> CONV_RULE (DEPTH_CONV BETA_CONV) 534 val th = prove(i |> concl |> rand, 535 MATCH_MP_TAC i \\ SIMP_TAC std_ss [ind_hyp] 536 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 537 \\ EVERY (map IMP_RES_TAC zs) \\ FULL_SIMP_TAC std_ss []) 538 val rs = (map (fn p => RW [ind_hyp] (SPEC p th) 539 |> CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [GSYM R_ap_SET_ENV]))) ps) 540 (* split the common definition *) 541 fun define_parts ((name,name_tm,t,args,v,lemma),th) = let 542 val tm = th |> concl |> rand |> rand |> pairSyntax.dest_pair |> fst 543 val vs = free_vars tm 544 val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` vs 545 val new_fun = mk_var(simplify_name name,ty) 546 val l = foldl (fn (x,y) => mk_comb(y,x)) new_fun (fst (listSyntax.dest_list args)) 547 val part = Define [ANTIQUOTE (mk_eq(l,tm))] 548 in part end 549 val defs = map define_parts (zip data rs) 550 val result = map (RW (map GSYM defs)) rs 551 val real_defs = RW (map GSYM defs) def |> CONJUNCTS 552 val _ = map (fn (name,def) => save_thm(simplify_name name ^ "_def",def)) (zip names real_defs) 553 val _ = map (fn (name,res) => save_thm("R_ev_" ^ simplify_name name,res)) (zip names result) 554 (* install for future use *) 555 val _ = map (fn (name,res) => atbl_install name res) (zip names result) 556 in def end; 557 558 559(* G_ev a function which evaluates the semantics of any functions *) 560 561local 562 val R_ev_format = ``b ==> R_ev x (x1,x2,x3,x4)`` 563 val R_ev_EXAPND_LEMMA = prove( 564 ``(b ==> R_ev x y) ==> 565 (b ==> R_ev x (FST y,FST (SND y),FST (SND (SND y)),SND (SND (SND y))))``, 566 SIMP_TAC std_ss []); 567in 568 fun R_ev_EXPAND th = 569 if can (match_term R_ev_format) (concl th) then th else 570 MATCH_MP R_ev_EXAPND_LEMMA th 571end 572 573fun TUPLE_CONV c tm = 574 if pairSyntax.is_pair tm then 575 ((RATOR_CONV o RAND_CONV) c THENC 576 RAND_CONV (TUPLE_CONV c)) tm 577 else c tm 578 579fun G_ev (Const c) = SPEC c R_ev_Const 580 | G_ev (Var v) = SPEC (mk_string v) R_ev_Var 581 | G_ev (If (x,y,z)) = let 582 val th = LIST_CONJ [G_ev y, G_ev z] 583 val th = MATCH_MP (MATCH_MP R_ev_If_GENERAL th) (R_ev_EXPAND (G_ev x)) 584 val th = CONV_RULE (BINOP_CONV (REWRITE_CONV [])) th 585 in th end 586 | G_ev (Or []) = R_ev_Or_NIL 587 | G_ev (Or [x]) = PRW1 [R_ev_Or_SING_EQ] (G_ev x) 588 | G_ev (Or (x::y::xs)) = let 589 val th = (G_ev (Or (y::xs))) 590 val th = MATCH_MP (MATCH_MP R_ev_Or_CONS_CONS_GENERAL th) (R_ev_EXPAND (G_ev x)) 591 val th = CONV_RULE (BINOP_CONV (REWRITE_CONV [])) th 592 in th end 593 | G_ev (App (f,args)) = let 594 fun R_evl [] = DISCH T R_evl_NIL 595 | R_evl (x::xs) = MATCH_MP (MATCH_MP R_evl_CONS_GENERAL (R_evl xs)) x 596 val th = R_evl (map (R_ev_EXPAND o G_ev) args) 597 val th = MATCH_MP (MATCH_MP R_ev_App (R_ap f)) th 598 val c = REWRITE_CONV [TL,HD,EL_simp_restricted,LENGTH,EL] 599 val th = CONV_RULE (BINOP_CONV c) th 600 in th end 601 | G_ev (Let (xs,x)) = let 602 val prefix = "let " ^ concat (map ((fn x => x ^ " ") o fst) xs) ^ ": " 603 val _ = print (prefix ^ "starts\n") 604 fun R_evl [] = DISCH T R_evl_NIL 605 | R_evl (x::xs) = MATCH_MP (MATCH_MP R_evl_CONS_GENERAL (R_evl xs)) x 606 val s = REWRITE_CONV [FST_SND_IF,pairTheory.FST,pairTheory.SND] 607 val th = R_evl (map (R_ev_EXPAND o G_ev o snd) xs) 608 |> CONV_RULE ((RAND_CONV o RAND_CONV) (TUPLE_CONV s)) 609 val exps = th |> concl |> rand |> rand |> rator |> rand 610 val xs1 = listSyntax.mk_list(map mk_string (map fst xs),``:string``) 611 val th = MATCH_MP (SPEC xs1 R_ev_Let_GENERAL) th 612 val th = PRW1 [pairTheory.SND,pairTheory.FST] th 613 val _ = print (prefix ^ "down\n") 614 val th0 = G_ev x 615 val _ = print (prefix ^ "up, expanding\n") 616 val th1 = R_ev_EXPAND th0 617 val _ = print (prefix ^ "simp\n") 618 val th1 = CONV_RULE ((RAND_CONV o RAND_CONV) (TUPLE_CONV s)) th1 619 val _ = print (prefix ^ "match\n") 620 val tm1 = th1 |> concl |> rand |> rator |> rand |> rand 621 val tm2 = th |> concl |> dest_imp |> fst |> rand |> rator |> rand |> rand 622 val th = MATCH_MP th (INST (fst (match_term tm1 tm2)) th1) 623 val _ = print (prefix ^ "cleaning\n") 624 val c = REWRITE_CONV [TL,HD,EL_simp_restricted,LENGTH,EL,ZIP] 625 val th = CONV_RULE (BINOP_CONV c) th 626 val tm = th |> concl |> rand |> rand 627 val pre = th |> concl |> rator |> rand 628 val xs3 = map (fn x => mk_var(simplify_name(fst x),``:SExp``)) xs 629 val xs4 = fst (listSyntax.dest_list exps) 630 val sub = [``VarBind ^xs1 ^exps`` |-> 631 ``VarBind ^xs1 ^(listSyntax.mk_list(xs3,``:SExp``))``] 632 val tm2 = subst sub tm 633 val pre2 = subst sub pre 634 val tm3 = pairSyntax.mk_anylet(zip xs3 xs4,tm2) 635 val pre3 = pairSyntax.mk_anylet(zip xs3 xs4,pre2) 636 val rw = SYM (pairLib.let_CONV tm3) 637 val pre_rw = SYM (pairLib.let_CONV pre3) 638 val th = CONV_RULE ((RAND_CONV o RAND_CONV) (REWR_CONV rw) THENC 639 (RATOR_CONV o RAND_CONV) (REWR_CONV pre_rw)) th 640 val _ = print (prefix ^ "done\n") 641 in th end 642 | G_ev (LamApp (vs,body,args)) = let 643 val th = MATCH_MP R_ev_LamApp (G_ev (Let (zip vs args,body))) 644 val th = CONV_RULE ((RAND_CONV o RATOR_CONV o RAND_CONV o 645 RATOR_CONV o RAND_CONV) EVAL) th 646 in th end 647 | G_ev (LetStar ([],x)) = PRW1 [R_ev_LetStar_NIL] (G_ev x) 648 | G_ev (LetStar ((v::vs),x)) = PRW1 [R_ev_LetStar_CONS] (G_ev (Let ([v],LetStar (vs,x)))) 649 | G_ev (First x) = MATCH_MP R_ev_FIRST_GENERAL (G_ev x) 650 | G_ev (Second x) = MATCH_MP R_ev_SECOND_GENERAL (G_ev x) 651 | G_ev (Third x) = MATCH_MP R_ev_THIRD_GENERAL (G_ev x) 652 | G_ev (Fourth x) = MATCH_MP R_ev_FOURTH_GENERAL (G_ev x) 653 | G_ev (Fifth x) = MATCH_MP R_ev_FIFTH_GENERAL (G_ev x) 654 | G_ev (And []) = PRW1 [R_ev_And_NIL] (G_ev (Const ``Sym "T"``)) 655 | G_ev (And [x]) = PRW1 [R_ev_And_SING] (G_ev x) 656 | G_ev (And (x::y::xs)) = PRW1 [R_ev_And_CONS] (G_ev (If (x,And (y::xs),Const ``Sym "NIL"``))) 657 | G_ev (List []) = PRW1 [R_ev_List_NIL] (G_ev (Const ``Sym "NIL"``)) 658 | G_ev (List (x::xs)) = PRW1 [R_ev_List_CONS] (G_ev (App (PrimitiveFun op_CONS,[x,List xs]))) 659 | G_ev (Cond []) = PRW1 [R_ev_Cond_NIL] (G_ev (Const ``Sym "NIL"``)) 660 | G_ev (Cond ((x1,x2)::xs)) = PRW1 [R_ev_Cond_CONS] (G_ev (If (x1,x2,Cond xs))) 661 | G_ev _ = failwith("Unsupported construct.") 662 663 664(* extraction of impure functions *) 665 666val let_intro_rule = let 667 val let_lemma = prove(``!f x. f x = LET (f:'a->'b) x``,SIMP_TAC std_ss [LET_DEF]) 668 fun let_intro_conv_aux tm = let 669 val (x,y) = dest_comb tm 670 val (vs,a) = pairSyntax.dest_pabs x 671 val _ = pairSyntax.is_pair vs orelse fail() 672 in ISPEC y (ISPEC x let_lemma) end 673 in CONV_RULE (DEPTH_CONV let_intro_conv_aux) end; 674 675val expand_pair_eq_rule = let 676 val pair_eq_lemma = prove( 677 ``!p x y. ((x,y) = p) = (((x:'a) = FST p) /\ ((y:'b) = SND p))``, 678 Cases_on `p` \\ SIMP_TAC std_ss []) 679 fun let_intro_conv_aux tm = let 680 val (xy,p) = dest_eq tm 681 val (x,y) = dest_pair xy 682 in ISPEC y (ISPEC x (ISPEC p pair_eq_lemma)) end 683 in PURE_REWRITE_RULE [pair_eq_lemma] end 684 685fun mk_fun_ty t x = mk_type("fun",[t,x]) 686 687val R_ap_format = ``R_ap x y`` 688 689fun extract_side_condition tm = 690 if tm ~~ T then T else let 691 val (x,y) = dest_conj tm 692 val x1 = extract_side_condition x 693 val y1 = extract_side_condition y 694 in if x1 ~~ T then y1 else 695 if y1 ~~ T then x1 else mk_conj(x1,y1) end 696 handle HOL_ERR _ => let 697 val fns_assum = hd (hyp (get_lookup_thm())) 698 val _ = match_term fns_assum tm 699 in T end 700 handle HOL_ERR _ => let 701 val (x,y,z) = dest_cond tm 702 val y1 = extract_side_condition y 703 val z1 = extract_side_condition z 704 in if y1 ~~ T andalso z1 ~~ T then T else mk_cond(x,y1,z1) end 705 handle HOL_ERR _ => let 706 val (x,y) = dest_imp tm 707 val y1 = extract_side_condition y 708 in if y1 ~~ T then T else mk_imp(x,y1) end 709 handle HOL_ERR _ => let 710 val _ = match_term R_ap_format tm 711 in T end 712 handle HOL_ERR _ => let 713 val (xs,b) = pairSyntax.dest_anylet tm 714 val b1 = extract_side_condition b 715 in if b1 ~~ T then T else pairSyntax.mk_anylet(xs,b1) end 716 handle HOL_ERR _ => tm 717 718fun impure_extract_aux name term_tac use_short_cut = let 719 val _ = print ("extracting: "^name^"\n") 720 (* evaluate semantics *) 721 val name_tm = stringSyntax.fromMLstring name 722 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` 723 |> REWRITE_CONV [get_lookup_thm()] 724 |> concl |> rand |> pairSyntax.dest_pair 725 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring 726 |> map (fn s => mk_var(simplify_name s,``:SExp``)) 727 |> (fn xs => listSyntax.mk_list(xs,``:SExp``)) 728 val ty = ``:(string |-> string list # term) # string # bool`` 729 val v = mk_var("__result__",``:SExp list # ^ty -> SExp # ^ty``) 730 val v2 = mk_var("__result_side__",``:SExp list # ^ty -> bool``) 731 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v (args,fns,io,ok))``) 732 |> DISCH ``^v2 (args,fns,io,ok)`` |> PURE_REWRITE_RULE [AND_IMP_INTRO] 733 val _ = atbl_install name lemma 734 fun FORCE_UNDISCH th = UNDISCH th handle HOL_ERR _ => th 735 val mt = dest_term t 736 val th0 = G_ev mt 737 val th1 = FORCE_UNDISCH (SIMP_RULE std_ss [FST_SND_IF,EL,HD] th0) |> remove_primes 738 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) res`` 739 |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH] 740 val tm2 = th2 |> concl |> rator |> rand 741 val tm1 = th1 |> concl 742 val s = fst (match_term (rator tm1) (rator tm2)) 743 val c = DEPTH_CONV eval_fappy_conv 744 val th4 = MATCH_MP th2 (INST s th1) |> DISCH_ALL |> RW [AND_IMP_INTRO] 745 |> CONV_RULE (BINOP_CONV c) |> RW [isTrue_T] 746 val th4 = if not use_short_cut then th4 else 747 SPECL [name_tm,ps,args,t] R_ap_NOT_OK 748 |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH] 749 |> (fn th5 => MATCH_MP th5 th4) |> DISCH_ALL |> RW [AND_IMP_INTRO] 750 (* invent function *) 751 val good_name = simplify_name name 752 val params1 = listSyntax.dest_list args |> fst 753 val tm = R_ev_Const |> SPEC_ALL |> Q.INST [`fns`|->`k`] |> concl |> rand |> rand |> rand 754 val params = params1 @ rev (free_vars tm) 755 val fun_ty = foldr (fn (x,y) => mk_fun_ty (type_of x) y) ``:SExp # ^ty`` params 756 val new_fun = mk_var(good_name,fun_ty) 757 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params 758 fun mk_els [] access = [] 759 | mk_els (x::xs) access = ((x:term) |-> ``HD ^access``) :: mk_els xs ``TL ^access`` 760 val args_var = ``args:SExp list`` 761 val vars = ``(args,k,io,ok): (SExp list # (string |-> string list # term) # string # bool)`` 762 val tm = pairSyntax.mk_pabs(vars,subst (mk_els params1 args_var) lhs) 763 val th5 = INST [v|->tm] th4 |> SIMP_RULE std_ss [HD,TL,isTrue_if] |> let_intro_rule 764 val rhs = th5 |> concl |> rand |> rand 765 val def_tm = mk_eq(lhs,rhs) 766 val (def,ind) = new_def def_tm term_tac 767 val const_tm = def |> SPEC_ALL |> concl |> rator |> rand |> repeat rator 768 (* invent side condition *) 769 val fns_assum = hd (hyp (get_lookup_thm())) 770 val tm = fst (dest_imp (concl th4)) 771 val side_fun_ty = foldr (fn (x,y) => mk_fun_ty (type_of x) y) ``:bool`` params 772 val side_new_fun = mk_var(good_name ^ "_side",side_fun_ty) 773 val side_lhs = foldl (fn (x,y) => mk_comb(y,x)) side_new_fun params 774 val side_tm = pairSyntax.mk_pabs(vars,subst (mk_els params1 args_var) side_lhs) 775 val side_rhs = subst [v2|->side_tm] (extract_side_condition tm) 776 |> QCONV (SIMP_CONV std_ss [HD,TL,FST_SND_IF,isTrue_if]) 777 |> let_intro_rule |> concl |> rand 778 val side_def_tm = mk_eq(side_lhs,side_rhs) 779 val (side_def,_) = new_def side_def_tm term_tac 780 val side_const_tm_full = side_def |> SPEC_ALL |> concl |> rator |> rand 781 val side_const_tm = side_const_tm_full |> repeat rator 782 val th6 = INST [v2|->side_tm] th5 |> SIMP_RULE std_ss [HD,TL,isTrue_if] |> let_intro_rule 783 (* prove certificate theorem *) 784 val th7 = INST [new_fun |-> const_tm, side_new_fun |-> side_const_tm] th6 |> RW1 [GSYM def] 785 val lhs = mk_conj(hd (hyp (get_lookup_thm())),side_const_tm_full) 786 val goal = mk_imp(lhs,th7 |> concl |> rand) 787 val f = foldr mk_abs goal params 788 val forall_goal = foldr mk_forall goal params 789(* 790 val (SOME i) = ind 791 set_goal([],i |> concl |> rand) 792 set_goal([],forall_goal) 793*) 794 val result = case ind of 795 NONE => let 796 val result = prove(forall_goal, 797 PURE_ONCE_REWRITE_TAC [side_def] 798 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC th7 799 \\ FULL_SIMP_TAC std_ss [LET_DEF] 800 \\ SRW_TAC [] [] 801 \\ FULL_SIMP_TAC std_ss (get_assum_clauses())) |> SPECL params 802 in result end 803 | SOME i => let 804 val i = SIMP_RULE std_ss [] (expand_pair_eq_rule i) 805 val i = ISPEC f i |> CONV_RULE (DEPTH_CONV BETA_CONV) 806 val result = prove(i |> concl |> rand, 807 PURE_ONCE_REWRITE_TAC [R_ap_SET_ENV] 808 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] i) \\ REPEAT STRIP_TAC 809 \\ Q.PAT_ASSUM [ANTIQUOTE side_const_tm_full] MP_TAC 810 \\ ONCE_REWRITE_TAC [side_def] \\ REPEAT STRIP_TAC 811 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] th7) \\ ASM_REWRITE_TAC [] 812 \\ FULL_SIMP_TAC std_ss [LET_DEF] 813 \\ REPEAT (POP_ASSUM MP_TAC) 814 \\ CONV_TAC (DEPTH_CONV (PairRules.PBETA_CONV)) 815 \\ ONCE_REWRITE_TAC [R_ap_SET_ENV] 816 \\ FULL_SIMP_TAC std_ss (get_assum_clauses()) 817 \\ METIS_TAC []) |> SPECL params 818 in result end 819 (* derive assum clause *) 820 val func_tm = def |> SPEC_ALL |> concl |> rator |> rand 821 val assum_tm = (hd (hyp (get_lookup_thm()))) 822 val goal = mk_imp(assum_tm,mk_comb(rator assum_tm,mk_fst(mk_snd(func_tm)))) 823 val f = foldr mk_abs goal params 824 val forall_goal = foldr mk_forall goal params 825(* 826 val (SOME i) = ind 827 set_goal([],i |> concl |> rand) 828 set_goal([],forall_goal) 829*) 830 val clause_rw = (fns_assum_add_def_IMP:: 831 fns_assum_funcall_IMP:: 832 (map (RW[get_assum_rw()]) (get_assum_clauses()))) 833 val clause = case ind of 834 NONE => let 835 val clause = prove(forall_goal, 836 SRW_TAC [] [def,LET_DEF,get_assum_rw()] 837 \\ IMP_RES_TAC fns_assum_funcall_IMP 838 \\ FULL_SIMP_TAC std_ss clause_rw) |> SPECL params 839 handle HOL_ERR _ => TRUTH 840 in clause end 841 | SOME i => let 842 val i = SIMP_RULE std_ss [] (expand_pair_eq_rule i) 843 val i = ISPEC f i |> CONV_RULE (DEPTH_CONV BETA_CONV) 844 val clause = prove(i |> concl |> rand, 845 MATCH_MP_TAC i \\ SRW_TAC [] [get_assum_rw()] 846 \\ REPEAT STRIP_TAC 847 \\ ONCE_REWRITE_TAC [def] 848 \\ FULL_SIMP_TAC std_ss [LET_DEF] 849 \\ CONV_TAC (DEPTH_CONV (PairRules.PBETA_CONV)) 850 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [EL] 851 \\ FULL_SIMP_TAC std_ss clause_rw 852 \\ METIS_TAC clause_rw) |> SPECL params 853 in clause end 854 (* install for future use *) 855 val _ = atbl_install name result 856 val _ = add_assum_clause clause 857 val _ = save_thm(good_name ^ "_def",def) 858 val _ = save_thm("R_ev_" ^ good_name,result) 859 in def end; 860 861fun impure_extract name term_tac = 862 impure_extract_aux name term_tac false 863 864fun impure_extract_cut name term_tac = 865 impure_extract_aux name term_tac true 866 867 868(* generator *) 869 870fun deep_embeddings base_name defs_inds = let 871 (* generate deep embeddings *) 872 fun fromMLstring s = stringSyntax.fromMLstring (string_uppercase s) 873 fun parts (def,ind) = let 874 val (x,y) = dest_eq (concl (SPEC_ALL def)) 875 val (body,rw) = shallow_to_deep y 876 fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ [y] end 877 handle HOL_ERR _ => [tm]; 878 val xs = list_dest dest_comb x 879 val params = xs |> tl |> map (fst o dest_var) 880 val name = xs |> hd |> dest_const |> fst 881 val strs = listSyntax.mk_list(map fromMLstring params,``:string``) 882 val x1 = pairSyntax.mk_pair(strs,body) 883 val x1 = pairSyntax.mk_pair(fromMLstring name,x1) 884 in (name,params,def,ind,body,rw,x1) end; 885 val ps = map parts defs_inds 886 val xs = ps |> map (fn (name,params,def,ind,body,rw,x1) => x1) 887 val xs = listSyntax.mk_list(xs,type_of (hd xs)) 888 val x = SPEC xs (Q.SPEC `k` fns_assum_def) |> concl |> dest_eq |> fst 889 val tm = ``v k = ^x`` 890 val v = tm |> dest_eq |> fst |> repeat rator 891 val vv = mk_var(base_name,type_of v) 892 val fns_assum = new_definition(base_name^"_def",subst [v|->vv] tm) |> SPEC_ALL 893 (* prove correspondence *) 894 val _ = install_assum_eq fns_assum 895(* 896 val (name,params,def,ind,body,rw,x1) = el 1 ps 897*) 898 fun prove_corr (name,params,def,ind,body,rw,x1) = let 899 val name_tm = fromMLstring name 900 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` 901 |> REWRITE_CONV [get_lookup_thm()] 902 |> concl |> rand |> pairSyntax.dest_pair 903 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring 904 |> map (fn s => mk_var(simplify_name s,``:SExp``)) 905 |> (fn xs => listSyntax.mk_list(xs,``:SExp``)) 906 val v = mk_var("__result__",``:SExp list -> SExp``) 907 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``) 908 val _ = atbl_install (string_uppercase name) lemma 909 fun FORCE_UNDISCH th = UNDISCH th handle HOL_ERR _ => th 910 val mt = dest_term t 911 val th1 = FORCE_UNDISCH (SIMP_RULE std_ss [] (R_ev mt)) |> remove_primes 912 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 913 |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH] 914 val tm2 = th2 |> concl |> rator |> rand 915 val tm1 = th1 |> concl 916 val s = fst (match_term (rator tm1) (rator tm2)) 917 val c = DEPTH_CONV eval_fappy_conv 918 val th4 = MATCH_MP th2 (INST s th1) |> DISCH_ALL |> RW [AND_IMP_INTRO] 919 |> CONV_RULE (BINOP_CONV c) 920 (* connect function *) 921 val good_name = simplify_name name 922 val params = listSyntax.dest_list args |> fst 923 val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` params 924 val new_fun = def |> concl |> dest_eq |> fst |> repeat rator 925 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params 926 fun mk_els [] access = [] 927 | mk_els (x::xs) access = ((x:term) |-> ``HD ^access``) :: mk_els xs ``TL ^access`` 928 val args_var = ``args:SExp list`` 929 val tm = mk_abs(args_var,subst (mk_els params args_var) lhs) 930 val th5 = INST [v|->tm] th4 |> SIMP_RULE std_ss [HD,TL,isTrue_if] 931 val def1 = def |> ONCE_REWRITE_RULE [rw] 932 val th6 = th5 |> REWRITE_RULE [lisp_sexpTheory.LISP_CONS_def] 933 |> CONV_RULE ((RAND_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM def1])) 934 (* prove certificate theorem *) 935 val goal = mk_imp(hd (hyp (get_lookup_thm())),th6 |> concl |> rand) 936 val f = foldr mk_abs goal params 937 val forall_goal = foldr mk_forall goal params 938 val result = if concl ind ~~ T then RW [] th6 else let 939 val i = ISPEC f ind |> CONV_RULE (DEPTH_CONV BETA_CONV) 940 val i = REWRITE_RULE [isTrue_INTRO] i 941 val result = prove(i |> concl |> rand, 942 PURE_ONCE_REWRITE_TAC [R_ap_SET_ENV] 943 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] i) \\ REPEAT STRIP_TAC 944 \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] th6) \\ ASM_REWRITE_TAC [] 945 \\ REPEAT STRIP_TAC \\ METIS_TAC [isTrue_INTRO]) |> SPECL params 946 in result end 947 (* install for future use *) 948 val _ = atbl_install (string_uppercase name) result 949 val _ = save_thm("R_ap_" ^ name,result) 950 in result end; 951 val thms = map prove_corr ps 952 in (fns_assum,thms) end; 953 954 955end; 956