dev.hl

(* load_path := "/Users/monad/Work/git/compute-hol-light" :: !load_path;; *)
(* load_path := "/Users/monad/Work/git/formal_ineqs" :: !load_path;; *)
needs "tame/tame_defs.hl";;
needs "tame/tame_defs_unrolled.hl";;
needs "tests/common.hl";;
loadt "tame/tame_support.hl";;
loadt "tame/tame_db.hl";;

let rules = [
  "APPEND_UNROLL8", APPEND_UNROLL8, [];
  "map_of_DEF", map_of_DEF, [];
  "the_DEF", the_DEF, [];
  "is_none_DEF", is_none_DEF, [];
  "funpow_UNROLL5", funpow_UNROLL5, [];
  "nth_UNROLL15", nth_UNROLL15, [];
  "fold_DEF", fold_DEF, [];
  "rev_DEF", rev_DEF, [];
  "upt_DEF", upt_DEF, [];
  "zip_ALT", zip_ALT, [];
  "null_DEF", null_DEF, [];
  "last_DEF", last_DEF, [];
  "maps_UNROLL7", maps_UNROLL7, [];
  "foldl_DEF", foldl_DEF, [];
  "foldr_ALT", foldr_ALT, [];
  "concat_DEF", concat_DEF, [];
  "filter_DEF", filter_DEF, [];
  "member_DEF", member_DEF, [];
  "rotate1_DEF", rotate1_DEF, [];
  "rotate_ALT", rotate_ALT, [];
  "bool_to_num_DEF", bool_to_num_DEF, [];
  "count_UNROLL7", count_UNROLL7, [];
  "hd_DEF", hd_DEF, [];
  "tl_DEF", tl_DEF, [];
  "list_ex_DEF", list_ex_DEF, [];
  "remdups_DEF", remdups_DEF, [];
  "remove1_DEF", remove1_DEF, [];
  "map_UNROLL11", map_UNROLL11, [];
  "pred_list_UNROLL11", pred_list_UNROLL11, [];
  "replicate_DEF", replicate_DEF, [];
  "gen_length_DEF", gen_length_DEF, [];
  "map_filter_DEF", map_filter_DEF, [];
  "list_update_DEF", list_update_DEF, [];
  "all_interval_nat_DEF", all_interval_nat_DEF, [];
  "size_list_UNROLL15", size_list_UNROLL15, [];
  "fst_DEF", fst_DEF, [];
  "snd_DEF", snd_DEF, [];
  "mapAt_DEF", mapAt_DEF, [];
  "splitAtRec_DEF", splitAtRec_DEF, [];
  "splitAt_DEF", splitAt_DEF, [];
  "between_ALT", between_ALT, [];
  "minimall_ALT", minimall_ALT, [];
  "replace_DEF", replace_DEF, [];
  "removeKey_DEF", removeKey_DEF, [];
  "removeKeyList_DEF", removeKeyList_DEF, [];

  "vertices_face_DEF", vertices_face_DEF, [];
  "final_face_DEF", final_face_DEF, [];
  "faceListAt_DEF", faceListAt_DEF, [];
  "facesAt_DEF", facesAt_DEF, [];
  "tri_ALT", tri_ALT, [];
  "quad_ALT", quad_ALT, [];
  "faces_DEF", faces_DEF, [];
  "graph_ALT", graph_ALT, [];
  "degree_DEF", degree_DEF, [];
  "except_ALT", except_ALT, [];
  "finals_DEF", finals_DEF, [];
  "heights_DEF", heights_DEF, [];
  "height_DEF", height_DEF, [];
  "nextElem_ALT", nextElem_ALT, [];
  "setFinal_DEF", setFinal_DEF, [];
  "nextVertex_ALT", nextVertex_ALT, [];
  "neighbors_DEF", neighbors_DEF, [];
  "nonFinals_DEF", nonFinals_DEF, [];
  "vertextype_DEF", vertextype_DEF, [];
  "finalVertex_DEF", finalVertex_DEF, [];
  "final_graph_ALT", final_graph_ALT, [];
  "nextVertices_DEF", nextVertices_DEF, [];
  "countVertices_DEF", countVertices_DEF, [];
  "directedLength_DEF", directedLength_DEF, [];
  "vertices_graph_DEF", vertices_graph_DEF, [];

  "tame10_ALT", tame10_ALT, [];
  "tame11a_DEF", tame11a_DEF, [];
  "tame11b_DEF", tame11b_DEF, [];
  "tame12o_ALT", tame12o_ALT, [];
  "tame10ub_DEF", tame10ub_DEF, [];
  "excessTCount_DEF", excessTCount_DEF, [];
  "squanderTarget_DEF", squanderTarget_DEF, [];
  "squanderFace_ALT", squanderFace_ALT, [];
  "squanderVertex_ALT", squanderVertex_ALT, [];
  "maxGon_ALT", maxGon_ALT, [];
  "seed_DEF", seed_DEF, [];
  "duplicateEdge_DEF", duplicateEdge_DEF, [];
  "containsUnacceptableEdgeSnd_ALT", containsUnacceptableEdgeSnd_ALT, [];
  "containsUnacceptableEdge_ALT", containsUnacceptableEdge_ALT, [];
  "containsDuplicateEdge_DEF", containsDuplicateEdge_DEF, [];

  "alist_DEF", alist_DEF, [];
  "values_DEF", values_DEF, [];
  "lookup_DEF", lookup_DEF, [];
  "rem_alist_DEF", rem_alist_DEF, [];
  "update_DEF", update_DEF, [];

  "minimalFace_ALT", minimalFace_ALT, [];
  "minimalVertex_DEF", minimalVertex_DEF, [];
  "listSum_DEF", listSum_DEF, [];
  "heightsNewVertices_DEF", heightsNewVertices_DEF, [];
  "replacefacesAt_DEF", replacefacesAt_DEF, [];
  "split_face_ALT", split_face_ALT, [];
  "splitFace_ALT", splitFace_ALT, [];
  "makeFaceFinalFaceList_DEF", makeFaceFinalFaceList_DEF, [];
  "makeFaceFinal_DEF", makeFaceFinal_DEF, [];
  "subdivFacea_ALT", subdivFacea_ALT, [];
  "subdivFace_DEF", subdivFace_DEF, [];

  "enumAppend_DEF", enumAppend_DEF, [];
  "enumBase_DEF", enumBase_DEF, [];
  "enumerator_ALT", enumerator_ALT, [];
  "enum_ALT", enum_ALT, [];

  "hideDupsRec_DEF", hideDupsRec_DEF, [];
  "hideDups_DEF", hideDups_DEF, [];
  "indexToVertexList_DEF", indexToVertexList_DEF, [];
  "notame_DEF", notame_DEF, [];
  "excessAtType_ALT", excessAtType_ALT, [];
  "excessAt_DEF", excessAt_DEF, [];
  "faceSquanderLowerBound_DEF", faceSquanderLowerBound_DEF, [];
  "deleteAround_ALT", deleteAround_ALT, [];
  
  "excessNotAtRec_ALT", excessNotAtRec_ALT, [];
  "excessTable_ALT", excessTable_ALT, [];
  "excessNotAt_ALT", excessNotAt_ALT, [];
  "squanderLowerBound_DEF", squanderLowerBound_DEF, [];
  "polysizes_ALT", polysizes_ALT, [];
  "is_tame13a_ALT", is_tame13a_ALT, [];
  "generatePolygonTame_ALT", generatePolygonTame_ALT, [];
  "next_tame0_ALT", next_tame0_ALT, [];
  "is_tame_DEF", is_tame_DEF, [];
  "next_tame_ALT", next_tame_ALT, [];
  "worklist_tree_aux_DEF", worklist_tree_aux_DEF, [];
  "worklist_tree_ALT", worklist_tree_ALT, [];
  "nof_vertices_ALT", nof_vertices_ALT, [];

  "qsort_DEF", qsort_DEF, [];
  "hash_ALT", hash_ALT, [];
  "fgraph_DEF", fgraph_DEF, [];
  "merge_ALT", merge_ALT, [];
  "compat_DEF", compat_DEF, [];

  "pr_iso_test_rec_ALT", pr_iso_test_rec_ALT, [];
  "pr_iso_test_DEF", pr_iso_test_DEF, [];
  "iso_test_DEF", iso_test_DEF, [];
  "insert_mod_trie_ALT", insert_mod_trie_ALT, [];
  (* "insert_mod2_trie_DEF", insert_mod2_trie_DEF;
  "worklist_tree_coll_aux_trie_ALT", worklist_tree_coll_aux_trie_ALT;
  "worklist_tree_coll_trie_DEF", worklist_tree_coll_trie_DEF;
  "enum_filter_finals_ALT", enum_filter_finals_ALT; *)
  "tameEnumFilter_ALT", tameEnumFilter_ALT, [];

  "worklist_tree_bounded_ALT", worklist_tree_bounded_ALT, [];
  "tameEnumFilterBounded_DEF", tameEnumFilterBounded_DEF, [];
  "tameCountFinalsBounded_DEF", tameCountFinalsBounded_DEF, [];
];;

let db = add_thms (tame_default_db ~eliminate_abs:true ()) rules;;
let consts = dependencies db `tameEnumFilterBounded`;;
(* let consts = dependencies db `tameEnumFilterBounded` ~inst_types:false *)
set_extra_for_consts db (Extra_memo (Assoc_memo 10000)) [
(* set_extra_for_consts db (Extra_memo (Assoc_lru (10000, 2))) [ *)
(* set_extra_for_consts db (Extra_memo Hashtbl_memo) [ *)
  `size_list:(num)list->num`;
  `excessAtType`;
  `vertices_face`;
  `heightsNewVertices`;
  `upt`;
  `nextVertex`;
  `rev:(num)list->(num)list`;
  `APPEND:(num)list->(num)list->(num)list`;
  `nextVertices`;
  `member:(num)list->num->bool`;
  `enum`;
  `splitAtRec:num->(num)list->(num)list->(num)list#(num)list`;
  `map:(num->(num)list)->(num)list->((num)list)list`;
  `map:((num)list->(num)list)->((num)list)list->((num)list)list`;
  (* `bool_to_num`; *)
  (* `fst:num#num->num`; *)
  (* `is_none:(num#num)option->bool`; *)
  (* `final_face`; *)
  (* `nextElem:(num)list->num->num->num`; *)
  (* `nth:(num)list->num->num`; *)
  (* `faceListAt`; *)
  (* `filter:(num#num->bool)->(num#num)list->(num#num)list`; *)
  (* `removeKeyList:(num)list->(num#num)list->(num#num)list`; *)
  (* `nth:((face)list)list->num->(face)list`; *)
  (* `excessNotAtRec`; *)
];;

let () =
  set_extra_for_all db (Extra_counter 0);
  set_extra_for_names db (Extra_counter 100) ["worklist_tree_bounded"];
  (* set_rule db `(=):A->A->bool`; *)
  (* set_extra_for_all db Extra_arg_list; *)
  (* write_rules_names db "out.hl" const_names *)
  write_rules_consts db "tame/out.hl" consts;;
loadt "tame/out.hl";;

(* 40.714s *)
(* original: 0.0171s *)
(* ratio: 2381 *)

(* 26.144s with COND instead of AND/OR *)
(* 25.406s with new AND/OR *)
(* 23.614s with size_list_ALT with 15 cases *)
(* 18.631s with custom types (COND, f_EQ still use INST_TYPE) *)
(* 17.927s with custom types (including COND but without f_EQ) *)
(* 17.995s with custom types everywhere *)
(* 14.663s with nth_ALT with 10 cases *)
(* 14.538s with funpow_ALT2 with 5 cases *)
(* 14.487s with maps_ALT, count_ALT, map_ALT, pred_list_ALT *)
(* 9.915s with fast arithmetic *)
(* 9.859s with fast arithmetic + standardize *)
(* 9.797s with APPEND_UNROLL8 *)
(* 9.653s with nth_UNROLL15, maps_UNROLL7, count_UNROLL7 *)
(* 8.874s with memos *)
(* 3.275s with eliminate_abs and without memos *)
(* 3.246s with Weak_memo *)
(* 2.649s with Hashtbl_memo *)
(* 2.688s with Assoc_memo *)
(* 2.481s with eval_compile_tree *)
(* 2.574s with tail_rec (Assoc_memo) *)
(* reset_core_counters() *)
let () = ();;
let () =
  reset_all_counters();
  clear_arg_lists();
  clear_all_memos();;
test 1 (f_tameEnumFilterBounded (numeral `0`) (numeral `100`)) None;;
test 1 (f_tameEnumFilterBounded (numeral `0`)) (numeral `100`);;

(* 397s with Weak_memo *)
(* 255s with Hashtbl_memo *)
(* 262s with Assoc_memo *)
(* 263s with Assoc_lru 10000, 2 *)
(* 230s with tail_rec (Assoc_memo) *)
test 1 (f_tameEnumFilterBounded (numeral `0`) (numeral `10000`)) None;;
test 1 (f_tameEnumFilterBounded (numeral `0`)) (numeral `10000`);;

(* 518s with Hashtbl_memo *)
(* 517s without memo for removeKeyList *)
(* 530s with Assoc_memo *)
(* 594s with Assoc_lru 10000, 5*)
(* 597s with Assoc_lru 10000, 2*)
(* 478s with tail rec main loop with Assoc *)
(* 451s with tail rec main loop, Assoc (another run) *)
(* 468s with tail_rec, Assoc *)
(* 460s new tame support *)
test 1 (f_tameEnumFilterBounded (numeral `0`) (numeral `20000`)) None;;
test 1 (f_tameEnumFilterBounded (numeral `0`)) (numeral `20000`);;

(* 100000: 2908s (non-exclusive) *)
(* all: 11493s *)
test 1 (f_tameEnumFilterBounded (numeral `0`) (numeral `100000`)) None;;
test 1 (f_tameEnumFilterBounded (numeral `0`)) (numeral `100000`);;

let res, tm = it;;

let rec all_values tm =
  let op, al = dest_comb tm in
  let _, vs = dest_comb op in
  dest_list vs @ 
    (List.fold_left (@) [] (map (all_values o snd o dest_pair) (dest_list al)));;

all_values (rand (concl res));;

let all_values =
  `all_values (Tries vs al) = APPEND vs (maps (\(_, t). all_values t) al)`;;

(* After 241000 steps *)
(* 31106 *)
Hashtbl.length (create_memo "f_APPEND_num");;
(* 12 *)
Hashtbl.length (create_memo "f_map_num_num_list");;
(* 138 *)
Hashtbl.length (create_memo "f_upt");;
(* 23 *)
Hashtbl.length (create_memo "f_map_num_list_num_list");;
(* 15 *)
Hashtbl.length (create_memo "f_heightsNewVertices");;
(* 2518 *)
Hashtbl.length (create_memo "f_size_list_num");;
(* 9303 *)
Hashtbl.length (create_memo "f_nextVertex");;
(* 4108 *)
Hashtbl.length (create_memo "f_vertices_face");;
(* 3263591 *)
Hashtbl.length (create_memo "f_removeKeyList_num_num");;
(* 5 *)
Hashtbl.length (create_memo "f_squanderVertex");;
(* 5 *)
Hashtbl.length (create_memo "f_excessAtType");;
(* 52 *)
Hashtbl.length (create_memo "f_rev_num");;
(* 164240 *)
Hashtbl.length (create_memo "f_member_num");;
(* 32459 *)
Hashtbl.length (create_memo "f_splitAtRec_num");;
(* 1 *)
Hashtbl.length (create_memo "f_squanderFace");;

Hashtbl.length (create_memo "f_maxGon");;

let get_thms name =
  let m = create_memo name in
  Hashtbl.fold (fun k v r -> v :: r) m [];;

get_thms "f_maxGon";;

(* New orda improves performance *)
(* type_of 5566376 *)
(* type_of 2913467 with new MK_COMB *)
(* No significant difference in performance *)
core_counters();;
reset_core_counters();;

time (f_tameEnumFilterBounded `0`) `100000`;;
setify_types !eq_types;;

get_all_counters();;
get_counter "f_gen_length";;
Hashtbl.fold (fun k v r -> k :: r) (create_memo "f_size_list") [];;

(* nth -> unroll up to 15 *)
(* maps -> up to 7 *)
(* count -> up to 7 *)

analyze_arg_lists();;

let args = lazy !(create_arg_list "f_squanderVertex");;
let n = Lazy.force args |> length;;
Lazy.force args |> map (length o dest_list o el 0) |> freqs;;
Lazy.force args |> map (Nat_arith.dest_nat o el 0) |> freqs;;
Lazy.force args |> freqs;;
let t = Lazy.force args |> freqs |> length;;
float (n - t) /. float n;;

Nat_arith.reset_cache();;

setify !cond_types |>
  map (fun ty -> ty, fix_identifier @@ string_of_type ty);;

(* set_extra db Extra_memo ["size_list"];; *)