Start on refactoring the CakeML compset infrastructure

In each directory dirname, there should be a file compute_dirnameLib.sml
It should contain functions add_whatever_compset that adds theorems and
conversion relevant to the whatever to a given compset. It should also
contain a definition the_dirname_compset that creates a compset with
everything needed to run the various whatevers in dirname.

It doesn't work currently, because label removal in bytecode relies on
el_check which is defined in compiler, but the directories depend the
other way around.

The unify and label removal infrastructure had global state, I've
refactored so that the state is created locally to the add_..._compset
call.

Holmakefile

@@ -1 +1,2 @@
+INCLUDES = $(HOLDIR)/examples/parsing
 OPTIONS = QUIT_ON_FAILURE

bytecode/labels_computeLib.sml → bytecode/compute_bytecodeLib.sml

@@ -1,6 +1,66 @@
-structure labels_computeLib = struct
-local
-  open HolKernel boolLib bossLib bytecodeLabelsTheory labels_computeTheory patriciaLib
+structure compute_bytecodeLib = struct
+  open HolKernel boolLib bossLib lcsymtacs
+
+val bc_fetch_aux_0_thm = prove(
+  ``∀code pc. bc_fetch_aux code (K 0) pc =
+    if no_labels code then el_check pc code
+    else FAIL (bc_fetch_aux code (K 0) pc) "code has labels"``,
+  REWRITE_TAC[bytecodeLabelsTheory.no_labels_def] >>
+  Induct >> simp[bytecodeTheory.bc_fetch_aux_def] >>
+  rw[] >> fs[combinTheory.FAIL_DEF] >>
+  simp[rich_listTheory.EL_CONS,arithmeticTheory.PRE_SUB1])
+
+  val SUC_TO_NUMERAL_RULE = CONV_RULE(!Defn.SUC_TO_NUMERAL_DEFN_CONV_hook)
+
+val eval_real_inst_length =
+  let
+    val compset = reduceLib.num_compset()
+    val () = intReduce.add_int_compset compset
+    val () = computeLib.add_thms [bytecodeExtraTheory.real_inst_length_compute] compset
+  in
+    computeLib.CBV_CONV compset
+  end
+
+
+  fun add_bytecode_compset compset = let
+
+    local open bytecodeTheory in
+      val () = computeLib.add_thms
+        [bool_to_tag_def
+        ,unit_tag_def
+        ,closure_tag_def
+        ,string_tag_def
+        ,block_tag_def
+        ,bump_pc_def
+        ,bc_fetch_def
+        ,bv_to_string_def
+        ,bvs_to_chars_def
+        ,bc_equality_result_to_val_def
+        ,bool_to_val_def
+        ,bool_to_tag_def
+        ,bc_find_loc_def
+        ,bytecodeTerminationTheory.bc_equal_def
+        ] compset
+    end
+
+    local open bytecodeEvalTheory in
+      val () = computeLib.add_thms
+        [bc_eval_compute
+        ,bc_eval1_def
+        ,bc_eval_stack_def
+        ,bc_fetch_aux_0_thm
+        ,SUC_TO_NUMERAL_RULE bc_evaln_def
+        ,listTheory.LUPDATE_compute
+        ,el_check_def
+        ] compset
+    end
+    val () = computeLib.add_datatype_info compset (valOf(TypeBase.fetch``:bc_state``))
+    val () = computeLib.add_datatype_info compset (valOf(TypeBase.fetch``:bc_value``))
+  in () end
+
+  fun add_labels_compset compset = let
+
+  open bytecodeLabelsTheory labels_computeTheory patriciaLib
 
   val Addr_tm = ``Addr``
   fun mk_Addr x = mk_comb(Addr_tm,x)
@@ -153,7 +213,6 @@ local
   val init_db = Net.insert (rand(concl(code_labels_ok_nil)),code_labels_ok_nil) Net.empty
   val db = ref init_db
 
-in
   val quiet = quiet
 
   fun reset_code_labels_ok_db () = db := init_db
@@ -171,7 +230,7 @@ in
     case Net.index tm (!db) of th::_ => th
     | [] =>
       ( last_code_not_found := tm
-      ; raise (mk_HOL_ERR "labels_computeLib" "get_code_labels_ok_thm" "code_labels_ok theorem not found."))
+      ; raise (mk_HOL_ERR "compute_bytecode_Lib" "get_code_labels_ok_thm" "code_labels_ok theorem not found."))
   fun code_labels_ok_thms() = Net.listItems(!db)
 
   val mk_def = let
@@ -207,5 +266,20 @@ in
       MP th (CONJ th2 th0)
     end
 
+    val () = reset_code_labels_ok_db()
+    val () = computeLib.add_conv (``code_labels``,2,code_labels_conv eval_real_inst_length) compset
+  in () end
+
+  val the_bytecode_compset = let
+    val c = wordsLib.words_compset ()
+    val () = compute_basicLib.add_basic_compset c
+    val () = compute_semanticsLib.add_ast_compset c
+    val () = add_bytecode_compset c
+    val () = add_labels_compset c
+  in
+    c
+  end
+
+
 end
-end
+

compiler/compilerLib.lem

@@ -6,8 +6,6 @@ import List_extra
 val all2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
 declare hol target_rep function all2 = `EVERY2`
 
-let rec el_check n ls = if n < List.length ls then Just (List_extra.nth ls n) else Nothing
-
 val num_fold : forall 'a. ('a -> 'a) -> 'a -> nat -> 'a
 let rec num_fold f a n = if n = 0 then a else num_fold f (f a) (n-1)
 declare termination_argument num_fold = automatic

compute_basicLib.sml

@@ -0,0 +1,68 @@
+structure compute_basicLib = struct
+open HolKernel boolLib bossLib lcsymtacs
+
+fun add_datatype tm compset =
+  (computeLib.add_datatype_info compset o valOf o TypeBase.fetch) tm
+
+(* compset needs to have at least wordsLib.words_compset in it *)
+fun add_basic_compset compset =
+let
+  (* good libraries which provide compsets :) *)
+  val () = intReduce.add_int_compset compset
+  (* included in words_compset
+  val () = listLib.list_rws compset
+  val () = numposrepLib.add_numposrep_compset compset
+  val () = ASCIInumbersLib.add_ASCIInumbers_compset compset
+  *)
+  val () = stringLib.add_string_compset compset
+  val () = sumSimps.SUM_rws compset
+  val () = optionLib.OPTION_rws compset
+  val () = pred_setLib.add_pred_set_compset compset
+  val () = combinLib.add_combin_compset compset
+  val () = pairLib.add_pair_compset compset
+  val () = finite_mapLib.add_finite_map_compset compset
+  val () = pegLib.add_peg_compset compset
+(* rich_list doesnt' provide a compset :( *)
+  val () = computeLib.add_thms
+  [rich_listTheory.SPLITP_compute
+  ,rich_listTheory.SPLITP_AUX_def
+  ] compset
+(* sptree doesn't provide a compset :( *)
+  val () = computeLib.add_thms
+  [sptreeTheory.lookup_compute
+  ,sptreeTheory.insert_compute
+  ,sptreeTheory.delete_compute
+  ,sptreeTheory.lrnext_thm
+  ,sptreeTheory.wf_def
+  ,sptreeTheory.mk_BN_def
+  ,sptreeTheory.mk_BS_def
+  ,sptreeTheory.fromList_def
+  ,sptreeTheory.size_def
+  ,sptreeTheory.union_def
+  ,sptreeTheory.inter_def
+  ,sptreeTheory.domain_def
+  ,sptreeTheory.foldi_def
+  ,sptreeTheory.toListA_def
+  ,sptreeTheory.toList_def
+  ,sptreeTheory.mk_wf_def
+  ] compset
+  val () = computeLib.add_thms 
+  [miscTheory.find_index_def
+  ,miscTheory.LEAST_thm
+  ,miscTheory.least_from_thm
+  ] compset
+  val () = add_datatype ``:'a spt`` compset
+in
+  ()
+end
+
+  val the_basic_compset = 
+    let
+      val c = wordsLib.words_compset ()
+      val () = add_basic_compset c
+    in
+      c
+    end
+
+end
+

inference/compute_inferenceLib.sml

@@ -0,0 +1,60 @@
+structure compute_inferenceLib = struct
+  open HolKernel boolLib bossLib lcsymtacs
+
+  fun add_inference_compset compset =
+  let
+
+    open inferTheory
+    val () = computeLib.add_thms
+    [infer_prog_def
+    ,infer_top_def
+    ,infer_d_def
+    ,infer_ds_def
+    ,infer_e_def
+    ,infer_p_def
+    ,st_ex_bind_def
+    ,st_ex_return_def
+    ,lookup_tenvC_st_ex_def
+    ,lookup_st_ex_def
+    ,init_state_def
+    ,get_next_uvar_def
+    ,fresh_uvar_def
+    ,n_fresh_uvar_def
+    ,guard_def
+    ,add_constraint_def
+    ,add_constraints_def
+    ,read_def
+    ,generalise_def
+    ,apply_subst_list_def
+    ,append_decls_def
+    ,constrain_op_def
+    ,infer_deBruijn_subst_def
+    ,Infer_Tfn_def
+    ,Infer_Tint_def
+    ,Infer_Tbool_def
+    ,Infer_Tref_def
+    ,Infer_Tunit_def
+    ,infer_type_subst_def
+    ,check_signature_def
+    ] compset
+
+    val () = compute_basicLib.add_datatype ``:infer_t`` compset
+    val () = compute_basicLib.add_datatype ``:atom`` compset
+    val () = compute_basicLib.add_datatype ``:('a,'b)exc`` compset
+    val () = compute_basicLib.add_datatype ``:'a infer_st`` compset
+  in
+    ()
+  end
+
+  val the_infer_compset = let
+    val c = wordsLib.words_compset ()
+    val () = compute_basicLib.add_basic_compset c
+    val () = compute_semanticsLib.add_ast_compset c
+    val get_wfs = unifyLib.add_unify_compset c
+    val () = add_inference_compset c
+  in
+    ()
+  end
+
+
+end

inference/unifyLib.sml

@@ -17,67 +17,69 @@ local
     ]
 
   val init_db = Net.insert (rand(concl(t_wfs_FEMPTY)),t_wfs_FEMPTY) Net.empty
-  val db = ref init_db
-  fun get_wfs s =
-    case Net.index s (!db) of
-      (th::_) => th
-    | _ => raise mk_HOL_ERR "unifyLib" "get_wfs" (term_to_string s)
 
 in
 
-  fun reset_wfs_thms() = db := init_db
-  fun wfs_thms() = Net.listItems(!db)
+  fun add_unify_compset compset = let
 
-  fun t_unify_conv eval tm = let
-    val (_,[s,t1,t2]) = strip_comb tm
-    val wfs_s = get_wfs s
-    val th1 = SPECL [t1,t2] (MATCH_MP unifyTheory.t_unify_eqn wfs_s)
-    val th2 = eval (rhs(concl th1))
-    val th3 = TRANS th1 th2
-    val res = rhs(concl th2)
-    val _ = if optionSyntax.is_some res then
-            let val key = rand res in
-              if null (Net.index key (!db)) then
-                db := Net.insert
-                  (key, PROVE[wfs_s,t_unify_wfs,th3]
-                        (mk_comb(rator(concl wfs_s),key)))
-                  (!db)
+    val db = ref init_db
+    fun get_wfs s =
+      case Net.index s (!db) of
+        (th::_) => th
+      | _ => raise mk_HOL_ERR "unifyLib" "get_wfs" (term_to_string s)
+
+
+    fun wfs_thms() = Net.listItems(!db)
+
+    fun t_unify_conv eval tm = let
+      val (_,[s,t1,t2]) = strip_comb tm
+      val wfs_s = get_wfs s
+      val th1 = SPECL [t1,t2] (MATCH_MP unifyTheory.t_unify_eqn wfs_s)
+      val th2 = eval (rhs(concl th1))
+      val th3 = TRANS th1 th2
+      val res = rhs(concl th2)
+      val _ = if optionSyntax.is_some res then
+              let val key = rand res in
+                if null (Net.index key (!db)) then
+                  db := Net.insert
+                    (key, PROVE[wfs_s,t_unify_wfs,th3]
+                          (mk_comb(rator(concl wfs_s),key)))
+                    (!db)
+                else ()
+              end
               else ()
-            end
-            else ()
-    in th3 end
-  fun t_vwalk_conv eval tm = let
-    val (_,[s,t]) = strip_comb tm
-    val wfs_s = get_wfs s
-    val th1 = SPEC t (MATCH_MP unifyTheory.t_vwalk_eqn wfs_s)
-    val th2 = eval (rhs(concl th1))
-    in TRANS th1 th2 end
-  fun t_oc_conv eval tm = let
-    val (_,[s,t1,t2]) = strip_comb tm
-    val wfs_s = get_wfs s
-    val th1 = SPECL [t1,t2] (MATCH_MP unifyTheory.t_oc_eqn wfs_s)
-    val th2 = eval (rhs(concl th1))
-    in TRANS th1 th2 end
-  fun t_walkstar_conv eval tm = let
-    val (_,[s,t]) = strip_comb tm
-    val wfs_s = get_wfs s
-    val th1 = SPEC t (MATCH_MP unifyTheory.t_walkstar_eqn wfs_s)
-    val th2 = eval (rhs(concl th1))
-    in TRANS th1 th2 end
+      in th3 end
+    fun t_vwalk_conv eval tm = let
+      val (_,[s,t]) = strip_comb tm
+      val wfs_s = get_wfs s
+      val th1 = SPEC t (MATCH_MP unifyTheory.t_vwalk_eqn wfs_s)
+      val th2 = eval (rhs(concl th1))
+      in TRANS th1 th2 end
+    fun t_oc_conv eval tm = let
+      val (_,[s,t1,t2]) = strip_comb tm
+      val wfs_s = get_wfs s
+      val th1 = SPECL [t1,t2] (MATCH_MP unifyTheory.t_oc_eqn wfs_s)
+      val th2 = eval (rhs(concl th1))
+      in TRANS th1 th2 end
+    fun t_walkstar_conv eval tm = let
+      val (_,[s,t]) = strip_comb tm
+      val wfs_s = get_wfs s
+      val th1 = SPEC t (MATCH_MP unifyTheory.t_walkstar_eqn wfs_s)
+      val th2 = eval (rhs(concl th1))
+      in TRANS th1 th2 end
 
-  local
     fun convs eval =
     [(``t_unify``,3,t_unify_conv eval)
     ,(``t_vwalk``,2,t_vwalk_conv eval)
     ,(``t_walkstar``,2,t_walkstar_conv eval)
     ,(``t_oc``,3,t_oc_conv eval)
     ]
-  in
-    fun add_unify_compset compset =
-      (computeLib.add_thms funs compset
-      ;List.app (Lib.C computeLib.add_conv compset) (convs (computeLib.CBV_CONV compset))
-      )
-  end
+
+    val () = computeLib.add_thms funs compset
+    val () = List.app (Lib.C computeLib.add_conv compset) (convs (computeLib.CBV_CONV compset))
+    in
+      wfs_thms
+    end
 
 end
 end

parsing/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = $(HOLDIR)/examples/parsing ../semantics
+INCLUDES = $(HOLDIR)/examples/parsing .. ../semantics
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY