diff --git a/compiler/bootstrap/translation/caml_lexProgScript.sml b/compiler/bootstrap/translation/caml_lexProgScript.sml index 093f1ce40d..7dbb382343 100644 --- a/compiler/bootstrap/translation/caml_lexProgScript.sml +++ b/compiler/bootstrap/translation/caml_lexProgScript.sml @@ -11,6 +11,7 @@ open preamble caml_lexTheory; open parserProgTheory ml_translatorLib ml_translatorTheory; val _ = translation_extends "parserProg"; +val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "caml_lexProg"); (* ------------------------------------------------------------------------- * Translator setup @@ -169,6 +170,6 @@ val r = translate scan_float_or_int_def; val r = translate (caml_lexTheory.next_sym_def |> REWRITE_RULE [GSYM sub_check_def]); val r = translate caml_lexTheory.lexer_fun_def; - +val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE); val () = ml_translatorLib.clean_on_exit := true; diff --git a/compiler/bootstrap/translation/reg_allocProgScript.sml b/compiler/bootstrap/translation/reg_allocProgScript.sml index c918a94a3b..07b217f4e9 100644 --- a/compiler/bootstrap/translation/reg_allocProgScript.sml +++ b/compiler/bootstrap/translation/reg_allocProgScript.sml @@ -20,6 +20,8 @@ open basisProgTheory val _ = temp_delsimps ["NORMEQ_CONV"] val _ = translation_extends "pancake_parseProg"; +val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "reg_allocProg"); + val _ = ml_translatorLib.use_string_type true; val _ = ml_translatorLib.use_sub_check true; (* @@ -452,4 +454,5 @@ val _ = disable_astPP() *) +val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE); val _ = (ml_translatorLib.clean_on_exit := true); diff --git a/translator/alist_tree2Lib.sig b/translator/alist_tree2Lib.sig new file mode 100644 index 0000000000..d8d0f28506 --- /dev/null +++ b/translator/alist_tree2Lib.sig @@ -0,0 +1,52 @@ +(* Code to recall that some partial functions (of type 'a -> 'b option) +can be represented as sorted alists, and derive a fast conversion on +applications of those functions. *) + +signature alist_tree2Lib = sig + +include Abbrev + +(* Syntax *) +val alookup_tm : term; +val option_choice_tm : term; +val repr_tm : term; + +(* The repr set type *) +type 'a alist_reprs + +(* + Representations of partial functions using sorted trees. + Requires a relation R and a theorem that shows + it is irreflexive and transitive. The destructor maps terms + of the domain type to some type that can be sorted in ML. + The conversion must prove R x y for any x, y where x is + sorted before y by the destructor and comparison. +*) +val mk_alist_reprs : thm -> conv -> (term -> 'a) + -> (('a * 'a) -> order) -> 'a alist_reprs + +(* + The representation set contains representations of various + partial functions, initially none. +*) +val peek_functions_in_rs : 'a alist_reprs -> term list + +(* + Adds a function's representation. + + Requires a theorem f = rhs with a valid rhs. + A valid rhs is: + - ALOOKUP xs + - a function g in the repr set. + - option_choice_f of two valid rhs values +*) +val add_alist_repr : 'a alist_reprs -> thm -> unit + +(* + Converts f x to a concrete value (SOME y/NONE) + for functions f in the repr set. +*) +val reprs_conv : 'a alist_reprs -> conv + +end + diff --git a/translator/alist_tree2Lib.sml b/translator/alist_tree2Lib.sml new file mode 100644 index 0000000000..180e0b68a6 --- /dev/null +++ b/translator/alist_tree2Lib.sml @@ -0,0 +1,398 @@ +(* + Code to recall that some partial functions (of type 'a -> 'b option) + can be represented as sorted alists, and derive a fast conversion on + applications of those functions. +*) +structure alist_tree2Lib :> alist_tree2Lib = +struct + +open HolKernel Parse boolLib simpLib bossLib + +open alist_treeTheory comparisonTheory + +(* Copied from Drule.sml faster than ISPECL for subtituting big terms*) +local + fun strip [] _ = [] (* Returns a list of (pat,ob) pairs. *) + | strip (tm :: tml) M = + let + val (Bvar, Body) = dest_forall M + in + (type_of Bvar, type_of tm)::strip tml Body + end + fun merge [] theta = theta + | merge ((x as {redex, residue})::rst) theta = + case subst_assoc (equal redex) theta of + NONE => x :: merge rst theta + | SOME rdue => if residue = rdue then merge rst theta + else raise ERR "ISPECL" "" + fun err s = raise ERR "ISPECL" s +in + fun ISPECL [] = I + | ISPECL [tm] = ISPEC tm + | ISPECL tms = + fn th => + let + val pairs = + strip tms (concl th) + handle HOL_ERR _ => err "list of terms too long for theorem" + val inst = + rev_itlist + (fn (pat, ob) => fn ty_theta => + let + val theta = Type.match_type pat ob + in + merge theta ty_theta + end) pairs [] + handle HOL_ERR _ => err "can't type-instantiate input theorem" + val genvars = List.map (genvar o type_of) tms + val ss = ListPair.map (op |->) (genvars,tms) + in + INST_TYPE inst th + |> SPECL genvars + |> INST ss + handle HOL_ERR _ => err "type variable free in assumptions" + end +end + +(* Syntax *) + +val alookup_tm = prim_mk_const {Name = "ALOOKUP", Thy = "alist"} + +fun mkc nm = prim_mk_const {Name = nm, Thy = "alist_tree"} + +val count_append_tm = mkc "count_append" +val is_insert_tm = mkc "is_insert" +val option_choice_tm = mkc "option_choice_f" +val is_lookup_tm = mkc "is_lookup" +val repr_tm = mkc "sorted_alist_repr" + +(* trivia *) +val err = mk_HOL_ERR "alist_treeLib" + +(* the repr set object *) +datatype 'a alist_reprs = AList_Reprs of {R_thm: thm, conv: conv, + dest: term -> 'a, cmp: ('a * 'a) -> order, + dict: (term, thm) Redblackmap.dict ref} + +fun mk_alist_reprs R_thm conv dest cmp + = AList_Reprs {R_thm = R_thm, conv = conv, cmp = cmp, + dest = dest, dict = ref (Redblackmap.mkDict Term.compare)} + +fun peek_functions_in_rs (AList_Reprs inn_rs) + = Redblackmap.listItems (! (#dict inn_rs)) |> map fst + +fun peek_repr (AList_Reprs inn_rs) tm = Redblackmap.peek (! (#dict inn_rs), tm) + +(* constructing is_insert thms *) + +fun find_key_rec is_last [] = raise Empty + | find_key_rec is_last (t :: ts) = if listSyntax.is_nil t + then find_key_rec is_last ts + else let + val (f, xs) = strip_comb t + val do_rev = if is_last then rev else I + in if same_const f count_append_tm + then find_key_rec is_last (do_rev (tl xs) @ ts) + else hd (do_rev (fst (listSyntax.dest_list t))) end + +fun hd_key t = find_key_rec false [t] |> pairSyntax.dest_pair |> fst +fun last_key t = find_key_rec true [t] |> pairSyntax.dest_pair |> fst + +fun mk_singleton x = listSyntax.mk_list ([x], type_of x) + +val simp_count_append = SIMP_CONV bool_ss [count_append_HD_LAST, pairTheory.FST] + +fun assume_prems thm = if not (is_imp (concl thm)) then thm + else let + val thm = CONV_RULE (RATOR_CONV simp_count_append) thm + val l_asm = fst (dest_imp (concl thm)) + val prem = if l_asm ~~ T then TRUTH else ASSUME l_asm + in + assume_prems (MP thm prem) + end + +fun do_inst_mp insts mp_thm arg_thm = let + val (prem, _) = dest_imp (concl mp_thm) + fun rerr e s = let + val m = s ^ ": " ^ message_of e + in print ("error in do_inst_mp: " ^ m ^ "\n"); + print_thm mp_thm; print "\n"; print_thm arg_thm; print "\n"; + raise (err "do_inst_mp" m) end + val (more_insts, ty_insts) = match_term prem (concl arg_thm) + handle HOL_ERR e => rerr e "match_term" + val ty_i_thm = INST_TYPE ty_insts mp_thm + val ithm = INST (more_insts @ insts) ty_i_thm + handle HOL_ERR e => rerr e "INST" + in MP ithm arg_thm handle HOL_ERR e => rerr e "MP" end + +fun build_insert (dest : term -> 'a) cmp R k x = + let + val dest_k = dest k + fun chk thm = if same_const is_insert_tm (fst (strip_comb (concl thm))) + then thm + else (print "Not an insert_tm:\n"; print_thm thm; print "\n"; + raise (err "build_insert" "check")) + val pp = chk o assume_prems + fun build t = if listSyntax.is_nil t + then pp (ISPECL [R, k, x] is_insert_to_empty) + else if listSyntax.is_cons t then let + val (xs, _) = listSyntax.dest_list t + val _ = length xs = 1 orelse raise (err "build_insert" "malformed") + val v = hd xs + in case cmp (dest_k, dest (fst (pairSyntax.dest_pair v))) of + EQUAL => pp (ISPECL [R, k, x, v] is_insert_overwrite) + | GREATER => pp (ISPECL [R, k, x, t] is_insert_far_right) + | LESS => pp (ISPECL [R, k, x, t] is_insert_far_left) + end else let + val (f, xs) = strip_comb t + val _ = same_const count_append_tm f + orelse raise (err "build_insert" "unknown") + val (n, l, r) = case xs of [n, l, r] => (n, l, r) + | _ => raise (err "build_insert" "num args") + fun vsub nm v = [mk_var (nm, type_of v) |-> v] + in if not (cmp (dest_k, dest (hd_key r)) = LESS) + then do_inst_mp (vsub "l" l) (SPEC n is_insert_r) (build r) + else if cmp (dest_k, dest (last_key l)) = GREATER + then ISPECL [R, n, k, x] is_insert_centre + |> INST (vsub "l" l @ vsub "r" r) |> pp + else do_inst_mp (vsub "r" r) (SPEC n is_insert_l) (build l) + end + in build end + +fun prove_assum_by_conv conv thm = let + val (x,y) = dest_imp (concl thm) + val thm = CONV_RULE ((RATOR_CONV o RAND_CONV) conv) thm + in MP thm TRUTH handle HOL_ERR e => + (print "Failed to prove assum by conv:\n"; + print_term x; + print "\n -- reduced to:\n"; + print_term (fst (dest_imp (concl thm))); + raise HOL_ERR e) + end + +(* balancing count_append trees *) +fun get_depth tm = let + val (f, xs) = strip_comb tm + in if same_const f count_append_tm + then numSyntax.int_of_term (hd xs) + else if listSyntax.is_cons tm then 1 + else raise (err "get_depth" "unknown") + end + +fun balance iter bias tm = if iter > 1000 then + (print "error: looping balance\n"; print_term tm; + raise (err "balance" "looping")) + else let + val (f, xs) = strip_comb tm + val _ = same_const f count_append_tm orelse raise UNCHANGED + val _ = is_arb (hd xs) orelse bias <> "N" orelse raise UNCHANGED + val step_conv = (RAND_CONV (balance 0 "N")) + THENC (RATOR_CONV (RAND_CONV (balance 0 "N"))) + val thm = QCONV step_conv tm + val tm = rhs (concl thm) + val l_sz = get_depth (rand (rator tm)) + val r_sz = get_depth (rand tm) + val reb = if l_sz > (r_sz + 1) orelse (bias = "R" andalso l_sz > r_sz) + then "R" + else if r_sz > (l_sz + 1) orelse (bias = "L" andalso r_sz > l_sz) + then "L" else "N" + val conv1 = if reb = "R" then RATOR_CONV (RAND_CONV (balance 0 "L")) + else if reb = "L" then RAND_CONV (balance 0 "R") else ALL_CONV + val conv2 = if reb = "R" then REWR_CONV balance_r + else if reb = "L" then REWR_CONV balance_l else ALL_CONV + val thm = CONV_RULE (QCONV (RHS_CONV (conv1 THENC conv2 THENC step_conv))) thm + val tm = rhs (concl thm) + val l_sz = get_depth (rand (rator tm)) + val r_sz = get_depth (rand tm) + val sz = numSyntax.term_of_int (1 + Int.max (l_sz, r_sz)) + val set = REWR_CONV (set_count |> SPEC sz) + val final = if Int.abs (l_sz - r_sz) < 2 then set else balance (iter + 1) "N" + in CONV_RULE (RHS_CONV final) thm end + +fun prove_insert R conv dest cmp k x al = let + val thm = build_insert dest cmp R k x al + fun prove thm = if not (is_imp (concl thm)) then thm + else prove (prove_assum_by_conv conv thm) + in thm |> DISCH_ALL |> prove |> CONV_RULE (RAND_CONV (balance 0 "N")) end + +(* making repr theorems *) + +fun mk_insert_repr (AList_Reprs rs) prev_repr k_x = let + val (k, x) = pairSyntax.dest_pair k_x + val (R, al) = case strip_comb (concl prev_repr) + of (_, [R, al, _]) => (R, al) + | _ => raise (err "mk_insert_repr" "unexpected") + val insert = prove_insert R (#conv rs) (#dest rs) (#cmp rs) k x al + in MATCH_MP repr_insert (CONJ prev_repr insert) end + +fun dest_alookup_single tm = let + val (f, xs) = strip_comb tm + in if not (length xs = 1 andalso same_const f alookup_tm) + then NONE + else if listSyntax.is_nil (hd xs) then SOME NONE + else case total listSyntax.dest_cons (hd xs) of + SOME (y, ys) => if listSyntax.is_nil ys then SOME (SOME y) else NONE + | NONE => NONE + end + +fun mk_repr_step rs tm = let + val (AList_Reprs inn_rs) = rs + val (f, xs) = strip_comb tm + val is_short = + not (option_eq (option_eq aconv) (dest_alookup_single tm) NONE) + val is_merge = same_const option_choice_tm f + val is_repr_merge = is_merge andalso (case peek_repr rs (hd xs) of + SOME _ => true | NONE => false) + val (is_insert, insert_tm) = if not is_merge then (false, T) + else case dest_alookup_single (hd xs) of + SOME (SOME t) => (true, t) | _ => (false, T) + in if is_short + then MATCH_MP (ISPEC (hd xs) alist_repr_refl) (#R_thm inn_rs) + |> prove_assum_by_conv (SIMP_CONV list_ss [sortingTheory.SORTED_DEF]) + else if is_insert + then mk_insert_repr rs (mk_repr rs (rand tm)) insert_tm + else if is_repr_merge + then let + val l_repr_thm = mk_repr rs (hd xs) + val l_repr_al = rand (rator (concl l_repr_thm)) + val look = mk_icomb (alookup_tm, l_repr_al) + val half_repr = list_mk_icomb (option_choice_tm, [look, List.last xs]) + val next_repr = mk_repr rs half_repr + in MATCH_MP alist_repr_choice_trans_left (CONJ l_repr_thm next_repr) end + else CHANGED_CONV (SIMP_CONV bool_ss [alookup_to_option_choice, + option_choice_f_assoc, alookup_empty_option_choice_f, + count_append_def, alookup_append_option_choice_f, + empty_is_ALOOKUP]) tm + handle HOL_ERR _ => raise err "mk_repr_step" + ("no progress from SIMP_CONV: " ^ Parse.term_to_string tm) + end +and mk_repr_known_step rs tm = + case peek_repr rs tm of + SOME thm => thm + | NONE => mk_repr_step rs tm +and mk_repr rs tm = let + val thm = mk_repr_known_step rs tm + in if is_eq (concl thm) + then mk_repr rs (rhs (concl thm)) + |> CONV_RULE (RAND_CONV (REWR_CONV (SYM thm))) + else thm + end + +fun add_alist_repr rs thm = let + val AList_Reprs inn_rs = rs + val (f, rhs) = dest_eq (concl thm) + val repr_thm = case peek_repr rs rhs of + SOME rhs_thm => if is_eq (concl rhs_thm) + then TRANS thm rhs_thm + else thm + | NONE => (mk_repr rs rhs + |> CONV_RULE (RAND_CONV (REWR_CONV (SYM thm)))) + in + #dict inn_rs := Redblackmap.insert (! (#dict inn_rs), f, repr_thm) + end + +fun timeit msg f v = let + val start = Portable.timestamp () + val r = f v + val time = Time.-(Portable.timestamp (), start) + in print ("Time to " ^ msg ^ ": " ^ Portable.time_to_string time ^ "\n"); + r end + +(* testing *) + +fun test_rs () = let + val thm1 = DB.fetch "comparison" "good_cmp_Less_irrefl_trans" + val thm2 = DB.fetch "comparison" "num_cmp_good" + val R_thm = MATCH_MP thm1 thm2 + in mk_alist_reprs R_thm EVAL numSyntax.int_of_term Int.compare end + +fun test_mk_alookup ns = let + open numSyntax + val _ = I + fun f i = ((i * 157) mod 1000) + fun el i = pairSyntax.mk_pair (term_of_int (f i), term_of_int i) + in mk_icomb (alookup_tm, listSyntax.mk_list (map el ns, type_of (el 0))) end + +fun test_200 rs = let + val al1 = test_mk_alookup (upto 1 200) + val al2 = test_mk_alookup [1, 4, 3] + val merge = list_mk_icomb (option_choice_tm, [al1, al2]) + in mk_repr rs merge end + +(* +val rs = test_rs () +val thm_200 = timeit "build repr" test_200 rs +*) + +(* proving and using is_lookup thms *) + +fun build_lookup (dest : term -> 'a) cmp R k = + let + val dest_k = dest k + fun chk thm = if same_const is_lookup_tm (fst (strip_comb (concl thm))) + then thm + else (print "Not a lookup_tm:\n"; print_thm thm; print "\n"; + raise (err "build_lookup" "check")) + val pp = chk o assume_prems + fun build t = if listSyntax.is_nil t + then pp (ISPECL [R, k, t] is_lookup_empty) + else if listSyntax.is_cons t then let + val (xs, _) = listSyntax.dest_list t + val _ = length xs = 1 orelse raise (err "build_insert" "malformed") + val (k', v) = pairSyntax.dest_pair (hd xs) + in case cmp (dest_k, dest k') of + EQUAL => pp (ISPECL [R, k, k', v] is_lookup_hit) + | GREATER => pp (ISPECL [R, k, k', v] is_lookup_far_right) + | LESS => pp (ISPECL [R, k, k', v] is_lookup_far_left) + end else let + val (f, xs) = strip_comb t + val _ = same_const count_append_tm f + orelse raise (err "build_lookup" "unknown") + val (n, l, r) = case xs of [n, l, r] => (n, l, r) + | _ => raise (err "build_lookup" "num args") + fun vsub nm v = [mk_var (nm, type_of v) |-> v] + in if not (cmp (dest_k, dest (hd_key r)) = LESS) + then do_inst_mp (vsub "l" l) (SPEC n is_lookup_r) (build r) + else if cmp (dest_k, dest (last_key l)) = GREATER + then pp (ISPECL [R, n, l, r, k] is_lookup_centre) + else do_inst_mp (vsub "r" r) (SPEC n is_lookup_l) (build l) + end + in build end + +fun prove_lookup R conv dest cmp k al = let + val thm = build_lookup dest cmp R k al + fun prove thm = if not (is_imp (concl thm)) then thm + else prove (prove_assum_by_conv conv thm) + in thm |> DISCH_ALL |> prove end + +fun repr_prove_lookup conv dest cmp repr_thm k = let + val (f, xs) = strip_comb (concl repr_thm) + val f = same_const f repr_tm orelse + raise (err "repr_prove_lookup" "unexpected") + val (R, al, f) = case xs of [R, al, f] => (R, al, f) + | _ => raise (err "repr_prove_lookup" "num args") + val lookup = prove_lookup R conv dest cmp k al + in MATCH_MP lookup_repr (CONJ repr_thm lookup) end + +fun reprs_conv rs tm = let + val AList_Reprs inn_rs = rs + val (f, x) = dest_comb tm handle HOL_ERR _ => raise UNCHANGED + val repr_thm = case peek_repr rs f of + NONE => raise UNCHANGED | SOME thm => thm + in if is_eq (concl repr_thm) + then (RATOR_CONV (REWR_CONV repr_thm) THENC reprs_conv rs) tm + else repr_prove_lookup (#conv inn_rs) (#dest inn_rs) (#cmp inn_rs) + repr_thm x + end + +fun extract_test f rs i = mk_comb (f, numSyntax.term_of_int i) |> reprs_conv rs + +fun extract_test_1000 rs = let + val alookup = test_mk_alookup (upto 1 300) + val f = mk_var ("f", type_of alookup) + val f_def = new_definition ("f", mk_eq (f, alookup)) + val res1 = timeit "add def" (add_alist_repr rs) f_def + val res2 = timeit "map extract" (map (extract_test f rs)) (upto 1 1000) + in res2 end + +end diff --git a/translator/ml_progLib.sml b/translator/ml_progLib.sml index dc70a03c9f..f11b99aba7 100644 --- a/translator/ml_progLib.sml +++ b/translator/ml_progLib.sml @@ -6,7 +6,7 @@ structure ml_progLib :> ml_progLib = struct open preamble; -open ml_progTheory astSyntax packLib alist_treeLib comparisonTheory; +open ml_progTheory astSyntax packLib alist_tree2Lib comparisonTheory; fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f @@ -33,7 +33,7 @@ local val nsLookup_repr_set = let val irrefl_thm = MATCH_MP good_cmp_Less_irrefl_trans string_cmp_good - in alist_treeLib.mk_alist_reprs irrefl_thm EVAL + in alist_tree2Lib.mk_alist_reprs irrefl_thm EVAL str_dest (list_compare Int.compare) end @@ -106,8 +106,9 @@ val nsLookup_conv_arg1_xs = [boolSyntax.conjunction, boolSyntax.disjunction, fun nsLookup_arg1_conv conv tm = let val (f, xs) = strip_comb tm val _ = exists (same_const f) nsLookup_conv_arg1_xs orelse raise UNCHANGED - in if length xs > 1 then RATOR_CONV (nsLookup_arg1_conv conv) tm - else if length xs = 1 then RAND_CONV conv tm + val len = length xs + in if len > 1 then RATOR_CONV (nsLookup_arg1_conv conv) tm + else if len = 1 then RAND_CONV conv tm else raise UNCHANGED end @@ -120,9 +121,10 @@ val nsLookup_rewrs = List.concat (map BODY_CONJUNCTS nsLookup_Short_Bind, nsLookup_Mod1_Bind, nsLookup_merge_env_eqs, nsLookup_empty_eqs, alistTheory.ALOOKUP_def]) +val nsLookup_rewrs_conv = GEN_REWRITE_CONV I Rewrite.empty_rewrites nsLookup_rewrs + fun nsLookup_conv tm = REPEATC (BETA_CONV ORELSEC FIRST_CONV - (map REWR_CONV nsLookup_rewrs - @ map (RATOR_CONV o REWR_CONV) nsLookup_rewrs + ([nsLookup_rewrs_conv,RATOR_CONV nsLookup_rewrs_conv] @ map QCHANGED_CONV [nsLookup_arg1_conv nsLookup_conv, nsLookup_pf_conv])) tm @@ -272,24 +274,32 @@ fun let_v_abbrev nm conv op_nm (th, ML_code (ss, envs, vs, ml_th)) = let (* val tm = ``!n. n = 5 ==> n < 8`` *) +local +val conv1 = REWR_CONV UNWIND_FORALL_THM1 +val conv2 = REWR_CONV UNWIND_FORALL_THM2 +in fun unwind_forall_conv tm = let val (v,_) = dest_forall tm in (QUANT_CONV (RAND_CONV (UNBETA_CONV v)) - THENC (REWR_CONV UNWIND_FORALL_THM1 ORELSEC - REWR_CONV UNWIND_FORALL_THM2) + THENC (conv1 ORELSEC conv2) THENC BETA_CONV) tm end +end +local +val conv1 = REWR_CONV SOME_11 +in fun forall_nsLookup_upd nm (th,x) = (CONV_RULE (QUANT_CONV ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) (nsLookup_conv THENC EVAL) - THENC (RATOR_CONV o RAND_CONV) (REWR_CONV SOME_11)) + THENC (RATOR_CONV o RAND_CONV) (conv1)) THENC unwind_forall_conv) th, x) handle HOL_ERR _ => failwith "forall_nsLookup_upd: nsLookup failed to produce SOME" +end fun solve_ml_imp f nm (th, ML_code code) = let val msg = "solve_ml_imp: " ^ nm ^ ": not imp" diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index fc0a5d865f..2ebfa944f2 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -466,9 +466,8 @@ in fun mk_cons_name tm = let val (_, ty) = strip_fun (type_of tm) - val info = Option.valOf (TypeBase.fetch ty) - val (thyn, tyn) = TypeBasePure.ty_name_of info - val name = term_to_string tm + val {Thy = thyn,Tyop = tyn,...} = Type.dest_thy_type ty + val name = dest_const tm |> fst in (* separating with underscores is more prone to name clashes *) String.concat ["%%", thyn, "%%", tyn, "%%", name, "%%"] @@ -1786,17 +1785,14 @@ val th = inv_defs |> map #2 |> hd val input_var = filter (fn x => not (tmem x (free_vars cases_tm))) (free_vars exp) |> hd val ret_ty = type_of exp val xs = rev (map rand (find_terms is_eq (concl case_th))) - fun add_nums [] = [] - | add_nums (x::xs) = (x,length xs+1) :: add_nums xs - val ys = rev (add_nums (rev (zip (map snd vs) xs))) + fun add_nums xs = mapi (fn i => fn x => (x,i + 1)) xs + val ys = add_nums (zip (map snd vs) xs) fun str_tl s = implode (tl (explode s)) - fun list_app x [] = x - | list_app x (y::ys) = list_app (mk_comb(x,y)) ys val start_mk_vars = start_timing "mk_vars" fun mk_vars ((f,tm),n) = let val xs = rev (free_vars tm) - val fxs = list_app f xs - val pxs = list_app (mk_var("b" ^ int_to_string n,list_mk_type xs bool)) xs + val fxs = list_mk_comb(f, xs) + val pxs = list_mk_comb(mk_var("b" ^ int_to_string n,list_mk_type xs bool), xs) val xs = map (fn x => let val s = str_tl (fst (dest_var x)) in (x,mk_var("n" ^ s,stringSyntax.string_ty), mk_var("v" ^ s,v_ty)) end) xs @@ -2746,7 +2742,7 @@ fun split_let_and_conv tm = let THEN REWRITE_TAC []) in lemma end handle HOL_ERR _ => NO_CONV tm; -fun mk_fun_type ty1 ty2 = mk_type("fun",[ty1,ty2]) +fun mk_fun_type ty1 ty2 = ty1 --> ty2 fun list_mk_fun_type [ty] = ty | list_mk_fun_type (ty1::tys) = @@ -2807,9 +2803,7 @@ fun get_induction_for_def def = let val step = mk_abs(v,list_mk_forall(xs @ ys,prop)) in (P,(goal,step)) end val res = map goal_step xs - fun ISPEC_LIST [] th = th - | ISPEC_LIST (x::xs) th = ISPEC_LIST xs (ISPEC x th) - val ind = ISPEC_LIST (map (snd o snd) res) raw_ind + val ind = ISPECL (map (snd o snd) res) raw_ind |> CONV_RULE (DEPTH_CONV BETA_CONV) val goal1 = ind |> concl |> dest_imp |> snd val goal2 = list_mk_conj (map (fst o snd) res) @@ -3444,9 +3438,9 @@ fun hol2deep tm = if (tm ~~ TRUE) then Eval_Val_BOOL_TRUE else if (tm ~~ FALSE) then Eval_Val_BOOL_FALSE else (* data-type constructor *) - inst_cons_thm tm hol2deep handle HOL_ERR _ => + if can cons_for tm then inst_cons_thm tm hol2deep else (* data-type pattern-matching *) - inst_case_thm tm hol2deep handle HOL_ERR _ => + if can TypeBase.dest_case tm then inst_case_thm tm hol2deep else (* recursive pattern *) if can match_rec_pattern tm then let val (lhs,fname,pre_var) = match_rec_pattern tm @@ -3475,6 +3469,7 @@ fun hol2deep tm = val result = apply_arrow h ys in check_inv "rec_pattern" tm result end else (* previously translated term *) + if can lookup_abs_v_thm tm then let val th = lookup_abs_v_thm tm val _ = check_no_ind_assum tm th @@ -3484,7 +3479,7 @@ fun hol2deep tm = val (ss,ii) = match_term res target handle HOL_ERR _ => match_term (rm_fix res) (rm_fix target) handle HOL_ERR _ => ([],[]) val result = INST ss (INST_TYPE ii th) - in check_inv "lookup_abs_v_thm" tm result end handle NotFoundVThm _ => + in check_inv "lookup_abs_v_thm" tm result end else (* previously translated term *) if can lookup_v_thm tm then let val th = lookup_v_thm tm @@ -3687,6 +3682,7 @@ fun hol2deep tm = val th2 = INST [v|->z] th2 val result = MATCH_MP Eval_Let (CONJ th1 th2) in check_inv "let" tm result end else + (* TODO stop recursively case spliting *) (* special pattern *) let fun pat_match pat tm = (match_term pat tm; rator pat) val r = pat_match MAP_pattern tm handle HOL_ERR _ =>