Add no-std examples

CoqOfRust/alloc/links/raw_vec.v

@@ -0,0 +1,55 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import alloc.links.alloc.
+Require Import alloc.raw_vec.
+
+Module RawVec.
+  Parameter t : Set -> Set -> Set.
+
+  Parameter to_value : forall {T A : Set}, t T A -> Value.t.
+
+  Global Instance IsLink (T A : Set) `(Link T) `(Link A) : Link (t T A) := {
+    Φ := Ty.apply (Ty.path "alloc::raw_vec::RawVec") [] [Φ T; Φ A];
+    φ := to_value;
+  }.
+
+  Definition of_ty (T' A' : Ty.t) : 
+    OfTy.t T' ->
+    OfTy.t A' ->
+    OfTy.t (Ty.apply (Ty.path "alloc::raw_vec::RawVec") [] [T'; A']).
+  Proof. 
+    intros [T] [A].
+    eapply OfTy.Make with (A := t T A). 
+    subst.
+    reflexivity. 
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+End RawVec.
+
+Module Impl_RawVec_T_A.
+  Definition Self (T A : Set) `{Link T} `{Link A} : Set :=
+    RawVec.t T A.
+
+  (*
+    pub const fn new_in(alloc: A) -> Self
+  *)
+  Instance run_new_in {T A : Set} `{Link T} `{Link A} (alloc : A) :
+    Run.Trait
+      (raw_vec.Impl_alloc_raw_vec_RawVec_T_A.new_in (Φ T) (Φ A)) [] [] [φ alloc]
+      (Self T A).
+  Admitted.
+End Impl_RawVec_T_A.
+Export Impl_RawVec_T_A.
+
+Module Impl_RawVec_T.
+  Definition Self (T : Set) `{Link T} : Set :=
+    RawVec.t T Global.t.
+
+  (*
+    pub const fn new() -> Self
+  *)
+  Instance run_new {T : Set} `{Link T} :
+    Run.Trait (raw_vec.Impl_alloc_raw_vec_RawVec_T_alloc_alloc_Global.new (Φ T)) [] [] [] (Self T).
+  Admitted.
+End Impl_RawVec_T.
+Export Impl_RawVec_T.

CoqOfRust/alloc/vec/links/mod.v

@@ -2,23 +2,32 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import alloc.vec.mod.
 Require Import links.M.
 Require Import alloc.links.alloc.
+Require Import alloc.links.raw_vec.
 Require Import core.links.clone.
 Require Import core.links.default.
 Require Import core.links.option.
 Require Import core.ops.links.deref.
 Require Import core.ops.links.index.
 
+(*
+pub struct Vec<T, A: Allocator = Global> {
+    buf: RawVec<T, A>,
+    len: usize,
+}
+*)
 Module Vec.
   Record t {T A : Set} : Set := {
-    value : list T;
+    buf : RawVec.t T A;
+    len : Usize.t;
   }.
   Arguments t : clear implicits.
 
-  Parameter to_value : forall {T A : Set}, t T A -> Value.t.
-
   Global Instance IsLink (T A : Set) `(Link T) `(Link A) : Link (t T A) := {
     Φ := Ty.apply (Ty.path "alloc::vec::Vec") [] [Φ T; Φ A];
-    φ := to_value;
+    φ x := Value.StructRecord "alloc::vec::Vec" [] [Φ T; Φ A] [
+      ("buf", φ x.(buf));
+      ("len", φ x.(len))
+    ];
   }.
 
   Definition of_ty (T' A' : Ty.t) : 
@@ -32,6 +41,40 @@ Module Vec.
     reflexivity. 
   Defined.
   Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with {T A : Set} `{Link T} `{Link A}
+    (buf' : Value.t) (buf : RawVec.t T A)
+    (len' : Value.t) (len : Usize.t) :
+    buf' = φ buf ->
+    len' = φ len ->
+    Value.StructRecord "alloc::vec::Vec" [] [Φ T; Φ A] [("buf", buf'); ("len", len')] =
+      φ ({| buf := buf; len := len |} : t T A).
+  Proof.
+    now intros; subst.
+  Qed.
+  Smpl Add unshelve eapply of_value_with : of_value.
+
+  Definition of_value
+    (T' A' : Ty.t)
+    (H_T : OfTy.t T')
+    (H_A : OfTy.t A')
+    (buf' : Value.t) (buf : RawVec.t (OfTy.get_Set H_T) (OfTy.get_Set H_A))
+    (len' : Value.t) (len : Usize.t) :
+    buf' = φ buf ->
+    len' = φ len ->
+    OfValue.t (Value.StructRecord "alloc::vec::Vec" [] [T'; A'] [
+      ("buf", buf');
+      ("len", len')
+    ]).
+  Proof.
+    intros.
+    destruct H_T as [T].
+    destruct H_A as [A].
+    eapply OfValue.Make with (value := Build_t T A buf len).
+    subst.
+    reflexivity.
+  Defined.
+  Smpl Add unshelve eapply of_value : of_value.
 End Vec.
 
 Module Impl_Clone_for_Vec.
@@ -80,7 +123,14 @@ Module Impl_Vec_T.
   *)
   Instance run_new {T : Set} `{Link T} :
     Run.Trait (vec.Impl_alloc_vec_Vec_T_alloc_alloc_Global.new (Φ T)) [] [] [] (Self T).
-  Admitted.
+  Proof.
+    constructor.
+    run_symbolic.
+    2: {
+      change (Ty.path "alloc::alloc::Global") with (Φ Global.t).
+      repeat smpl of_value.
+    }
+  Defined.
 
   (* pub fn with_capacity(capacity: usize) -> Self *)
   Instance run_with_capacity {T : Set} `{Link T} (capacity : Usize.t) :

CoqOfRust/examples/axiomatized/examples/custom/loops.v

@@ -0,0 +1,23 @@
+(* Generated by coq-of-rust *)
+Require Import CoqOfRust.CoqOfRust.
+
+Parameter sum_checked : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_sum_checked : M.IsFunction.C "loops::sum_checked" sum_checked.
+Admitted.
+
+Parameter reverse_in_place : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_reverse_in_place :
+  M.IsFunction.C "loops::reverse_in_place" reverse_in_place.
+Admitted.
+
+Parameter is_sorted : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_is_sorted : M.IsFunction.C "loops::is_sorted" is_sorted.
+Admitted.
+
+Parameter max_array : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_max_array : M.IsFunction.C "loops::max_array" max_array.
+Admitted.

CoqOfRust/examples/axiomatized/examples/custom/loops_free.v

@@ -0,0 +1,38 @@
+(* Generated by coq-of-rust *)
+Require Import CoqOfRust.CoqOfRust.
+
+Parameter max2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_max2 : M.IsFunction.C "loops_free::max2" max2.
+Admitted.
+
+Parameter abs_i32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_abs_i32 : M.IsFunction.C "loops_free::abs_i32" abs_i32.
+Admitted.
+
+Parameter bool_and : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_bool_and : M.IsFunction.C "loops_free::bool_and" bool_and.
+Admitted.
+
+Parameter get_or_zero : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_get_or_zero :
+  M.IsFunction.C "loops_free::get_or_zero" get_or_zero.
+Admitted.
+
+Parameter eq2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_eq2 : M.IsFunction.C "loops_free::eq2" eq2.
+Admitted.
+
+Parameter eq_pair : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_eq_pair : M.IsFunction.C "loops_free::eq_pair" eq_pair.
+Admitted.
+
+Parameter min3 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
+
+Global Instance Instance_IsFunction_min3 : M.IsFunction.C "loops_free::min3" min3.
+Admitted.