From deeb9050ff8996e724d4616ea977fa8d4e165be0 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 21 Aug 2023 09:55:03 +0200 Subject: [PATCH 01/15] Define from/to functions for basic library types --- .../cv_compute/automation/cv_typesScript.sml | 186 ++++++++++++++++++ 1 file changed, 186 insertions(+) create mode 100644 src/num/theories/cv_compute/automation/cv_typesScript.sml diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml new file mode 100644 index 0000000000..a8a691c222 --- /dev/null +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -0,0 +1,186 @@ +open HolKernel Parse boolLib bossLib cvTheory; +open integerTheory wordsTheory; + +val _ = new_theory "cv_types"; + +val _ = set_grammar_ancestry ["cv", "one", "option", "list", "sum", "pair", "words"]; + +Overload c2n[local] = “cv$c2n” +Overload c2b[local] = “cv$c2b” +Overload Num[local] = “cv$Num” +Overload Pair[local] = “cv$Pair” + +(* every from/to function must satisfy: *) + +Definition from_to_def: + from_to (f:'a -> cv) (t:cv -> 'a) = !x. t (f x) = x +End + +(* unit *) + +Definition from_unit_def: + from_unit (u:unit) = (Num 0):cv +End + +Definition to_unit_def: + to_unit (x:cv) = () +End + +Theorem from_to_unit: + from_to from_unit to_unit +Proof + fs [from_to_def] +QED + +(* bool *) + +Theorem from_to_bool: + from_to b2c c2b +Proof + fs [from_to_def] \\ Cases \\ fs [b2c_def] +QED + +(* num *) + +Theorem from_to_num: + from_to Num c2n +Proof + fs [from_to_def] +QED + +(* char *) + +Definition from_char_def: + from_char (c:char) = Num (ORD c) +End + +Definition to_char_def: + to_char x = CHR (c2n x) +End + +Theorem from_to_char: + from_to from_char to_char +Proof + fs [from_to_def] \\ Cases \\ fs [from_char_def,to_char_def] +QED + +(* int *) + +Definition from_int_def: + from_int (i:int) = + if integer$int_lt i (integer$int_of_num 0) then + Pair (Num (integer$Num i)) (Num 0) + else Num (integer$Num i) +End + +Definition to_int_def: + to_int (Num n) = integer$int_of_num n /\ + to_int (Pair x y) = integer$int_neg (integer$int_of_num (c2n x)) +End + +Theorem from_to_int: + from_to from_int to_int +Proof + fs [from_to_def] \\ Cases \\ fs [from_int_def,to_int_def] +QED + +(* word *) + +Definition from_word_def: + from_word (w:'a words$word) = Num (words$w2n w) +End + +Definition to_word_def: + to_word n = words$n2w (c2n n) :'a words$word +End + +Theorem from_to_word: + from_to from_word to_word +Proof + fs [from_to_def] \\ Cases \\ fs [from_word_def,to_word_def] +QED + +(* option *) + +Definition from_option_def: + from_option f NONE = Num 0 /\ + from_option f (SOME x) = + case f x of + | Num n => Num (n+1) + | other => other +End + +Definition to_option_def: + to_option t (Num n) = (if n = 0 then NONE else SOME (t (Num (n - 1)))) /\ + to_option t other = SOME (t other) +End + +Theorem from_to_option: + from_to f t ==> + from_to (from_option f) (to_option t) +Proof + fs [from_to_def] \\ strip_tac + \\ Cases \\ fs [from_option_def] + \\ Cases_on ‘f x'’ \\ fs [to_option_def] + \\ pop_assum $ assume_tac o GSYM \\ fs [] +QED + +(* pair *) + +Definition from_prod_def: + from_prod f1 f2 (x,y) = Pair (f1 x) (f2 y) +End + +Definition to_prod_def: + to_prod t1 t2 (Pair x y) = (t1 x, t2 y) +End + +Theorem from_to_prod: + from_to f1 t1 /\ from_to f2 t2 ==> + from_to (from_prod f1 f2) (to_prod t1 t2) +Proof + fs [from_to_def] \\ strip_tac + \\ Cases \\ fs [from_prod_def,to_prod_def] +QED + +(* sum *) + +Definition from_sum_def: + from_sum f1 f2 (INL x) = Pair (Num 0) (f1 x) /\ + from_sum f1 f2 (INR y) = Pair (Num 1) (f2 y) +End + +Definition to_sum_def: + to_sum t1 t2 (Pair x y) = + if x = Num 0 then INL (t1 y) else INR (t2 y) +End + +Theorem from_to_sum: + from_to f1 t1 /\ from_to f2 t2 ==> + from_to (from_sum f1 f2) (to_sum t1 t2) +Proof + fs [from_to_def] \\ strip_tac + \\ Cases \\ fs [from_sum_def,to_sum_def] +QED + +(* list *) + +Definition from_list_def: + from_list f [] = Num 0 /\ + from_list f (x::xs) = Pair (f x) (from_list f xs) +End + +Definition to_list_def: + to_list f (Num n) = [] /\ + to_list f (Pair x y) = f x :: to_list f y +End + +Theorem from_to_list: + from_to f t ==> + from_to (from_list f) (to_list t) +Proof + fs [from_to_def] \\ strip_tac + \\ Induct \\ fs [from_list_def,to_list_def] +QED + +val _ = export_theory(); From 81a000674a4c305c52a993ef2070e293c5e28e13 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 08:57:36 +0200 Subject: [PATCH 02/15] First sketch of automation --- .../cv_compute/automation/cv_typesScript.sml | 500 +++++++++++++++++- 1 file changed, 483 insertions(+), 17 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index a8a691c222..e94d2e1393 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -104,15 +104,12 @@ QED Definition from_option_def: from_option f NONE = Num 0 /\ - from_option f (SOME x) = - case f x of - | Num n => Num (n+1) - | other => other + from_option f (SOME x) = Pair (Num 1) (f x) End Definition to_option_def: - to_option t (Num n) = (if n = 0 then NONE else SOME (t (Num (n - 1)))) /\ - to_option t other = SOME (t other) + to_option t (Num n) = NONE /\ + to_option t (Pair x y) = if x = Num 1 then SOME (t y) else NONE End Theorem from_to_option: @@ -120,27 +117,26 @@ Theorem from_to_option: from_to (from_option f) (to_option t) Proof fs [from_to_def] \\ strip_tac - \\ Cases \\ fs [from_option_def] - \\ Cases_on ‘f x'’ \\ fs [to_option_def] - \\ pop_assum $ assume_tac o GSYM \\ fs [] + \\ Cases \\ fs [from_option_def,to_option_def] QED (* pair *) -Definition from_prod_def: - from_prod f1 f2 (x,y) = Pair (f1 x) (f2 y) +Definition from_pair_def: + from_pair f1 f2 (x,y) = Pair (f1 x) (f2 y) End -Definition to_prod_def: - to_prod t1 t2 (Pair x y) = (t1 x, t2 y) +Definition to_pair_def: + to_pair t1 t2 (Pair x y) = (t1 x, t2 y) /\ + to_pair t1 t2 _ = ARB End -Theorem from_to_prod: +Theorem from_to_pair: from_to f1 t1 /\ from_to f2 t2 ==> - from_to (from_prod f1 f2) (to_prod t1 t2) + from_to (from_pair f1 f2) (to_pair t1 t2) Proof fs [from_to_def] \\ strip_tac - \\ Cases \\ fs [from_prod_def,to_prod_def] + \\ Cases \\ fs [from_pair_def,to_pair_def] QED (* sum *) @@ -151,8 +147,10 @@ Definition from_sum_def: End Definition to_sum_def: + to_sum t1 t2 (Num n) = ARB /\ to_sum t1 t2 (Pair x y) = - if x = Num 0 then INL (t1 y) else INR (t2 y) + if x = Num 0 then INL (t1 y) else + if x = Num 1 then INR (t2 y) else ARB End Theorem from_to_sum: @@ -183,4 +181,472 @@ Proof \\ Induct \\ fs [from_list_def,to_list_def] QED +(* used in definitions of to-functions of user-defined datatype *) + +Definition cv_has_shape_def: + cv_has_shape (SOME n::xs) (Pair x y) = (x = Num n /\ cv_has_shape xs y) /\ + cv_has_shape (NONE::xs) (Pair x y) = cv_has_shape xs y /\ + cv_has_shape (_::xs) (Num _) = F /\ + cv_has_shape [] c = T +End + +Theorem cv_has_shape_expand: + cv_has_shape [] cv = T /\ + cv_has_shape (NONE::xs) cv = (?x y. cv = Pair x y /\ cv_has_shape xs y) /\ + cv_has_shape (SOME n::xs) cv = (?y. cv = Pair (Num n) y /\ cv_has_shape xs y) +Proof + Cases_on ‘cv’ \\ fs [cv_has_shape_def] +QED + +(* lemmas for automation *) + +Theorem get_to_pair: + (if cv_has_shape [NONE] v then (t1 (cv_fst v),t2 (cv_snd v)) else ARB) = + to_pair t1 t2 v +Proof + Cases_on ‘v’ + \\ fs [to_pair_def,cv_has_shape_def] +QED + +Theorem get_to_option: + (if cv_has_shape [SOME 1] v then SOME (t (cv_snd v)) else NONE) = to_option t v +Proof + Cases_on ‘v’ + \\ fs [to_option_def,cv_has_shape_def] +QED + +Theorem get_to_sum: + (if cv_has_shape [SOME 0] v then INL (t1 (cv_snd v)) + else if cv_has_shape [SOME 1] v then INR (t2 (cv_snd v)) + else ARB) = to_sum t1 t2 v +Proof + Cases_on ‘v’ + \\ fs [to_sum_def,cv_has_shape_def] +QED + +Theorem get_from_sum: + (case v of INL x => Pair (Num 0) (f0 x) | INR y => Pair (Num 1) (f1 y)) = + from_sum f0 f1 v +Proof + Cases_on ‘v’ \\ fs [from_sum_def] +QED + +Theorem get_from_option: + (case v of NONE => Num 0 | SOME x => Pair (Num 1) (f x)) = + from_option f v +Proof + Cases_on ‘v’ \\ fs [from_option_def] +QED + +Theorem get_from_pair: + (case v of (v0,v1) => Pair (f0 v0) (f1 v1)) = + from_pair f0 f1 v +Proof + Cases_on ‘v’ \\ fs [from_pair_def] +QED + +(* ------------- automation ---------------- *) + +val ERR = mk_HOL_ERR "cv_typesLib"; + +fun type_of_cases_const ty = let + val th = TypeBase.case_def_of ty + val ty = th |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL + |> concl |> dest_eq |> fst |> repeat rator |> type_of + in ty end + +fun auto_prove proof_name (goal,tac:tactic) = let + val (rest,validation) = tac ([],goal) + handle HOL_ERR r => raise (ERR "auto_prove" "tactic failure") + | Empty => raise (ERR "auto_prove" "tactic raised Empty") + in if length rest = 0 then validation [] else let + in failwith("auto_prove failed for " ^ proof_name) end end + +fun dest_fun_type ty = let + val (name,args) = dest_type ty + in if name = "fun" then (el 1 args, el 2 args) else failwith("not fun type") end; + +fun find_mutrec_types ty = let (* e.g. input ``:v`` gives [``:exp``,``:v``] *) + fun is_pair_ty ty = fst (dest_type ty) = "prod" + val xs = TypeBase.axiom_of ty + |> SPEC_ALL |> concl |> strip_exists + |> #1 |> map (#1 o dest_fun_type o type_of) + |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls) + in if is_pair_ty ty then [ty] else if length xs = 0 then [ty] else xs end + +fun matching_induction_of typ = let + val ind = TypeBase.induction_of typ + val ind_c = concl ind |> strip_forall |> snd |> dest_imp |> snd + val var_tys = strip_conj ind_c |> map (type_of o fst o dest_forall) + val matches = mapfilter (fn vty => match_type vty typ) var_tys + in case matches of + [] => failwith ("matching_induction_of: " ^ type_to_string typ) + | _ => INST_TYPE (hd matches) ind + end + +fun mk_funtype arg_tys ret_ty = + if null arg_tys then ret_ty else + mk_funtype (butlast arg_tys) (mk_type("fun",[last arg_tys,ret_ty])); + +fun make_stem fname args ret_ty = let + val f_ty = mk_funtype (map type_of args) ret_ty + in list_mk_comb(mk_var(fname,f_ty),args) end + +fun alookup x [] = NONE + | alookup x ((y,z)::xs) = if x = y then SOME z else alookup x xs; + +fun dest_fun_types ty = + let + val (x,y) = dest_fun_type ty + val (xs,z) = dest_fun_types y + in + (x::xs,z) + end handle HOL_ERR _ => ([],ty); + +local + val sum_case = sumTheory.sum_case_def + |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator + val tys = dest_fun_types (type_of sum_case) |> fst + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(sum_case,pat_args) + val thm = REFL pat |> GENL pat_args +in + fun mk_sum_case x y z = ISPECL [x,y,z] thm |> concl |> rand +end + +fun mk_sum_type l_ty r_ty = + mk_thy_type {Args = [l_ty, r_ty], Thy = "sum", Tyop = "sum"}; + +fun mk_pairs [] = cvSyntax.mk_cv_num(numSyntax.term_of_int 0) + | mk_pairs [x] = x + | mk_pairs (x::xs) = cvSyntax.mk_cv_pair(x, mk_pairs xs); + +fun constructors_of ty = let + val conses = TypeBase.constructors_of ty + fun match_ret_type c = + inst (match_type (repeat (snd o dest_fun_type) (type_of c)) ty) c + in map match_ret_type conses end + +fun from_to_for ty = + if ty = “:unit” then from_to_unit else + if ty = “:bool” then from_to_bool else + if ty = “:num” then from_to_num else + if ty = “:int” then from_to_int else + if listSyntax.is_list_type ty then + let val a = from_to_for (listSyntax.dest_list_type ty) + in MATCH_MP from_to_list a end + else fail() + +fun from_for ty = from_to_for ty |> concl |> rator |> rand; +fun to_for ty = from_to_for ty |> concl |> rand; + +val num_ty = arithmeticTheory.ODD_EVEN |> concl |> dest_forall |> fst |> type_of +val cv_has_shape_tm = + cv_has_shape_def |> CONJUNCT1 |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator; + +fun replicate 0 x = [] + | replicate n x = x :: replicate (n-1) x; + +(* +val ty = “:('d, 'c) b” +*) +fun define_from_to ty = let + (* extract target structure from induction theorem *) + val mutrec_count = length (find_mutrec_types ty) + val ind = TypeBase.induction_of ty + val inputs = ind |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCTS |> map (fst o dest_forall o concl) + val tyvars = dest_type (type_of (hd inputs)) |> snd + val first_name = inputs |> hd |> type_of |> dest_type |> fst + val names = inputs |> mapi (fn i => fn v => + if i < mutrec_count then + ((v |> type_of |> dest_type |> fst), type_of v) + else + (first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) + (* define encoding into cv type, i.e. "from function" *) + val tyvar_encoders = mapi (fn i => fn ty => + mk_var("f" ^ int_to_string i,mk_type("fun",[ty,cvSyntax.cv]))) tyvars + val from_names = names |> + map (fn (fname,ty) => + make_stem ("from_" ^ fname) tyvar_encoders (mk_funtype [ty] cvSyntax.cv)) + val lookups = + map (fn tm => (tm |> type_of |> dest_fun_type |> fst, tm)) (from_names @ tyvar_encoders) + (* + val from_f = el 4 from_names + *) + fun from_lines from_f = let + val conses = from_f |> type_of |> dest_type |> snd |> hd |> constructors_of + (* + val i = 0 + val cons_tm = el 2 conses + *) + fun from_line i cons_tm = let + val (tys,target_ty) = dest_fun_types (type_of cons_tm) + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(cons_tm,pat_args) + val lhs_tm = mk_comb(from_f,pat) + val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) + fun process_arg v = + case alookup (type_of v) lookups of + SOME tm => mk_comb(tm,v) + | NONE => mk_comb(from_for (type_of v),v) + val args = map process_arg pat_args + val smart_mk_pairs = + (if listSyntax.is_cons pat then mk_pairs o tl else + if pairSyntax.is_pair pat then mk_pairs o tl else + mk_pairs) + val rhs_tm = smart_mk_pairs (tag_num :: args) + in mk_eq(lhs_tm,rhs_tm) end + val lines = mapi from_line conses + in lines end + val all_lines = map from_lines from_names |> flatten + val tm = list_mk_conj all_lines + val from_def = Define [ANTIQUOTE tm] + (* define decoding from cv type, i.e. "to function" *) + val tyvar_decoders = mapi (fn i => fn ty => + mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars + val to_names = names |> + map (fn (fname,ty) => + make_stem ("to_" ^ fname) tyvar_decoders (mk_funtype [cvSyntax.cv] ty)) + val lookups = + map (fn tm => (tm |> type_of |> dest_fun_type |> snd, tm)) (to_names @ tyvar_decoders) + val cv_var = mk_var("v",cvSyntax.cv) + (* + val to_f = el 2 to_names + *) + fun to_lines to_f = let + val conses = to_f |> type_of |> dest_type |> snd |> el 2 |> constructors_of + val lhs_tm = mk_comb(to_f,cv_var) + (* + val i = 0 + val cons_tm = el 1 conses + *) + fun to_line i cons_tm = let + val (tys,_) = dest_fun_types (type_of cons_tm) + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(cons_tm,pat_args) + fun get_args v [] = [] + | get_args v [x] = [(x,v)] + | get_args v (x::xs) = + (x,cvSyntax.mk_cv_fst v) :: get_args (cvSyntax.mk_cv_snd v) xs + val special = (listSyntax.is_cons pat orelse pairSyntax.is_pair pat) + val init_var = (if special then cv_var else cvSyntax.mk_cv_snd cv_var) + val args = get_args init_var tys + fun process_arg (ty,v) = + case alookup ty lookups of + SOME tm => mk_comb(tm,v) + | NONE => mk_comb(to_for ty,v) + val xs = map process_arg args + fun lemmas_for_arg (ty,v) = + case alookup ty lookups of + SOME tm => [] + | NONE => [from_to_for ty] + val ys = map lemmas_for_arg args |> flatten + val build = list_mk_comb (cons_tm,xs) + val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) + val c2b = c2b_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator + val none_num = optionSyntax.mk_none(num_ty) + val test = if null tys then mk_eq(cv_var,tag_num) else + list_mk_comb(cv_has_shape_tm, + [listSyntax.mk_list( + (if special then [] else [optionSyntax.mk_some(tag_num |> rand)]) + @ replicate (length tys - 1) none_num, + type_of none_num), + cv_var]) + in (ys,(test,build)) end + val lemmas_lines = mapi to_line conses + val lemmas = map fst lemmas_lines |> flatten + val lines = map snd lemmas_lines + fun partition p [] = ([],[]) + | partition p (x::xs) = + let val (xs1,ys1) = partition p xs + in if p x then (x::xs1,ys1) else (xs1,x::ys1) end + val common_vars = cv_var :: tyvar_decoders + fun every p [] = true + | every p (x::xs) = (p x andalso every p xs) + fun exists p [] = false + | exists p (x::xs) = (p x orelse exists p xs) + fun subset xs ys = every (fn x => exists (aconv x) ys) xs + val (lines1,lines2) = + partition (fn (x,tm) => not (subset (free_vars tm) common_vars)) lines + val lines = lines1 @ lines2 + fun mk_rhs [] = fail() + | mk_rhs [(t,x)] = if null lines2 then mk_cond(t,x,mk_arb(type_of x)) else x + | mk_rhs ((t,x)::xs) = mk_cond(t,x,mk_rhs xs) + in (mk_eq(lhs_tm,mk_rhs lines),lemmas) end + val (all_lines,lemmas1) = unzip (map to_lines to_names) + val lemmas = lemmas1 |> flatten + val tm = list_mk_conj all_lines + val cv_size = + cv_size_def |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> rator + val args = pairSyntax.list_mk_pair (tyvar_decoders @ [cv_var]) + val size_tm = pairSyntax.mk_pabs(args, mk_comb(cv_size,cv_var)) + fun mk_measure_input_ty [] = type_of args + | mk_measure_input_ty [x] = type_of args + | mk_measure_input_ty (x::xs) = + mk_sum_type (type_of args) (mk_measure_input_ty xs) + val measure_ty = mk_measure_input_ty all_lines + val measure_var = mk_var("x",measure_ty) + fun mk_cases [] = fail() + | mk_cases [x] = size_tm + | mk_cases (x::xs) = + mk_abs (mk_var("x",mk_measure_input_ty (x::xs)), + (mk_sum_case + (mk_var("x",mk_measure_input_ty (x::xs))) + size_tm (mk_cases xs))) + val measure_tm = mk_cases all_lines + val full_measure_tm = ISPEC measure_tm prim_recTheory.WF_measure |> concl |> rand + val to_def_name = (to_names |> hd |> repeat rator |> dest_var |> fst) + val to_def = tDefine to_def_name [ANTIQUOTE tm] + (WF_REL_TAC [ANTIQUOTE full_measure_tm] + \\ rewrite_tac [cv_has_shape_expand] + \\ rpt strip_tac \\ gvs [cv_size_def]) + (* from from_to theorems *) + val assums = + map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) + (tyvar_encoders) (tyvar_decoders) + val assum = if null assums then T else list_mk_conj assums + fun term_all_distinct [] = [] + | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) + val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) + val from_cs = from_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) + |> term_all_distinct + val goals = + map2 (fn f => fn t => + let + val ty = f |> type_of |> dest_fun_type |> fst + val v = mk_var("v",ty) + in mk_abs(v,mk_eq(mk_comb(t,mk_comb(f,v)),v)) end) from_cs to_cs + val lemma = ISPECL goals ind |> CONV_RULE (DEPTH_CONV BETA_CONV) + val main_goal = lemma |> concl |> dest_imp |> snd + val the_goal = mk_imp(assum,main_goal) + (* + set_goal([],the_goal) + *) + val from_to_thm = auto_prove "from_to_thm" (the_goal, + strip_tac + \\ match_mp_tac lemma + \\ rpt conj_tac + \\ rpt gen_tac + \\ rpt disch_tac + \\ once_rewrite_tac [from_def] + \\ once_rewrite_tac [to_def] + \\ rewrite_tac [cv_has_shape_def,cv_fst_def,cv_snd_def] + \\ EVERY (map assume_tac lemmas) + \\ fs [from_to_def]) + val from_to_thms = + from_to_thm |> REWRITE_RULE [GSYM from_to_def] + |> UNDISCH_ALL |> CONJUNCTS + |> (fn xs => List.take(xs,mutrec_count)) + |> map DISCH_ALL + (* simplify from_def *) + val froms = from_def |> CONJUNCTS |> map SPEC_ALL + val pick = (rator o fst o dest_eq o concl) + val from_heads = froms |> map pick |> term_all_distinct + val from_eqs = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) + (List.drop(from_heads,mutrec_count)) + |> map (DefnBase.one_line_ify NONE) + fun simp_from_eq from_eq = let + val v = from_eq |> concl |> dest_eq |> fst |> rand + val tyname = v |> type_of |> dest_type |> fst + in if tyname = "prod" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_pair) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "option" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_option) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "sum" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_sum) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "list" then + let + val tm0 = from_eq |> concl |> dest_eq |> fst |> rator + val tm1 = from_eq |> concl |> rand |> rand |> dest_abs |> snd + |> dest_abs |> snd |> rator |> rand |> rator + val tm2 = from_list_def |> CONJUNCT1 |> ISPEC tm1 |> concl + |> dest_eq |> fst |> rator + val list_goal = mk_eq(tm0,tm2) + val res = auto_prove "simp_from_eq_list" + (list_goal, + rewrite_tac [FUN_EQ_THM] + \\ Induct + \\ once_rewrite_tac [from_list_def,from_eq] \\ fs []) + in res end + else failwith ("simp_from_eq can't do: " ^ tyname) end + val from_simps = map simp_from_eq from_eqs + val from_def = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) + (List.take(from_heads,mutrec_count)) + |> LIST_CONJ |> REWRITE_RULE from_simps + (* simplify to_def *) + val ts = to_def |> CONJUNCTS + val ts0 = List.take(ts,mutrec_count) + val ts1 = List.drop(ts,mutrec_count) |> map SPEC_ALL + (* + val to_eq = el 1 ts1 + *) + fun simp_one to_eq = let + val ty = to_eq |> concl |> dest_eq |> snd |> type_of + val tyname = dest_type ty |> fst + in if tyname = "option" then + to_eq |> REWRITE_RULE [get_to_option] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "sum" then + to_eq |> REWRITE_RULE [get_to_sum] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "prod" then + to_eq |> REWRITE_RULE [get_to_pair] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "list" then + let + val tm1 = to_eq |> concl |> dest_eq |> fst |> rator + val tm2 = to_eq |> concl |> dest_eq |> snd |> rator + |> rand |> rator |> rand |> rator + val tm3 = to_list_def |> CONJUNCT1 |> ISPEC tm2 |> SPEC_ALL + |> concl |> dest_eq |> fst |> rator + val list_goal = mk_eq(tm1,tm3) + val res = auto_prove "to_list_eq" + (list_goal, + rewrite_tac [FUN_EQ_THM] + \\ Induct + \\ once_rewrite_tac [to_eq] + \\ asm_rewrite_tac [to_list_def,cv_has_shape_def, + cv_fst_def,cv_snd_def]) + in res end + else failwith ("don't know: " ^ tyname) end + val to_simps = map simp_one ts1 + val to_def = ts0 |> map SPEC_ALL |> LIST_CONJ |> REWRITE_RULE to_simps + (* save all results *) + val th1 = save_thm("from_" ^ first_name ^ "_def[compute]", from_def) + val th2 = save_thm("to_" ^ first_name ^ "_def[compute]", to_def) + fun save_from_to_thms th = let + val to_name = th |> UNDISCH_ALL |> concl |> rand |> repeat rator |> dest_const |> fst + in save_thm("from_" ^ to_name ^ "_thm", th) end + val thms = List.map save_from_to_thms from_to_thms + in (from_def,to_def,from_to_thms) end + +(* tests *) + +Datatype: + a = A1 (num list) (((a # b) list) list) + | A2 ((a + b) list) ; + b = B1 + | B2 + | B3 (c option) ; + c = C1 + | C2 a 'aa 'bb +End + +val ty = “:('d, 'c) b” +val res = define_from_to ty + +Datatype: + tree = Leaf + | Branch ((tree list + tree) option list) +End + +val ty = “:tree” +val res = define_from_to ty + val _ = export_theory(); From cd477427b54c4d51978e9726514de24e96c837c3 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 13:06:47 +0200 Subject: [PATCH 03/15] Refine automation --- .../cv_compute/automation/cv_typesScript.sml | 58 ++++++++++++++----- 1 file changed, 43 insertions(+), 15 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index e94d2e1393..281653943a 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -311,6 +311,8 @@ local val pat = list_mk_comb(sum_case,pat_args) val thm = REFL pat |> GENL pat_args in + val sum_ty = hd tys + val is_sum_type = can (match_type sum_ty) fun mk_sum_case x y z = ISPECL [x,y,z] thm |> concl |> rand end @@ -347,6 +349,12 @@ val cv_has_shape_tm = fun replicate 0 x = [] | replicate n x = x :: replicate (n-1) x; +fun list_dest_comb tm = + if is_comb tm then + let val (f,xs) = list_dest_comb (rator tm) + in (f,xs @ [rand tm]) end + else (tm,[]); + (* val ty = “:('d, 'c) b” *) @@ -362,6 +370,17 @@ fun define_from_to ty = let ((v |> type_of |> dest_type |> fst), type_of v) else (first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) + fun should_be_headless pat = + (* should return true if pat has at least two variables and belongs + to a type where all other constructors take no arguments *) + let + val (cons_tm,args) = list_dest_comb pat + fun all_other_patterns_are_nil () = let + val cs = TypeBase.constructors_of (type_of pat) + val others = filter (fn t => not (can (match_term t) cons_tm)) cs + val non_nil = filter (fn t => can dest_fun_type (type_of t)) others + in null non_nil end + in 1 < length args andalso all_other_patterns_are_nil () end (* define encoding into cv type, i.e. "from function" *) val tyvar_encoders = mapi (fn i => fn ty => mk_var("f" ^ int_to_string i,mk_type("fun",[ty,cvSyntax.cv]))) tyvars @@ -390,17 +409,15 @@ fun define_from_to ty = let SOME tm => mk_comb(tm,v) | NONE => mk_comb(from_for (type_of v),v) val args = map process_arg pat_args - val smart_mk_pairs = - (if listSyntax.is_cons pat then mk_pairs o tl else - if pairSyntax.is_pair pat then mk_pairs o tl else - mk_pairs) + val special = should_be_headless pat + val smart_mk_pairs = (if special then mk_pairs o tl else mk_pairs) val rhs_tm = smart_mk_pairs (tag_num :: args) in mk_eq(lhs_tm,rhs_tm) end val lines = mapi from_line conses in lines end val all_lines = map from_lines from_names |> flatten val tm = list_mk_conj all_lines - val from_def = Define [ANTIQUOTE tm] + val from_def = zDefine [ANTIQUOTE tm] (* define decoding from cv type, i.e. "to function" *) val tyvar_decoders = mapi (fn i => fn ty => mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars @@ -414,7 +431,8 @@ fun define_from_to ty = let val to_f = el 2 to_names *) fun to_lines to_f = let - val conses = to_f |> type_of |> dest_type |> snd |> el 2 |> constructors_of + val cons_ty = to_f |> type_of |> dest_type |> snd |> el 2 + val conses = cons_ty |> constructors_of val lhs_tm = mk_comb(to_f,cv_var) (* val i = 0 @@ -428,7 +446,7 @@ fun define_from_to ty = let | get_args v [x] = [(x,v)] | get_args v (x::xs) = (x,cvSyntax.mk_cv_fst v) :: get_args (cvSyntax.mk_cv_snd v) xs - val special = (listSyntax.is_cons pat orelse pairSyntax.is_pair pat) + val special = should_be_headless pat val init_var = (if special then cv_var else cvSyntax.mk_cv_snd cv_var) val args = get_args init_var tys fun process_arg (ty,v) = @@ -469,8 +487,9 @@ fun define_from_to ty = let val (lines1,lines2) = partition (fn (x,tm) => not (subset (free_vars tm) common_vars)) lines val lines = lines1 @ lines2 + val needs_final_arb = (null lines2 orelse is_sum_type cons_ty) fun mk_rhs [] = fail() - | mk_rhs [(t,x)] = if null lines2 then mk_cond(t,x,mk_arb(type_of x)) else x + | mk_rhs [(t,x)] = if needs_final_arb then mk_cond(t,x,mk_arb(type_of x)) else x | mk_rhs ((t,x)::xs) = mk_cond(t,x,mk_rhs xs) in (mk_eq(lhs_tm,mk_rhs lines),lemmas) end val (all_lines,lemmas1) = unzip (map to_lines to_names) @@ -496,10 +515,14 @@ fun define_from_to ty = let val measure_tm = mk_cases all_lines val full_measure_tm = ISPEC measure_tm prim_recTheory.WF_measure |> concl |> rand val to_def_name = (to_names |> hd |> repeat rator |> dest_var |> fst) - val to_def = tDefine to_def_name [ANTIQUOTE tm] - (WF_REL_TAC [ANTIQUOTE full_measure_tm] - \\ rewrite_tac [cv_has_shape_expand] - \\ rpt strip_tac \\ gvs [cv_size_def]) + val (to_def, to_ind) = + let + val to_defn = Hol_defn to_def_name [ANTIQUOTE tm] + in Defn.tprove(to_defn, + WF_REL_TAC [ANTIQUOTE full_measure_tm] + \\ rewrite_tac [cv_has_shape_expand] + \\ rpt strip_tac \\ gvs [cv_size_def]) + end (* from from_to theorems *) val assums = map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) @@ -643,10 +666,15 @@ val res = define_from_to ty Datatype: tree = Leaf - | Branch ((tree list + tree) option list) + | Branch ((tree list + bool) option list) End -val ty = “:tree” -val res = define_from_to ty +val res = define_from_to “:tree” + +Datatype: + t1 = T1 num (t1 list) +End + +val res = define_from_to “:t1” val _ = export_theory(); From 5e3b58eeb831e9e70143746a56d9ba4564f569d7 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 13:33:14 +0200 Subject: [PATCH 04/15] Avoid t and f params for unused tyvars --- .../cv_compute/automation/cv_typesScript.sml | 43 ++++++++++++++++--- 1 file changed, 38 insertions(+), 5 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index 281653943a..3dc9ff32e3 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -334,10 +334,13 @@ fun from_to_for ty = if ty = “:bool” then from_to_bool else if ty = “:num” then from_to_num else if ty = “:int” then from_to_int else - if listSyntax.is_list_type ty then + if wordsSyntax.is_word_type ty then + let val ty = wordsSyntax.dest_word_type ty + in INST_TYPE [alpha|->ty] from_to_word end + else if listSyntax.is_list_type ty then let val a = from_to_for (listSyntax.dest_list_type ty) in MATCH_MP from_to_list a end - else fail() + else failwith ("from_to_for: " ^ type_to_string ty) fun from_for ty = from_to_for ty |> concl |> rator |> rand; fun to_for ty = from_to_for ty |> concl |> rand; @@ -355,15 +358,24 @@ fun list_dest_comb tm = in (f,xs @ [rand tm]) end else (tm,[]); +fun term_all_distinct [] = [] + | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) + +exception UnusedTypeVars of hol_type list; + (* +val ignore_tyvars = tl [alpha] +val ignore_tyvars = [alpha,gamma] +val ty = “:('a,'b,'c) word_tree” val ty = “:('d, 'c) b” *) -fun define_from_to ty = let +fun define_from_to_aux ignore_tyvars ty = let (* extract target structure from induction theorem *) val mutrec_count = length (find_mutrec_types ty) val ind = TypeBase.induction_of ty val inputs = ind |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCTS |> map (fst o dest_forall o concl) val tyvars = dest_type (type_of (hd inputs)) |> snd + |> filter (fn tyvar => not (mem tyvar ignore_tyvars)) val first_name = inputs |> hd |> type_of |> dest_type |> fst val names = inputs |> mapi (fn i => fn v => if i < mutrec_count then @@ -417,6 +429,14 @@ fun define_from_to ty = let in lines end val all_lines = map from_lines from_names |> flatten val tm = list_mk_conj all_lines + val _ = let (* check which tyvar encoders are actually used *) + val cs = map (rator o fst o dest_eq) all_lines |> term_all_distinct + val substs = map (fn c => c |-> mk_arb(type_of c)) cs + val fvs = free_vars (subst substs tm) + val unused = filter (fn f => not (exists (fn t => aconv t f) fvs)) tyvar_encoders + in if null ignore_tyvars andalso not (null unused) then + raise UnusedTypeVars (map (fst o dest_fun_type o type_of) unused) + else () end val from_def = zDefine [ANTIQUOTE tm] (* define decoding from cv type, i.e. "to function" *) val tyvar_decoders = mapi (fn i => fn ty => @@ -528,8 +548,6 @@ fun define_from_to ty = let map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) (tyvar_encoders) (tyvar_decoders) val assum = if null assums then T else list_mk_conj assums - fun term_all_distinct [] = [] - | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) val from_cs = from_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) |> term_all_distinct @@ -648,6 +666,9 @@ fun define_from_to ty = let in save_thm("from_" ^ to_name ^ "_thm", th) end val thms = List.map save_from_to_thms from_to_thms in (from_def,to_def,from_to_thms) end + handle UnusedTypeVars ignore_tyvars => define_from_to_aux ignore_tyvars ty; + +fun define_from_to ty = define_from_to_aux [] ty; (* tests *) @@ -677,4 +698,16 @@ End val res = define_from_to “:t1” +Datatype: + word_tree = + | Fork word_tree word_tree + | Word1 ('a word) + | Other 'b + | Word2 ('c word) +End + +val ty = “:('a,'b,'c) word_tree” +val res = define_from_to ty +val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() + val _ = export_theory(); From ad34f282a9808c975d06359c4bd98618d77323cb Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 13:38:33 +0200 Subject: [PATCH 05/15] Use long names for non-local types --- .../theories/cv_compute/automation/cv_typesScript.sml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index 3dc9ff32e3..33d03615ab 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -364,8 +364,8 @@ fun term_all_distinct [] = [] exception UnusedTypeVars of hol_type list; (* -val ignore_tyvars = tl [alpha] val ignore_tyvars = [alpha,gamma] +val ignore_tyvars = tl [alpha] val ty = “:('a,'b,'c) word_tree” val ty = “:('d, 'c) b” *) @@ -377,11 +377,13 @@ fun define_from_to_aux ignore_tyvars ty = let val tyvars = dest_type (type_of (hd inputs)) |> snd |> filter (fn tyvar => not (mem tyvar ignore_tyvars)) val first_name = inputs |> hd |> type_of |> dest_type |> fst + val thy_name = inputs |> hd |> type_of |> dest_thy_type |> #Thy + val name_prefix = (if thy_name <> current_theory() then thy_name ^ "_" else "") val names = inputs |> mapi (fn i => fn v => if i < mutrec_count then - ((v |> type_of |> dest_type |> fst), type_of v) + (name_prefix ^ (v |> type_of |> dest_type |> fst), type_of v) else - (first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) + (name_prefix ^ first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) fun should_be_headless pat = (* should return true if pat has at least two variables and belongs to a type where all other constructors take no arguments *) @@ -710,4 +712,7 @@ val ty = “:('a,'b,'c) word_tree” val res = define_from_to ty val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() +open sptreeTheory +val res = define_from_to “:'a spt” + val _ = export_theory(); From 59b4477a52168d8a75a0f2f0afe083e95b6ec463 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 14:42:53 +0200 Subject: [PATCH 06/15] Support more basic types --- .../cv_compute/automation/cv_typesScript.sml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index 33d03615ab..f311e1ca39 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -1,5 +1,5 @@ open HolKernel Parse boolLib bossLib cvTheory; -open integerTheory wordsTheory; +open integerTheory wordsTheory sptreeTheory; val _ = new_theory "cv_types"; @@ -333,10 +333,24 @@ fun from_to_for ty = if ty = “:unit” then from_to_unit else if ty = “:bool” then from_to_bool else if ty = “:num” then from_to_num else + if ty = “:char” then from_to_char else if ty = “:int” then from_to_int else if wordsSyntax.is_word_type ty then let val ty = wordsSyntax.dest_word_type ty in INST_TYPE [alpha|->ty] from_to_word end + else if can pairSyntax.dest_prod ty then let + val (a,b) = pairSyntax.dest_prod ty + val a = from_to_for a + val b = from_to_for b + in MATCH_MP from_to_pair (CONJ a b) end + else if can sumSyntax.dest_sum ty then let + val (a,b) = sumSyntax.dest_sum ty + val a = from_to_for a + val b = from_to_for b + in MATCH_MP from_to_sum (CONJ a b) end + else if can optionSyntax.dest_option ty then let + val a = from_to_for (optionSyntax.dest_option ty) + in MATCH_MP from_to_option a end else if listSyntax.is_list_type ty then let val a = from_to_for (listSyntax.dest_list_type ty) in MATCH_MP from_to_list a end @@ -712,7 +726,6 @@ val ty = “:('a,'b,'c) word_tree” val res = define_from_to ty val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() -open sptreeTheory -val res = define_from_to “:'a spt” +val res = define_from_to “:'a sptree$spt” val _ = export_theory(); From 27e564b971283f6118d1e22467516fe0797a9cbe Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 22 Aug 2023 16:14:24 +0200 Subject: [PATCH 07/15] Split from_to development into several files --- .../cv_compute/automation/cv_typesLib.sig | 14 + .../cv_compute/automation/cv_typesLib.sml | 482 +++++++++++++++++ .../cv_compute/automation/cv_typesScript.sml | 485 +----------------- .../automation/cv_types_demoScript.sml | 55 ++ 4 files changed, 552 insertions(+), 484 deletions(-) create mode 100644 src/num/theories/cv_compute/automation/cv_typesLib.sig create mode 100644 src/num/theories/cv_compute/automation/cv_typesLib.sml create mode 100644 src/num/theories/cv_compute/automation/cv_types_demoScript.sml diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sig b/src/num/theories/cv_compute/automation/cv_typesLib.sig new file mode 100644 index 0000000000..d9522613e0 --- /dev/null +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sig @@ -0,0 +1,14 @@ +signature cv_typesLib = +sig + include Abbrev + + (* manually add a from_to_theorem *) + val add_from_to_thm : thm -> unit + + (* returns a list of all from_to theorems *) + val from_to_thms : unit -> thm list + + (* automatically define new from/to functions for a user-defined datatype *) + val define_from_to : hol_type -> thm * thm * thm list + +end diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml new file mode 100644 index 0000000000..85b9ef0a8a --- /dev/null +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -0,0 +1,482 @@ +structure cv_typesLib :> cv_typesLib = +struct + +open HolKernel Parse boolLib bossLib cvTheory; +open integerTheory wordsTheory cv_typesTheory; + +(* --------------------------------------------------- * + Memory management + * --------------------------------------------------- *) + +(* Updates the set given a delta *) +fun apply_delta (ThmSetData.ADD(_, th)) thml = th :: thml + | apply_delta _ _ = failwith "unimplemented case of apply_delta" + +(* Defines/Setups the from_to theorem set *) +val {update_global_value = from_to_apply_global_update, + record_delta = from_to_record_delta, + get_deltas = from_to_get_deltas, + get_global_value = from_to_thm_list, + DB = eval_ruleuction_map_by_theory,...} = + ThmSetData.export_with_ancestry { + settype = "from_to", + delta_ops = {apply_to_global = apply_delta, (* How to update the set (globally) *) + uptodate_delta = K true, + thy_finaliser = NONE, + initial_value = [], (* The initial value of the set *) + apply_delta = apply_delta} + } + +(* Add a theorem to the from_to set *) +fun add_from_to_thm th = + from_to_apply_global_update (curry (op ::) th) + +(* Get a list of all the theorems in the from_to set *) +val from_to_thms = from_to_thm_list + +(* --------------------------------------------------- * + Preliminaries + * --------------------------------------------------- *) + +val ERR = mk_HOL_ERR "cv_typesLib"; + +fun auto_prove proof_name (goal,tac:tactic) = let + val (rest,validation) = tac ([],goal) + handle HOL_ERR r => raise (ERR "auto_prove" "tactic failure") + | Empty => raise (ERR "auto_prove" "tactic raised Empty") + in if length rest = 0 then validation [] else let + in failwith("auto_prove failed for " ^ proof_name) end end + +fun dest_fun_type ty = let + val (name,args) = dest_type ty + in if name = "fun" then (el 1 args, el 2 args) else failwith("not fun type") end; + +fun find_mutrec_types ty = let (* e.g. input ``:v`` gives [``:exp``,``:v``] *) + fun is_pair_ty ty = fst (dest_type ty) = "prod" + val xs = TypeBase.axiom_of ty + |> SPEC_ALL |> concl |> strip_exists + |> #1 |> map (#1 o dest_fun_type o type_of) + |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls) + in if is_pair_ty ty then [ty] else if length xs = 0 then [ty] else xs end + +fun matching_induction_of typ = let + val ind = TypeBase.induction_of typ + val ind_c = concl ind |> strip_forall |> snd |> dest_imp |> snd + val var_tys = strip_conj ind_c |> map (type_of o fst o dest_forall) + val matches = mapfilter (fn vty => match_type vty typ) var_tys + in case matches of + [] => failwith ("matching_induction_of: " ^ type_to_string typ) + | _ => INST_TYPE (hd matches) ind + end + +fun mk_funtype arg_tys ret_ty = + if null arg_tys then ret_ty else + mk_funtype (butlast arg_tys) (mk_type("fun",[last arg_tys,ret_ty])); + +fun make_stem fname args ret_ty = let + val f_ty = mk_funtype (map type_of args) ret_ty + in list_mk_comb(mk_var(fname,f_ty),args) end + +fun alookup x [] = NONE + | alookup x ((y,z)::xs) = if x = y then SOME z else alookup x xs; + +fun dest_fun_types ty = + let + val (x,y) = dest_fun_type ty + val (xs,z) = dest_fun_types y + in + (x::xs,z) + end handle HOL_ERR _ => ([],ty); + +local + val sum_case = sumTheory.sum_case_def + |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator + val tys = dest_fun_types (type_of sum_case) |> fst + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(sum_case,pat_args) + val thm = REFL pat |> GENL pat_args +in + val sum_ty = hd tys + val is_sum_type = can (match_type sum_ty) + fun mk_sum_case x y z = ISPECL [x,y,z] thm |> concl |> rand +end + +fun mk_sum_type l_ty r_ty = + mk_thy_type {Args = [l_ty, r_ty], Thy = "sum", Tyop = "sum"}; + +fun mk_pairs [] = cvSyntax.mk_cv_num(numSyntax.term_of_int 0) + | mk_pairs [x] = x + | mk_pairs (x::xs) = cvSyntax.mk_cv_pair(x, mk_pairs xs); + +fun constructors_of ty = let + val conses = TypeBase.constructors_of ty + fun match_ret_type c = + inst (match_type (repeat (snd o dest_fun_type) (type_of c)) ty) c + in map match_ret_type conses end + +val num_ty = arithmeticTheory.ODD_EVEN |> concl |> dest_forall |> fst |> type_of +val cv_has_shape_tm = + cv_has_shape_def |> CONJUNCT1 |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator; + +fun replicate 0 x = [] + | replicate n x = x :: replicate (n-1) x; + +fun list_dest_comb tm = + if is_comb tm then + let val (f,xs) = list_dest_comb (rator tm) + in (f,xs @ [rand tm]) end + else (tm,[]); + +fun term_all_distinct [] = [] + | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) + +(* --------------------------------------------------- * + Loading from_to theorems + * --------------------------------------------------- *) + +fun from_to_for ty = + if ty = “:unit” then from_to_unit else + if ty = “:bool” then from_to_bool else + if ty = “:num” then from_to_num else + if ty = “:char” then from_to_char else + if ty = “:int” then from_to_int else + if wordsSyntax.is_word_type ty then + let val ty = wordsSyntax.dest_word_type ty + in INST_TYPE [alpha|->ty] from_to_word end + else if can pairSyntax.dest_prod ty then let + val (a,b) = pairSyntax.dest_prod ty + val a = from_to_for a + val b = from_to_for b + in MATCH_MP from_to_pair (CONJ a b) end + else if can sumSyntax.dest_sum ty then let + val (a,b) = sumSyntax.dest_sum ty + val a = from_to_for a + val b = from_to_for b + in MATCH_MP from_to_sum (CONJ a b) end + else if can optionSyntax.dest_option ty then let + val a = from_to_for (optionSyntax.dest_option ty) + in MATCH_MP from_to_option a end + else if listSyntax.is_list_type ty then + let val a = from_to_for (listSyntax.dest_list_type ty) + in MATCH_MP from_to_list a end + else failwith ("from_to_for: " ^ type_to_string ty) + +fun from_for ty = from_to_for ty |> concl |> rator |> rand; +fun to_for ty = from_to_for ty |> concl |> rand; + +(* --------------------------------------------------- * + Defining new from/to functions for a datatype + * --------------------------------------------------- *) + +exception UnusedTypeVars of hol_type list; + +(* +val ignore_tyvars = [alpha,gamma] +val ignore_tyvars = tl [alpha] +val ty = “:('a,'b,'c) word_tree” +val ty = “:('d, 'c) b” +*) +fun define_from_to_aux ignore_tyvars ty = let + (* extract target structure from induction theorem *) + val mutrec_count = length (find_mutrec_types ty) + val ind = TypeBase.induction_of ty + val inputs = ind |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCTS |> map (fst o dest_forall o concl) + val tyvars = dest_type (type_of (hd inputs)) |> snd + |> filter (fn tyvar => not (mem tyvar ignore_tyvars)) + val first_name = inputs |> hd |> type_of |> dest_type |> fst + val thy_name = inputs |> hd |> type_of |> dest_thy_type |> #Thy + val name_prefix = (if thy_name <> current_theory() then thy_name ^ "_" else "") + val names = inputs |> mapi (fn i => fn v => + if i < mutrec_count then + (name_prefix ^ (v |> type_of |> dest_type |> fst), type_of v) + else + (name_prefix ^ first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) + fun should_be_headless pat = + (* should return true if pat has at least two variables and belongs + to a type where all other constructors take no arguments *) + let + val (cons_tm,args) = list_dest_comb pat + fun all_other_patterns_are_nil () = let + val cs = TypeBase.constructors_of (type_of pat) + val others = filter (fn t => not (can (match_term t) cons_tm)) cs + val non_nil = filter (fn t => can dest_fun_type (type_of t)) others + in null non_nil end + in 1 < length args andalso all_other_patterns_are_nil () end + (* define encoding into cv type, i.e. "from function" *) + val tyvar_encoders = mapi (fn i => fn ty => + mk_var("f" ^ int_to_string i,mk_type("fun",[ty,cvSyntax.cv]))) tyvars + val from_names = names |> + map (fn (fname,ty) => + make_stem ("from_" ^ fname) tyvar_encoders (mk_funtype [ty] cvSyntax.cv)) + val lookups = + map (fn tm => (tm |> type_of |> dest_fun_type |> fst, tm)) (from_names @ tyvar_encoders) + (* + val from_f = el 4 from_names + *) + fun from_lines from_f = let + val conses = from_f |> type_of |> dest_type |> snd |> hd |> constructors_of + (* + val i = 0 + val cons_tm = el 2 conses + *) + fun from_line i cons_tm = let + val (tys,target_ty) = dest_fun_types (type_of cons_tm) + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(cons_tm,pat_args) + val lhs_tm = mk_comb(from_f,pat) + val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) + fun process_arg v = + case alookup (type_of v) lookups of + SOME tm => mk_comb(tm,v) + | NONE => mk_comb(from_for (type_of v),v) + val args = map process_arg pat_args + val special = should_be_headless pat + val smart_mk_pairs = (if special then mk_pairs o tl else mk_pairs) + val rhs_tm = smart_mk_pairs (tag_num :: args) + in mk_eq(lhs_tm,rhs_tm) end + val lines = mapi from_line conses + in lines end + val all_lines = map from_lines from_names |> flatten + val tm = list_mk_conj all_lines + val _ = let (* check which tyvar encoders are actually used *) + val cs = map (rator o fst o dest_eq) all_lines |> term_all_distinct + val substs = map (fn c => c |-> mk_arb(type_of c)) cs + val fvs = free_vars (subst substs tm) + val unused = filter (fn f => not (exists (fn t => aconv t f) fvs)) tyvar_encoders + in if null ignore_tyvars andalso not (null unused) then + raise UnusedTypeVars (map (fst o dest_fun_type o type_of) unused) + else () end + val from_def = zDefine [ANTIQUOTE tm] + (* define decoding from cv type, i.e. "to function" *) + val tyvar_decoders = mapi (fn i => fn ty => + mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars + val to_names = names |> + map (fn (fname,ty) => + make_stem ("to_" ^ fname) tyvar_decoders (mk_funtype [cvSyntax.cv] ty)) + val lookups = + map (fn tm => (tm |> type_of |> dest_fun_type |> snd, tm)) (to_names @ tyvar_decoders) + val cv_var = mk_var("v",cvSyntax.cv) + (* + val to_f = el 2 to_names + *) + fun to_lines to_f = let + val cons_ty = to_f |> type_of |> dest_type |> snd |> el 2 + val conses = cons_ty |> constructors_of + val lhs_tm = mk_comb(to_f,cv_var) + (* + val i = 0 + val cons_tm = el 1 conses + *) + fun to_line i cons_tm = let + val (tys,_) = dest_fun_types (type_of cons_tm) + val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys + val pat = list_mk_comb(cons_tm,pat_args) + fun get_args v [] = [] + | get_args v [x] = [(x,v)] + | get_args v (x::xs) = + (x,cvSyntax.mk_cv_fst v) :: get_args (cvSyntax.mk_cv_snd v) xs + val special = should_be_headless pat + val init_var = (if special then cv_var else cvSyntax.mk_cv_snd cv_var) + val args = get_args init_var tys + fun process_arg (ty,v) = + case alookup ty lookups of + SOME tm => mk_comb(tm,v) + | NONE => mk_comb(to_for ty,v) + val xs = map process_arg args + fun lemmas_for_arg (ty,v) = + case alookup ty lookups of + SOME tm => [] + | NONE => [from_to_for ty] + val ys = map lemmas_for_arg args |> flatten + val build = list_mk_comb (cons_tm,xs) + val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) + val c2b = c2b_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator + val none_num = optionSyntax.mk_none(num_ty) + val test = if null tys then mk_eq(cv_var,tag_num) else + list_mk_comb(cv_has_shape_tm, + [listSyntax.mk_list( + (if special then [] else [optionSyntax.mk_some(tag_num |> rand)]) + @ replicate (length tys - 1) none_num, + type_of none_num), + cv_var]) + in (ys,(test,build)) end + val lemmas_lines = mapi to_line conses + val lemmas = map fst lemmas_lines |> flatten + val lines = map snd lemmas_lines + fun partition p [] = ([],[]) + | partition p (x::xs) = + let val (xs1,ys1) = partition p xs + in if p x then (x::xs1,ys1) else (xs1,x::ys1) end + val common_vars = cv_var :: tyvar_decoders + fun every p [] = true + | every p (x::xs) = (p x andalso every p xs) + fun exists p [] = false + | exists p (x::xs) = (p x orelse exists p xs) + fun subset xs ys = every (fn x => exists (aconv x) ys) xs + val (lines1,lines2) = + partition (fn (x,tm) => not (subset (free_vars tm) common_vars)) lines + val lines = lines1 @ lines2 + val needs_final_arb = (null lines2 orelse is_sum_type cons_ty) + fun mk_rhs [] = fail() + | mk_rhs [(t,x)] = if needs_final_arb then mk_cond(t,x,mk_arb(type_of x)) else x + | mk_rhs ((t,x)::xs) = mk_cond(t,x,mk_rhs xs) + in (mk_eq(lhs_tm,mk_rhs lines),lemmas) end + val (all_lines,lemmas1) = unzip (map to_lines to_names) + val lemmas = lemmas1 |> flatten + val tm = list_mk_conj all_lines + val cv_size = + cv_size_def |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> rator + val args = pairSyntax.list_mk_pair (tyvar_decoders @ [cv_var]) + val size_tm = pairSyntax.mk_pabs(args, mk_comb(cv_size,cv_var)) + fun mk_measure_input_ty [] = type_of args + | mk_measure_input_ty [x] = type_of args + | mk_measure_input_ty (x::xs) = + mk_sum_type (type_of args) (mk_measure_input_ty xs) + val measure_ty = mk_measure_input_ty all_lines + val measure_var = mk_var("x",measure_ty) + fun mk_cases [] = fail() + | mk_cases [x] = size_tm + | mk_cases (x::xs) = + mk_abs (mk_var("x",mk_measure_input_ty (x::xs)), + (mk_sum_case + (mk_var("x",mk_measure_input_ty (x::xs))) + size_tm (mk_cases xs))) + val measure_tm = mk_cases all_lines + val full_measure_tm = ISPEC measure_tm prim_recTheory.WF_measure |> concl |> rand + val to_def_name = (to_names |> hd |> repeat rator |> dest_var |> fst) + val (to_def, to_ind) = + let + val to_defn = Hol_defn to_def_name [ANTIQUOTE tm] + in Defn.tprove(to_defn, + WF_REL_TAC [ANTIQUOTE full_measure_tm] + \\ rewrite_tac [cv_has_shape_expand] + \\ rpt strip_tac \\ gvs [cv_size_def]) + end + (* from from_to theorems *) + val assums = + map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) + (tyvar_encoders) (tyvar_decoders) + val assum = if null assums then T else list_mk_conj assums + val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) + val from_cs = from_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) + |> term_all_distinct + val goals = + map2 (fn f => fn t => + let + val ty = f |> type_of |> dest_fun_type |> fst + val v = mk_var("v",ty) + in mk_abs(v,mk_eq(mk_comb(t,mk_comb(f,v)),v)) end) from_cs to_cs + val lemma = ISPECL goals ind |> CONV_RULE (DEPTH_CONV BETA_CONV) + val main_goal = lemma |> concl |> dest_imp |> snd + val the_goal = mk_imp(assum,main_goal) + (* + set_goal([],the_goal) + *) + val from_to_thm = auto_prove "from_to_thm" (the_goal, + strip_tac + \\ match_mp_tac lemma + \\ rpt conj_tac + \\ rpt gen_tac + \\ rpt disch_tac + \\ once_rewrite_tac [from_def] + \\ once_rewrite_tac [to_def] + \\ rewrite_tac [cv_has_shape_def,cv_fst_def,cv_snd_def] + \\ EVERY (map assume_tac lemmas) + \\ fs [from_to_def]) + val from_to_thms = + from_to_thm |> REWRITE_RULE [GSYM from_to_def] + |> UNDISCH_ALL |> CONJUNCTS + |> (fn xs => List.take(xs,mutrec_count)) + |> map DISCH_ALL + (* simplify from_def *) + val froms = from_def |> CONJUNCTS |> map SPEC_ALL + val pick = (rator o fst o dest_eq o concl) + val from_heads = froms |> map pick |> term_all_distinct + val from_eqs = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) + (List.drop(from_heads,mutrec_count)) + |> map (DefnBase.one_line_ify NONE) + fun simp_from_eq from_eq = let + val v = from_eq |> concl |> dest_eq |> fst |> rand + val tyname = v |> type_of |> dest_type |> fst + in if tyname = "prod" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_pair) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "option" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_option) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "sum" then + from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_sum) + |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] + else if tyname = "list" then + let + val tm0 = from_eq |> concl |> dest_eq |> fst |> rator + val tm1 = from_eq |> concl |> rand |> rand |> dest_abs |> snd + |> dest_abs |> snd |> rator |> rand |> rator + val tm2 = from_list_def |> CONJUNCT1 |> ISPEC tm1 |> concl + |> dest_eq |> fst |> rator + val list_goal = mk_eq(tm0,tm2) + val res = auto_prove "simp_from_eq_list" + (list_goal, + rewrite_tac [FUN_EQ_THM] + \\ Induct + \\ once_rewrite_tac [from_list_def,from_eq] \\ fs []) + in res end + else failwith ("simp_from_eq can't do: " ^ tyname) end + val from_simps = map simp_from_eq from_eqs + val from_def = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) + (List.take(from_heads,mutrec_count)) + |> LIST_CONJ |> REWRITE_RULE from_simps + (* simplify to_def *) + val ts = to_def |> CONJUNCTS + val ts0 = List.take(ts,mutrec_count) + val ts1 = List.drop(ts,mutrec_count) |> map SPEC_ALL + (* + val to_eq = el 1 ts1 + *) + fun simp_one to_eq = let + val ty = to_eq |> concl |> dest_eq |> snd |> type_of + val tyname = dest_type ty |> fst + in if tyname = "option" then + to_eq |> REWRITE_RULE [get_to_option] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "sum" then + to_eq |> REWRITE_RULE [get_to_sum] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "prod" then + to_eq |> REWRITE_RULE [get_to_pair] |> GEN cv_var + |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] + |> CONV_RULE (DEPTH_CONV ETA_CONV) + else if tyname = "list" then + let + val tm1 = to_eq |> concl |> dest_eq |> fst |> rator + val tm2 = to_eq |> concl |> dest_eq |> snd |> rator + |> rand |> rator |> rand |> rator + val tm3 = to_list_def |> CONJUNCT1 |> ISPEC tm2 |> SPEC_ALL + |> concl |> dest_eq |> fst |> rator + val list_goal = mk_eq(tm1,tm3) + val res = auto_prove "to_list_eq" + (list_goal, + rewrite_tac [FUN_EQ_THM] + \\ Induct + \\ once_rewrite_tac [to_eq] + \\ asm_rewrite_tac [to_list_def,cv_has_shape_def, + cv_fst_def,cv_snd_def]) + in res end + else failwith ("don't know: " ^ tyname) end + val to_simps = map simp_one ts1 + val to_def = ts0 |> map SPEC_ALL |> LIST_CONJ |> REWRITE_RULE to_simps + (* save all results *) + val th1 = save_thm("from_" ^ first_name ^ "_def[compute]", from_def) + val th2 = save_thm("to_" ^ first_name ^ "_def[compute]", to_def) + fun save_from_to_thms th = let + val to_name = th |> UNDISCH_ALL |> concl |> rand |> repeat rator |> dest_const |> fst + in save_thm("from_" ^ to_name ^ "_thm", th) end + val thms = List.map save_from_to_thms from_to_thms + in (from_def,to_def,from_to_thms) end + handle UnusedTypeVars ignore_tyvars => define_from_to_aux ignore_tyvars ty; + +fun define_from_to ty = define_from_to_aux [] ty; + +end diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index f311e1ca39..548b080b19 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -1,5 +1,5 @@ open HolKernel Parse boolLib bossLib cvTheory; -open integerTheory wordsTheory sptreeTheory; +open integerTheory wordsTheory; val _ = new_theory "cv_types"; @@ -245,487 +245,4 @@ Proof Cases_on ‘v’ \\ fs [from_pair_def] QED -(* ------------- automation ---------------- *) - -val ERR = mk_HOL_ERR "cv_typesLib"; - -fun type_of_cases_const ty = let - val th = TypeBase.case_def_of ty - val ty = th |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL - |> concl |> dest_eq |> fst |> repeat rator |> type_of - in ty end - -fun auto_prove proof_name (goal,tac:tactic) = let - val (rest,validation) = tac ([],goal) - handle HOL_ERR r => raise (ERR "auto_prove" "tactic failure") - | Empty => raise (ERR "auto_prove" "tactic raised Empty") - in if length rest = 0 then validation [] else let - in failwith("auto_prove failed for " ^ proof_name) end end - -fun dest_fun_type ty = let - val (name,args) = dest_type ty - in if name = "fun" then (el 1 args, el 2 args) else failwith("not fun type") end; - -fun find_mutrec_types ty = let (* e.g. input ``:v`` gives [``:exp``,``:v``] *) - fun is_pair_ty ty = fst (dest_type ty) = "prod" - val xs = TypeBase.axiom_of ty - |> SPEC_ALL |> concl |> strip_exists - |> #1 |> map (#1 o dest_fun_type o type_of) - |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls) - in if is_pair_ty ty then [ty] else if length xs = 0 then [ty] else xs end - -fun matching_induction_of typ = let - val ind = TypeBase.induction_of typ - val ind_c = concl ind |> strip_forall |> snd |> dest_imp |> snd - val var_tys = strip_conj ind_c |> map (type_of o fst o dest_forall) - val matches = mapfilter (fn vty => match_type vty typ) var_tys - in case matches of - [] => failwith ("matching_induction_of: " ^ type_to_string typ) - | _ => INST_TYPE (hd matches) ind - end - -fun mk_funtype arg_tys ret_ty = - if null arg_tys then ret_ty else - mk_funtype (butlast arg_tys) (mk_type("fun",[last arg_tys,ret_ty])); - -fun make_stem fname args ret_ty = let - val f_ty = mk_funtype (map type_of args) ret_ty - in list_mk_comb(mk_var(fname,f_ty),args) end - -fun alookup x [] = NONE - | alookup x ((y,z)::xs) = if x = y then SOME z else alookup x xs; - -fun dest_fun_types ty = - let - val (x,y) = dest_fun_type ty - val (xs,z) = dest_fun_types y - in - (x::xs,z) - end handle HOL_ERR _ => ([],ty); - -local - val sum_case = sumTheory.sum_case_def - |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator - val tys = dest_fun_types (type_of sum_case) |> fst - val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys - val pat = list_mk_comb(sum_case,pat_args) - val thm = REFL pat |> GENL pat_args -in - val sum_ty = hd tys - val is_sum_type = can (match_type sum_ty) - fun mk_sum_case x y z = ISPECL [x,y,z] thm |> concl |> rand -end - -fun mk_sum_type l_ty r_ty = - mk_thy_type {Args = [l_ty, r_ty], Thy = "sum", Tyop = "sum"}; - -fun mk_pairs [] = cvSyntax.mk_cv_num(numSyntax.term_of_int 0) - | mk_pairs [x] = x - | mk_pairs (x::xs) = cvSyntax.mk_cv_pair(x, mk_pairs xs); - -fun constructors_of ty = let - val conses = TypeBase.constructors_of ty - fun match_ret_type c = - inst (match_type (repeat (snd o dest_fun_type) (type_of c)) ty) c - in map match_ret_type conses end - -fun from_to_for ty = - if ty = “:unit” then from_to_unit else - if ty = “:bool” then from_to_bool else - if ty = “:num” then from_to_num else - if ty = “:char” then from_to_char else - if ty = “:int” then from_to_int else - if wordsSyntax.is_word_type ty then - let val ty = wordsSyntax.dest_word_type ty - in INST_TYPE [alpha|->ty] from_to_word end - else if can pairSyntax.dest_prod ty then let - val (a,b) = pairSyntax.dest_prod ty - val a = from_to_for a - val b = from_to_for b - in MATCH_MP from_to_pair (CONJ a b) end - else if can sumSyntax.dest_sum ty then let - val (a,b) = sumSyntax.dest_sum ty - val a = from_to_for a - val b = from_to_for b - in MATCH_MP from_to_sum (CONJ a b) end - else if can optionSyntax.dest_option ty then let - val a = from_to_for (optionSyntax.dest_option ty) - in MATCH_MP from_to_option a end - else if listSyntax.is_list_type ty then - let val a = from_to_for (listSyntax.dest_list_type ty) - in MATCH_MP from_to_list a end - else failwith ("from_to_for: " ^ type_to_string ty) - -fun from_for ty = from_to_for ty |> concl |> rator |> rand; -fun to_for ty = from_to_for ty |> concl |> rand; - -val num_ty = arithmeticTheory.ODD_EVEN |> concl |> dest_forall |> fst |> type_of -val cv_has_shape_tm = - cv_has_shape_def |> CONJUNCT1 |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator; - -fun replicate 0 x = [] - | replicate n x = x :: replicate (n-1) x; - -fun list_dest_comb tm = - if is_comb tm then - let val (f,xs) = list_dest_comb (rator tm) - in (f,xs @ [rand tm]) end - else (tm,[]); - -fun term_all_distinct [] = [] - | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) - -exception UnusedTypeVars of hol_type list; - -(* -val ignore_tyvars = [alpha,gamma] -val ignore_tyvars = tl [alpha] -val ty = “:('a,'b,'c) word_tree” -val ty = “:('d, 'c) b” -*) -fun define_from_to_aux ignore_tyvars ty = let - (* extract target structure from induction theorem *) - val mutrec_count = length (find_mutrec_types ty) - val ind = TypeBase.induction_of ty - val inputs = ind |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCTS |> map (fst o dest_forall o concl) - val tyvars = dest_type (type_of (hd inputs)) |> snd - |> filter (fn tyvar => not (mem tyvar ignore_tyvars)) - val first_name = inputs |> hd |> type_of |> dest_type |> fst - val thy_name = inputs |> hd |> type_of |> dest_thy_type |> #Thy - val name_prefix = (if thy_name <> current_theory() then thy_name ^ "_" else "") - val names = inputs |> mapi (fn i => fn v => - if i < mutrec_count then - (name_prefix ^ (v |> type_of |> dest_type |> fst), type_of v) - else - (name_prefix ^ first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) - fun should_be_headless pat = - (* should return true if pat has at least two variables and belongs - to a type where all other constructors take no arguments *) - let - val (cons_tm,args) = list_dest_comb pat - fun all_other_patterns_are_nil () = let - val cs = TypeBase.constructors_of (type_of pat) - val others = filter (fn t => not (can (match_term t) cons_tm)) cs - val non_nil = filter (fn t => can dest_fun_type (type_of t)) others - in null non_nil end - in 1 < length args andalso all_other_patterns_are_nil () end - (* define encoding into cv type, i.e. "from function" *) - val tyvar_encoders = mapi (fn i => fn ty => - mk_var("f" ^ int_to_string i,mk_type("fun",[ty,cvSyntax.cv]))) tyvars - val from_names = names |> - map (fn (fname,ty) => - make_stem ("from_" ^ fname) tyvar_encoders (mk_funtype [ty] cvSyntax.cv)) - val lookups = - map (fn tm => (tm |> type_of |> dest_fun_type |> fst, tm)) (from_names @ tyvar_encoders) - (* - val from_f = el 4 from_names - *) - fun from_lines from_f = let - val conses = from_f |> type_of |> dest_type |> snd |> hd |> constructors_of - (* - val i = 0 - val cons_tm = el 2 conses - *) - fun from_line i cons_tm = let - val (tys,target_ty) = dest_fun_types (type_of cons_tm) - val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys - val pat = list_mk_comb(cons_tm,pat_args) - val lhs_tm = mk_comb(from_f,pat) - val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) - fun process_arg v = - case alookup (type_of v) lookups of - SOME tm => mk_comb(tm,v) - | NONE => mk_comb(from_for (type_of v),v) - val args = map process_arg pat_args - val special = should_be_headless pat - val smart_mk_pairs = (if special then mk_pairs o tl else mk_pairs) - val rhs_tm = smart_mk_pairs (tag_num :: args) - in mk_eq(lhs_tm,rhs_tm) end - val lines = mapi from_line conses - in lines end - val all_lines = map from_lines from_names |> flatten - val tm = list_mk_conj all_lines - val _ = let (* check which tyvar encoders are actually used *) - val cs = map (rator o fst o dest_eq) all_lines |> term_all_distinct - val substs = map (fn c => c |-> mk_arb(type_of c)) cs - val fvs = free_vars (subst substs tm) - val unused = filter (fn f => not (exists (fn t => aconv t f) fvs)) tyvar_encoders - in if null ignore_tyvars andalso not (null unused) then - raise UnusedTypeVars (map (fst o dest_fun_type o type_of) unused) - else () end - val from_def = zDefine [ANTIQUOTE tm] - (* define decoding from cv type, i.e. "to function" *) - val tyvar_decoders = mapi (fn i => fn ty => - mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars - val to_names = names |> - map (fn (fname,ty) => - make_stem ("to_" ^ fname) tyvar_decoders (mk_funtype [cvSyntax.cv] ty)) - val lookups = - map (fn tm => (tm |> type_of |> dest_fun_type |> snd, tm)) (to_names @ tyvar_decoders) - val cv_var = mk_var("v",cvSyntax.cv) - (* - val to_f = el 2 to_names - *) - fun to_lines to_f = let - val cons_ty = to_f |> type_of |> dest_type |> snd |> el 2 - val conses = cons_ty |> constructors_of - val lhs_tm = mk_comb(to_f,cv_var) - (* - val i = 0 - val cons_tm = el 1 conses - *) - fun to_line i cons_tm = let - val (tys,_) = dest_fun_types (type_of cons_tm) - val pat_args = mapi (fn i => fn ty => mk_var("v" ^ int_to_string i, ty)) tys - val pat = list_mk_comb(cons_tm,pat_args) - fun get_args v [] = [] - | get_args v [x] = [(x,v)] - | get_args v (x::xs) = - (x,cvSyntax.mk_cv_fst v) :: get_args (cvSyntax.mk_cv_snd v) xs - val special = should_be_headless pat - val init_var = (if special then cv_var else cvSyntax.mk_cv_snd cv_var) - val args = get_args init_var tys - fun process_arg (ty,v) = - case alookup ty lookups of - SOME tm => mk_comb(tm,v) - | NONE => mk_comb(to_for ty,v) - val xs = map process_arg args - fun lemmas_for_arg (ty,v) = - case alookup ty lookups of - SOME tm => [] - | NONE => [from_to_for ty] - val ys = map lemmas_for_arg args |> flatten - val build = list_mk_comb (cons_tm,xs) - val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) - val c2b = c2b_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator - val none_num = optionSyntax.mk_none(num_ty) - val test = if null tys then mk_eq(cv_var,tag_num) else - list_mk_comb(cv_has_shape_tm, - [listSyntax.mk_list( - (if special then [] else [optionSyntax.mk_some(tag_num |> rand)]) - @ replicate (length tys - 1) none_num, - type_of none_num), - cv_var]) - in (ys,(test,build)) end - val lemmas_lines = mapi to_line conses - val lemmas = map fst lemmas_lines |> flatten - val lines = map snd lemmas_lines - fun partition p [] = ([],[]) - | partition p (x::xs) = - let val (xs1,ys1) = partition p xs - in if p x then (x::xs1,ys1) else (xs1,x::ys1) end - val common_vars = cv_var :: tyvar_decoders - fun every p [] = true - | every p (x::xs) = (p x andalso every p xs) - fun exists p [] = false - | exists p (x::xs) = (p x orelse exists p xs) - fun subset xs ys = every (fn x => exists (aconv x) ys) xs - val (lines1,lines2) = - partition (fn (x,tm) => not (subset (free_vars tm) common_vars)) lines - val lines = lines1 @ lines2 - val needs_final_arb = (null lines2 orelse is_sum_type cons_ty) - fun mk_rhs [] = fail() - | mk_rhs [(t,x)] = if needs_final_arb then mk_cond(t,x,mk_arb(type_of x)) else x - | mk_rhs ((t,x)::xs) = mk_cond(t,x,mk_rhs xs) - in (mk_eq(lhs_tm,mk_rhs lines),lemmas) end - val (all_lines,lemmas1) = unzip (map to_lines to_names) - val lemmas = lemmas1 |> flatten - val tm = list_mk_conj all_lines - val cv_size = - cv_size_def |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> rator - val args = pairSyntax.list_mk_pair (tyvar_decoders @ [cv_var]) - val size_tm = pairSyntax.mk_pabs(args, mk_comb(cv_size,cv_var)) - fun mk_measure_input_ty [] = type_of args - | mk_measure_input_ty [x] = type_of args - | mk_measure_input_ty (x::xs) = - mk_sum_type (type_of args) (mk_measure_input_ty xs) - val measure_ty = mk_measure_input_ty all_lines - val measure_var = mk_var("x",measure_ty) - fun mk_cases [] = fail() - | mk_cases [x] = size_tm - | mk_cases (x::xs) = - mk_abs (mk_var("x",mk_measure_input_ty (x::xs)), - (mk_sum_case - (mk_var("x",mk_measure_input_ty (x::xs))) - size_tm (mk_cases xs))) - val measure_tm = mk_cases all_lines - val full_measure_tm = ISPEC measure_tm prim_recTheory.WF_measure |> concl |> rand - val to_def_name = (to_names |> hd |> repeat rator |> dest_var |> fst) - val (to_def, to_ind) = - let - val to_defn = Hol_defn to_def_name [ANTIQUOTE tm] - in Defn.tprove(to_defn, - WF_REL_TAC [ANTIQUOTE full_measure_tm] - \\ rewrite_tac [cv_has_shape_expand] - \\ rpt strip_tac \\ gvs [cv_size_def]) - end - (* from from_to theorems *) - val assums = - map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) - (tyvar_encoders) (tyvar_decoders) - val assum = if null assums then T else list_mk_conj assums - val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) - val from_cs = from_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) - |> term_all_distinct - val goals = - map2 (fn f => fn t => - let - val ty = f |> type_of |> dest_fun_type |> fst - val v = mk_var("v",ty) - in mk_abs(v,mk_eq(mk_comb(t,mk_comb(f,v)),v)) end) from_cs to_cs - val lemma = ISPECL goals ind |> CONV_RULE (DEPTH_CONV BETA_CONV) - val main_goal = lemma |> concl |> dest_imp |> snd - val the_goal = mk_imp(assum,main_goal) - (* - set_goal([],the_goal) - *) - val from_to_thm = auto_prove "from_to_thm" (the_goal, - strip_tac - \\ match_mp_tac lemma - \\ rpt conj_tac - \\ rpt gen_tac - \\ rpt disch_tac - \\ once_rewrite_tac [from_def] - \\ once_rewrite_tac [to_def] - \\ rewrite_tac [cv_has_shape_def,cv_fst_def,cv_snd_def] - \\ EVERY (map assume_tac lemmas) - \\ fs [from_to_def]) - val from_to_thms = - from_to_thm |> REWRITE_RULE [GSYM from_to_def] - |> UNDISCH_ALL |> CONJUNCTS - |> (fn xs => List.take(xs,mutrec_count)) - |> map DISCH_ALL - (* simplify from_def *) - val froms = from_def |> CONJUNCTS |> map SPEC_ALL - val pick = (rator o fst o dest_eq o concl) - val from_heads = froms |> map pick |> term_all_distinct - val from_eqs = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) - (List.drop(from_heads,mutrec_count)) - |> map (DefnBase.one_line_ify NONE) - fun simp_from_eq from_eq = let - val v = from_eq |> concl |> dest_eq |> fst |> rand - val tyname = v |> type_of |> dest_type |> fst - in if tyname = "prod" then - from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_pair) - |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] - else if tyname = "option" then - from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_option) - |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] - else if tyname = "sum" then - from_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_from_sum) - |> GEN v |> SIMP_RULE std_ss [GSYM FUN_EQ_THM,SF ETA_ss] - else if tyname = "list" then - let - val tm0 = from_eq |> concl |> dest_eq |> fst |> rator - val tm1 = from_eq |> concl |> rand |> rand |> dest_abs |> snd - |> dest_abs |> snd |> rator |> rand |> rator - val tm2 = from_list_def |> CONJUNCT1 |> ISPEC tm1 |> concl - |> dest_eq |> fst |> rator - val list_goal = mk_eq(tm0,tm2) - val res = auto_prove "simp_from_eq_list" - (list_goal, - rewrite_tac [FUN_EQ_THM] - \\ Induct - \\ once_rewrite_tac [from_list_def,from_eq] \\ fs []) - in res end - else failwith ("simp_from_eq can't do: " ^ tyname) end - val from_simps = map simp_from_eq from_eqs - val from_def = map (fn h => LIST_CONJ (filter (fn tm => aconv (pick tm) h) froms)) - (List.take(from_heads,mutrec_count)) - |> LIST_CONJ |> REWRITE_RULE from_simps - (* simplify to_def *) - val ts = to_def |> CONJUNCTS - val ts0 = List.take(ts,mutrec_count) - val ts1 = List.drop(ts,mutrec_count) |> map SPEC_ALL - (* - val to_eq = el 1 ts1 - *) - fun simp_one to_eq = let - val ty = to_eq |> concl |> dest_eq |> snd |> type_of - val tyname = dest_type ty |> fst - in if tyname = "option" then - to_eq |> REWRITE_RULE [get_to_option] |> GEN cv_var - |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] - |> CONV_RULE (DEPTH_CONV ETA_CONV) - else if tyname = "sum" then - to_eq |> REWRITE_RULE [get_to_sum] |> GEN cv_var - |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] - |> CONV_RULE (DEPTH_CONV ETA_CONV) - else if tyname = "prod" then - to_eq |> REWRITE_RULE [get_to_pair] |> GEN cv_var - |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] - |> CONV_RULE (DEPTH_CONV ETA_CONV) - else if tyname = "list" then - let - val tm1 = to_eq |> concl |> dest_eq |> fst |> rator - val tm2 = to_eq |> concl |> dest_eq |> snd |> rator - |> rand |> rator |> rand |> rator - val tm3 = to_list_def |> CONJUNCT1 |> ISPEC tm2 |> SPEC_ALL - |> concl |> dest_eq |> fst |> rator - val list_goal = mk_eq(tm1,tm3) - val res = auto_prove "to_list_eq" - (list_goal, - rewrite_tac [FUN_EQ_THM] - \\ Induct - \\ once_rewrite_tac [to_eq] - \\ asm_rewrite_tac [to_list_def,cv_has_shape_def, - cv_fst_def,cv_snd_def]) - in res end - else failwith ("don't know: " ^ tyname) end - val to_simps = map simp_one ts1 - val to_def = ts0 |> map SPEC_ALL |> LIST_CONJ |> REWRITE_RULE to_simps - (* save all results *) - val th1 = save_thm("from_" ^ first_name ^ "_def[compute]", from_def) - val th2 = save_thm("to_" ^ first_name ^ "_def[compute]", to_def) - fun save_from_to_thms th = let - val to_name = th |> UNDISCH_ALL |> concl |> rand |> repeat rator |> dest_const |> fst - in save_thm("from_" ^ to_name ^ "_thm", th) end - val thms = List.map save_from_to_thms from_to_thms - in (from_def,to_def,from_to_thms) end - handle UnusedTypeVars ignore_tyvars => define_from_to_aux ignore_tyvars ty; - -fun define_from_to ty = define_from_to_aux [] ty; - -(* tests *) - -Datatype: - a = A1 (num list) (((a # b) list) list) - | A2 ((a + b) list) ; - b = B1 - | B2 - | B3 (c option) ; - c = C1 - | C2 a 'aa 'bb -End - -val ty = “:('d, 'c) b” -val res = define_from_to ty - -Datatype: - tree = Leaf - | Branch ((tree list + bool) option list) -End - -val res = define_from_to “:tree” - -Datatype: - t1 = T1 num (t1 list) -End - -val res = define_from_to “:t1” - -Datatype: - word_tree = - | Fork word_tree word_tree - | Word1 ('a word) - | Other 'b - | Word2 ('c word) -End - -val ty = “:('a,'b,'c) word_tree” -val res = define_from_to ty -val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() - -val res = define_from_to “:'a sptree$spt” - val _ = export_theory(); diff --git a/src/num/theories/cv_compute/automation/cv_types_demoScript.sml b/src/num/theories/cv_compute/automation/cv_types_demoScript.sml new file mode 100644 index 0000000000..1e7e38137f --- /dev/null +++ b/src/num/theories/cv_compute/automation/cv_types_demoScript.sml @@ -0,0 +1,55 @@ +open HolKernel Parse boolLib bossLib cvTheory; +open integerTheory wordsTheory sptreeTheory cv_typesTheory cv_typesLib; + +val _ = new_theory "cv_types_demo"; + +val _ = set_grammar_ancestry ["cv_types"]; + +Overload c2n[local] = “cv$c2n” +Overload c2b[local] = “cv$c2b” +Overload Num[local] = “cv$Num” +Overload Pair[local] = “cv$Pair” + +(* tests *) + +Datatype: + a = A1 (num list) (((a # b) list) list) + | A2 ((a + b) list) ; + b = B1 + | B2 + | B3 (c option) ; + c = C1 + | C2 a 'aa 'bb +End + +val ty = “:('d, 'c) b” +val res = define_from_to ty + +Datatype: + tree = Leaf + | Branch ((tree list + bool) option list) +End + +val res = define_from_to “:tree” + +Datatype: + t1 = T1 num (t1 list) +End + +val res = define_from_to “:t1” + +Datatype: + word_tree = + | Fork word_tree word_tree + | Word1 ('a word) + | Other 'b + | Word2 ('c word) +End + +val ty = “:('a,'b,'c) word_tree” +val res = define_from_to ty +val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() + +val res = define_from_to “:'a sptree$spt” + +val _ = export_theory(); From 0fbb66773009b001eb8dcf21806054fd281e1d96 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 23 Aug 2023 09:13:37 +0200 Subject: [PATCH 08/15] Remove redundant checks in decoding (to) functions --- .../cv_compute/automation/cv_typesLib.sml | 40 +++++++++++++------ .../cv_compute/automation/cv_typesScript.sml | 9 ++--- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index 85b9ef0a8a..09dbfd907e 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -170,6 +170,8 @@ fun to_for ty = from_to_for ty |> concl |> rand; exception UnusedTypeVars of hol_type list; +datatype tag_sum = TagNil of int | TagCons of (int * (int option) list); + (* val ignore_tyvars = [alpha,gamma] val ignore_tyvars = tl [alpha] @@ -289,16 +291,9 @@ fun define_from_to_aux ignore_tyvars ty = let | NONE => [from_to_for ty] val ys = map lemmas_for_arg args |> flatten val build = list_mk_comb (cons_tm,xs) - val tag_num = cvSyntax.mk_cv_num(numSyntax.term_of_int i) - val c2b = c2b_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator - val none_num = optionSyntax.mk_none(num_ty) - val test = if null tys then mk_eq(cv_var,tag_num) else - list_mk_comb(cv_has_shape_tm, - [listSyntax.mk_list( - (if special then [] else [optionSyntax.mk_some(tag_num |> rand)]) - @ replicate (length tys - 1) none_num, - type_of none_num), - cv_var]) + val test = if null tys then TagNil i else + (TagCons (i,(if special then [] else [SOME i]) + @ replicate (length tys - 1) NONE)) in (ys,(test,build)) end val lemmas_lines = mapi to_line conses val lemmas = map fst lemmas_lines |> flatten @@ -316,6 +311,25 @@ fun define_from_to_aux ignore_tyvars ty = let val (lines1,lines2) = partition (fn (x,tm) => not (subset (free_vars tm) common_vars)) lines val lines = lines1 @ lines2 + fun make_last_non_nil_all_none [] = (false,[]) + | make_last_non_nil_all_none ((tag,tm)::rest) = let + val (has_marked,res) = make_last_non_nil_all_none rest + in if has_marked then (has_marked,(tag,tm)::res) else + case tag of + TagNil i => (has_marked,(tag,tm)::res) + | TagCons (i,ns) => (true,(TagCons (i,map (K NONE) ns),tm)::res) + end + val lines = lines |> make_last_non_nil_all_none |> snd + val none_num = optionSyntax.mk_none(num_ty) + fun cv_num_from_int i = cvSyntax.mk_cv_num(numSyntax.term_of_int i) + fun opt_num_from_opt_int NONE = none_num + | opt_num_from_opt_int (SOME i) = optionSyntax.mk_some(numSyntax.term_of_int i) + fun test_to_term (TagNil i,tm) = (mk_eq(cv_var,cv_num_from_int i),tm:term) + | test_to_term (TagCons (i,ns),tm) = + (list_mk_comb(cv_has_shape_tm, + [listSyntax.mk_list(map opt_num_from_opt_int ns,type_of none_num), + cv_var]),tm) + val lines = lines |> map test_to_term val needs_final_arb = (null lines2 orelse is_sum_type cons_ty) fun mk_rhs [] = fail() | mk_rhs [(t,x)] = if needs_final_arb then mk_cond(t,x,mk_arb(type_of x)) else x @@ -437,15 +451,15 @@ fun define_from_to_aux ignore_tyvars ty = let val ty = to_eq |> concl |> dest_eq |> snd |> type_of val tyname = dest_type ty |> fst in if tyname = "option" then - to_eq |> REWRITE_RULE [get_to_option] |> GEN cv_var + to_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_to_option) |> GEN cv_var |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] |> CONV_RULE (DEPTH_CONV ETA_CONV) else if tyname = "sum" then - to_eq |> REWRITE_RULE [get_to_sum] |> GEN cv_var + to_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_to_sum) |> GEN cv_var |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] |> CONV_RULE (DEPTH_CONV ETA_CONV) else if tyname = "prod" then - to_eq |> REWRITE_RULE [get_to_pair] |> GEN cv_var + to_eq |> CONV_RULE (RAND_CONV $ REWR_CONV get_to_pair) |> GEN cv_var |> SIMP_RULE std_ss [GSYM FUN_EQ_THM] |> CONV_RULE (DEPTH_CONV ETA_CONV) else if tyname = "list" then diff --git a/src/num/theories/cv_compute/automation/cv_typesScript.sml b/src/num/theories/cv_compute/automation/cv_typesScript.sml index 548b080b19..0ee16e716c 100644 --- a/src/num/theories/cv_compute/automation/cv_typesScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typesScript.sml @@ -109,7 +109,7 @@ End Definition to_option_def: to_option t (Num n) = NONE /\ - to_option t (Pair x y) = if x = Num 1 then SOME (t y) else NONE + to_option t (Pair x y) = SOME (t y) End Theorem from_to_option: @@ -149,8 +149,7 @@ End Definition to_sum_def: to_sum t1 t2 (Num n) = ARB /\ to_sum t1 t2 (Pair x y) = - if x = Num 0 then INL (t1 y) else - if x = Num 1 then INR (t2 y) else ARB + if x = Num 0 then INL (t1 y) else INR (t2 y) End Theorem from_to_sum: @@ -209,7 +208,7 @@ Proof QED Theorem get_to_option: - (if cv_has_shape [SOME 1] v then SOME (t (cv_snd v)) else NONE) = to_option t v + (if cv_has_shape [NONE] v then SOME (t (cv_snd v)) else NONE) = to_option t v Proof Cases_on ‘v’ \\ fs [to_option_def,cv_has_shape_def] @@ -217,7 +216,7 @@ QED Theorem get_to_sum: (if cv_has_shape [SOME 0] v then INL (t1 (cv_snd v)) - else if cv_has_shape [SOME 1] v then INR (t2 (cv_snd v)) + else if cv_has_shape [NONE] v then INR (t2 (cv_snd v)) else ARB) = to_sum t1 t2 v Proof Cases_on ‘v’ From ab7d763259e38a0daa9bcbbf0280d4b511aaa4e0 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 23 Aug 2023 09:55:14 +0200 Subject: [PATCH 09/15] Support basic memory lookups --- .../cv_compute/automation/cv_typesLib.sml | 45 +++++++++++++++++-- 1 file changed, 41 insertions(+), 4 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index 09dbfd907e..86482773e2 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -130,10 +130,18 @@ fun list_dest_comb tm = fun term_all_distinct [] = [] | term_all_distinct (x::xs) = x :: term_all_distinct (filter (fn c => not (aconv c x)) xs) +fun list_dest_conj tm = + let + val (x,y) = dest_conj tm + in x :: list_dest_conj y end + handle HOL_ERR e => [tm]; + (* --------------------------------------------------- * Loading from_to theorems * --------------------------------------------------- *) +exception Missing_from_to of hol_type; + fun from_to_for ty = if ty = “:unit” then from_to_unit else if ty = “:bool” then from_to_bool else @@ -159,7 +167,34 @@ fun from_to_for ty = else if listSyntax.is_list_type ty then let val a = from_to_for (listSyntax.dest_list_type ty) in MATCH_MP from_to_list a end - else failwith ("from_to_for: " ^ type_to_string ty) + else (* look through memory *) + let + val thms = from_to_thms () + fun match_from_to_thm th = + let + val th1 = th |> UNDISCH_ALL + val ty1 = th1 |> concl |> rand |> type_of |> dest_fun_type |> snd + val i = match_type ty1 ty + val th2 = th |> INST_TYPE i |> DISCH_ALL + in + if not (is_imp (concl th2)) then th2 else + let + val th3 = th2 |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] + val tms = th3 |> concl |> dest_imp |> fst |> list_dest_conj + fun prove_from_to_thm tm = + let + val ty1 = tm |> rand |> type_of |> dest_fun_type |> snd + in from_to_for ty1 end + val th4 = LIST_CONJ (map prove_from_to_thm tms) + in MATCH_MP th3 th4 end + end + fun find_first f [] = NONE + | find_first f (x::xs) = SOME (f x) handle HOL_ERR e => find_first f xs + in + case find_first match_from_to_thm thms of + SOME th => th + | NONE => raise Missing_from_to ty + end fun from_for ty = from_to_for ty |> concl |> rator |> rand; fun to_for ty = from_to_for ty |> concl |> rand; @@ -192,7 +227,7 @@ fun define_from_to_aux ignore_tyvars ty = let if i < mutrec_count then (name_prefix ^ (v |> type_of |> dest_type |> fst), type_of v) else - (name_prefix ^ first_name ^ int_to_string (i - mutrec_count + 1), type_of v)) + (name_prefix ^ first_name ^ "___" ^ int_to_string (i - mutrec_count + 1), type_of v)) fun should_be_headless pat = (* should return true if pat has at least two variables and belongs to a type where all other constructors take no arguments *) @@ -486,8 +521,10 @@ fun define_from_to_aux ignore_tyvars ty = let val th2 = save_thm("to_" ^ first_name ^ "_def[compute]", to_def) fun save_from_to_thms th = let val to_name = th |> UNDISCH_ALL |> concl |> rand |> repeat rator |> dest_const |> fst - in save_thm("from_" ^ to_name ^ "_thm", th) end - val thms = List.map save_from_to_thms from_to_thms + val _ = save_thm("from_" ^ to_name ^ "_thm", th) + val _ = add_from_to_thm th + in () end + val _ = List.app save_from_to_thms from_to_thms in (from_def,to_def,from_to_thms) end handle UnusedTypeVars ignore_tyvars => define_from_to_aux ignore_tyvars ty; From b59c507df69fae05082cd160992fb8a5152c46d3 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 23 Aug 2023 10:37:00 +0200 Subject: [PATCH 10/15] Improve support for tyvars --- .../cv_compute/automation/cv_typesLib.sml | 51 ++++++++++--------- 1 file changed, 28 insertions(+), 23 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index 86482773e2..f2cbc61666 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -142,7 +142,7 @@ fun list_dest_conj tm = exception Missing_from_to of hol_type; -fun from_to_for ty = +fun from_to_for tyvars_alist ty = if ty = “:unit” then from_to_unit else if ty = “:bool” then from_to_bool else if ty = “:num” then from_to_num else @@ -153,21 +153,24 @@ fun from_to_for ty = in INST_TYPE [alpha|->ty] from_to_word end else if can pairSyntax.dest_prod ty then let val (a,b) = pairSyntax.dest_prod ty - val a = from_to_for a - val b = from_to_for b + val a = from_to_for tyvars_alist a + val b = from_to_for tyvars_alist b in MATCH_MP from_to_pair (CONJ a b) end else if can sumSyntax.dest_sum ty then let val (a,b) = sumSyntax.dest_sum ty - val a = from_to_for a - val b = from_to_for b + val a = from_to_for tyvars_alist a + val b = from_to_for tyvars_alist b in MATCH_MP from_to_sum (CONJ a b) end else if can optionSyntax.dest_option ty then let - val a = from_to_for (optionSyntax.dest_option ty) + val a = from_to_for tyvars_alist (optionSyntax.dest_option ty) in MATCH_MP from_to_option a end else if listSyntax.is_list_type ty then - let val a = from_to_for (listSyntax.dest_list_type ty) + let val a = from_to_for tyvars_alist (listSyntax.dest_list_type ty) in MATCH_MP from_to_list a end - else (* look through memory *) + else + case alookup ty tyvars_alist of + SOME tyvar_assum => ASSUME tyvar_assum + | NONE => (* look through memory *) let val thms = from_to_thms () fun match_from_to_thm th = @@ -184,7 +187,7 @@ fun from_to_for ty = fun prove_from_to_thm tm = let val ty1 = tm |> rand |> type_of |> dest_fun_type |> snd - in from_to_for ty1 end + in from_to_for tyvars_alist ty1 end val th4 = LIST_CONJ (map prove_from_to_thm tms) in MATCH_MP th3 th4 end end @@ -196,8 +199,8 @@ fun from_to_for ty = | NONE => raise Missing_from_to ty end -fun from_for ty = from_to_for ty |> concl |> rator |> rand; -fun to_for ty = from_to_for ty |> concl |> rand; +fun from_for tyvars_alist ty = from_to_for tyvars_alist ty |> concl |> rator |> rand; +fun to_for tyvars_alist ty = from_to_for tyvars_alist ty |> concl |> rand; (* --------------------------------------------------- * Defining new from/to functions for a datatype @@ -239,9 +242,16 @@ fun define_from_to_aux ignore_tyvars ty = let val non_nil = filter (fn t => can dest_fun_type (type_of t)) others in null non_nil end in 1 < length args andalso all_other_patterns_are_nil () end - (* define encoding into cv type, i.e. "from function" *) + (* tyvar assumptions *) val tyvar_encoders = mapi (fn i => fn ty => mk_var("f" ^ int_to_string i,mk_type("fun",[ty,cvSyntax.cv]))) tyvars + val tyvar_decoders = mapi (fn i => fn ty => + mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars + val tyvar_assums = + map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) + (tyvar_encoders) (tyvar_decoders) + val tyvars_alist = zip tyvars tyvar_assums + (* define encoding into cv type, i.e. "from function" *) val from_names = names |> map (fn (fname,ty) => make_stem ("from_" ^ fname) tyvar_encoders (mk_funtype [ty] cvSyntax.cv)) @@ -265,7 +275,7 @@ fun define_from_to_aux ignore_tyvars ty = let fun process_arg v = case alookup (type_of v) lookups of SOME tm => mk_comb(tm,v) - | NONE => mk_comb(from_for (type_of v),v) + | NONE => mk_comb(from_for tyvars_alist (type_of v),v) val args = map process_arg pat_args val special = should_be_headless pat val smart_mk_pairs = (if special then mk_pairs o tl else mk_pairs) @@ -285,8 +295,6 @@ fun define_from_to_aux ignore_tyvars ty = let else () end val from_def = zDefine [ANTIQUOTE tm] (* define decoding from cv type, i.e. "to function" *) - val tyvar_decoders = mapi (fn i => fn ty => - mk_var("t" ^ int_to_string i,mk_type("fun",[cvSyntax.cv,ty]))) tyvars val to_names = names |> map (fn (fname,ty) => make_stem ("to_" ^ fname) tyvar_decoders (mk_funtype [cvSyntax.cv] ty)) @@ -318,12 +326,12 @@ fun define_from_to_aux ignore_tyvars ty = let fun process_arg (ty,v) = case alookup ty lookups of SOME tm => mk_comb(tm,v) - | NONE => mk_comb(to_for ty,v) + | NONE => mk_comb(to_for tyvars_alist ty,v) val xs = map process_arg args fun lemmas_for_arg (ty,v) = case alookup ty lookups of SOME tm => [] - | NONE => [from_to_for ty] + | NONE => [from_to_for tyvars_alist ty] val ys = map lemmas_for_arg args |> flatten val build = list_mk_comb (cons_tm,xs) val test = if null tys then TagNil i else @@ -371,7 +379,7 @@ fun define_from_to_aux ignore_tyvars ty = let | mk_rhs ((t,x)::xs) = mk_cond(t,x,mk_rhs xs) in (mk_eq(lhs_tm,mk_rhs lines),lemmas) end val (all_lines,lemmas1) = unzip (map to_lines to_names) - val lemmas = lemmas1 |> flatten + val lemmas = lemmas1 |> flatten |> map DISCH_ALL val tm = list_mk_conj all_lines val cv_size = cv_size_def |> CONJUNCTS |> hd |> SPEC_ALL |> concl |> dest_eq |> fst |> rator @@ -402,10 +410,7 @@ fun define_from_to_aux ignore_tyvars ty = let \\ rpt strip_tac \\ gvs [cv_size_def]) end (* from from_to theorems *) - val assums = - map2 (fn f => fn t => ISPECL [f,t] from_to_def |> concl |> dest_eq |> fst) - (tyvar_encoders) (tyvar_decoders) - val assum = if null assums then T else list_mk_conj assums + val assum = if null tyvar_assums then T else list_mk_conj tyvar_assums val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) val from_cs = from_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) |> term_all_distinct @@ -431,7 +436,7 @@ fun define_from_to_aux ignore_tyvars ty = let \\ once_rewrite_tac [to_def] \\ rewrite_tac [cv_has_shape_def,cv_fst_def,cv_snd_def] \\ EVERY (map assume_tac lemmas) - \\ fs [from_to_def]) + \\ gs [from_to_def]) val from_to_thms = from_to_thm |> REWRITE_RULE [GSYM from_to_def] |> UNDISCH_ALL |> CONJUNCTS From 0056f8702dc56424bd28fd19e630a437a0206fc7 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 23 Aug 2023 10:47:56 +0200 Subject: [PATCH 11/15] Handle non-recursive datatypes --- src/num/theories/cv_compute/automation/cv_typesLib.sml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index f2cbc61666..9de8fbc33e 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -402,13 +402,14 @@ fun define_from_to_aux ignore_tyvars ty = let val full_measure_tm = ISPEC measure_tm prim_recTheory.WF_measure |> concl |> rand val to_def_name = (to_names |> hd |> repeat rator |> dest_var |> fst) val (to_def, to_ind) = + (new_definition(to_def_name,tm),TRUTH) handle HOL_ERR _ => let val to_defn = Hol_defn to_def_name [ANTIQUOTE tm] in Defn.tprove(to_defn, WF_REL_TAC [ANTIQUOTE full_measure_tm] \\ rewrite_tac [cv_has_shape_expand] \\ rpt strip_tac \\ gvs [cv_size_def]) - end + end (* from from_to theorems *) val assum = if null tyvar_assums then T else list_mk_conj tyvar_assums val to_cs = to_def |> CONJUNCTS |> map (rator o fst o dest_eq o concl o SPEC_ALL) From 8eb06e4c8d8733428e9c977e33292dae68f94321 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 23 Aug 2023 13:13:29 +0200 Subject: [PATCH 12/15] Add recursive definition of from/to functions --- .../cv_compute/automation/cv_typesLib.sig | 4 ++++ .../cv_compute/automation/cv_typesLib.sml | 24 +++++++++++++++++++ .../automation/cv_types_demoScript.sml | 14 +++++++++++ 3 files changed, 42 insertions(+) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sig b/src/num/theories/cv_compute/automation/cv_typesLib.sig index d9522613e0..6a285e5939 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sig +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sig @@ -10,5 +10,9 @@ sig (* automatically define new from/to functions for a user-defined datatype *) val define_from_to : hol_type -> thm * thm * thm list + val rec_define_from_to : hol_type -> thm list + + (* define_from_to can raise this: *) + exception Missing_from_to of hol_type end diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index 9de8fbc33e..700e1872ce 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -536,4 +536,28 @@ fun define_from_to_aux ignore_tyvars ty = let fun define_from_to ty = define_from_to_aux [] ty; +(* --------------------------------------------------- * + Recursively define new from/to functions + * --------------------------------------------------- *) + +fun get_type_name ty = dest_type ty |> fst + +fun rec_define_from_to ty = let + fun loop acc ty = + let + val (to_def,from_def,thms) = define_from_to ty + val _ = print ("Finished to/from for " ^ get_type_name ty ^ "\n\n") + val _ = print_thm to_def + val _ = print "\n\n" + in thms @ acc end + handle Missing_from_to needs_ty => + let + val _ = print ("Interrupting " ^ get_type_name ty ^ + " since " ^ get_type_name needs_ty ^ " needed.\n") + val acc = loop acc needs_ty + val _ = print ("Continuing " ^ get_type_name ty ^ + " since " ^ get_type_name needs_ty ^ " exists.\n") + in loop acc ty end + in loop [] ty end + end diff --git a/src/num/theories/cv_compute/automation/cv_types_demoScript.sml b/src/num/theories/cv_compute/automation/cv_types_demoScript.sml index 1e7e38137f..f8175ae279 100644 --- a/src/num/theories/cv_compute/automation/cv_types_demoScript.sml +++ b/src/num/theories/cv_compute/automation/cv_types_demoScript.sml @@ -52,4 +52,18 @@ val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() val res = define_from_to “:'a sptree$spt” +Datatype: + op = Add | Sub +End + +Datatype: + exp = Var string | Const int | Op op (exp list) +End + +Datatype: + prog = Skip | Seq prog prog | Assign string exp +End + +val thms = rec_define_from_to “:prog”; + val _ = export_theory(); From c94e9ccdd0fd9a035f515ed93458e1fd93e73448 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 25 Aug 2023 08:28:42 +0200 Subject: [PATCH 13/15] Change demo script into a selftest.sml --- .../cv_compute/automation/Holmakefile | 14 +++++++ .../{cv_types_demoScript.sml => selftest.sml} | 41 +++++++------------ 2 files changed, 28 insertions(+), 27 deletions(-) create mode 100644 src/num/theories/cv_compute/automation/Holmakefile rename src/num/theories/cv_compute/automation/{cv_types_demoScript.sml => selftest.sml} (71%) diff --git a/src/num/theories/cv_compute/automation/Holmakefile b/src/num/theories/cv_compute/automation/Holmakefile new file mode 100644 index 0000000000..fda006ff96 --- /dev/null +++ b/src/num/theories/cv_compute/automation/Holmakefile @@ -0,0 +1,14 @@ +all: $(DEFAULT_TARGETS) selftest.exe +.PHONY: all + +selftest.exe: selftest.uo + $(HOLMOSMLC) -o $@ $< + +EXTRA_CLEANS = selftest.exe selftest.log + +ifdef HOLSELFTESTLEVEL +all: selftest.log + +selftest.log: selftest.exe + $(tee ./$< 2>&1, $@) +endif diff --git a/src/num/theories/cv_compute/automation/cv_types_demoScript.sml b/src/num/theories/cv_compute/automation/selftest.sml similarity index 71% rename from src/num/theories/cv_compute/automation/cv_types_demoScript.sml rename to src/num/theories/cv_compute/automation/selftest.sml index f8175ae279..64e198a625 100644 --- a/src/num/theories/cv_compute/automation/cv_types_demoScript.sml +++ b/src/num/theories/cv_compute/automation/selftest.sml @@ -1,18 +1,7 @@ open HolKernel Parse boolLib bossLib cvTheory; open integerTheory wordsTheory sptreeTheory cv_typesTheory cv_typesLib; -val _ = new_theory "cv_types_demo"; - -val _ = set_grammar_ancestry ["cv_types"]; - -Overload c2n[local] = “cv$c2n” -Overload c2b[local] = “cv$c2b” -Overload Num[local] = “cv$Num” -Overload Pair[local] = “cv$Pair” - -(* tests *) - -Datatype: +val _ = Datatype ‘ a = A1 (num list) (((a # b) list) list) | A2 ((a + b) list) ; b = B1 @@ -20,31 +9,31 @@ Datatype: | B3 (c option) ; c = C1 | C2 a 'aa 'bb -End +’ val ty = “:('d, 'c) b” val res = define_from_to ty -Datatype: +val _ = Datatype ‘ tree = Leaf | Branch ((tree list + bool) option list) -End +’ val res = define_from_to “:tree” -Datatype: +val _ = Datatype ‘ t1 = T1 num (t1 list) -End +’ val res = define_from_to “:t1” -Datatype: +val _ = Datatype ‘ word_tree = | Fork word_tree word_tree | Word1 ('a word) | Other 'b | Word2 ('c word) -End +’ val ty = “:('a,'b,'c) word_tree” val res = define_from_to ty @@ -52,18 +41,16 @@ val _ = (type_of “from_word_tree f0 t” = “:cv”) orelse fail() val res = define_from_to “:'a sptree$spt” -Datatype: +val _ = Datatype‘ op = Add | Sub -End +’ -Datatype: +val _ = Datatype ‘ exp = Var string | Const int | Op op (exp list) -End +’ -Datatype: +val _ = Datatype ‘ prog = Skip | Seq prog prog | Assign string exp -End +’ val thms = rec_define_from_to “:prog”; - -val _ = export_theory(); From 5d5e37e43ac13e80553097567108cd80a6c8e46e Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 25 Aug 2023 10:35:46 +0200 Subject: [PATCH 14/15] Include cv_types automation in HOL bin/build --- src/num/theories/cv_compute/automation/Holmakefile | 10 +++++++++- src/parallel_builds/core/Holmakefile | 1 + 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/num/theories/cv_compute/automation/Holmakefile b/src/num/theories/cv_compute/automation/Holmakefile index fda006ff96..1ff20adb01 100644 --- a/src/num/theories/cv_compute/automation/Holmakefile +++ b/src/num/theories/cv_compute/automation/Holmakefile @@ -1,5 +1,13 @@ all: $(DEFAULT_TARGETS) selftest.exe -.PHONY: all + +.PHONY: all link-to-sigobj + +ifdef HOLBUILD +all: link-to-sigobj +.PHONY: link-to-sigobj +link-to-sigobj: $(DEFAULT_TARGETS) + $(HOL_LNSIGOBJ) +endif selftest.exe: selftest.uo $(HOLMOSMLC) -o $@ $< diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile index e778230f4b..050fa29f2c 100644 --- a/src/parallel_builds/core/Holmakefile +++ b/src/parallel_builds/core/Holmakefile @@ -11,6 +11,7 @@ SRCRELNAMES = \ integer \ monad/more_monads \ n-bit \ + num/theories/cv_compute/automation \ pred_set/src/more_theories probability \ rational real real/analysis res_quan/src ring/src \ search sort string \ From c0726a20e7c2e083c7d417a5fd0d7aff191b1cdc Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sun, 27 Aug 2023 22:47:09 +0200 Subject: [PATCH 15/15] Add some entry points --- .../theories/cv_compute/automation/cv_typesLib.sig | 13 +++++++++++-- .../theories/cv_compute/automation/cv_typesLib.sml | 14 ++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sig b/src/num/theories/cv_compute/automation/cv_typesLib.sig index 6a285e5939..fd91010165 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sig +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sig @@ -2,7 +2,16 @@ signature cv_typesLib = sig include Abbrev - (* manually add a from_to_theorem *) + (* --- main entry points --- *) + + (* ask for from_to info (derives missing info automatically) *) + val from_to_thm_for : hol_type -> thm + val from_term_for : hol_type -> term + val to_term_for : hol_type -> term + + (* --- less useful entry points --- *) + + (* manually add a from_to theorem *) val add_from_to_thm : thm -> unit (* returns a list of all from_to theorems *) @@ -12,7 +21,7 @@ sig val define_from_to : hol_type -> thm * thm * thm list val rec_define_from_to : hol_type -> thm list - (* define_from_to can raise this: *) + (* define_from_to can raise this *) exception Missing_from_to of hol_type end diff --git a/src/num/theories/cv_compute/automation/cv_typesLib.sml b/src/num/theories/cv_compute/automation/cv_typesLib.sml index 700e1872ce..7ef20ed6d0 100644 --- a/src/num/theories/cv_compute/automation/cv_typesLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typesLib.sml @@ -560,4 +560,18 @@ fun rec_define_from_to ty = let in loop acc ty end in loop [] ty end +(* --------------------------------------------------- * + Smart functions for retrieving/creating from_to + * --------------------------------------------------- *) + +fun from_to_thm_for ty = + from_to_for [] ty + handle Missing_from_to needs_ty => + let + val th = rec_define_from_to needs_ty + in from_to_thm_for ty end + +fun from_term_for ty = from_to_thm_for ty |> concl |> rator |> rand; +fun to_term_for ty = from_to_thm_for ty |> concl |> rand; + end