Commit 4c7bf5e4 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Add OakTypes.v

This allows heterogenous treament of Oak types and values.
parent 3612b7af
Pipeline #10817 failed with stage
in 3 minutes and 5 seconds
......@@ -15,9 +15,15 @@ variables:
- opam config list
- opam repo list
- opam list
- git clone --branch various-fixes https://github.com/StekiKun/containers.git dep-coq-containers
- cd dep-coq-containers
- make -j
- make -f Makefile.coq install
- cd ..
- rm -rf dep-coq-containers
script:
- sudo chown -R coq:coq "$CI_PROJECT_DIR"
- make
- make -j
coq:8.6:
extends: .build
......
-R src SmartContracts
src/Blockchain.v
src/Congress.v
src/OakTypes.v
-R vendor/record-update RecordUpdate
vendor/record-update/RecordSet.v
vendor/record-update/RecordUpdate.v
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.
Lemma eq_oak_type_dec
: forall (t1 t2 : OakType), {t1 = t2} + {t1 <> t2}.
Proof.
decide equality.
Defined.
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.
Fixpoint interp_with_ordering (t : OakType) : {T : Type & OrderedType T} :=
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 =>
let 'existT aT _ := interp_with_ordering a in
let 'existT bT _ := interp_with_ordering b in
existT OrderedType (aT + bT)%type _
| oak_pair a b =>
let 'existT aT _ := interp_with_ordering a in
let 'existT bT _ := interp_with_ordering b in
existT OrderedType (aT * bT)%type _
| oak_list a =>
let 'existT aT _ := interp_with_ordering a in
existT OrderedType (list aT) _
| oak_set a =>
let 'existT aT _ := interp_with_ordering a in
existT OrderedType (set aT) _
| oak_map a b =>
let 'existT aT _ := interp_with_ordering a in
let 'existT bT _ := interp_with_ordering b in
existT OrderedType Map[aT, bT] _
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)).
Check @MapAVL.Raw.Proofs.L.map_OrderedType.
Set Typeclasses Debug.
Check (option_map SetInterface.elements oak_value_extract (oak_set oak_int) test_set).
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment