Merge pull request #250 from FStarLang/afromher_steel

Native extraction of Steel loops

src/Simplify.ml

@@ -1544,6 +1544,10 @@ let combinators = object(self)
       when KString.starts_with s "for_loop" ->
         self#mk_for start finish body K.UInt32
 
+    | EQualified (["Steel"; "Loops"], s), [ start; finish; _inv; { node = EFun (_, body, _); _ } ]
+      when KString.starts_with s "for_loop" ->
+        self#mk_for start finish body K.UInt32
+
     | EQualified ("C" :: (["Loops"]|["Compat";"Loops"]), s), [ _measure; _inv; tcontinue; body; init ]
         when KString.starts_with s "total_while_gen"
        ->
@@ -1622,6 +1626,13 @@ let combinators = object(self)
         EWhile (DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () test),
           DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () body))
 
+    | EQualified (["Steel"; "Loops"], s), [ _inv;
+        { node = EFun (_, test, _); _ };
+        { node = EFun (_, body, _); _ } ]
+      when KString.starts_with s "while_loop" ->
+        EWhile (DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () test),
+          DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () body))
+
     | EQualified ("C" :: (["Loops"]|["Compat";"Loops"]), s), [ { node = EFun (_, body, _); _ } ]
       when KString.starts_with s "do_while" ->
         EWhile (etrue, with_unit (

test/Makefile

@@ -69,7 +69,7 @@ ifndef NODEPEND
 # AF: The Steel files should not be extracted by KaRaMeL, they are filtered out
 .depend: .FORCE
 	$(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \
-	  $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel' > $@
+	  $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel.Effect,-Steel.Effect.Atomic,-Steel.HigherReference,-Steel.Reference,-Steel.Semantics.Hoare.MST' > $@
 
 .PHONY: .FORCE
 .FORCE:
@@ -78,6 +78,19 @@ endif
 
 include .depend
 
+# AF: The Steel files should not be extracted by KaRaMeL, they are filtered out
+FILTERED_STEEL_FILES = \
+  $(OUTPUT_DIR)/FStar_MSTTotal.krml \
+  $(OUTPUT_DIR)/FStar_NMSTTotal.krml \
+  $(OUTPUT_DIR)/FStar_NMST.krml \
+  $(OUTPUT_DIR)/FStar_MST.krml \
+  $(OUTPUT_DIR)/Steel_Effect.krml \
+  $(OUTPUT_DIR)/Steel_Effect_Atomic.krml \
+  $(OUTPUT_DIR)/Steel_HigherReference.krml \
+  $(OUTPUT_DIR)/Steel_Reference.krml \
+  $(OUTPUT_DIR)/Steel_Semantics_Hoare_MST.krml
+FILTERED_KRML_FILES = $(filter-out $(FILTERED_STEEL_FILES), $(ALL_KRML_FILES))
+
 $(HINTS_DIR):
 	mkdir -p $@
 

test/SteelLoops.fst

@@ -0,0 +1,35 @@
+module SteelLoops
+
+open Steel.Effect.Atomic
+open Steel.Effect
+open Steel.Reference
+open Steel.Loops
+
+let sum_to_n_for (r:ref UInt32.t) : SteelT unit (vptr r) (fun _ -> vptr r) =
+  for_loop
+    0ul
+    10ul
+    (fun _ -> vptr r)
+    (fun _ -> let x = read r in write r (x `FStar.UInt32.add_mod` 1ul))
+
+let sum_to_n_while (r:ref UInt32.t) : SteelT unit (vptr r) (fun _ -> vptr r) =
+  intro_exists (Ghost.hide true) (fun _ -> vptr r);
+  while_loop
+    (fun _ -> vptr r)
+    (fun _ ->
+      let _ = witness_exists () in
+      let n = read r in
+      FStar.UInt32.lt n 10ul
+    )
+    (fun _ ->
+      let n = read r in
+      write r (n `FStar.UInt32.add_mod` 1ul);
+      intro_exists (Ghost.hide true) (fun _ -> vptr r)
+    )
+
+let main () : SteelT Int32.t emp (fun _ -> emp) =
+  let r = malloc 0ul in
+  sum_to_n_for r;
+  sum_to_n_while r;
+  free r;
+  return 0l