Translate inlining (with many side conditions)

compiler/backend/passes/pure_comp_confScript.sml

@@ -6,32 +6,48 @@ open HolKernel Parse boolLib bossLib mlstringTheory;
 
 val _ = new_theory "pure_comp_conf";
 
+Datatype:
+  inline_opts = <|
+    depth           : num ;
+    heuristic       : num ;
+  |>
+End
+
 Datatype:
   compiler_opts = <|
-      do_pure_sort  : bool ;  (* pure-to-pure binding group analysis *)
-      do_pure_clean : bool ;  (* pure-to-pure cleaning / deadcode elimination *)
-      do_demands    : bool ;  (* demand analysis *)
-      do_mk_delay   : bool ;  (* thunk-to-thunk smart mk_delay constructor *)
-      do_let_force  : bool ;  (* thunk-to-thunk simplify let force *)
-      do_split_dlam : bool ;  (* thunk-to-thunk split delayed lambdas *)
-      do_app_unit   : bool ;  (* state-to-state *)
-      do_final_gc   : bool ;  (* invoke GC at end of CakeML program *)
+      do_pure_sort  : bool ;        (* pure-to-pure binding group analysis *)
+      do_pure_clean : bool ;        (* pure-to-pure cleaning / deadcode elimination *)
+      do_demands    : bool ;        (* demand analysis *)
+      inlining      : inline_opts ; (* inlining *)
+      do_mk_delay   : bool ;        (* thunk-to-thunk smart mk_delay constructor *)
+      do_let_force  : bool ;        (* thunk-to-thunk simplify let force *)
+      do_split_dlam : bool ;        (* thunk-to-thunk split delayed lambdas *)
+      do_app_unit   : bool ;        (* state-to-state *)
+      do_final_gc   : bool ;        (* invoke GC at end of CakeML program *)
     |>
 End
 
 Overload pure_sort_flag[local]  = “strlit "-sort"”
 Overload pure_clean_flag[local] = “strlit "-clean"”
 Overload demands_flag[local]    = “strlit "-demands"”
+Overload inline_off_flag[local] = “strlit "-inline"”
+Overload inline_max_flag[local] = “strlit "-inline_max"”
 Overload mk_delay_flag[local]   = “strlit "-mk_delay"”
 Overload let_force_flag[local]  = “strlit "-let_force"”
 Overload dlam_flag[local]       = “strlit "-dlam"”
 Overload unit_flag[local]       = “strlit "-unit"”
 Overload final_gc_flag[local]   = “strlit "-final_gc"”
 
+Overload inline_off_opts[local] = “<| depth := 0 ; heuristic := 0 |>”
+Overload inline_default_opts[local] = “<| depth := 50 ; heuristic := 100 |>”
+Overload inline_max_opts[local] = “<| depth := 5000 ; heuristic := 10000 |>”
+
 Definition all_flags_def:
   all_flags = [pure_sort_flag;
                pure_clean_flag;
                demands_flag;
+               inline_off_flag;
+               inline_max_flag;
                mk_delay_flag;
                let_force_flag;
                dlam_flag;
@@ -46,6 +62,11 @@ Definition read_cline_args_def:
     | [] => INL <| do_pure_sort  := ¬ MEM pure_sort_flag cl  ;
                    do_pure_clean := ¬ MEM pure_clean_flag cl ;
                    do_demands    := ¬ MEM demands_flag cl    ;
+                   inlining      := if MEM inline_off_flag cl then
+                                      inline_off_opts
+                                    else if MEM inline_max_flag cl then
+                                      inline_max_opts
+                                    else inline_default_opts ;
                    do_mk_delay   := ¬ MEM mk_delay_flag cl   ;
                    do_let_force  := ¬ MEM let_force_flag cl  ;
                    do_split_dlam := ¬ MEM dlam_flag cl       ;

compiler/backend/passes/pure_inline_cexpScript.sml

@@ -5,7 +5,7 @@ open HolKernel Parse boolLib bossLib BasicProvers;
 open listTheory pairTheory topological_sortTheory;
 open pure_cexpTheory pure_varsTheory balanced_mapTheory
      pure_freshenTheory pure_letrec_spec_cexpTheory
-     pure_dead_letTheory;
+     pure_dead_letTheory pure_comp_confTheory;
 
 val _ = new_theory "pure_inline_cexp";
 
@@ -84,18 +84,18 @@ And so goint further won't do anything
 
 Definition SPLIT_AT_GO_def:
   SPLIT_AT_GO (0: num) xs ys = (xs, ys) ∧
-  SPLIT_AT_GO n xs [] = (xs, []) ∧
-  SPLIT_AT_GO n xs (y::ys) =
-    SPLIT_AT_GO (n - 1) (xs ++ [y]) ys
+  SPLIT_AT_GO (SUC n) xs [] = (xs, []) ∧
+  SPLIT_AT_GO (SUC n) xs (y::ys) =
+    SPLIT_AT_GO n (xs ++ [y]) ys
 End
 
 Definition SPLIT_AT_def:
   SPLIT_AT (n: num) xs = SPLIT_AT_GO n [] xs
 End
 
 Definition Lets_def:
-  Lets a [] [] e = e ∧
-  Lets a (v::vs) (e::es) e1 = Let a v e (Lets a vs es e1)
+  Lets a (v::vs) (e::es) e1 = Let a v e (Lets a vs es e1) ∧
+  Lets a _ _ e = e
 End
 
 Definition make_Let_def:
@@ -263,9 +263,35 @@ Termination
   \\ qspec_then ‘bs’ assume_tac size_lemma \\ fs []
 End
 
+Definition boundvars_of_def:
+  boundvars_of (Var c x) = empty_vars ∧
+  boundvars_of (Prim c cop ces) =
+   FOLDR (λce s. var_union s $ boundvars_of ce) empty_vars ces ∧
+  boundvars_of (App c ce ces) =
+   FOLDR (λce s. var_union s $ boundvars_of ce) (boundvars_of ce) ces ∧
+  boundvars_of (Lam c xs ce) = insert_vars (boundvars_of ce) xs ∧
+  boundvars_of (Let c x ce1 ce2) =
+    insert_var (var_union (boundvars_of ce1) (boundvars_of ce2)) x ∧
+  boundvars_of (Letrec c fns ce) =
+    FOLDR (λ(f,body) s. var_union s $ insert_var (boundvars_of body) f)
+      (boundvars_of ce) fns ∧
+  boundvars_of (Case c ce x css us) =
+    var_union (insert_var (boundvars_of ce) x) $
+    var_union (case us of NONE => empty_vars | SOME (_,ce) => boundvars_of ce) $
+    FOLDR (λ(cn,vs,ce) s. var_union s $ insert_vars (boundvars_of ce) vs)
+      empty_vars css ∧
+  boundvars_of (NestedCase c ce x p pce pces) =
+    var_union (insert_var (boundvars_of ce) x) $
+    var_union (insert_vars (boundvars_of pce) (cepat_vars_l p)) $
+    FOLDR (λ(p,ce) s. var_union s $ insert_vars (boundvars_of ce) (cepat_vars_l p))
+      empty_vars pces
+Termination
+  WF_REL_TAC `measure $ cexp_size (K 0)`
+End
+
 Definition inline_all_def:
-  inline_all cl h e = 
-    let (e1, s) = freshen_cexp e empty_vars
+  inline_all cl h e =
+    let (e1, s) = freshen_cexp e (boundvars_of e)
     in let (inlined_e, _) = inline empty s cl h e1
     in dead_let inlined_e
 End
@@ -333,8 +359,15 @@ Termination
 End
 
 Definition tree_size_heuristic_def:
-  tree_size_heuristic n =
-    (λe. tree_size_heuristic_rec n e ≥ 0)
+  tree_size_heuristic n e =
+    (tree_size_heuristic_rec n e ≥ 0)
+End
+
+(*******************)
+
+Definition inline_top_level_def:
+  inline_top_level c e =
+    inline_all c.inlining.depth (tree_size_heuristic c.inlining.heuristic) e
 End
 
 (*******************)

compiler/backend/passes/pure_letrec_spec_cexpScript.sml

@@ -147,9 +147,9 @@ Termination
 End
 
 Definition take_non_const_def:
-  take_non_const [] args = args ∧
   take_non_const (NONE::xs) (arg::args) = arg :: (take_non_const xs args) ∧
-  take_non_const ((SOME x)::xs) (arg::args) = take_non_const xs args
+  take_non_const ((SOME x)::xs) (arg::args) = take_non_const xs args ∧
+  take_non_const _ args = args
 End
 
 (*

compiler/binary/pure_frontendProgScript.sml

@@ -5,13 +5,17 @@ open basis
      pure_demands_analysisTheory
      pure_letrec_cexpTheory
      pure_freshenTheory
+     pure_dead_letTheory
+     pure_letrec_spec_cexpTheory
+     pure_inline_cexpTheory
      pure_compilerTheory
      pure_inferProgTheory;
 
 val _ = new_theory "pure_frontendProg";
 
 val _ = set_grammar_ancestry ["pure_inferProg", "pure_letrec_cexp",
-                              "pure_demands_analysis", "pure_freshen"];
+                              "pure_demands_analysis", "pure_freshen",
+                              "pure_inline_cexp"];
 
 val _ = translation_extends "pure_inferProg";
 
@@ -100,6 +104,39 @@ val r = translate fresh_boundvars_def;
 val r = translate_no_ind freshen_aux_def; (* TODO bad induction *)
 val r = translate freshen_cexp_def;
 
+(*-----------------------------------------------------------------------*
+   inlining TODO various unproved side conditions
+ *-----------------------------------------------------------------------*)
+
+val r = translate_no_ind dead_let_def; (* TODO bad induction *)
+val r = translate_no_ind boundvars_of_def; (* TODO bad induction *)
+
+
+val r = translate min_call_args_def;
+val r = translate const_call_args_def;
+val r = translate_no_ind inline_def;
+
+Triviality inline_ind:
+  inline_ind (:'a)
+Proof
+  once_rewrite_tac[fetch "-" "inline_ind_def"] >>
+  rpt gen_tac >>
+  rpt $ disch_then strip_assume_tac >>
+  match_mp_tac $ latest_ind () >>
+  rpt strip_tac >>
+  last_x_assum match_mp_tac >>
+  rpt strip_tac >>
+  gvs[FORALL_PROD, LAMBDA_PROD, ADD1] >>
+  metis_tac[PAIR]
+QED
+
+val r = inline_ind |> update_precondition;
+
+val r = translate inline_all_def;
+val r = translate_no_ind tree_size_heuristic_rec_def; (* TODO bad induction *)
+val r = translate tree_size_heuristic_def;
+val r = translate inline_top_level_def;
+
 (*-----------------------------------------------------------------------*
    ast_to_string
  *-----------------------------------------------------------------------*)

compiler/pure_compilerScript.sml

@@ -6,13 +6,13 @@ open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
      optionTheory pairTheory ltreeTheory llistTheory bagTheory dep_rewrite
      BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory;
 open pure_cexpTheory pure_to_cakeTheory pureParseTheory pure_inferenceTheory
-     pure_letrec_cexpTheory pure_demands_analysisTheory
+     pure_letrec_cexpTheory pure_demands_analysisTheory pure_inline_cexpTheory
      fromSexpTheory simpleSexpParseTheory;
 
 val _ = set_grammar_ancestry
           ["pure_cexp", "pure_to_cake", "pureParse", "pure_inference",
-           "pure_letrec_cexp", "pure_demands_analysis", "fromSexp",
-           "simpleSexpParse"];
+           "pure_letrec_cexp", "pure_demands_analysis",
+           "pure_inline_cexp", "fromSexp", "simpleSexpParse"];
 
 val _ = new_theory "pure_compiler";
 
@@ -39,7 +39,9 @@ Definition compile_def:
           let _ = empty_ffi (strlit "clean_cexp") in
           let e4 = demands_analysis c e3 in
           let _ = empty_ffi (strlit "demands_analysis") in
-            SOME (ast_to_string $ pure_to_cake c ns e4)
+          let e5 = inline_top_level c e4 in
+          let _ = empty_ffi (strlit "inlining") in
+            SOME (ast_to_string $ pure_to_cake c ns e5)
 End
 
 Definition compile_to_ast_def:
@@ -54,7 +56,8 @@ Definition compile_to_ast_def:
         | SOME _ =>
           let e3 = clean_cexp c e2 in
           let e4 = demands_analysis c e3 in
-          SOME (pure_to_cake c ns e4)
+          let e5 = inline_top_level c e4 in
+          SOME (pure_to_cake c ns e5)
 End
 
 (********** Alternative phrasings **********)
@@ -67,7 +70,8 @@ Theorem compile_monadically:
     to_option $ infer_types ns e2 ;
     e3 <<- clean_cexp c e2 ;
     e4 <<- demands_analysis c e3 ;
-    return (ast_to_string $ pure_to_cake c ns e4)
+    e5 <<- inline_top_level c e4 ;
+    return (ast_to_string $ pure_to_cake c ns e5)
   od
 Proof
   simp[compile_def] >> EVERY_CASE_TAC >> simp[]
@@ -99,7 +103,8 @@ Theorem compile_to_ast_alt_def:
     | SOME (e2,ns) =>
         let e3 = clean_cexp c e2 in
         let e4 = demands_analysis c e3 in
-        SOME (pure_to_cake c ns e4)
+        let e5 = inline_top_level c e4 in
+        SOME (pure_to_cake c ns e5)
 Proof
   rw[compile_to_ast_def, frontend_def] >>
   rpt (TOP_CASE_TAC >> simp[])