Merge pull request #720 from CakeML/flat-to-clos

Compile flaLang directly to closLang

compiler/backend/Holmakefile

@@ -1,6 +1,7 @@
 INCLUDES = $(HOLDIR)/examples/machine-code/multiword\
 					 $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics $(CAKEMLDIR)/semantics/proofs\
 					 $(CAKEMLDIR)/basis/pure\
+					 pattern_matching\
 					 ../encoders/asm reg_alloc reachability
 
 all: $(DEFAULT_TARGETS) README.md

compiler/backend/README.md

@@ -178,15 +178,14 @@ replaces it with an alloc call with 0.
 [flat_elimScript.sml](flat_elimScript.sml):
 Implementation for flatLang dead-code elimination.
 
-[flat_exh_matchScript.sml](flat_exh_matchScript.sml):
-This compiler phase ensures that all pattern matches are exhaustive.
+[flat_patternScript.sml](flat_patternScript.sml):
+Interface between flatLang and pattern compiler.
 
-[flat_reorder_matchScript.sml](flat_reorder_matchScript.sml):
-This compiler phase reorders patterns in pattern matches to improve
-code quality.
-
-[flat_to_patScript.sml](flat_to_patScript.sml):
-This phase performs pattern-match compilation.
+[flat_to_closScript.sml](flat_to_closScript.sml):
+Compilation from flatLang to closLang. This compiler phase converts
+explicit variable names of flatLang to de Bruijn indexing of
+closLang. It also makes all division-by-zero and out-of-bounds
+exceptions raised explicitly.
 
 [flat_uncheck_ctorsScript.sml](flat_uncheck_ctorsScript.sml):
 This compiler phase replaces tuples with constructors (with tag 0).
@@ -220,17 +219,8 @@ compiler configuration.
 [mips](mips):
 This directory contains the mips-specific part of the compiler backend.
 
-[patLangScript.sml](patLangScript.sml):
-The patLang intermediate language follows immediately after
-pattern-match compilation from flatLang. The patLang language
-differs from earlier languages in that it uses de Bruijn indices
-for variable names.
-
-[pat_to_closScript.sml](pat_to_closScript.sml):
-The translation from patLang to closLang is very simple.
-Its main purpose is simplifying the semantics of some operations,
-for example to explicitly raise an exception for Div so the semantics
-in closLang can make more assumptions about the arguments.
+[pattern_matching](pattern_matching):
+The CakeML pattern matching expressions compiler
 
 [presLangScript.sml](presLangScript.sml):
 Functions for converting various intermediate languages

compiler/backend/backendComputeLib.sml

@@ -26,6 +26,7 @@ val add_backend_compset = computeLib.extend_compset
   [computeLib.Tys
     [ (* ---- configurations ---- *)
      ``:source_to_flat$config``
+    ,``:flat_pattern$config``
     ,``:clos_to_bvl$config``
     ,``:bvl_to_bvi$config``
     ,``:data_to_word$config``
@@ -72,16 +73,29 @@ val add_backend_compset = computeLib.extend_compset
     [ (* ---- source_to_flat ---- *)
      flatLangTheory.bool_id_def
     ,flatLangTheory.Bool_def
+    ,miscTheory.enumerate_def
     ]
   ,computeLib.Defs (theory_computes "source_to_flat")
       (* ---- flat_elim ---- *)
   ,computeLib.Defs (theory_computes "flat_elim")
+  ,computeLib.Defs (theory_computes "flat_pattern")
+  ,computeLib.Defs (theory_computes "flatLang")
+  ,computeLib.Defs (theory_computes "pattern_semantics")
+  ,computeLib.Defs (theory_computes "pattern_comp")
   ,computeLib.Defs (theory_computes "reachable_spt")
   ,computeLib.Tys
     [``:flatLang$op``
     ,``:flatLang$pat``
     ,``:flatLang$exp``
     ,``:flatLang$dec``
+    ,``:pattern_semantics$pat``
+    ,``:pattern_semantics$dTest``
+    ,``:pattern_semantics$dGuard``
+    ,``:pattern_semantics$dTree``
+    ,``:pattern_semantics$term``
+    ,``:pattern_common$position``
+    ,``:pattern_common$pmatchResult``
+    ,``:pattern_common$matchResult``
     ,``:source_to_flat$environment``
     ,``:source_to_flat$next_indices``
     ,``:source_to_flat$config``
@@ -93,27 +107,15 @@ val add_backend_compset = computeLib.extend_compset
 
   ,computeLib.Defs (theory_computes "flat_uncheck_ctors")
 
-  ,computeLib.Tys
-    [ (* ---- patLang ---- *)
-     ``:patLang$exp``
-    ,``:patLang$op``
-    ]
+  ,computeLib.Defs (theory_computes "flat_to_clos")
 
-      (* ---- flat_to_pat ---- *)
-  ,computeLib.Defs
-    [flat_to_patTheory.Bool_def
-    ,flat_to_patTheory.isBool_def
-    ,flat_to_patTheory.sIf_def
-    ,flat_to_patTheory.pure_op_op_eqn (* could put this in the compute set and avoid listing explicitly *)
-    ,flat_to_patTheory.pure_op_def
-    ,flat_to_patTheory.pure_def
-    ,flat_to_patTheory.ground_def
-    ,flat_to_patTheory.sLet_def
-    ,flat_to_patTheory.Let_Els_compute
-    ,flat_to_patTheory.compile_pat_def
-    ,flat_to_patTheory.compile_row_def
-    ,flat_to_patTheory.compile_exp_def
-    ,flat_to_patTheory.compile_def
+  ,computeLib.Tys
+    [``:closLang$exp``
+    ,``:closLang$op``
+    ,``:clos_known$val_approx``
+    ,``:clos_known$globalOpt``
+    ,``:clos_known$inliningDecision``
+    ,``:clos_known$config``
     ]
 
   ,computeLib.Tys
@@ -128,13 +130,6 @@ val add_backend_compset = computeLib.extend_compset
   ,computeLib.Defs
     [closLangTheory.pure_def
     ,closLangTheory.pure_op_def
-      (* ---- pat_to_clos ---- *)
-    ,pat_to_closTheory.dest_WordToInt_def
-    ,pat_to_closTheory.CopyByteStr_def
-    ,pat_to_closTheory.CopyByteAw8_def
-    ,pat_to_closTheory.vector_tag_def
-    ,pat_to_closTheory.compile_def
-      (*,pat_to_closTheory.pat_tag_shift_def*)
       (* ---- clos_mti ---- *)
     ,clos_mtiTheory.intro_multi_def
     ,clos_mtiTheory.collect_args_def

compiler/backend/backendScript.sml

@@ -6,8 +6,7 @@
 
 open preamble
      source_to_flatTheory
-     flat_to_patTheory
-     pat_to_closTheory
+     flat_to_closTheory
      clos_to_bvlTheory
      bvl_to_bviTheory
      bvi_to_dataTheory
@@ -46,12 +45,9 @@ val compile_tap_def = Define`
     let td = tap_flat c.tap_conf p [] in
     let _ = empty_ffi (strlit "finished: source_to_flat") in
     let c = c with source_conf := c' in
-    let p = flat_to_pat$compile p in
-    let td = tap_pat c.tap_conf p td in
-    let _ = empty_ffi (strlit "finished: flat_to_pat") in
-    let p = MAP pat_to_clos$compile p in
+    let p = flat_to_clos$compile_decs p in
     let td = tap_clos c.tap_conf p td in
-    let _ = empty_ffi (strlit "finished: pat_to_clos") in
+    let _ = empty_ffi (strlit "finished: flat_to_clos") in
     let (c',p) = clos_to_bvl$compile c.clos_conf p in
     let c = c with clos_conf := c' in
     let _ = empty_ffi (strlit "finished: clos_to_bvl") in
@@ -87,16 +83,10 @@ val to_flat_def = Define`
     let c = c with source_conf := c' in
     (c,p)`;
 
-val to_pat_def = Define`
-  to_pat c p =
-  let (c,p) = to_flat c p in
-  let p = flat_to_pat$compile p in
-  (c,p)`;
-
 val to_clos_def = Define`
   to_clos c p =
-  let (c,p) = to_pat c p in
-  let p = MAP pat_to_clos$compile p in
+  let (c,p) = to_flat c p in
+  let p = flat_to_clos$compile_decs p in
   (c,p)`;
 
 val to_bvl_def = Define`
@@ -160,7 +150,6 @@ Proof
      to_bvi_def,
      to_bvl_def,
      to_clos_def,
-     to_pat_def,
      to_flat_def] >>
   unabbrev_all_tac >>
   rpt (CHANGED_TAC (srw_tac[][] >> full_simp_tac(srw_ss())[] >> srw_tac[][] >> rev_full_simp_tac(srw_ss())[]))
@@ -215,15 +204,10 @@ val from_clos_def = Define`
   let c = c with clos_conf := c' in
   from_bvl c p`;
 
-val from_pat_def = Define`
-  from_pat c p =
-  let p = MAP pat_to_clos$compile p in
-  from_clos c p`;
-
 val from_flat_def = Define`
   from_flat c p =
-  let p = flat_to_pat$compile p in
-  from_pat c p`;
+  let p = flat_to_clos$compile_decs p in
+  from_clos c p`;
 
 val from_source_def = Define`
   from_source c p =
@@ -243,7 +227,6 @@ Proof
      from_bvi_def,
      from_bvl_def,
      from_clos_def,
-     from_pat_def,
      from_flat_def] >>
   unabbrev_all_tac >>
   rpt (CHANGED_TAC (srw_tac[][] >> full_simp_tac(srw_ss())[] >> srw_tac[][] >> rev_full_simp_tac(srw_ss())[]))
@@ -307,7 +290,6 @@ Proof
      to_bvi_def,
      to_bvl_def,
      to_clos_def,
-     to_pat_def,
      to_flat_def,to_livesets_def] >>
   fs[compile_def,compile_tap_def]>>
   pairarg_tac>>
@@ -352,7 +334,6 @@ Proof
      to_bvi_def,
      to_bvl_def,
      to_clos_def,
-     to_pat_def,
      to_flat_def,to_livesets_def] >>
   unabbrev_all_tac>>fs[]>>
   rpt(rfs[]>>fs[])
@@ -370,7 +351,7 @@ Theorem to_data_change_config:
                  bvl_conf := c1'.bvl_conf |>,
       prog')
 Proof
-  rw[to_data_def,to_bvi_def,to_bvl_def,to_clos_def,to_pat_def,to_flat_def]
+  rw[to_data_def,to_bvi_def,to_bvl_def,to_clos_def,to_flat_def]
   \\ rpt (pairarg_tac \\ fs[]) \\ rw[] \\ fs[] \\ rfs[] \\ rveq \\ fs[] \\ rfs[] \\ rveq \\ fs[]
   \\ simp[config_component_equality]
 QED

compiler/backend/bvl_to_bviScript.sml

@@ -120,7 +120,7 @@ val ConcatByte_location_eq = save_thm("ConcatByte_location_eq",
 val AllocGlobal_code_def = Define`
   AllocGlobal_code = (0:num,
     Let [Op GlobalsPtr []]
-     (Let [Op Deref [Op (Const 0) []; Var 0]]
+     (Let [Op El [Op (Const 0) []; Var 0]]
        (Let [Op Update [Op Add [Var 0; Op(Const 1)[]]; Op (Const 0) []; Var 1]]
          (Let [Op Length [Var 2]]
            (If (Op Less [Var 0; Var 2]) (Var 1)
@@ -130,7 +130,7 @@ val AllocGlobal_code_def = Define`
 
 val CopyGlobals_code_def = Define`
   CopyGlobals_code = (3:num, (* ptr to new array, ptr to old array, index to copy *)
-    Let [Op Update [Op Deref [Var 2; Var 1]; Var 2; Var 0]]
+    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)))`;
 
@@ -209,7 +209,7 @@ local val compile_op_quotation = `
     dtcase op of
     | Const i => (dtcase c1 of [] => compile_int i
                   | _ => Let [Op (Const 0) c1] (compile_int i))
-    | Global n => Op Deref (c1++[compile_int(&(n+1)); Op GlobalsPtr []])
+    | Global n => Op El (c1++[compile_int(&(n+1)); Op GlobalsPtr []])
     | SetGlobal n => Op Update (c1++[compile_int(&(n+1)); Op GlobalsPtr []])
     | AllocGlobal =>
         (dtcase c1 of [] => Call 0 (SOME AllocGlobal_location) [] NONE

compiler/backend/closLangScript.sml

@@ -25,7 +25,7 @@ val _ = Datatype `
                         indicating the first element, and how many, should be
                         copied into the end of the new block. The fourth
                         argument is the total size of the new block. *)
-     | El            (* read Block field index *)
+     | El            (* read Block field index or loads a value from a reference *)
      | LengthBlock   (* get length of Block *)
      | Length        (* get length of reference *)
      | LengthByte    (* get length of byte array *)
@@ -43,9 +43,9 @@ val _ = Datatype `
      | LengthByteVec (* get length of ByteVector *)
      | DerefByteVec  (* load a byte from a ByteVector *)
      | TagLenEq num num (* check Block's tag and length *)
+     | LenEq num     (* check Block's length *)
      | TagEq num     (* check Block's tag *)
      | Ref           (* makes a reference *)
-     | Deref         (* loads a value from a reference *)
      | Update        (* updates a reference *)
      | Label num     (* constructs a CodePtr *)
      | FFI string    (* calls the FFI *)

compiler/backend/clos_to_bvlScript.sml

@@ -126,7 +126,7 @@ val code_for_recc_case_def = Define `
   code_for_recc_case n num_args (c:bvl$exp) =
     (num_args + 1,
      Let [mk_el (Var num_args) (mk_const 2)]
-      (Let (GENLIST (\a. Var (a + 1)) num_args ++ GENLIST (\i. Op Deref [mk_const i; Var 0]) n) c))`;
+      (Let (GENLIST (\a. Var (a + 1)) num_args ++ GENLIST (\i. Op El [mk_const i; Var 0]) n) c))`;
 
 val build_aux_def = Define `
   (build_aux i [] aux = (i:num,aux)) /\