More SC fixes

CoqOfRust/M.v

@@ -1,6 +1,8 @@
 (** * The definition of a Rust monad. *)
 Require Coq.Strings.String.
 
+Local Open Scope list.
+
 Inductive sigS {A : Type} (P : A -> Set) : Set :=
 | existS : forall (x : A), P x -> sigS P.
 Arguments existS {_ _}.
@@ -79,11 +81,13 @@ Module LowM.
   | Pure : A -> t A
   | CallPrimitive {B : Set} : Primitive B -> (B -> t A) -> t A
   | Cast {B1 B2 : Set} : B1 -> (B2 -> t A) -> t A
+  | Loop {B : Set} : t B -> (B -> bool) -> (B -> t A) -> t A
   | Impossible : t A
   | Call {B : Set} : t B -> (B -> t A) -> t A.
   Arguments Pure {_}.
   Arguments CallPrimitive {_ _}.
   Arguments Cast {_ _ _}.
+  Arguments Loop {_ _}.
   Arguments Impossible {_}.
   Arguments Call {_ _}.
 
@@ -94,6 +98,7 @@ Module LowM.
       CallPrimitive primitive (fun v => let_ (k v) f)
     | Cast v k =>
       Cast v (fun v' => let_ (k v') f)
+    | Loop body is_break k => Loop body is_break (fun v => let_ (k v) f)
     | Impossible => Impossible
     | Call e k => Call e (fun v => let_ (k v) f)
     end.
@@ -108,6 +113,8 @@ Module Exception.
   | Continue : t
   (** exceptions for Rust's `break` *)
   | Break : t
+  (** to translate the [match] patterns with (de)references *)
+  | BreakMatch : t
   | Panic : Coq.Strings.String.string -> t.
 End Exception.
 Definition Exception : Set := Exception.t.
@@ -167,32 +174,15 @@ Definition continue {A : Set} : M A :=
 Definition break {A : Set} : M A :=
   raise Exception.Break.
 
+Definition break_match {A : Set} : M A :=
+  raise Exception.BreakMatch.
+
 Definition panic {A : Set} (message : Coq.Strings.String.string) : M A :=
   raise (Exception.Panic message).
 
 Definition call {A : Set} (e : M A) : M A :=
   LowM.Call e LowM.Pure.
 
-(* TODO: define for every (A : Set) in (M A) *)
-(** the definition of a function representing the loop construction *)
-(* Definition loop (m : M unit) : M unit :=
-  fix F (fuel : nat) {struct fuel} :=
-    match fuel with
-    | 0 => LowM.Pure (inr Exception.NonTermination)
-    | S fuel' =>
-      let- v := m fuel in
-      match v with
-      (* only Break ends the loop *)
-      | inl tt                 => F fuel'
-      | inr Exception.Continue => F fuel'
-      | inr Exception.Break    => LowM.Pure (inl tt)
-      (* every other exception is kept *)
-      | inr (Exception.Return _)
-      | inr (Exception.Panic _)
-      | inr Exception.NonTermination => LowM.Pure (v)
-      end
-    end. *)
-
 Definition alloc {A : Set} (v : A) : M (Ref A) :=
   let- ref := LowM.CallPrimitive (Primitive.StateAlloc v) LowM.Pure in
   LowM.Pure (inl ref).
@@ -257,3 +247,51 @@ Definition catch_return {A : Set} (body : M A) : M A :=
       | _ => raise exception
       end
     ).
+
+Definition catch_continue (body : M unit) : M unit :=
+  catch
+    body
+    (fun exception =>
+      match exception with
+      | Exception.Continue => pure tt
+      | _ => raise exception
+      end
+    ).
+
+Definition catch_break (body : M unit) : M unit :=
+  catch
+    body
+    (fun exception =>
+      match exception with
+      | Exception.Break => pure tt
+      | _ => raise exception
+      end
+    ).
+
+Definition loop (body : M unit) : M unit :=
+  LowM.Loop
+    (catch_continue body)
+    (fun result =>
+      match result with
+      | inl _ => false
+      | inr _ => true
+      end)
+    (fun result =>
+      catch_break (LowM.Pure result)).
+
+Fixpoint match_operator {A B : Set}
+    (scrutinee : A)
+    (arms : list (A -> M B)) :
+    M B :=
+  match arms with
+  | nil => impossible
+  | arm :: arms =>
+    catch
+      (arm scrutinee)
+      (fun exception =>
+        match exception with
+        | Exception.BreakMatch => match_operator scrutinee arms
+        | _ => raise exception
+        end
+      )
+  end.

CoqOfRust/core/iter.v

@@ -427,8 +427,8 @@ Module traits.
       where
           I: Iterator,
       *)
-      Global Instance I_Iterator (I Item : Set)
-          {H0 : iterator.Iterator.Trait I (Item := Item)} :
+      Global Instance I_Iterator {I Item : Set}
+          (H0 : iterator.Iterator.Trait I (Item := Item)) :
           IntoIterator.Trait I := {
         Item := Item;
         IntoIter := I;
@@ -442,7 +442,7 @@ End traits.
 (*
 impl<'a, T> Iterator for Iter<'a, T>
 *)
-Global Instance I_Iter (T : Set) :
+Global Instance I_Iter {T : Set} :
   traits.iterator.Iterator.Trait (slice.iter.Iter.t T) (Item := T).
 Admitted.
 
@@ -451,9 +451,9 @@ impl<A, B> Iterator for Zip<A, B>where
     A: Iterator,
     B: Iterator,
 *)
-Global Instance I_Zip (A B Item_A Item_B : Set)
-    {H0 : traits.iterator.Iterator.Trait A (Item := Item_A)}
-    {H1 : traits.iterator.Iterator.Trait B (Item := Item_B)} :
-    traits.iterator.Iterator.Trait
-      (adapters.zip.Zip.t A B) (Item := Item_A * Item_B).
+Global Instance I_Zip {A B Item_A Item_B : Set}
+  (H0 : traits.iterator.Iterator.Trait A (Item := Item_A))
+  (H1 : traits.iterator.Iterator.Trait B (Item := Item_B)) :
+  traits.iterator.Iterator.Trait
+    (adapters.zip.Zip.t A B) (Item := Item_A * Item_B).
 Admitted.

CoqOfRust/core/ops.v

@@ -603,6 +603,22 @@ Module control_flow.
     | Break : B -> t B C.
     Arguments Continue {_ _}.
     Arguments Break {_ _}.
+
+    Global Instance Get_Continue_0 {B C : Set} : Notations.Dot "Continue.0" := {
+      Notations.dot :=
+        Ref.map (Big := t B C)
+          (fun α => match α with | Continue α0 => Some α0 | _ => None end)
+          (fun β α =>
+            match α with | Continue _ => Some (Continue β) | _ => None end);
+    }.
+
+    Global Instance Get_Break_0 {B C : Set} : Notations.Dot "Break.0" := {
+      Notations.dot :=
+        Ref.map (Big := t B C)
+          (fun α => match α with | Break α0 => Some α0 | _ => None end)
+          (fun β α =>
+            match α with | Break _ => Some (Break β) | _ => None end);
+    }.
   End ControlFlow.
 End control_flow.
 

CoqOfRust/core/option.v

@@ -44,6 +44,21 @@ Module Option.
   | Some : T -> t T.
   Arguments None {_}.
   Arguments Some {_}.
+
+  Global Instance Get_Some_0 {T : Set} : Notations.Dot "Some.0" := {
+      Notations.dot :=
+        Ref.map (Big := t T)
+          (fun α =>
+            match α with
+            | Some α0 => Datatypes.Some α0
+            | _ => Datatypes.None
+            end)
+          (fun β α =>
+            match α with
+            | Some _ => Datatypes.Some (Some β)
+            | _ => Datatypes.None
+            end);
+    }.
 End Option.
 
 Module Impl_Option. Section Impl_Option.

CoqOfRust/core/result_types.v

@@ -48,4 +48,18 @@ Module Result.
   | Err : E -> t T E.
   Arguments Ok {T E} _.
   Arguments Err {T E} _.
+
+  Global Instance Get_Ok_0 {T E : Set} : Notations.Dot "Ok.0" := {
+    Notations.dot :=
+      Ref.map (Big := t T E)
+        (fun α => match α with Ok α0 => Some α0 | _ => None end)
+        (fun β α => match α with Ok _ => Some (Ok β) | _ => None end);
+  }.
+
+  Global Instance Get_Err_0 {T E : Set} : Notations.Dot "Err.0" := {
+    Notations.dot :=
+      Ref.map (Big := t T E)
+        (fun α => match α with Err α0 => Some α0 | _ => None end)
+        (fun β α => match α with Err _ => Some (Err β) | _ => None end);
+  }.
 End Result.