Oak.v 2.85 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
From Coq Require Import ZArith.
From Containers Require Import Sets Maps.

Inductive OakType :=
  | oak_empty : OakType
  | oak_unit : OakType
  | oak_int : OakType
  | oak_bool : OakType
  | oak_sum : OakType -> OakType -> OakType
  | oak_pair : OakType -> OakType -> OakType
  | oak_list : OakType -> OakType
  | oak_set : OakType -> OakType
  | oak_map : OakType -> OakType -> OakType.

15
16
Definition eq_oak_type_dec (t1 t2 : OakType) : {t1 = t2} + {t1 <> t2}
  := ltac:(decide equality).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
17
18
19
20
21
22
23

Program Instance Empty_set_StrictOrder
  : OrderedType.StrictOrder (fun (_ _ : Empty_set) => False) (@eq Empty_set).
Solve Obligations with contradiction.
Program Instance Empty_set_OrderedType : UsualOrderedType Empty_set.
Solve Obligations with contradiction.
  
24
Local Fixpoint interp_with_ordering (t : OakType) : {T : Type & OrderedType T} :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
25
26
27
28
29
30
  match t with
  | oak_empty => existT OrderedType Empty_set _
  | oak_unit => existT OrderedType unit _
  | oak_int => existT OrderedType Z _
  | oak_bool => existT OrderedType bool _
  | oak_sum a b =>
31
32
33
    let 'existT aT _ := interp_with_ordering a in
    let 'existT bT _ := interp_with_ordering b in
    existT OrderedType (aT + bT)%type _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
34
  | oak_pair a b =>
35
36
37
    let 'existT aT _ := interp_with_ordering a in
    let 'existT bT _ := interp_with_ordering b in
    existT OrderedType (aT * bT)%type _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
38
  | oak_list a =>
39
40
    let 'existT aT _ := interp_with_ordering a in
    existT OrderedType (list aT) _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
41
  | oak_set a =>
42
43
    let 'existT aT _ := interp_with_ordering a in
    existT OrderedType (set aT) _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
44
  | oak_map a b =>
45
46
47
    let 'existT aT _ := interp_with_ordering a in
    let 'existT bT _ := interp_with_ordering b in
    existT OrderedType Map[aT, bT] _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
  end.

Definition interp (t : OakType) : Type :=
  projT1 (interp_with_ordering t).

Record OakValue :=
  build_oak_value {
    oak_value_type : OakType;
    oak_value : interp oak_value_type;
  }.

Definition oak_value_extract (t : OakType) (value : OakValue) : option (interp t).
Proof.
  destruct value as [ty val].
  destruct (eq_oak_type_dec t ty); subst.
  - apply (Some val).
  - apply None.
Defined.

(*
Examples:
Definition test_bool : OakValue := build_oak_value oak_bool true.
Definition test_int : OakValue := build_oak_value oak_int 5%Z.
Definition test_set : OakValue := build_oak_value (oak_set oak_int) {5%Z; {6%Z; {}}}.
Definition test_map : OakValue := build_oak_value (oak_map oak_int oak_int) [][5%Z <- 10%Z].

Compute (oak_value_extract oak_bool test_bool) : option bool.
Compute (oak_value_extract oak_int test_bool) : option Z.
Compute (oak_value_extract oak_bool test_int) : option bool.
Compute (oak_value_extract oak_int test_int) : option Z.
Compute (oak_value_extract (oak_set oak_int) test_set) : option (set Z).
Compute (option_map SetInterface.elements (oak_value_extract (oak_set oak_int) test_set)).
Compute (option_map elements (oak_value_extract (oak_map oak_int oak_int) test_map)).
81
*)