Oak.v 3.24 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}.
Proof. decide equality. Defined.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
17

18
Program Instance empty_set_strict_order
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
19
20
  : OrderedType.StrictOrder (fun (_ _ : Empty_set) => False) (@eq Empty_set).
Solve Obligations with contradiction.
21
Program Instance empty_set_ordered_type : UsualOrderedType Empty_set.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
22
Solve Obligations with contradiction.
23

24
Local Fixpoint interp_type_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
    let 'existT aT _ := interp_type_with_ordering a in
    let 'existT bT _ := interp_type_with_ordering b in
33
    existT OrderedType (aT + bT)%type _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
34
  | oak_pair a b =>
35
36
    let 'existT aT _ := interp_type_with_ordering a in
    let 'existT bT _ := interp_type_with_ordering b in
37
    existT OrderedType (aT * bT)%type _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
38
  | oak_list a =>
39
    let 'existT aT _ := interp_type_with_ordering a in
40
    existT OrderedType (list aT) _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
41
  | oak_set a =>
42
    let 'existT aT _ := interp_type_with_ordering a in
43
    existT OrderedType (set aT) _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
44
  | oak_map a b =>
45
46
    let 'existT aT _ := interp_type_with_ordering a in
    let 'existT bT _ := interp_type_with_ordering b in
47
    existT OrderedType Map[aT, bT] _
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
48
49
  end.

50
51
Definition interp_type (t : OakType) : Type :=
  projT1 (interp_type_with_ordering t).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
52
53
54
55

Record OakValue :=
  build_oak_value {
    oak_value_type : OakType;
56
    oak_value : interp_type oak_value_type;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
57
58
  }.

59
Definition extract_oak_value (t : OakType) (value : OakValue) : option (interp_type t).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
60
61
Proof.
  destruct value as [ty val].
62
63
64
  destruct (eq_oak_type_dec t ty).
  - subst. exact (Some val).
  - exact None.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
65
66
67
68
69
70
Defined.

(*
Examples:
Definition test_bool : OakValue := build_oak_value oak_bool true.
Definition test_int : OakValue := build_oak_value oak_int 5%Z.
71
72
73
74
75
76
77
78
79
80
81
82
83
Definition test_set : OakValue :=
  build_oak_value
    (oak_set oak_int)
    {5; {6; {}}}%Z.
Definition test_map : OakValue :=
  build_oak_value
    (oak_map oak_int oak_int)
    [][5 <- 10][6 <- 10][5 <- 15]%Z.

Definition test_map2 : OakValue :=
  build_oak_value
    (oak_map (oak_map oak_int oak_int) oak_int)
    [][[][5 <- 10][6 <- 10][5 <- 15] <- 15]%Z.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
84

85
86
87
88
89
Compute (extract_oak_value oak_bool test_bool) : option bool.
Compute (extract_oak_value oak_int test_bool) : option Z.
Compute (extract_oak_value oak_bool test_int) : option bool.
Compute (extract_oak_value oak_int test_int) : option Z.
Compute (extract_oak_value (oak_set oak_int) test_set) : option (set Z).
90
Compute
91
  (extract_oak_value
92
93
94
95
96
     (oak_map
        (oak_map oak_int oak_int)
        oak_int)
     test_map2)
  : option Map[Map[Z, Z], Z].
97
98
Compute (option_map SetInterface.elements (extract_oak_value (oak_set oak_int) test_set)).
Compute (option_map elements (extract_oak_value (oak_map oak_int oak_int) test_map)).
99
*)