Permalink
Browse files

Merge branch 'logging' into standalonetac

  • Loading branch information...
2 parents 7926a17 + 3e8ecc5 commit beb0771801c1ed8b8b70a571058fc8164e73a40b @xrchz xrchz committed Feb 17, 2012
@@ -8,5 +8,6 @@ clean:
cd lisp-runtime/implementation && Holmake cleanAll && cd ../..
cd lisp-runtime/parse && Holmake cleanAll && cd ../..
cd lisp-runtime/spec && Holmake cleanAll && cd ../..
+ cd lisp-runtime/extract && Holmake cleanAll && cd ../..
cd milawa-prover && Holmake cleanAll && cd ..
cd milawa-prover/soundness-thm && Holmake cleanAll && cd ../..
@@ -19,8 +19,8 @@ Two subdirectories:
The top-level result is in milawa-prover/soundness-thm where a theorem
states: when Milawa is run on top of the verified runtime it will only
-ever prove statements that can be derived from the (sound!) inference
-rules -- no matter how reflection or any other feature is used.
+ever prove statements that are true w.r.t. the semantics of Milawa's
+formulas -- no matter how reflection or any other feature is used.
Copyright Magnus O. Myreen 2012
@@ -2883,6 +2883,90 @@ val term2sexp_def = tDefine "term2sexp" `
THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC)
\\ DECIDE_TAC);
+val fun_name_ok_def = Define `
+ (fun_name_ok (Fun f) = ~MEM f reserved_names) /\
+ (fun_name_ok _ = T)`;
+
+val no_bad_names_def = tDefine "no_bad_names" `
+ (no_bad_names (Const s) = T) /\
+ (no_bad_names (Var v) = ~(v = "T") /\ ~(v = "NIL")) /\
+ (no_bad_names (App fc vs) = fun_name_ok fc /\ EVERY no_bad_names vs) /\
+ (no_bad_names (If x y z) = no_bad_names x /\ no_bad_names y /\ no_bad_names z) /\
+ (no_bad_names (LamApp xs z ys) = no_bad_names z /\ EVERY no_bad_names ys) /\
+ (no_bad_names (Let zs x) = EVERY (\x. no_bad_names (SND x)) zs /\ no_bad_names x) /\
+ (no_bad_names (LetStar zs x) = EVERY (\x. no_bad_names (SND x)) zs /\ no_bad_names x) /\
+ (no_bad_names (Cond qs) = EVERY (\x. no_bad_names (FST x) /\ no_bad_names (SND x)) qs) /\
+ (no_bad_names (Or ts) = EVERY no_bad_names ts) /\
+ (no_bad_names (And ts) = EVERY no_bad_names ts) /\
+ (no_bad_names (List ts) = EVERY no_bad_names ts) /\
+ (no_bad_names (First x) = no_bad_names x) /\
+ (no_bad_names (Second x) = no_bad_names x) /\
+ (no_bad_names (Third x) = no_bad_names x) /\
+ (no_bad_names (Fourth x) = no_bad_names x) /\
+ (no_bad_names (Fifth x) = no_bad_names x) /\
+ (no_bad_names (Defun fname ps s) = T)`
+ (WF_REL_TAC `measure (term_size)` \\ SRW_TAC [] []
+ THEN1 (Induct_on `vs` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 DECIDE_TAC
+ THEN1 DECIDE_TAC
+ THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 DECIDE_TAC
+ THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `ys` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC)
+ THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC)
+ \\ DECIDE_TAC);
+
+val sexp2list_list2sexp = prove(
+ ``!x. sexp2list (list2sexp x) = x``,
+ Induct \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []);
+
+val MAP_EQ_IMP = prove(
+ ``!xs f. (!x. MEM x xs ==> (f x = x)) ==> (MAP f xs = xs)``,
+ Induct \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ METIS_TAC []);
+
+val sexp2term_term2sexp = store_thm("sexp2term_term2sexp",
+ ``!t. no_bad_names t ==> (sexp2term (term2sexp t) = t)``,
+ HO_MATCH_MP_TAC (fetch "-" "term2sexp_ind") \\ REPEAT STRIP_TAC
+ \\ FULL_SIMP_TAC std_ss [no_bad_names_def]
+ THEN1 (EVAL_TAC \\ FULL_SIMP_TAC std_ss [])
+ THEN1 (EVAL_TAC \\ FULL_SIMP_TAC std_ss [])
+ THEN1
+ (SIMP_TAC (srw_ss()) [term2sexp_def,LET_DEF]
+ \\ Cases_on `fc` THEN TRY
+ (ASM_SIMP_TAC (srw_ss()) [func2sexp_def,list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def]
+ \\ SIMP_TAC (srw_ss()) [Once sexp2term_def,LET_DEF] \\ TRY (Cases_on `l`)
+ \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def,
+ getSym_def,prim2sym_def,sym2prim_def,sexp2list_list2sexp,
+ MAP_MAP_o,combinTheory.o_DEF,fun_name_ok_def]
+ \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM] \\ NO_TAC)
+ \\ FULL_SIMP_TAC (srw_ss()) [func2sexp_def,fun_name_ok_def]
+ \\ FULL_SIMP_TAC (srw_ss()) [reserved_names_def,MEM,APPEND,macro_names_def]
+ \\ SIMP_TAC (srw_ss()) [Once sexp2term_def,LET_DEF]
+ \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def,
+ getSym_def,prim2sym_def,sym2prim_def,sexp2list_list2sexp,
+ MAP_MAP_o,combinTheory.o_DEF]
+ \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM])
+ THEN1
+ (SIMP_TAC (srw_ss()) [term2sexp_def,Once sexp2term_def,LET_DEF]
+ \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def])
+ THEN
+ (SIMP_TAC (srw_ss()) [term2sexp_def,Once sexp2term_def,LET_DEF]
+ \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def,
+ getSym_def,sym2prim_def,sexp2list_list2sexp,MAP_MAP_o,combinTheory.o_DEF]
+ \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM]));
+
+val verified_string_def = Define `
+ verified_string xs =
+ if ~ALL_DISTINCT (MAP FST xs) then NONE else
+ if ~EVERY (\(name,params,body). no_bad_names body) xs then NONE else
+ SOME (FLAT (MAP ( \ (name,params,body). sexp2string
+ (list2sexp [Sym "DEFUN"; Sym name;
+ list2sexp (MAP Sym params); term2sexp body]) ++ "\n") xs))`
+
(* translation sexp2sexp *)
@@ -0,0 +1,2 @@
+INCLUDES = ../parse ../spec ../bytecode
+OPTIONS=QUIT_ON_FAILURE
@@ -3,14 +3,18 @@ sig
include Abbrev
- (* main functions *)
+ (* main functions for extraction *)
val pure_extract : string -> tactic option -> thm
val pure_extract_mutual_rec : string list -> tactic option -> thm
val impure_extract : string -> tactic option -> thm
val impure_extract_cut : string -> tactic option -> thm
- (* setting the state *)
+ (* function used for code synthesis *)
+
+ val deep_embeddings : string -> (thm * thm) list -> thm * thm list
+
+ (* setting the state of the extractor *)
val set_lookup_thm : thm -> unit
val install_assum_eq : thm -> unit
@@ -78,7 +78,6 @@ fun dest_primitive_op tm =
if tm = ``opSYMBOL_LESS`` then op_SYMBOL_LESS else
if tm = ``opADD`` then op_ADD else
if tm = ``opSUB`` then op_SUB else
- if tm = ``opATOMP`` then op_ATOMP else
if tm = ``opCONSP`` then op_CONSP else
if tm = ``opSYMBOLP`` then op_SYMBOLP else
if tm = ``opNATP`` then op_NATP else
@@ -130,6 +129,85 @@ fun dest_term tm = let
end
+(* mapping from shallow embeddings to deep embeddings *)
+
+infix $$
+val op $$ = mk_comb
+
+val string_uppercase = let
+ fun uppercase_char c =
+ if #"a" <= c andalso c <= #"z" then chr (ord c - (ord #"a" - ord #"A")) else c
+ in String.translate (fn c => implode [uppercase_char c]) end
+
+fun shallow_to_deep tm = let
+ fun fromHOLstring s = string_uppercase (stringSyntax.fromHOLstring s)
+ fun fromMLstring s = stringSyntax.fromMLstring (string_uppercase s)
+ fun is_const tm =
+ (if rator tm = ``Sym`` then can fromHOLstring (rand tm) else
+ if rator tm = ``Val`` then can numSyntax.int_of_term (rand tm) else
+ if rator (rator tm) = ``Dot`` then is_const (rand (rator tm)) andalso
+ is_const (rand tm)
+ else false) handle HOL_ERR _ => false
+ val lisp_primitives =
+ [(``Dot``,``opCONS``),
+ (``LISP_CONS``,``opCONS``),
+ (``LISP_EQUAL:SExp->SExp->SExp``,``opEQUAL``),
+ (``LISP_LESS``,``opLESS``),
+ (``LISP_SYMBOL_LESS``,``opSYMBOL_LESS``),
+ (``LISP_ADD``,``opADD``),
+ (``LISP_SUB``,``opSUB``),
+ (``LISP_CONSP``,``opCONSP``),
+ (``LISP_SYMBOLP``,``opSYMBOLP``),
+ (``LISP_NUMBERP``,``opNATP``),
+ (``CAR``,``opCAR``),
+ (``CDR``,``opCDR``)]
+ fun aux_fail tm =
+ failwith("Unable to translate: \n\n" ^ term_to_string tm ^ "\n\n")
+ fun aux tm =
+ if is_const tm then ``Const`` $$ tm else
+ if can (match_term ``Val n``) tm then aux_fail tm else
+ if can (match_term ``Sym s``) tm then aux_fail tm else
+ if is_var tm then let
+ val (s,ty) = dest_var tm
+ val _ = ty = ``:SExp`` orelse failwith("Variable of wrong type: " ^ s)
+ in ``Var`` $$ fromMLstring s end
+ else if is_cond tm then let
+ val (x1,x2,x3) = dest_cond tm
+ val _ = if rator x1 = ``isTrue`` then () else aux_fail x1
+ in ``If`` $$ aux (rand x1) $$ aux x2 $$ aux x3 end
+ else if can pairSyntax.dest_anylet tm then let
+ val (xs,x) = pairSyntax.dest_anylet tm
+ val ys = map (fn (x,y) => pairSyntax.mk_pair(x |> dest_var |> fst |> fromMLstring, aux y)) xs
+ val y = listSyntax.mk_list(ys,``:string # term``)
+ in ``Let`` $$ y $$ (aux x) end
+ else (* general function application *) let
+ fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ [y] end
+ handle HOL_ERR _ => [tm];
+ val xs = list_dest dest_comb tm
+ val (x,xs) = (hd xs, tl xs)
+ fun lookup x [] = fail()
+ | lookup x ((y,z)::zs) = if x = y then z else lookup x zs
+ val f = ``PrimitiveFun`` $$ lookup x lisp_primitives handle HOL_ERR _ =>
+ ``Fun`` $$ fromMLstring (fst (dest_const x))
+ handle HOL_ERR _ => aux_fail x
+ val ys = map aux xs
+ in ``App`` $$ f $$ listSyntax.mk_list(ys,``:term``) end
+ fun preprocess tm = QCONV (REWRITE_CONV [isTrue_INTRO]) tm
+ val th = preprocess tm
+ val tm2 = rand (concl th)
+ in (aux tm2, th) end
+
+(*
+val tm = ``let x = LISP_ADD x y in let z = y in LISP_SUB x y``
+dest_term (fst (shallow_to_deep tm))
+
+ plan: provide a method which, given a list of definition and
+ induction thm pairs, produces deep embeddings and correspondence
+ proofs.
+
+*)
+
+
(* state of extraction function *)
local
@@ -775,4 +853,92 @@ fun impure_extract name term_tac =
fun impure_extract_cut name term_tac =
impure_extract_aux name term_tac true
+
+(* generator *)
+
+fun deep_embeddings base_name defs_inds = let
+ (* generate deep embeddings *)
+ fun fromMLstring s = stringSyntax.fromMLstring (string_uppercase s)
+ fun parts (def,ind) = let
+ val (x,y) = dest_eq (concl (SPEC_ALL def))
+ val (body,rw) = shallow_to_deep y
+ fun list_dest f tm = let val (x,y) = f tm in list_dest f x @ [y] end
+ handle HOL_ERR _ => [tm];
+ val xs = list_dest dest_comb x
+ val params = xs |> tl |> map (fst o dest_var)
+ val name = xs |> hd |> dest_const |> fst
+ val strs = listSyntax.mk_list(map fromMLstring params,``:string``)
+ val x1 = pairSyntax.mk_pair(strs,body)
+ val x1 = pairSyntax.mk_pair(fromMLstring name,x1)
+ in (name,params,def,ind,body,rw,x1) end;
+ val ps = map parts defs_inds
+ val xs = ps |> map (fn (name,params,def,ind,body,rw,x1) => x1)
+ val xs = listSyntax.mk_list(xs,type_of (hd xs))
+ val x = SPEC xs (Q.SPEC `k` fns_assum_def) |> concl |> dest_eq |> fst
+ val tm = ``v k = ^x``
+ val v = tm |> dest_eq |> fst |> repeat rator
+ val vv = mk_var(base_name,type_of v)
+ val fns_assum = new_definition(base_name^"_def",subst [v|->vv] tm) |> SPEC_ALL
+ (* prove correspondence *)
+ val _ = install_assum_eq fns_assum
+(*
+ val (name,params,def,ind,body,rw,x1) = el 1 ps
+*)
+ fun prove_corr (name,params,def,ind,body,rw,x1) = let
+ val name_tm = fromMLstring name
+ val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm``
+ |> REWRITE_CONV [get_lookup_thm()]
+ |> concl |> rand |> pairSyntax.dest_pair
+ val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring
+ |> map (fn s => mk_var(simplify_name s,``:SExp``))
+ |> (fn xs => listSyntax.mk_list(xs,``:SExp``))
+ val v = mk_var("__result__",``:SExp list -> SExp``)
+ val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``)
+ val _ = atbl_install (string_uppercase name) lemma
+ fun FORCE_UNDISCH th = UNDISCH th handle HOL_ERR _ => th
+ val mt = dest_term t
+ val th1 = FORCE_UNDISCH (SIMP_RULE std_ss [] (R_ev mt)) |> remove_primes
+ val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
+ |> SIMP_RULE std_ss [get_lookup_thm(),LENGTH]
+ val tm2 = th2 |> concl |> rator |> rand
+ val tm1 = th1 |> concl
+ val s = fst (match_term (rator tm1) (rator tm2))
+ val c = DEPTH_CONV eval_fappy_conv
+ val th4 = MATCH_MP th2 (INST s th1) |> DISCH_ALL |> RW [AND_IMP_INTRO]
+ |> CONV_RULE (BINOP_CONV c)
+ (* connect function *)
+ val good_name = simplify_name name
+ val params = listSyntax.dest_list args |> fst
+ val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` params
+ val new_fun = def |> concl |> dest_eq |> fst |> repeat rator
+ val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
+ fun mk_els [] access = []
+ | mk_els (x::xs) access = ((x:term) |-> ``HD ^access``) :: mk_els xs ``TL ^access``
+ val args_var = ``args:SExp list``
+ val tm = mk_abs(args_var,subst (mk_els params args_var) lhs)
+ val th5 = INST [v|->tm] th4 |> SIMP_RULE std_ss [HD,TL,isTrue_if]
+ val def1 = def |> ONCE_REWRITE_RULE [rw]
+ val th6 = th5 |> REWRITE_RULE [lisp_sexpTheory.LISP_CONS_def]
+ |> CONV_RULE ((RAND_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM def1]))
+ (* prove certificate theorem *)
+ val goal = mk_imp(hd (hyp (get_lookup_thm())),th6 |> concl |> rand)
+ val f = foldr mk_abs goal params
+ val forall_goal = foldr mk_forall goal params
+ val result = if concl ind = T then RW [] th6 else let
+ val i = ISPEC f ind |> CONV_RULE (DEPTH_CONV BETA_CONV)
+ val i = REWRITE_RULE [isTrue_INTRO] i
+ val result = prove(i |> concl |> rand,
+ PURE_ONCE_REWRITE_TAC [R_ap_SET_ENV]
+ \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] i) \\ REPEAT STRIP_TAC
+ \\ MATCH_MP_TAC (RW1 [R_ap_SET_ENV] th6) \\ ASM_REWRITE_TAC []
+ \\ REPEAT STRIP_TAC \\ METIS_TAC [isTrue_INTRO]) |> SPECL params
+ in result end
+ (* install for future use *)
+ val _ = atbl_install (string_uppercase name) result
+ val _ = save_thm("R_ap_" ^ name,result)
+ in result end;
+ val thms = map prove_corr ps
+ in (fns_assum,thms) end;
+
+
end;
@@ -525,4 +525,37 @@ val FST_SND_IF = store_thm("FST_SND_IF",
val isTrue_T = save_thm("isTrue_T",EVAL ``isTrue (Sym "T")``);
+val isTrue_INTRO = store_thm("isTrue_INTRO",
+ ``((x = y) = isTrue (LISP_EQUAL x y)) /\
+ (isTrue x /\ isTrue y = isTrue (if isTrue x then y else Sym "NIL")) /\
+ (isTrue x \/ isTrue y = isTrue (if isTrue x then Sym "T" else y)) /\
+ (LISP_CONS = Dot) /\
+ (~isTrue x = isTrue (if isTrue x then Sym "NIL" else Sym "T")) /\
+ (getVal x < getVal y = isTrue (LISP_LESS x y)) /\
+ (getVal x > getVal y = isTrue (LISP_LESS y x)) /\
+ (getVal x <= getVal y = ~(getVal x > getVal y)) /\
+ (getVal x >= getVal y = ~(getVal x < getVal y)) /\
+ (getSym x < getSym y = isTrue (LISP_SYMBOL_LESS x y)) /\
+ (isDot x = isTrue (LISP_CONSP x)) /\
+ (isVal x = isTrue (LISP_NUMBERP x)) /\
+ (isSym x = isTrue (LISP_SYMBOLP x))``,
+ SIMP_TAC std_ss [FUN_EQ_THM] \\ EVAL_TAC \\ SRW_TAC [] [] \\ DECIDE_TAC);
+
+val PAIR_LEMMA = prove(
+ ``!x. (x = (FST x,x2)) = (SND x = x2)``,
+ Cases \\ SRW_TAC [] []);
+
+val SND_SND_SND_funcall_IMP = store_thm("SND_SND_SND_funcall_IMP",
+ ``R_ap (Funcall,(Sym f)::xs,ARB,k,io,ok) (x1,x2,x3,ok2) /\
+ SND (SND (SND (funcall ((Sym f)::xs) k io ok))) ==> ok2``,
+ SIMP_TAC std_ss [funcall_def] \\ REPEAT STRIP_TAC
+ \\ `funcall_ok (Sym f::xs) k io ok` by METIS_TAC [funcall_ok_def]
+ \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `ok2` \\ SIMP_TAC std_ss []
+ \\ `!res. R_ap (Funcall,Sym f::xs,ARB,k,io,ok) res =
+ (res = (FST res, FST (SND res), FST (SND (SND res)),F))` by METIS_TAC [R_ap_F_11,pairTheory.PAIR]
+ \\ FULL_SIMP_TAC std_ss [PAIR_LEMMA]
+ \\ `?result:SExp # (string |-> string list # term) # string # bool. ~SND (SND (SND result))` by ALL_TAC
+ THEN1 (Q.EXISTS_TAC `(ARB,ARB,ARB,F)` \\ EVAL_TAC)
+ \\ METIS_TAC []);
+
val _ = export_theory();
@@ -0,0 +1,11 @@
+signature lisp_synthesisLib =
+sig
+
+ include Abbrev
+
+ val lisp_Define : term quotation -> thm
+ val lisp_tDefine : string -> term quotation -> tactic -> thm
+
+ val synthesise_deep_embeddings : unit -> thm
+
+end
Oops, something went wrong.

0 comments on commit beb0771

Please sign in to comment.