bvl_to_bviScript.sml

(*
  A compiler phases that transforms BVL programs into BVI programs. As
  part of this phase, certain primitive operations map to "stubs" code
  implemented in BVI; numeric constants are split into smaller ones to
  ease code generation later; Handle is fused with Call; and very
  large expressions are split into samller ones (in order to protect
  the register allocator from overly large inputs).
*)
open preamble bvlTheory bviTheory;
open backend_commonTheory
local open
  bvl_inlineTheory
  bvl_constTheory
  bvl_handleTheory
  bvi_letTheory
  bvi_tailrecTheory
  dataLangTheory
in end;

val _ = new_theory "bvl_to_bvi";

val _ = patternMatchesLib.ENABLE_PMATCH_CASES();

Definition destLet_def:
  (destLet ((Let xs b):bvl$exp) = (xs,b)) /\
  (destLet _ = ([],Var 0))
End

Theorem destLet_pmatch:
  ∀exp.
  destLet exp =
    case exp of
      Let xs b => (xs,b)
    | _ => ([],Var 0)
Proof
  rpt strip_tac
  >> rpt(CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV) >> every_case_tac)
  >> fs[destLet_def]
QED

val large_int = ``268435457:int`` (* 2**28-1 *)

Definition compile_int_def:
  compile_int (i:int) =
    bvi$Op (if -^large_int ≤ i ∧ i ≤ ^large_int then Const i else Build [Int i]) []
End

Definition alloc_glob_count_def:
  (alloc_glob_count [] = 0:num) /\
  (alloc_glob_count (x::y::xs) =
     alloc_glob_count [x] + alloc_glob_count (y::xs) /\
  (alloc_glob_count [(Var _):bvl$exp] = 0) /\
  (alloc_glob_count [If x y z] =
     alloc_glob_count [x] +
     alloc_glob_count [y] +
     alloc_glob_count [z]) /\
  (alloc_glob_count [Handle x y] =
     alloc_glob_count [x] +
     alloc_glob_count [y]) /\
  (alloc_glob_count [Tick x] = alloc_glob_count [x]) /\
  (alloc_glob_count [Raise x] = alloc_glob_count [x]) /\
  (alloc_glob_count [Let xs x] = alloc_glob_count (x::xs)) /\
  (alloc_glob_count [Call _ _ xs] = alloc_glob_count xs) /\
  (alloc_glob_count [Op op xs] =
     if op = AllocGlobal then 1 + alloc_glob_count xs
                         else alloc_glob_count xs) /\
  (alloc_glob_count [_] = 0))
Termination
  WF_REL_TAC `measure exp1_size`
End

val AllocGlobal_location_def = Define`
  AllocGlobal_location = data_num_stubs`;
val CopyGlobals_location_def = Define`
  CopyGlobals_location = AllocGlobal_location+1`;
val InitGlobals_location_def = Define`
  InitGlobals_location = CopyGlobals_location+1`;
val ListLength_location_def = Define`
  ListLength_location = InitGlobals_location+1`;
val FromListByte_location_def = Define`
  FromListByte_location = ListLength_location+1`;
val ToListByte_location_def = Define`
  ToListByte_location = FromListByte_location+1`;
val SumListLength_location_def = Define`
  SumListLength_location = ToListByte_location+1`;
val ConcatByte_location_def = Define`
  ConcatByte_location = SumListLength_location+1`;

val AllocGlobal_location_eq = save_thm("AllocGlobal_location_eq",
  ``AllocGlobal_location`` |> EVAL);
val CopyGlobals_location_eq = save_thm("CopyGlobals_location_eq",
  ``CopyGlobals_location`` |> EVAL);
val InitGlobals_location_eq = save_thm("InitGlobals_location_eq",
  ``InitGlobals_location`` |> EVAL);
val ListLength_location_eq = save_thm("ListLength_location_eq",
  ``ListLength_location`` |> EVAL);
val FromListByte_location_eq = save_thm("FromListByte_location_eq",
  ``FromListByte_location`` |> EVAL);
val ToListByte_location_eq = save_thm("ToListByte_location_eq",
  ``ToListByte_location`` |> EVAL);
val SumListLength_location_eq = save_thm("SumListLength_location_eq",
  ``SumListLength_location`` |> EVAL);
val ConcatByte_location_eq = save_thm("ConcatByte_location_eq",
  ``ConcatByte_location`` |> EVAL);

Definition AllocGlobal_code_def:
  AllocGlobal_code = (1:num,
    Let [Op GlobalsPtr []] $
    Let [Op El [Op (Const 0) []; Var 0]] $
    Let [Op Add [Var 0; Var 2]] $
    Let [Op Length [Var 2]] $
    Let [Op Update [Var 1; Op (Const 0) []; Var 3]] $
      If (Op Less [Var 1; Var 2]) (Var 0)
         (Let [Op RefArray [Op (Const 0) []; Op Add [Var 2; Var 2]]] $
          Let [Op SetGlobalsPtr [Var 0]] $
            Call 0 (SOME CopyGlobals_location)
              [Var 1; Var 6; Op Sub [Op (Const 1) []; Var 3]] NONE))
End

val CopyGlobals_code_def = Define`
  CopyGlobals_code = (3:num, (* ptr to new array, ptr to old array, index to copy *)
    Let [Op Update [Op El [Var 2; Var 1]; Var 2; Var 0]]
      (If (Op Equal [Op(Const 0)[]; Var 3]) (Var 0)
        (Call 0 (SOME CopyGlobals_location) [Var 1; Var 2; Op Sub [Op(Const 1)[];Var 3]] NONE)))`;

val InitGlobals_max_def = Define`
  InitGlobals_max = 10000n`;

val InitGlobals_code_def = Define`
  InitGlobals_code start n = (0:num,
    let n = MIN (MAX n 1) InitGlobals_max in
      Let [Op RefArray [Op (Const 0) []; Op (Const (&n)) []]]
        (Let [Op Update [Op (Const 1) []; Op (Const 0) []; Var 0]]
          (Let [Op SetGlobalsPtr [Var 1]]
             (Call 0 (SOME start) [] (SOME (Var 0))))))`;

val ListLength_code_def = Define `
  ListLength_code = (2n, (* ptr to array, accumulated length *)
    If (Op (TagLenEq nil_tag 0) [Var 0])
      (Var 1) (Call 0 (SOME ListLength_location)
                [Op El [Op (Const 1) []; Var 0];
                 Op Add [Var 1; Op (Const 1) []]] NONE))`

val FromListByte_code_def = Define`
  FromListByte_code = (3n, (* list, current index, byte array *)
    If (Op (TagLenEq nil_tag 0) [Var 0]) (Var 2)
      (Let [Op UpdateByte [Op El [Op (Const 0) []; Var 0]; Var 1; Var 2]]
        (Call 0 (SOME FromListByte_location)
          [Op El [Op (Const 1) []; Var 1];
           Op Add [Var 2; Op (Const 1) []];
           Var 3] NONE)))`;

val ToListByte_code_def = Define`
  ToListByte_code = (3n, (* list, current index, byte array *)
    If (Op (EqualConst (Int 0i)) [Var 1]) (Var 0)
      (Let [Op Sub [Op (Const 1) []; Var 1]]
      (Let [Op DerefByte [Var 0; Var 3]]
        (Call 0 (SOME ToListByte_location)
          [Op (Cons 0) [Var 2; Var 0];
           Var 1;
           Var 4] NONE))))`;

val SumListLength_code_def = Define`
  SumListLength_code = (2n, (* ptr to list, accumulated length *)
    If (Op (TagLenEq nil_tag 0) [Var 0])
      (Var 1)
      (Call 0 (SOME SumListLength_location)
         [Op El [Op (Const 1) []; Var 0];
          Op Add [Var 1; Op LengthByte
                           [Op El [Op (Const 0) []; Var 0]]]] NONE))`

val ConcatByte_code_def = Define`
  ConcatByte_code = (3n, (* list, current index, destination *)
    If (Op (TagLenEq nil_tag 0) [Var 0]) (Var 2)
      (Let [Op El [Op (Const 0) []; Var 0]]
        (Let [Op LengthByte [Var 0]]
          (Let [Op (CopyByte F)
                  [Var 3; Var 4; Var 0; Op (Const 0) []; Var 1]]
            (Call 0 (SOME ConcatByte_location)
              [Op El [Op (Const 1) []; Var 3];
               Op Add [Var 4; Var 1];
               Var 5] NONE)))))`;

val stubs_def = Define `
  stubs start n = [(AllocGlobal_location, AllocGlobal_code);
                   (CopyGlobals_location, CopyGlobals_code);
                   (InitGlobals_location, InitGlobals_code start n);
                   (ListLength_location, ListLength_code);
                   (FromListByte_location, FromListByte_code);
                   (ToListByte_location, ToListByte_code);
                   (SumListLength_location, SumListLength_code);
                   (ConcatByte_location, ConcatByte_code)]`;

Overload num_stubs[local] = ``backend_common$bvl_num_stubs``

local val compile_op_quotation = `
  compile_op op c1 =
    dtcase op of
    | Const i => (dtcase c1 of [] => compile_int i
                  | _ => Let [Op (Const 0) c1] (compile_int i))
    | Global n => (if NULL c1 then Op (Global (n+1)) []
                   else Let c1 (Op El [Op Add [Op (Const 2) []; Var 0];
                                       Op GlobalsPtr []]))
    | SetGlobal n => Op (SetGlobal (n+1)) c1
    | AllocGlobal => Call 0 (SOME AllocGlobal_location) c1 NONE
    | (FromList n) => Let (if NULL c1 then [Op (Const 0) []] else c1)
                        (Op (FromList n)
                        [Var 0; Call 0 (SOME ListLength_location)
                                   [Var 0; Op (Const 0) []] NONE])
    | Install => Let (if LENGTH c1 <> 2
                      then [Let c1 (Op (Const 0) []); Op (Const 0) []] else c1)
                        (Op Install
                        [Call 0 (SOME ListLength_location)
                           [Var 0; Op (Const 0) []] NONE;
                         Call 0 (SOME ListLength_location)
                           [Var 1; Op (Const 0) []] NONE;
                         Var 0; Var 1])
    | FromListByte =>
        Let (if NULL c1 then [Op (Const 0) []] else c1)
          (Call 0 (SOME FromListByte_location)
             [Var 0;
              Op (Const 0) [];
              Op (RefByte T)
                [Op (Const 0) [];
                 Call 0 (SOME ListLength_location)
                   [Var 0; Op (Const 0) []] NONE]]
             NONE)
    | ToListByte =>
        Let (if NULL c1 then [Op (Const 0) []] else c1)
          (Call 0 (SOME ToListByte_location)
             [Op (Cons 0) [];
              Op LengthByte [Var 0];
              Var 0]
             NONE)
    | ConcatByteVec =>
        Let (if NULL c1 then [Op (Const 0) []] else c1)
          (Call 0 (SOME ConcatByte_location)
            [Var 0;
             Op (Const 0) [];
             Op (RefByte T)
               [Op (Const 0) [];
                Call 0 (SOME SumListLength_location)
                  [Var 0; Op (Const 0) []] NONE]] NONE)
    | CopyByte T => (* TODO: this should eventually be implemented in data_to_word instead for efficiency *)
      Let (if LENGTH c1 < 3 then (c1 ++ REPLICATE 3 (Op (Const 0) [])) else c1)
        (Let [Op (RefByte T) [Op (Const 0) []; Var 0]]
           (Let [Op (CopyByte F) [Op (Const 0) []; Var 0; Var 1; Var 2; Var 3]]
             (Var 1)))
    | Label l => Op (Label (bvl_num_stubs + bvl_to_bvi_namespaces * l)) c1
    | Build ps => Op (Build ps) c1
    | EqualConst p => Op (EqualConst p) c1
    | _ => Op op c1`
in
val compile_op_def = Define compile_op_quotation;

Theorem compile_op_pmatch = Q.prove(
  `∀op c1.` @
    (compile_op_quotation |>
     map (fn QUOTE s => Portable.replace_string {from="dtcase",to="case"} s |> QUOTE
         | aq => aq)),
   rpt strip_tac
   >> rpt(CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV) >> every_case_tac)
   >> fs[compile_op_def]);
end

Overload "++"[local] = ``SmartAppend``
Overload "nss"[local] = ``bvl_to_bvi_namespaces``

Definition compile_aux_def:
  compile_aux (k,args,p) =
    List[(num_stubs + nss * k + 1, args, bvi_let$compile_exp p)]
End

Definition compile_exps_def:
  (compile_exps n [] = ([],Nil,n)) /\
  (compile_exps n ((x:bvl$exp)::y::xs) =
     let (c1,aux1,n1) = compile_exps n [x] in
     let (c2,aux2,n2) = compile_exps n1 (y::xs) in
       (c1 ++ c2, aux1 ++ aux2, n2)) /\
  (compile_exps n [Var v] = ([(Var v):bvi$exp], Nil, n)) /\
  (compile_exps n [If x1 x2 x3] =
     let (c1,aux1,n1) = compile_exps n [x1] in
     let (c2,aux2,n2) = compile_exps n1 [x2] in
     let (c3,aux3,n3) = compile_exps n2 [x3] in
       ([If (HD c1) (HD c2) (HD c3)],aux1++aux2++aux3,n3)) /\
  (compile_exps n [Let xs x2] =
     if NULL xs (* i.e. a marker *) then
       let (args,x0) = destLet x2 in
       let (c1,aux1,n1) = compile_exps n args in
       let (c2,aux2,n2) = compile_exps n1 [x0] in
       let n3 = n2 + 1 in
         ([Call 0 (SOME (num_stubs + nss * n2 + 1)) c1 NONE],
          aux1++aux2++compile_aux(n2,LENGTH args,HD c2), n3)
     else
       let (c1,aux1,n1) = compile_exps n xs in
       let (c2,aux2,n2) = compile_exps n1 [x2] in
         ([Let c1 (HD c2)], aux1++aux2, n2)) /\
  (compile_exps n [Raise x1] =
     let (c1,aux1,n1) = compile_exps n [x1] in
       ([Raise (HD c1)], aux1, n1)) /\
  (compile_exps n [Tick x1] =
     let (c1,aux1,n1) = compile_exps n [x1] in
       ([Tick (HD c1)], aux1, n1)) /\
  (compile_exps n [Op op xs] =
     let (c1,aux1,n1) = compile_exps n xs in
       ([compile_op op c1],aux1,n1)) /\
  (compile_exps n [Handle x1 x2] =
     let (args,x0) = destLet x1 in
     let (c1,aux1,n1) = compile_exps n args in
     let (c2,aux2,n2) = compile_exps n1 [x0] in
     let (c3,aux3,n3) = compile_exps n2 [x2] in
     let aux4 = compile_aux(n3,LENGTH args,HD c2) in
     let n4 = n3 + 1 in
       ([Call 0 (SOME (num_stubs + nss * n3 + 1)) c1 (SOME (HD c3))],
        aux1++aux2++aux3++aux4, n4)) /\
  (compile_exps n [Call ticks dest xs] =
     let (c1,aux1,n1) = compile_exps n xs in
       ([Call ticks
              (dtcase dest of
               | NONE => NONE
               | SOME n => SOME (num_stubs + nss * n)) c1 NONE],aux1,n1))
Termination
  WF_REL_TAC `measure (exp1_size o SND)`
  \\ REPEAT STRIP_TAC \\ TRY DECIDE_TAC
  \\ TRY (Cases_on `x1`) \\ fs [destLet_def]
  \\ TRY (Cases_on `x2`) \\ fs [destLet_def]
  \\ SRW_TAC [] [bvlTheory.exp_size_def] \\ DECIDE_TAC
End

val compile_exps_ind = theorem"compile_exps_ind";

val compile_exps_LENGTH_lemma = Q.prove(
  `!n xs. (LENGTH (FST (compile_exps n xs)) = LENGTH xs)`,
  HO_MATCH_MP_TAC compile_exps_ind \\ REPEAT STRIP_TAC
  \\ SIMP_TAC std_ss [compile_exps_def] \\ SRW_TAC [] []
  \\ FULL_SIMP_TAC (srw_ss()) [] \\ SRW_TAC [] [] \\ DECIDE_TAC);

Theorem compile_exps_LENGTH:
   (compile_exps n xs = (ys,aux,n1)) ==> (LENGTH ys = LENGTH xs)
Proof
  REPEAT STRIP_TAC \\ MP_TAC (SPEC_ALL compile_exps_LENGTH_lemma) \\ fs []
QED

Theorem compile_exps_SING:
   (compile_exps n [x] = (c,aux,n1)) ==> ?y. c = [y]
Proof
  REPEAT STRIP_TAC \\ IMP_RES_TAC compile_exps_LENGTH
  \\ Cases_on `c` \\ fs [LENGTH_NIL]
QED

Definition compile_single_def:
  compile_single n (name,arg_count,exp) =
    let (c,aux,n1) = compile_exps n [exp] in
      (List [(num_stubs + nss * name,arg_count,bvi_let$compile_exp (HD c))]
        ++ aux, n1)
End

Definition compile_list_def:
  (compile_list n [] = (List [],n)) /\
  (compile_list n (p::progs) =
     let (code1,n1) = compile_single n p in
     let (code2,n2) = compile_list n1 progs in
       (code1 ++ code2,n2))
End

Definition compile_inc_def: (* incremental version used by Install *)
  compile_inc n prog =
    let (p1,n1) = bvl_to_bvi$compile_list n prog in
      (n1,append p1)
End

Definition compile_prog_def:
  compile_prog start n prog =
    let k = alloc_glob_count (MAP (\(_,_,p). p) prog) in
    let (code,n1) = compile_list n prog in
      (InitGlobals_location, bvl_to_bvi$stubs (num_stubs + nss * start) k ++ append code, n1)
End

Datatype:
  config = <| inline_size_limit : num (* zero disables inlining *)
            ; exp_cut : num (* huge number effectively disables exp splitting *)
            ; split_main_at_seq : bool (* split main expression at Seqs *)
            ; next_name1 : num (* there should be as many of       *)
            ; next_name2 : num (* these as bvl_to_bvi_namespaces-1 *)
            ; inlines : (num # bvl$exp) spt
            |>
End

Definition default_config_def:
  default_config =
    <| inline_size_limit := 10
     ; exp_cut := 1000
     ; split_main_at_seq := T
     ; next_name1 := num_stubs + 1
     ; next_name2 := num_stubs + 2
     ; inlines := LN
     |>
End

Definition get_names_def:
  get_names final_nums old_names =
    fromAList (MAP (λn. (n,
      if n = InitGlobals_location then mlstring$strlit "start" else
      if n = AllocGlobal_location then mlstring$strlit "AllocGlobal" else
      if n = CopyGlobals_location then mlstring$strlit "CopyGlobals" else
      if n = ListLength_location then mlstring$strlit "ListLength" else
      if n = FromListByte_location then mlstring$strlit "FromListByte" else
      if n = ToListByte_location then mlstring$strlit "ToListByte" else
      if n = SumListLength_location then mlstring$strlit "SumListLength" else
      if n = ConcatByte_location then mlstring$strlit "ConcatByte" else
      if n < num_stubs then mlstring$strlit "bvi_unknown" else
        let k = n - num_stubs in
        let kd = k DIV nss in
        let km = k MOD nss in
        let n = (dtcase lookup kd old_names of
          | NONE => mlstring$strlit "bvi_unmapped"
          | SOME name => name) in
        let aux = (if km = 0 then mlstring$strlit "" else mlstring$strlit "_bvi_aux") in
          n ^ aux)) final_nums)
End

Definition compile_def:
  compile start c names prog =
    let (inlines, prog) = bvl_inline$compile_prog c.inline_size_limit
           c.split_main_at_seq c.exp_cut prog in
    let (loc, code, n1) = compile_prog start 0 prog in
    let (n2, code') = bvi_tailrec$compile_prog (num_stubs + 2) code in
      (loc, code', inlines, n1, n2, get_names (MAP FST code') names)
End

Definition bvl_to_bvi_compile_inc_all_def:
  bvl_to_bvi_compile_inc_all c p =
    let (inl, p) = bvl_inline$compile_inc c.inline_size_limit
        c.split_main_at_seq c.exp_cut c.inlines p in
    let c = c with <| inlines := inl |> in
    let (nn1, p) = bvl_to_bvi$compile_inc c.next_name1 p in
    let c = c with <| next_name1 := nn1 |> in
    let (nn2, p) = bvi_tailrec$compile_prog c.next_name2 p in
    let c = c with <| next_name2 := nn2 |> in
      (c, p)
End

val _ = export_theory();