Start of modelling oak_any

src/Extras.v

 From Coq Require Import List.
+From SmartContracts Require Import Monads.
 Import ListNotations.
 
 Fixpoint find_first {A B : Type} (f : A -> option B) (l : list A)
@@ -20,3 +21,11 @@ Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A)
                 end
   | [] => []
   end.
+
+Fixpoint mapM {A B : Type} (f : A -> option B) (l : list A) : option (list B) :=
+  match l with
+  | hd :: tl => do b <- f hd;
+                do bs <- mapM f tl;
+                Some (b :: bs)
+  | [] => Some []
+  end.

src/Oak.v

 From Coq Require Import ZArith.
 From SmartContracts Require Import Monads.
+From SmartContracts Require Import Extras.
 From SmartContracts Require Import Containers.
 From Coq Require Import List.
 
 Import ListNotations.
 
 Inductive OakType :=
-  | oak_empty : OakType
-  | oak_unit : OakType
   | oak_int : OakType
-  | oak_bool : OakType
+  | oak_any : OakType
   | oak_pair : OakType -> OakType -> OakType
   | oak_sum : OakType -> OakType -> OakType
-  | oak_list : OakType -> OakType
-  | oak_set : OakType -> OakType
-  | oak_map : OakType -> OakType -> OakType.
+  | oak_list : OakType -> OakType.
+
+Inductive OakTyped : OakType -> Type -> Type :=
+  | typ_int : OakTyped oak_int Z
+  | typ_any :
+      forall {ot t},
+        OakTyped ot t ->
+        OakTyped oak_any t
+  | typ_pair :
+      forall {lot rot lt rt},
+        OakTyped lot lt ->
+        OakTyped rot rt ->
+        OakTyped (oak_pair lot rot) (lt * rt)
+  | typ_sum :
+      forall {lot rot lt rt},
+        OakTyped lot lt ->
+        OakTyped rot rt ->
+        OakTyped (oak_sum lot rot) (lt + rt)
+  | typ_list :
+      forall {ot t},
+        OakTyped ot t -> OakTyped (oak_list ot) (list t).
 
-Definition eq_oak_type_dec (t1 t2 : OakType) : {t1 = t2} + {t1 <> t2}.
-Proof. decide equality. Defined.
+Set Primitive Projections.
+Record OakValue :=
+  build_oak_value {
+    ov_ot : OakType;
+    ov_t : Type;
+    ov_typed : OakTyped ov_ot ov_t;
+    ov_val : ov_t;
+  }.
+
+Arguments build_oak_value {_ _} _ _.
+
+Fixpoint interp_type (ot : OakType) : Type :=
+  match ot with
+  | oak_int => Z
+  | oak_any => OakValue
+  | oak_pair ot1 ot2 => (interp_type ot1) * (interp_type ot2)
+  | oak_sum ot1 ot2 => (interp_type ot1) + (interp_type ot2)
+  | oak_list ot => list (interp_type ot)
+  end.
 
-Proposition eq_oak_type_dec_refl (x : OakType) :
-  eq_oak_type_dec x x = left eq_refl.
+Definition extract_from_any
+         (extract_as : OakType)
+         (t : Type) (typed : OakTyped oak_any t)
+         (val : t)
+         (f : forall (extract_as : OakType)
+                     (ot : OakType) (t : Type) (typed : OakTyped ot t)
+                     (val : t), option (interp_type extract_as))
+  : option (interp_type extract_as).
 Proof.
-  induction x;
-    try simpl; try rewrite IHx; try rewrite IHx1; try rewrite IHx2; reflexivity.
-Qed.
+  inversion typed; subst.
+  exact (f extract_as ot t X val).
+Defined.
+
+(* Defining this as a fixpoint instead of by induction over typed
+allows us to handle oak_any generally for all cases *)
+Fixpoint extract_typed
+         (extract_as : OakType)
+         {ot : OakType} {t : Type} (typed : OakTyped ot t)
+         (val : t) {struct typed}
+  : option (interp_type extract_as).
+Proof.
+  revert typed val.
+  refine (
+      match extract_as, ot
+            return (forall (typed : OakTyped ot t) (val : t),
+                       option (interp_type extract_as)) with
+      | oak_any, ot =>
+        let f (typed : OakTyped ot t) (val : t) : option OakValue :=
+            Some (build_oak_value typed val) in f
+      | extract_as, oak_any =>
+        let f (typed : OakTyped oak_any t) (val : t) : option (interp_type extract_as) :=
+            extract_from_any extract_as t typed val extract_typed in f
+      | oak_int, oak_int => _
+      | oak_pair elot erot, oak_pair lot rot => _
+      | oak_sum elot erot, oak_sum lot rot => _
+      | oak_list eot, oak_list ot => _
+      | _, _ => fun typed val => None
+    end); intros typed val.
+  - inversion typed; subst; exact (Some val).
+  - inversion typed; subst.
+    exact (do l <- extract_typed elot lot lt X (fst val);
+           do r <- extract_typed erot rot rt X0 (snd val);
+           Some (l, r)).
+  - inversion typed; subst.
+    destruct val as [l | r].
+    + exact (option_map inl (extract_typed elot lot lt X l)).
+    + exact (option_map inr (extract_typed erot rot rt X0 r)).
+  - inversion typed; subst.
+    exact (mapM (extract_typed eot ot t0 X) val).
+Defined.
+
+Definition unpack_value (ot : OakType) (v : OakValue) : option (interp_type ot) :=
+  match v with
+  | build_oak_value typed val => extract_typed ot typed val
+  end.
+
+Definition test_int : OakValue :=
+  build_oak_value typ_int 10%Z.
+
+Definition test_int_any : OakValue :=
+  build_oak_value (typ_any typ_int) 10%Z.
+
+Compute unpack_value oak_int test_int.
+Compute (unpack_value oak_int test_int_any).
+
+Fixpoint pack_value_full (ot : OakType) (v : interp_type ot) {struct ot}
+  : { ov : OakValue & ov.(ov_ot) = ot }.
+Proof.
+  destruct ot as [| | t1 t2| t1 t2|ot].
+  - exact (existT (build_oak_value typ_int v) eq_refl).
+  - exact (existT (build_oak_value (typ_any v.(ov_typed)) v.(ov_val)) eq_refl).
+  - destruct v as [l r].
+    destruct (pack_value_full t1 l) as [[lot lt ltyped lval] lot_eq].
+    destruct (pack_value_full t2 r) as [[rot rt rtyped rval] rot_eq].
+    simpl in *; subst.
+    exact (existT (build_oak_value (typ_pair ltyped rtyped) (lval, rval)) eq_refl).
+  - destruct v as [l | r].
+    + destruct (pack_value_full t1 l) as [[lot lt ltyped lval] lot_eq].
+
+
+  (*
+  - refine (existT (build_oak_value typ_int v) _).
+    reflexivity.
+  - destruct v as [ot t typed v].
+    refine (existT (build_oak_value (typ_any typed) v) _).
+    reflexivity.
+  - destruct v as [l r].
+    destruct (pack_value_full t1 l) as [[lot lt ltyped lval] l_tsound].
+    destruct (pack_value_full t2 r) as [[rot rt rtyped rval] r_tsound].
+    simpl in *; subst.
+    refine (existT (build_oak_value (typ_pair ltyped rtyped) (lval, rval)) _).
+    reflexivity.
+  - destruct v as  [l | r].
+    + destruct (pack_value_full t1 l) as [[lot lt ltyped lval] l_tsound].
+      simpl in l_tsound; subst.
+      refine (existT (build_oak_value (typ_sum ltyped typ_int) (inl lval)) _).
+      reflexivity.
+    + destruct (pack_value_full t2 l) as [[rot rt rtyped rval] r_tsound].
+  match ot with
+  | oak_int => build_oak_value oak_int Z typ_int
+  | oak_any => id
+  | oak_pair t1 t2 =>
+    fun (p : interp_type t1 * interp_type t2) =>
+      let 'build_oak_value lot lt ltyped lval := pack_value t1 (fst p) in
+      let 'build_oak_value rot rt rtyped rval := pack_value t2 (snd p) in
+      build_oak_value
+        (oak_pair t1 t2)
+        (lt * rt)%type
+        (typ_pair lot rot lt rt ltyped rtyped)
+        (lval, rval)
+  | _ => fun t => build_oak_value oak_int Z typ_int 0
+  end.
+
+
 
 Set Primitive Projections.
 Record OakInterpretation :=