Merge remote-tracking branch 'origin/master' into let-lift

.gitignore

@@ -75,4 +75,8 @@ compiler/benchmarks/sml/polyc_*
 compiler/benchmarks/sml/sml_*
 compiler/benchmarks/*.dat
 compiler/benchmarks/*.eps
+
+#sexp files generated by Icing
+icing/examples/output/*/*.sexp.cml
+icing/examples/*_data_prog.txt
 .DS_Store

README.md

@@ -63,6 +63,10 @@ particular:
 - a list of how CakeML differs from SML and OCaml, and,
 - a number of small CakeML code examples.
 
+[icing](icing):
+Main implementation directory for the RealCake development, presented in
+"Verified Compilation and Optimization of Floating-Point Programs"
+
 [misc](misc):
 Auxiliary files providing glue between a standard HOL installation
 and what we want to use for CakeML development.

basis/ArrayProgScript.sml

@@ -113,7 +113,8 @@ val array_appi_aux = process_topdecs
   `fun appi_aux f arr max n =
     if n = max
       then ()
-    else (f n (sub arr n); app_aux f arr max (n + 1))`
+    else (f n (sub arr n): unit;
+          appi_aux f arr max (n + 1))`
 
 val _ = append_prog array_appi_aux;
 

basis/ArrayProofScript.sml

@@ -383,6 +383,79 @@ Proof
   rw [NUM_def]
 QED
 
+Theorem array_appi_aux_spec:
+   ∀l idx len_v idx_v a_v f_v eff.
+   NUM (LENGTH l) len_v ∧
+   NUM idx idx_v ∧
+   idx ≤ LENGTH l ∧
+   (!n n_v.
+      n < LENGTH l ∧
+      NUM n n_v ⇒
+      app p f_v [n_v; EL n l] (eff l n)
+                (POSTv v. &UNIT_TYPE () v * (eff l (n+1))))
+   ⇒
+   app (p:'ffi ffi_proj) Array_appi_aux_v [f_v; a_v; len_v; idx_v]
+     (eff l idx * ARRAY a_v l)
+     (POSTv v. &UNIT_TYPE () v * (eff l (LENGTH l)) * ARRAY a_v l)
+Proof
+  ntac 2 gen_tac >>
+  completeInduct_on `LENGTH l - idx` >>
+  xcf_with_def "Array.appi_aux" Array_appi_aux_v_def >>
+  rw [] >>
+  xlet `POSTv env_v. eff l idx * ARRAY a_v l * &BOOL (idx = LENGTH l) env_v`
+  >- (
+    xapp_spec eq_num_v_thm >>
+    xsimpl >>
+    fs [NUM_def, BOOL_def, INT_def]) >>
+  xif
+  >- (
+    xret >>
+    xsimpl) >>
+  xlet `POSTv x_v. eff l idx * ARRAY a_v l * &(EL idx l = x_v)`
+  >- (
+    xapp >>
+    xsimpl >>
+    qexists_tac `idx` >>
+    rw []) >>
+  xlet `POSTv u_v. eff l (idx + 1) * ARRAY a_v l`
+  >- (
+    first_x_assum (qspec_then `idx` mp_tac) >>
+    simp [] >>
+    disch_then xapp_spec >>
+    xsimpl) >>
+  xlet `POSTv next_idx_v. eff l (idx + 1) * ARRAY a_v l * & NUM (idx + 1) next_idx_v`
+  >- (
+    xapp >>
+    xsimpl >>
+    fs [NUM_def, INT_def] >>
+    intLib.ARITH_TAC) >>
+  first_x_assum xapp_spec >>
+  simp []
+QED
+
+(* eff is the effect of executing the function on the first n elements of l *)
+Theorem array_appi_spec:
+   ∀l a_v f_v eff.
+   (!n n_v.
+     n < LENGTH l ∧
+     NUM n n_v ⇒
+     app p f_v [n_v; EL n l] (eff l n)
+               (POSTv v. &UNIT_TYPE () v * (eff l (n+1))))
+   ⇒
+   app (p:'ffi ffi_proj) ^(fetch_v "Array.appi" array_st) [f_v; a_v]
+     (eff l 0 * ARRAY a_v l)
+     (POSTv v. &UNIT_TYPE () v * (eff l (LENGTH l)) * ARRAY a_v l)
+Proof
+  rw [] >>
+  xcf "Array.appi" array_st  >>
+  xlet `POSTv len_v. eff l 0 * ARRAY a_v l * &NUM (LENGTH l) len_v`
+  >- (
+    xapp >>
+    xsimpl) >>
+  xapp >>
+  rw [NUM_def]
+QED
+
 val list_rel_take_thm = Q.prove(
   `!A xs ys n.
       LIST_REL A xs ys ==> LIST_REL A (TAKE n xs) (TAKE n ys)`,

basis/MapProgScript.sml

@@ -66,34 +66,46 @@ val _ = translate insertMin_def;
 val _ = translate insertMax_def;
 val _ = translate bin_def;
 val _ = translate link_def;
+val _ = translate link2_def;
 val _ = translate filterLt_help_def;
 val _ = translate filterLt_def;
 val _ = translate filterGt_help_def;
 val _ = translate filterGt_def;
 val _ = translate insertR_def;
 val _ = translate hedgeUnion_def;
+val _ = next_ml_names := ["lookup"];
+val _ = translate lookup_def;
+val _ = translate hedgeUnionWithKey_def;
 val _ = translate splitLookup_def;
 val _ = translate submap'_def;
 
 (* Exported functions *)
 val _ = next_ml_names :=
-  ["null", "lookup", "member", "empty", "insert", "delete",
-            "union", "foldrWithKey", "toAscList", "compare", "map",
-            "isSubmapOfBy", "isSubmapOf", "fromList"];
+  ["null", "member", "empty", "insert", "delete",
+   "union", "unionWithKey", "unionWith", "foldrWithKey",
+   "toAscList", "compare", "mapWithKey", "map", "isSubmapOfBy",
+   "isSubmapOf", "fromList", "filterWithKey", "filter", "all",
+   "exists"];
 val _ = translate null_def;
-val _ = translate lookup_def;
 val _ = translate member_def;
 val _ = translate empty_def;
 val _ = translate insert_def;
 val _ = translate delete_def;
 val _ = translate union_def;
+val _ = translate unionWithKey_def;
+val _ = translate unionWith_def;
 val _ = translate foldrWithKey_def;
 val _ = translate toAscList_def;
 val _ = translate compare_def;
+val _ = translate mapWithKey_def;
 val _ = translate map_def;
 val _ = translate isSubmapOfBy_def;
 val _ = translate isSubmapOf_def;
 val _ = translate fromList_def;
+val _ = translate filterWithKey_def;
+val _ = translate filter_def;
+val _ = translate every_def;
+val _ = translate exists_def;
 
 val _ = ml_prog_update open_local_in_block;
 
@@ -111,14 +123,22 @@ val _ = next_ml_names := ["delete"];
 val _ = translate mlmapTheory.delete_def;
 val _ = next_ml_names := ["null"];
 val _ = translate mlmapTheory.null_def;
+val _ = next_ml_names := ["size"];
+val _ = translate mlmapTheory.size_def;
 val _ = next_ml_names := ["empty"];
 val _ = translate mlmapTheory.empty_def;
 val _ = next_ml_names := ["union"];
 val _ = translate mlmapTheory.union_def;
+val _ = next_ml_names := ["unionWith"];
+val _ = translate mlmapTheory.unionWith_def;
+val _ = next_ml_names := ["unionWithKey"];
+val _ = translate mlmapTheory.unionWithKey_def;
 val _ = next_ml_names := ["foldrWithKey"];
 val _ = translate mlmapTheory.foldrWithKey_def;
 val _ = next_ml_names := ["map"];
 val _ = translate mlmapTheory.map_def;
+val _ = next_ml_names := ["mapWithKey"];
+val _ = translate mlmapTheory.mapWithKey_def;
 val _ = next_ml_names := ["toAscList"];
 val _ = translate mlmapTheory.toAscList_def;
 val _ = next_ml_names := ["fromList"];
@@ -127,6 +147,14 @@ val _ = next_ml_names := ["isSubmapBy"];
 val _ = translate mlmapTheory.isSubmapBy_def;
 val _ = next_ml_names := ["isSubmap"];
 val _ = translate mlmapTheory.isSubmap_def;
+val _ = next_ml_names := ["all"];
+val _ = translate mlmapTheory.all_def;
+val _ = next_ml_names := ["exists"];
+val _ = translate mlmapTheory.exists_def;
+val _ = next_ml_names := ["filterWithKey"];
+val _ = translate mlmapTheory.filterWithKey_def;
+val _ = next_ml_names := ["filter"];
+val _ = translate mlmapTheory.filter_def;
 
 val _ = ml_prog_update (close_module NONE);
 

basis/TextIOProofScript.sml

@@ -824,7 +824,7 @@ val instream_buffered_inv_def = Define `
       bactive = TAKE (w-r) (DROP r bcontent))`;
       (*(bactive = [] <=> r = w))*)
 
-Overload TypeStamp_InstreamBuffered = “TypeStamp "InstreamBuffered" 12”;
+Overload TypeStamp_InstreamBuffered = “TypeStamp "InstreamBuffered" 35”;
 
 val INSTREAM_BUFFERED_def = Define `
   INSTREAM_BUFFERED bactive is =

basis/basisProgScript.sml

@@ -14,7 +14,7 @@ val eval_thm = let
   val state = get_ml_prog_state () |> ml_progLib.get_state
   val goal = list_mk_icomb (prim_mk_const {Thy="ml_prog", Name="eval_rel"},
     [state, env, print_e, state, mk_var ("x", v_ty)])
-  val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[])
+  val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[semanticPrimitivesTheory.state_component_equality])
   val v_thm = prove(mk_imp(lemma |> concl |> rand, goal),
     rpt strip_tac \\ rveq \\ match_mp_tac(#2(EQ_IMP_RULE lemma))
     \\ asm_simp_tac bool_ss [])