Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

More examples and basic interface for extensions.

  • Loading branch information...
commit fb65d726a8b89728577973ee012f615390704e0d 1 parent 4cf17fb
@myreen myreen authored
View
9 examples/miniML/ml_translatorLib.sig
@@ -5,11 +5,18 @@ sig
(* main functionality *)
- val translate : thm -> thm
+ val translate : thm -> thm (* e.g. try translate listTheory.MAP *)
+ val hol2deep : term -> thm (* e.g. try hol2deep ``\x.x`` *)
(* wrapper functions *)
val mlDefine : term quotation -> thm * thm
val mltDefine : string -> term quotation -> tactic -> thm * thm
+ (* interface for teaching the translator about new types *)
+
+ val add_type_inv : term -> unit
+ val store_eval_thm : thm -> thm
+ val store_eq_thm : thm -> thm
+
end
View
140 examples/miniML/ml_translatorLib.sml
@@ -19,6 +19,7 @@ fun dest_fun_type ty = let
local
val other_types = ref (fn (ty:hol_type) => (fail()):term)
+ val user_supplied_types = ref ([]:hol_type list)
in
fun get_type_inv ty =
if is_vartype ty then let
@@ -34,6 +35,12 @@ in
fun new_type_inv f = let
val old = (!other_types)
in (other_types := (fn y => (f y handle HOL_ERR _ => old y))) end
+ fun add_type_inv tm = let
+ val ty = fst (dest_fun_type (type_of tm))
+ val _ = user_supplied_types := ty::(!user_supplied_types)
+ val f = (fn x => if x = ty then tm else fail())
+ in new_type_inv f end
+ fun get_user_supplied_types () = !user_supplied_types
end
@@ -92,6 +99,12 @@ fun get_nchotomy_of ty = let (* ensures that good variables names are used *)
(*
val ty = ``:'a list``
+val ty = ``:'a # 'b``
+val ty = ``:unit``
+val _ = Hol_datatype `TREE = LEAF of 'a | BRANCH of TREE => TREE`;
+register_type ``:'a TREE``
+val _ = Hol_datatype `BTREE = BLEAF of ('a TREE) | BBRANCH of BTREE => BTREE`;
+val ty = ``:'a BTREE``
*)
fun derive_thms_for_type ty = let
@@ -138,6 +151,37 @@ fun derive_thms_for_type ty = let
val inv_def = define_abs name ty case_th
val inv_lhs = inv_def |> CONJUNCTS |> hd |> SPEC_ALL |> concl
|> dest_eq |> fst
+ (* prove EqualityType lemma, e.g. !a. EqualityType a ==> EqualityType (list a) *)
+ val eq_lemma = let
+ val tm = rator (rator inv_lhs)
+ fun list_dest f tm = let val (x,y) = f tm
+ in list_dest f x @ list_dest f y end handle HOL_ERR _ => [tm]
+ val xs =
+ inv_def |> RW [GSYM CONJ_ASSOC] |> SPEC_ALL |> CONJUNCTS
+ |> map (snd o dest_eq o concl o SPEC_ALL)
+ |> map (last o list_dest dest_exists)
+ |> map (tl o list_dest dest_conj) |> Lib.flatten
+ |> map (rator o rator) |> filter (fn t => t <> tm)
+ val ys = map (fn tm => ``EqualityType ^tm``) xs
+ val tm1 = ``EqualityType ^tm``
+ val tm2 = if ys = [] then T else list_mk_conj ys
+ val goal = mk_imp(tm2,tm1)
+ val eq_lemma = prove(goal,
+ REPEAT STRIP_TAC
+ \\ FULL_SIMP_TAC std_ss [EqualityType_def]
+ \\ STRIP_TAC THEN1
+ (REPEAT (Q.PAT_ASSUM `!x1 x2 x3 x4. bbb` (K ALL_TAC))
+ \\ (Induct ORELSE Cases)
+ \\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]
+ \\ REPEAT STRIP_TAC \\ RES_TAC)
+ THEN1
+ (REPEAT (Q.PAT_ASSUM `!x1 x2. bbb ==> bbbb` (K ALL_TAC))
+ \\ (Induct ORELSE Cases)
+ \\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]
+ \\ Cases_on `x2` \\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]
+ \\ REPEAT STRIP_TAC \\ METIS_TAC []))
+ in eq_lemma end handle HOL_ERR _ => TRUTH
+
(* make new inv_def part of get_type_inv *)
val inv = rator (rator inv_lhs)
fun extension_to_get_inv_type ty0 = let
@@ -266,10 +310,11 @@ fun derive_thms_for_type ty = let
\\ EXISTS_TAC witness \\ ASM_SIMP_TAC (srw_ss()) [inv_def,evaluate_list_SIMP])
in (pat,lemma) end;
val conses = map derive_cons ts
- in (ty,ret_ty,inv_def,conses,case_lemma,ts) end
+ in (ty,eq_lemma,inv_def,conses,case_lemma,ts) end
local
val memory = ref []
+ val user_defined_eq_lemmas = ref []
fun add_type ty = let
val res = derive_thms_for_type ty
val _ = (memory := res :: (!memory))
@@ -277,8 +322,11 @@ local
fun lookup ty = first (fn (ty1,_,_,_,_,_) => can (match_type ty1) ty) (!memory)
fun lookup_type ty = lookup ty handle HOL_ERR _ => add_type ty
fun conses_of ty = let
- val (ty,ret_ty,inv_def,conses,case_lemma,ts) = lookup ty
+ val (ty,eq_lemma,inv_def,conses,case_lemma,ts) = lookup ty
in conses end
+ fun stored_eq_lemmas () =
+ map (fn (ty,eq_lemma,inv_def,conses,case_lemma,ts) => eq_lemma) (!memory)
+ val init_eq_lemmas = map (DISCH T) (CONJUNCTS EqualityType_NUM_BOOL)
in
fun register_type ty = (lookup_type ty; ())
fun cons_for tm = let
@@ -291,17 +339,21 @@ in
in INST ss (INST_TYPE i th) end
handle HOL_ERR _ => failwith("Not a constructor for a registered type.")
fun case_of ty = let
- val (ty,ret_ty,inv_def,conses,case_lemma,ts) = lookup ty
+ val (ty,eq_lemma,inv_def,conses,case_lemma,ts) = lookup ty
in (case_lemma,ts) end
+ fun eq_lemmas () =
+ init_eq_lemmas @ filter (fn th => concl th <> T) (stored_eq_lemmas())
+ @ (!user_defined_eq_lemmas)
+ fun store_eq_thm th = ((user_defined_eq_lemmas := th::(!user_defined_eq_lemmas));th)
end
fun register_term_types tm = let
fun every_term f tm = (f tm ;
if is_abs tm then every_term f (snd (dest_abs tm)) else
if is_comb tm then (every_term f (rand tm); every_term f (rator tm)) else ())
- val special_types = [``:num``,``:bool``]
+ val special_types = [``:num``,``:bool``] @ get_user_supplied_types ()
fun ignore_type ty =
- if mem ty special_types then true else
+ if can (first (fn ty1 => can (match_type ty1) ty)) special_types then true else
if not (can dest_type ty) then true else
if can (dest_fun_type) ty then true else false
fun register_term_type tm = let
@@ -414,6 +466,22 @@ fun inst_case_thm tm hol2deep = let
REWRITE_CONV [])) th
in th end;
+fun SIMP_EqualityType_ASSUMS th = let
+ val lemmas = eq_lemmas () |> map (UNDISCH_ALL o RW [GSYM AND_IMP_INTRO])
+ val th = th |> DISCH_ALL |> PURE_REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL
+ val xs = map (fn th => (concl th,th)) lemmas
+ fun find_match [] tm = fail()
+ | find_match ((pat,th1)::xs) tm = let
+ val (ss,i) = match_term pat tm
+ in INST ss (INST_TYPE i th1) end
+ handle HOL_ERR _ => find_match xs tm
+ fun remove_one th = let
+ val hs = hyp th
+ val tm = first (can (find_match xs)) hs
+ val lemma = find_match xs tm
+ val th = MP (DISCH tm th) lemma
+ in remove_one th end handle HOL_ERR _ => th
+ in remove_one th end;
(* The preprocessor -- returns (def,ind). Here def is the original
definition stated as a single line:
@@ -430,6 +498,7 @@ fun single_line_def def = let
val lhs = def |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL
|> concl |> dest_eq |> fst
val const = lhs |> repeat rator
+ fun mk_container tm = ``CONTAINER ^tm``
in if filter (not o is_var) (args lhs) = [] then (def,NONE) else let
val name = const |> dest_const |> fst
val thy = #Thy (dest_thy_const const)
@@ -449,13 +518,15 @@ fun single_line_def def = let
handle HOL_ERR _ =>
fetch thy (name ^ "_primitive_DEF")
val (v,tm) = tp |> concl |> rand |> rand |> dest_abs
- val goal = mk_eq(tpc,subst [v|->tpc] tm)
+ val goal = mk_eq(tpc,(subst [v|->tpc] tm))
val lemma = prove(goal,
SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD,GSYM rw]
- THEN SRW_TAC [] []
- THEN REPEAT BasicProvers.FULL_CASE_TAC
- THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def]))
- THEN SRW_TAC [] [])
+ \\ REPEAT STRIP_TAC
+ \\ CONV_TAC (BINOP_CONV (REWR_CONV (GSYM CONTAINER_def)))
+ \\ SRW_TAC [] []
+ \\ REPEAT BasicProvers.FULL_CASE_TAC
+ \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def]))
+ \\ SRW_TAC [] [])
val new_def =
rw |> SPEC_ALL |> CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [lemma]))
|> CONV_RULE (RAND_CONV BETA_CONV)
@@ -482,17 +553,16 @@ fun single_line_def def = let
val tm = SIMP_CONV std_ss [Once pair_case_def,GSYM curried] (subst [a|->c,v|->cc] tm)
|> concl |> rand |> rator |> rand
val vs = free_vars tm
- val goal = mk_eq(c2,tm)
+ val goal = mk_eq(mk_container c2, mk_container tm)
val vs = filter (fn x => not (mem x vs)) (free_vars goal)
val goal = subst (map (fn v => v |-> ``():unit``) vs) goal
val goal = subst [mk_comb(c1,``():unit``)|->const] goal
val _ = not (can (find_term is_arb) goal) orelse failwith("Definition contains ARB.")
val lemma = prove(goal,
- SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD]
- THEN SRW_TAC [] []
- THEN REPEAT BasicProvers.FULL_CASE_TAC
- THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def]))
- THEN SRW_TAC [] [])
+ SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD] \\ SRW_TAC [] []
+ \\ REPEAT BasicProvers.FULL_CASE_TAC
+ \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def]))
+ \\ SRW_TAC [] []) |> CONV_RULE (BINOP_CONV (REWR_CONV CONTAINER_def))
in (lemma,SOME ind) end end
fun remove_pair_abs def = let
@@ -555,7 +625,6 @@ fun dest_builtin_binop tm = let
if p = ``($*):num->num->num`` then SPEC p Eval_Opn else
if p = ``($DIV):num->num->num`` then SPEC p Eval_Opn else
if p = ``($MOD):num->num->num`` then SPEC p Eval_Opn else
- if p = ``($=):num->num->bool`` then SPEC p Eval_Opb else
if p = ``($<):num->num->bool`` then SPEC p Eval_Opb else
if p = ``($<=):num->num->bool`` then SPEC p Eval_Opb else
if p = ``($>):num->num->bool`` then SPEC p Eval_Opb else
@@ -563,7 +632,6 @@ fun dest_builtin_binop tm = let
if p = ``($/\):bool->bool->bool`` then Eval_And else
if p = ``($\/):bool->bool->bool`` then Eval_Or else
if p = ``($==>):bool->bool->bool`` then Eval_Implies else
- if p = ``($=):bool->bool->bool`` then Eval_Bool_Equal else
failwith("Not a builtin operator"))
end
@@ -593,10 +661,6 @@ fun apply_Eval_Fun v th fix = let
else MATCH_MP Eval_Fun (GEN ``v:v`` (GEN v th1))
in th2 end;
-(*
-val v = (last rev_params)
-*)
-
fun apply_Eval_Recclosure fname v th = let
val vname = fst (dest_var v)
val vname_str = stringLib.fromMLstring vname
@@ -628,11 +692,15 @@ fun apply_Eval_Recclosure fname v th = let
val th4 = CONV_RULE (QCONV (DEPTH_CONV replace_conv)) th3
(* lift cl_env assumptions out *)
val cl_env = mk_var("cl_env",type_of old_env)
- val pattern = ``Eval env (Var name) (Eq x)``
+ val pattern = ``Eval env (Var name) ($= x)``
val cl_assums = find_terms (fn tm => can (match_term pattern) tm andalso
((tm |> rator |> rator |> rand) = cl_env)) (concl th4)
val th5 = REWRITE_RULE (map ASSUME cl_assums) th4
- in th5 end
+ (* lift EqualityType assumptions out *)
+ val pattern = ``EqualityType (a:'a->v->bool)``
+ val eq_assums = find_terms (can (match_term pattern)) (concl th5)
+ val th6 = REWRITE_RULE (map ASSUME eq_assums) th5
+ in th6 end
local
val memory = ref (tl [(T,TRUTH)])
@@ -643,6 +711,12 @@ in
fun get_mem () = !memory
end
+fun store_eval_thm th = let
+ val th1 = UNDISCH_ALL th
+ val pat = th1 |> concl |> rand |> rand
+ val _ = store_cert pat th1
+ in th end
+
local
val rec_pattern = ref T;
in
@@ -668,12 +742,12 @@ fun hol2deep tm =
val (name,ty) = dest_var tm
val inv = get_type_inv ty
val str = stringSyntax.fromMLstring name
- val result = ASSUME ``Eval env (Var ^str) (^inv ^tm)``
+ val result = ASSUME (mk_comb(``Eval env (Var ^str)``,mk_comb(inv,tm)))
in check_inv "var" tm result end else
(* constants *)
if numSyntax.is_numeral tm then SPEC tm Eval_Val_NUM else
if (tm = T) orelse (tm = F) then SPEC tm Eval_Val_BOOL else
- if is_const tm andalso can lookup_cert tm then let
+ if (* is_const tm andalso *) can lookup_cert tm then let
val th = lookup_cert tm
val res = th |> UNDISCH_ALL |> concl |> rand
val inv = get_type_inv (type_of tm)
@@ -718,6 +792,13 @@ fun hol2deep tm =
val th1 = hol2deep x1
val result = MATCH_MP Eval_Bool_Not th1
in check_inv "not" tm result end else
+ (* equality *)
+ if is_eq tm then let
+ val (x1,x2) = dest_eq tm
+ val th1 = hol2deep x1
+ val th2 = hol2deep x2
+ val result = MATCH_MP Eval_Equality (CONJ th1 th2) |> UNDISCH
+ in check_inv "equal" tm result end else
(* if statements *)
if is_cond tm then let
val (x1,x2,x3) = dest_cond tm
@@ -777,8 +858,9 @@ fun translate def = let
val fname = repeat rator lhs |> dest_const |> fst
val fname_str = stringLib.fromMLstring fname
val th = foldr (fn (v,th) => apply_Eval_Fun v th true) th (rev (butlast rev_params))
- val th = if is_rec then apply_Eval_Recclosure fname (last rev_params) th
- else apply_Eval_Fun (last rev_params) th true
+ val v = last rev_params
+ val th = if is_rec then apply_Eval_Recclosure fname v th
+ else apply_Eval_Fun v th true
|> MATCH_MP Eval_Eq_Fun
|> Q.INST [`env`|->`cl_env`] |> Q.SPEC `env` |> UNDISCH_ALL
|> Q.INST [`name`|->`^fname_str`]
@@ -815,6 +897,8 @@ fun translate def = let
val code_abbrev = new_definition(code_name ^ "_def",
mk_eq(mk_var(code_name,type_of code_tm),code_tm))
val th = REWRITE_RULE [GSYM code_abbrev] th |> UNDISCH_ALL
+ (* simpliy EqualityType *)
+ val th = SIMP_EqualityType_ASSUMS th
(* store certificate for later use *)
val _ = store_cert (repeat rator lhs) th
in th end
View
95 examples/miniML/ml_translatorScript.sml
@@ -34,8 +34,11 @@ val Fix_def = Define `
Fix (abs:'a->v->bool) x =
(\y v. (x = y) /\ abs y v)`;
-val Eq_def = Define `
- Eq x (v:v) = (v = x)`;
+val NUM_def = Define `
+ NUM n = \v. (v = Lit (Num n))`;
+
+val BOOL_def = Define `
+ BOOL b = \v. (v = Lit (Bool b))`;
val CONTAINER_def = Define `CONTAINER x = x`;
@@ -81,12 +84,6 @@ val Eval_Let = store_thm("Eval_Let",
\\ RES_TAC \\ Q.EXISTS_TAC `res''` \\ FULL_SIMP_TAC std_ss [LET_DEF,bind_def]
\\ Q.EXISTS_TAC `res'` \\ FULL_SIMP_TAC std_ss []);
-val NUM_def = Define `
- NUM n = \v. (v = Lit (Num n))`;
-
-val BOOL_def = Define `
- BOOL b = \v. (v = Lit (Bool b))`;
-
val Eval_Val = store_thm("Eval_Val",
``!x. Eval env (Val x) (\v. v = x)``,
SIMP_TAC (srw_ss()) [Once evaluate_cases,Eval_def]);
@@ -174,27 +171,13 @@ val Eval_If = store_thm("Eval_If",
val Eval_Bool_Not = store_thm("Eval_Bool_Not",
``Eval env x1 (BOOL b1) ==>
- Eval env (If x1 (Val (Lit (Bool F))) (Val (Lit (Bool T)))) (BOOL (~b1))``,
+ Eval env (App Equality x1 (Val (Lit (Bool F)))) (BOOL (~b1))``,
SIMP_TAC std_ss [Eval_def,NUM_def,BOOL_def] \\ SIMP_TAC std_ss []
\\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
\\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []
- \\ Q.EXISTS_TAC `(Lit (Bool b1))` \\ Cases_on `b1`
- \\ FULL_SIMP_TAC (srw_ss()) [do_if_def]
- \\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []);
-
-val Eval_Bool_Equal = store_thm("Eval_Bool_Equal",
- ``Eval env x1 (BOOL b1) ==>
- Eval env x2 (BOOL b2) ==>
- Eval env (If x1 x2 (If x2 (Val (Lit (Bool F))) (Val (Lit (Bool T)))))
- (BOOL (b1 = b2))``,
- SIMP_TAC std_ss [Eval_def,NUM_def,BOOL_def] \\ SIMP_TAC std_ss []
- \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
- \\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []
- \\ Q.EXISTS_TAC `(Lit (Bool b1))` \\ Cases_on `b1`
- \\ FULL_SIMP_TAC (srw_ss()) [do_if_def]
- \\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []
- \\ Q.EXISTS_TAC `(Lit (Bool b2))` \\ Cases_on `b2`
- \\ FULL_SIMP_TAC (srw_ss()) [do_if_def]
+ \\ Q.EXISTS_TAC `(Lit (Bool b1))`
+ \\ Q.EXISTS_TAC `(Lit (Bool F))`
+ \\ FULL_SIMP_TAC (srw_ss()) [do_app_def]
\\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []);
val Eval_Implies = store_thm("Eval_Implies",
@@ -274,9 +257,9 @@ val FUN_QUANT_SIMP = save_thm("FUN_QUANT_SIMP",
val Eval_Recclosure = store_thm("Eval_Recclosure",
``(!v. a n v ==>
Eval ((name,v)::(fname,Recclosure env2 [(fname,name,body)] fname)::env2) body (b (f n))) ==>
- Eval env (Var fname) (Eq (Recclosure env2 [(fname,name,body)] fname)) ==>
+ Eval env (Var fname) ($= (Recclosure env2 [(fname,name,body)] fname)) ==>
Eval env (Var fname) ((Fix a n --> b) f)``,
- FULL_SIMP_TAC std_ss [Eval_def,Arrow_def,Eq_def] \\ REPEAT STRIP_TAC
+ FULL_SIMP_TAC std_ss [Eval_def,Arrow_def] \\ REPEAT STRIP_TAC
\\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [evaluate_cases]
\\ FULL_SIMP_TAC (srw_ss()) [AppReturns_def,Fix_def,
do_app_def,evaluate_closure_def]
@@ -286,28 +269,74 @@ val Eval_Recclosure = store_thm("Eval_Recclosure",
val SafeVar_def = Define `SafeVar = Var`;
val Eval_Eq_Recclosure = store_thm("Eval_Eq_Recclosure",
- ``Eval env (Var name) (Eq (Recclosure x1 x2 x3)) ==>
+ ``Eval env (Var name) ($= (Recclosure x1 x2 x3)) ==>
(P f (Recclosure x1 x2 x3) =
Eval env (Var name) (P f))``,
- SIMP_TAC std_ss [Eval_Var_SIMP,Eval_def,Eq_def]
+ SIMP_TAC std_ss [Eval_Var_SIMP,Eval_def]
\\ SIMP_TAC (srw_ss()) [Once evaluate_cases]
\\ SIMP_TAC (srw_ss()) [Once evaluate_cases]);
val Eval_Eq_Fun = store_thm("Eval_Eq_Fun",
``Eval env (Fun v x) p ==>
- !env2. Eval env2 (Var name) (Eq (Closure env v x)) ==>
+ !env2. Eval env2 (Var name) ($= (Closure env v x)) ==>
Eval env2 (Var name) p``,
- SIMP_TAC std_ss [Eval_Var_SIMP,Eval_def,Eq_def]
+ SIMP_TAC std_ss [Eval_Var_SIMP,Eval_def]
\\ SIMP_TAC (srw_ss()) [Once evaluate_cases]
\\ SIMP_TAC (srw_ss()) [Once evaluate_cases]
\\ SIMP_TAC (srw_ss()) [Once evaluate_cases]);
+val Eval_WEAKEN = store_thm("Eval_WEAKEN",
+ ``Eval env exp P ==> (!v. P v ==> Q v) ==> Eval env exp Q``,
+ SIMP_TAC std_ss [Eval_def] \\ METIS_TAC []);
+
+
+(* Equality *)
+
+val no_closures_def = tDefine "no_closures" `
+ (no_closures (Lit l) = T) /\
+ (no_closures (Conv name vs) = EVERY no_closures vs) /\
+ (no_closures _ = F)`
+ (WF_REL_TAC `measure v_size` \\ REPEAT STRIP_TAC
+ \\ Induct_on `vs` \\ FULL_SIMP_TAC (srw_ss()) [MEM]
+ \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [MEM,exp_size_def]
+ \\ DECIDE_TAC)
+
+val EqualityType_def = Define `
+ EqualityType (abs:'a->v->bool) =
+ (!x1 v1. abs x1 v1 ==> no_closures v1) /\
+ !x1 v1 x2 v2.
+ abs x1 v1 /\ abs x2 v2 ==> ((v1 = v2) = (x1 = x2))`;
+
+val Eq_def = Define `
+ ((Eq abs):'a->v->bool) = \a v. EqualityType abs /\ abs a v`;
+
+val EqualityType_Eq = store_thm("EqualityType_Eq",
+ ``!a. EqualityType (Eq a)``,
+ SIMP_TAC std_ss [Eq_def,EqualityType_def] \\ METIS_TAC []);
+
+val EqualityType_NUM_BOOL = store_thm("EqualityType_NUM_BOOL",
+ ``EqualityType NUM /\ EqualityType BOOL``,
+ EVAL_TAC \\ FULL_SIMP_TAC (srw_ss()) [no_closures_def]);
+
+val Eval_Equality = store_thm("Eval_Equality",
+ ``Eval env x1 (a y1) /\ Eval env x2 (a y2) ==>
+ EqualityType a ==>
+ Eval env (App Equality x1 x2) (BOOL (y1 = y2))``,
+ SIMP_TAC std_ss [Eval_def,BOOL_def] \\ SIMP_TAC std_ss []
+ \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
+ \\ ONCE_REWRITE_TAC [evaluate_cases] \\ SIMP_TAC (srw_ss()) []
+ \\ Q.LIST_EXISTS_TAC [`res`,`res'`]
+ \\ FULL_SIMP_TAC (srw_ss()) [do_app_def]
+ \\ ONCE_REWRITE_TAC [evaluate_cases]
+ \\ FULL_SIMP_TAC (srw_ss()) [EqualityType_def]);
+
(* a few misc. lemmas that help the automation *)
val PULL_EXISTS = save_thm("PULL_EXISTS",
METIS_PROVE [] ``(((?x. P x) ==> Q) = !x. P x ==> Q) /\
- (((?x. P x) /\ Q) = ?x. P x /\ Q)``);
+ (((?x. P x) /\ Q) = ?x. P x /\ Q) /\
+ ((Q /\ (?x. P x)) = ?x. Q /\ P x)``);
val evaluate_list_SIMP = store_thm("evaluate_list_SIMP",
``(evaluate_list' env [] (Rval []) = T) /\
View
89 examples/miniML/ml_translator_demoScript.sml
@@ -1,9 +1,11 @@
open HolKernel Parse boolLib bossLib; val _ = new_theory "ml_translator_demo";
-open ml_translatorLib;
+open ml_translatorLib ml_translatorTheory;
open arithmeticTheory listTheory combinTheory pairTheory;
+open stringTheory;
+infix \\ val op \\ = op THEN;
(* ************************************************************************** *
@@ -12,14 +14,6 @@ open arithmeticTheory listTheory combinTheory pairTheory;
Partial definitions, e.g. HD, TL and ZIP, cannot be translated.
- MiniML only allows equality tests over num and bool, e.g. this
- means that functions such as MEM can only be translated for
- specific types, num and bool. Should equality types be implemented
- in MiniML?
-
- Shuold words and string, i.e. lists of characters, be supported by
- default?
-
* ************************************************************************** *)
@@ -55,9 +49,9 @@ val res = translate I_DEF;
val res = translate FAIL_DEF;
val res = translate PAD_RIGHT;
val res = translate PAD_LEFT;
-val res = translate (MEM |> INST_TYPE [alpha|->``:num``]);
-val res = translate (ALL_DISTINCT |> INST_TYPE [alpha|->``:num``]);
-val res = translate (isPREFIX |> INST_TYPE [alpha|->``:num``]);
+val res = translate MEM;
+val res = translate ALL_DISTINCT;
+val res = translate isPREFIX;
(* some locally defined examples *)
@@ -95,21 +89,70 @@ val (def,res) = mlDefine `
(silly (x,INR y) = x + y:num)`;
val (def,res) = mlDefine `
- (ODDS [] = []) /\
- (ODDS [x] = [x]) /\
- (ODDS (x::y::xs) = x :: ODDS xs)`;
+ (list_test1 [] = []) /\
+ (list_test1 [x] = [x]) /\
+ (list_test1 (x::y::xs) = x :: list_test1 xs)`;
+
+val (def,res) = mlDefine `
+ (list_test2 [] ys = []) /\
+ (list_test2 [x] ys = [(x,x)]) /\
+ (list_test2 (x::y::xs) (z1::z2::ys) = (x,z1) :: list_test2 xs ys) /\
+ (list_test2 _ _ = [])`;
val (def,res) = mlDefine `
- (EVENS [] ys = []) /\
- (EVENS [x] ys = [x]) /\
- (EVENS (x::y::xs) (z1::z2::ys) = x :: EVENS xs ys) /\
- (EVENS _ _ = [])`;
+ (list_test3 [] ys = 0) /\
+ (list_test3 (1::xs) ys = 1) /\
+ (list_test3 (2::xs) ys = 2 + list_test3 xs ys) /\
+ (list_test3 _ ys = LENGTH ys)`;
+
+
+(* chars, finite_maps, sets and lazy lists... *)
+
+(* teaching the translator about characters (represented as num) *)
+
+val CHAR_def = Define `
+ CHAR (c:char) = NUM (ORD c)`;
+
+val _ = add_type_inv ``CHAR``
+
+val EqualityType_CHAR = prove(
+ ``EqualityType CHAR``,
+ EVAL_TAC \\ SRW_TAC [] [] \\ EVAL_TAC)
+ |> store_eq_thm;
+
+val Eval_Val_CHAR = prove(
+ ``n < 256 ==> Eval env (Val (Lit (Num n))) (CHAR (CHR n))``,
+ SIMP_TAC (srw_ss()) [Eval_Val_NUM,CHAR_def])
+ |> store_eval_thm;
+
+val Eval_ORD = prove(
+ ``!v. ((NUM --> NUM) (\x.x)) v ==> ((CHAR --> NUM) ORD) v``,
+ SIMP_TAC std_ss [Arrow_def,AppReturns_def,CHAR_def])
+ |> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x:num``))
+ |> store_eval_thm;
+
+val Eval_CHR = prove(
+ ``!v. ((NUM --> NUM) (\n. n MOD 256)) v ==>
+ ((NUM --> CHAR) (\n. CHR (n MOD 256))) v``,
+ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,CHAR_def])
+ |> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\n. n MOD 256``))
+ |> store_eval_thm;
+
+val Eval_CHAR_LT = prove(
+ ``!v. ((NUM --> NUM --> BOOL) (\m n. m < n)) v ==>
+ ((CHAR --> CHAR --> BOOL) char_lt) v``,
+ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,CHAR_def,char_lt_def]
+ \\ METIS_TAC [])
+ |> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\m n. m < n:num``))
+ |> store_eval_thm;
+
+(* now we can translate e.g. less-than over strings *)
+
+val res = translate string_lt_def
val (def,res) = mlDefine `
- (LIT_TEST [] ys = 0) /\
- (LIT_TEST (1::xs) ys = 1) /\
- (LIT_TEST (2::xs) ys = 2 + LIT_TEST xs ys) /\
- (LIT_TEST _ ys = LENGTH ys)`;
+ hi n = if n = 0 then "!" else "hello " ++ hi (n-1)`
+
val _ = export_theory();
Please sign in to comment.
Something went wrong with that request. Please try again.