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