Add unit argument to unreachable.

This is a workaround for FStarLang/FStar#3473
FStarLang · Sep 12, 2024 · af2c55a · af2c55a
1 parent 44cad3e
commit af2c55a
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 11 deletions.
diff --git a/lib/pulse/lib/Pulse.Lib.Dv.fst b/lib/pulse/lib/Pulse.Lib.Dv.fst
@@ -18,4 +18,4 @@ module Pulse.Lib.Dv
 
 let while_ cond body = ()
 let par f1 f2 = ()
-let rec unreachable t = unreachable t
+let rec unreachable t () = unreachable t ()
diff --git a/lib/pulse/lib/Pulse.Lib.Dv.fsti b/lib/pulse/lib/Pulse.Lib.Dv.fsti
@@ -18,4 +18,4 @@ module Pulse.Lib.Dv
 
 val while_ (cond: unit -> Dv bool) (body: unit -> Dv unit) : Dv unit
 val par (f1: unit -> Dv unit) (f2: unit -> Dv unit) : Dv unit
-val unreachable (t: Type0) : Dv t
+val unreachable (t: Type0) : unit -> Dv t
diff --git a/src/checker/Pulse.Extract.Main.fst b/src/checker/Pulse.Extract.Main.fst
@@ -462,7 +462,7 @@ let rec extract_dv g (p:st_term) : T.Tac ECL.term =
 
     | Tm_Unreachable { c } ->
       ECL.mk_meta_monadic (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv ["Pulse"; "Lib"; "Dv"; "unreachable"])))
-        [comp_res c, R.Q_Explicit])
+        [comp_res c, R.Q_Explicit; unit_tm, R.Q_Explicit])
 
     | Tm_WithInv { body } -> extract_dv g body
 

diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
@@ -123,7 +123,7 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
     when (string_of_mlpath p = "Pulse.Lib.Dv.while_") ->
     EWhile(cb test, cb body)
 
-  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _ ])
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _ ])
     when (string_of_mlpath p = "Pulse.Lib.Dv.unreachable") ->
     EAbortS (string_of_mlpath p)
 

diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml
diff --git a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml