(* Explicit computations for hypermap_of_list *)
#load "str.cma";;
needs "../formal_lp/hypermap/ssreflect/list_hypermap_iso-compiled.hl";;
needs "../formal_lp/hypermap/computations/list_conversions2.hl";;
needs "../formal_lp/hypermap/computations/more_theory-compiled.hl";;
module List_hypermap_computations = struct
open Str;;
open List;;
open Misc_vars;;
open Arith_misc;;
open Arith_nat;;
open More_list_hypermap;;
open List_hypermap;;
open List_conversions;;
open List_hypermap_iso;;
let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
let TO_NUM = REWRITE_RULE[Arith_hash.NUM_THM] o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
let to_num = rand o concl o TO_NUM;;
(* Constants and variables *)
let hd_var_num = `hd:num` and
h_var_num = `h:num` and
h1_var_num = `h1:num` and
h2_var_num = `h2:num` and
t_var = `t:(num)list` and
x_var_pair = `x:num#num` and
d_var_pair = `d:num#num` and
h1_var_pair = `h1:num#num` and
h2_var_pair = `h2:num#num` and
acc_var = `acc:(num#num)list` and
f_var_fun = `f:num#num->num#num` and
l_cap_var = `L:((num)list)list` and
ll_var = `ll:((num)list)list` and
list_var = `list:(num#num)list` and
t_var_numnum_list = `t:(num#num)list` and
t_var_num_list = `t:(num)list` and
t_var_list_list = `t:((num)list)list` and
h_var_list = `h:(num)list` and
r_var_list = `r:(num)list` and
s1_var_list = `s1:(num)list` and
s2_var_list = `s2:(num)list`;;
let num_list_type = `:(num)list`;;
let num_list_list_type = `:((num)list)list`;;
let mem_const = `MEM:(num#num)->(num#num)list->bool` and
flatten_const = `flatten:((num#num)list)list -> (num#num)list`;;
let hypermap_of_list_const = `hypermap_of_list:((num)list)list->(num#num)hypermap` and
list_of_darts_const = `list_of_darts:((num)list)list->(num#num)list` and
list_of_edges_const = `list_of_edges:((num)list)list->((num#num)#(num#num))list` and
list_of_faces_const = `list_of_faces:((num)list)list->((num#num)list)list` and
list_of_nodes_const = `list_of_nodes:((num)list)list->((num#num)list)list` and
list_of_elements_const = `list_of_elements:((num)list)list->(num)list` and
good_list_const = `good_list:((num)list)list->bool` and
good_list_nodes_const = `good_list_nodes:((num)list)list->bool`;;
let num_pair_hash tm =
let ltm, rtm = dest_pair tm in
Arith_cache.num_tm_hash ltm ^ "," ^ Arith_cache.num_tm_hash rtm;;
let build_term_rewrite tm lhs =
let rec build_rewrite tm =
if tm = lhs then
(fun th -> th), true
else
match tm with
| Comb (l_tm, r_tm) ->
let l_f, l_flag = build_rewrite l_tm and
r_f, r_flag = build_rewrite r_tm in
if l_flag then
if r_flag then
(fun th -> MK_COMB (l_f th, r_f th)), true
else
(fun th -> AP_THM (l_f th) r_tm), true
else
if r_flag then
(fun th -> AP_TERM l_tm (r_f th)), true
else
I, false
| Abs (var_tm, b_tm) ->
let b_f, b_flag = build_rewrite b_tm in
if b_flag then
(fun th -> ABS var_tm (b_f th)), true
else
I, false
| _ -> I, false in
let f, flag = build_rewrite tm in
if flag then f else (fun th -> REFL tm);;
(* eq_th = |- lhs = rhs; rewrites exact occurrences of lhs in tm and returns |- tm = tm[lhs/rhs] *)
let term_rewrite tm eq_th =
let lhs, _ = dest_eq (concl eq_th) in
build_term_rewrite tm lhs eq_th;;
(*
let tm = `(x + 2) * 2 = 0 /\ (\y. (x + 2) * y) 3 = 2` and
th = ARITH_RULE `x + 2 = 1 * 2 + x`;;
let f = build_term_rewrite tm `x + 2`;;
term_rewrite tm th;;
f th;;
PURE_REWRITE_CONV[th] tm;;
(* 0.304 *)
test 10000 (term_rewrite tm) th;;
(* 0.216 *)
test 10000 f th;;
(* 2.808 *)
test 10000 (PURE_REWRITE_CONV[th]) tm;;
*)
(* example of java style string from hypermap generator. *)
let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;
let test_string = "149438122187 18 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 4 3 6 4 8 3 8 4 3 3 8 3 9 3 9 3 2 3 9 2 10 3 10 2 11 3 11 2 1 3 11 1 0 3 11 0 7 3 10 11 7 3 10 7 12 3 12 7 6 3 12 6 8 3 12 8 9 3 9 10 12 ";;
(* conversion to list. e.g. convert_to_list pentstring *)
let convert_to_list =
let split_sp= Str.split (regexp " +") in
let strip_ = global_replace (regexp "_") "" in
let rec movelist n (x,a) =
if n = 0 then (x,a) else
match x with
| [] -> failwith "convert_to_list"
| y::ys -> movelist (n-1) (ys, y::a) in
let getone (x,a) = match x with
| [] -> ([],a)
| y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
let rec getall (x,a) =
if (x=[]) then (x,a) else getall (getone (x,a)) in
fun s ->
let h::ss = (split_sp (strip_ s)) in
let _::ns = map int_of_string ss in
let (_,a) = getall (ns,[]) in
(h,rev (map rev a));;
let create_hol_list ll =
let s1 = map (map mk_small_numeral) ll in
let s2 = map (fun l -> mk_list (l, num_type)) s1 in
mk_list (s2, num_list_type);;
let create_hol_list_str =
create_hol_list o snd o convert_to_list;;
let test_list0 = create_hol_list_str test_string;;
let test_list = to_num test_list0;;
let print_num tm =
try
let n = raw_dest_hash tm in
let str = "'" ^ Num.string_of_num n in
Format.print_string str
with _ -> failwith "print_num";;
install_user_printer ("num", print_num);;
(********************************************)
let eval_mem_num_pair = eval_mem_univ pair_eq_conv_num;;
let mem_num_pair_conv = mem_conv_univ pair_eq_conv_num;;
(*************************************)
(* list_sum conversions *)
let list_sum_conv f_conv tm =
let ltm, f_tm = dest_comb tm in
let list_tm = rand ltm in
let list_ty = type_of list_tm in
let f_ty = type_of f_tm in
let ty = (hd o snd o dest_type) list_ty in
let f_var = mk_var("f", f_ty) and
h_var = mk_var("h", ty) and
t_var = mk_var("t", list_ty) in
let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
let list_sum_h = inst_t LIST_SUM_A_H and
list_sum_cons = inst_t LIST_SUM_A_CONS in
let rec list_sum_conv_raw = fun h_tm t_tm ->
if (is_comb t_tm) then
let h_tm', t_tm' = dest_comb t_tm in
let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
let ltm, rtm = dest_comb(rand(concl th0)) in
let plus_op, fh_tm = dest_comb ltm in
let f_th = f_conv fh_tm in
let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
TRANS th0 th2
else
let th0 = INST[h_tm, h_var] list_sum_h in
let f_th = f_conv (rand(concl th0)) in
TRANS th0 f_th in
if (is_comb list_tm) then
let h_tm, t_tm = dest_comb list_tm in
list_sum_conv_raw (rand h_tm) t_tm
else
inst_t LIST_SUM_A_EMPTY;;
(*********************************)
(* e_list conversions *)
let eval_e_list_num =
let th0 = prove(`
e_list (x:num,y:num) = y,x`,
REWRITE_TAC[
e_list]) in
fun d_tm ->
let ltm, y_tm = dest_comb d_tm in
let x_tm = rand ltm in
INST[x_tm, x_var_num; y_tm, y_var_num]
th0;;
let GOOD_LIST_COND3_EMPTY = prove(`
ALL (\d:num#num.
MEM (
SND d,
FST d) list) [] <=> T`,
REWRITE_TAC[
ALL]) and
GOOD_LIST_COND3_CONS_T = (UNDISCH_ALL o prove)(`(
MEM (y,x) list <=> T) ==>
(
ALL (\d:num#num.
MEM (
SND d,
FST d) list) (CONS (x,y) t) <=>
ALL (\d:num#num.
MEM (
SND d,
FST d) list) t)`, SIMP_TAC[
ALL]) and
GOOD_LIST_COND3_CONS_F = (UNDISCH_ALL o prove)(`(
MEM (y,x) list <=> F) ==>
(
ALL (\d:num#num.
MEM (
SND d,
FST d) list) (CONS (x,y) t) <=> F)`,
SIMP_TAC[
ALL]);;
let th_T = prove(`(\l. ~(l = [])) ((h:num) :: t) <=> T`,
REWRITE_TAC[
NOT_CONS_NIL]) and
th_F = prove(`(\l. ~(l = [])) ([]:(num)list) <=> F`, REWRITE_TAC[]) in
let test_f tm =
let list_tm = rand tm in
if is_comb list_tm then
let h_tm', t_tm = dest_comb list_tm in
INST[rand h_tm', h_var_num; t_tm, t_var_num_list]
th_T
else
th_F in
fun tm ->
all_conv_univ test_f tm;;