Merge pull request #759 from formal-land/guillaume-claret@more-instructions-simulate

simulate: support more instructions

Author: clarus

CoqOfRust/M.v

@@ -392,6 +392,7 @@ Module LowM.
   | LetAlloc (ty : Ty.t) (e : t A) (k : A -> t A)
   | Loop (ty : Ty.t) (body : t A) (k : A -> t A)
   | MatchTuple (tuple : Value.t) (k : list Value.t -> t A)
+  | IfThenElse (ty : Ty.t) (cond : Value.t) (then_ : t A) (else_ : t A) (k : A -> t A)
   | Impossible (message : string).
   Arguments Pure {_}.
   Arguments CallPrimitive {_}.
@@ -401,6 +402,7 @@ Module LowM.
   Arguments LetAlloc {_}.
   Arguments Loop {_}.
   Arguments MatchTuple {_}.
+  Arguments IfThenElse {_}.
   Arguments Impossible {_}.
 
   Fixpoint let_ {A : Set} (e1 : t A) (e2 : A -> t A) : t A :=
@@ -420,6 +422,8 @@ Module LowM.
       LetAlloc ty e (fun v => let_ (k v) e2)
     | MatchTuple tuple k =>
       MatchTuple tuple (fun fields => let_ (k fields) e2)
+    | IfThenElse ty cond then_ else_ k =>
+      IfThenElse ty cond then_ else_ (fun v => let_ (k v) e2)
     | Impossible message => Impossible message
     end.
 End LowM.
@@ -922,13 +926,8 @@ Module SubPointer.
   Parameter get_slice_rest : Value.t -> Z -> Z -> M.
 End SubPointer.
 
-(** Explicit definition to simplify the links later *)
-Definition if_then_else_bool (condition : Value.t) (then_ else_ : M) : M :=
-  match condition with
-  | Value.Bool true => then_
-  | Value.Bool false => else_
-  | _ => impossible "if_then_else_bool: expected a boolean"
-  end.
+Definition if_then_else_bool (ty : Ty.t) (condition : Value.t) (then_ else_ : M) : M :=
+  LowM.IfThenElse ty condition then_ else_ LowM.Pure.
 
 Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
   let* value := deref value in

CoqOfRust/core/ops/links/function.v

@@ -39,8 +39,7 @@ Module Impl_FnOnce_for_Function2.
     { constructor.
       destruct args as [a1 a2].
       with_strategy transparent [φ] cbn.
-      run_symbolic_closure.
-      intros []; run_symbolic.
+      run_symbolic.
     }
   Defined.
 

CoqOfRust/examples/default/examples/custom/simulate/mutations.v

@@ -13,7 +13,7 @@ Module Option.
 
   Lemma unwrap_or_eq {A : Set} `{Link A} (value : option A) (default : A) :
     {{
-      StackM.eval_f (Stack := []) (run_unwrap_or value default) tt 🌲
+      SimulateM.eval_f (Stack := []) (run_unwrap_or value default) tt 🌲
       (Output.Success (unwrap_or value default), tt)
     }}.
   Proof.
@@ -37,7 +37,7 @@ Lemma apply_duplicate_eq (numbers : Numbers.t) :
   let ref_numbers :=
     {| Ref.core := Ref.Core.Mutable (A := Numbers.t) 0%nat [] φ Some (fun _ => Some) |} in
   {{
-    StackM.eval_f (Stack := [_]) (run_apply_duplicate ref_numbers) (numbers, tt) 🌲
+    SimulateM.eval_f (Stack := [_]) (run_apply_duplicate ref_numbers) (numbers, tt) 🌲
     (Output.Success tt, (apply_duplicate numbers, tt))
   }}.
 Proof.
@@ -54,7 +54,7 @@ Lemma duplicate_eq (a b c : U64.t) :
   let ref_b := {| Ref.core := Ref.Core.Mutable (A := U64.t) 1%nat [] φ Some (fun _ => Some) |} in
   let ref_c := {| Ref.core := Ref.Core.Mutable (A := U64.t) 2%nat [] φ Some (fun _ => Some) |} in
   {{
-    StackM.eval_f (Stack := [_; _; _]) (run_duplicate ref_a ref_b ref_c) (a, (b, (c, tt))) 🌲
+    SimulateM.eval_f (Stack := [_; _; _]) (run_duplicate ref_a ref_b ref_c) (a, (b, (c, tt))) 🌲
     (Output.Success tt, (a, (a, (a, tt))))
   }}.
 Proof.

CoqOfRust/lib/lib.v

@@ -295,7 +295,7 @@ Global Opaque repeat.
 
 Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
   let* are_equal := M.call_closure (Ty.path "bool") BinOp.eq [value; expected_value] in
-  if_then_else_bool are_equal (pure (Value.Tuple [])) break_match.
+  if_then_else_bool (Ty.tuple []) are_equal (pure (Value.Tuple [])) break_match.
 
 (** There is an automatic instanciation of the function traits for closures and functions. *)
 Module FunctionTraitAutomaticImpl.