Commit 53505ab3 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Play around with OakTypable typeclasses

parent f3887710
Pipeline #10964 failed with stage
in 4 minutes and 40 seconds
......@@ -12,35 +12,60 @@ Inductive OakType :=
| oak_set : OakType -> OakType
| oak_map : OakType -> OakType -> OakType.
Definition eq_oak_type_dec (t1 t2 : OakType) : {t1 = t2} + {t1 <> t2}
:= ltac:(decide equality).
Definition eq_oak_type_dec (t1 t2 : OakType) : {t1 = t2} + {t1 <> t2}.
Proof. decide equality. Defined.
Program Instance Empty_set_StrictOrder
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.
Program Instance empty_set_OrderedType : UsualOrderedType Empty_set.
Solve Obligations with contradiction.
Local Fixpoint interp_type_with_ordering (t : OakType) : {T : Type & OrderedType T} :=
Set Primitive Projections.
Record sigT {A : Type} (P : A -> Type) := existT {projT1 : A; projT2 : P projT1}.
Arguments existT {_}.
Arguments projT1 {_ _}.
Arguments projT2 {_ _}.
Local Fixpoint interp_type_with_ordering (t : OakType)
(*: {T : Type & OrderedType T} :=*)
: sigT OrderedType :=
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_type_with_ordering a in
let 'existT bT _ := interp_type_with_ordering b in
existT OrderedType (aT + bT)%type _
let 'existT a_t a_ot := interp_type_with_ordering a in
let 'existT b_t b_ot := interp_type_with_ordering b in
existT OrderedType (a_t + b_t)%type (sum_OrderedType a_ot b_ot)
| oak_pair a b =>
let 'existT aT _ := interp_type_with_ordering a in
let 'existT bT _ := interp_type_with_ordering b in
existT OrderedType (aT * bT)%type _
let 'existT a_t a_ot := interp_type_with_ordering a in
let 'existT b_t b_ot := interp_type_with_ordering b in
existT OrderedType (a_t * b_t)%type (prod_OrderedType a_ot b_ot)
| oak_list a =>
let 'existT aT _ := interp_type_with_ordering a in
existT OrderedType (list aT) _
let 'existT a_t a_ot := interp_type_with_ordering a in
existT OrderedType (list a_t) (list_OrderedType a_ot)
(*
| oak_set a =>
let 'existT aT _ := interp_type_with_ordering a in
existT OrderedType (set aT) _
let
'@existT _ _ a_t o := interp_type_with_ordering a in
@existT Type OrderedType (@set a_t o (@SetAVLInstance.SetAVL_FSet a_t o))
(@SOT_as_OT (@set a_t o (@SetAVLInstance.SetAVL_FSet a_t o))
(Equal_pw (@set a_t o (@SetAVLInstance.SetAVL_FSet a_t o)) a_t
(@SetInterface.In a_t o (@SetAVLInstance.SetAVL_FSet a_t o)))
(@FSet_OrderedType a_t o (@SetAVLInstance.SetAVL_FSet a_t o)))
*)
(*
| oak_set a =>
let 'existT a_t a_ot := interp_type_with_ordering a in
let setT := @set a_t a_ot _ in
existT OrderedType setT (@SOT_as_OT setT (Equal_pw setT a_t (@SetInterface.In a_t a_ot _))
(@FSet_OrderedType a_t a_ot setT))
*)
| oak_set a =>
let 'existT a_t a_ot := interp_type_with_ordering a in
existT OrderedType (set a_t) _
| oak_map a b =>
let 'existT aT _ := interp_type_with_ordering a in
let 'existT bT _ := interp_type_with_ordering b in
......@@ -50,21 +75,207 @@ Local Fixpoint interp_type_with_ordering (t : OakType) : {T : Type & OrderedType
Definition interp_type (t : OakType) : Type :=
projT1 (interp_type_with_ordering t).
Definition interp_order (t : OakType) : OrderedType (interp_type t) :=
projT2 (interp_type_with_ordering t).
Record OakValue :=
build_oak_value {
oak_value_type : OakType;
oak_value : interp_type oak_value_type;
}.
Definition oak_value_extract (t : OakType) (value : OakValue) : option (interp_type t).
Class OakTypable (A : Type) :=
build_oak_typable {
oak_typable_type : OakType;
oak_typable_proof : interp_type oak_typable_type = A;
(*
oak_typable_order : OrderedType A;
(* We want interp_order oak_typable_type = oak_typable_order, but:
The term "oak_typable_order" has type "OrderedType A" while it
is expected to have type "OrderedType (interp_type oak_typable_type)".
The following turns (interp_order oak_typable_type)
: OrderedType (interp_type oak_typable_type)
into a term of type OrderedType A using the equality we have in context. *)
oak_typable_order_proof :
let order := interp_order oak_typable_type in
let order_typed : OrderedType A := ltac:(subst; exact order) in
oak_typable_order = order_typed;*)
}.
Arguments oak_typable_type {_}.
Arguments oak_typable_proof {_}.
(*
Arguments oak_typable_order {_}.
Arguments oak_typable_order_proof {_}.
*)
Program Instance oak_typable_empty : OakTypable Empty_set :=
{| oak_typable_type := oak_empty |}.
Program Instance oak_typable_unit : OakTypable unit :=
{| oak_typable_type := oak_unit |}.
Program Instance oak_typable_int : OakTypable Z :=
{| oak_typable_type := oak_int |}.
Program Instance oak_typable_bool : OakTypable bool :=
{| oak_typable_type := oak_bool |}.
Program Instance oak_typable_sum
{A B : Type}
{ot_a : OakTypable A}
{ot_b : OakTypable B}
: OakTypable (A + B)%type :=
let 'build_oak_typable ty_a _ := ot_a in
let 'build_oak_typable ty_b _ := ot_b in
{| oak_typable_type := oak_sum ty_a ty_b |}.
Program Instance oak_typable_pair
{A B : Type}
{ot_a : OakTypable A}
{ot_b : OakTypable B}
: OakTypable (A * B)%type :=
let 'build_oak_typable ty_a _ := ot_a in
let 'build_oak_typable ty_b _ := ot_b in
{| oak_typable_type := oak_pair ty_a ty_b |}.
Program Instance oak_typable_list
{A : Type}
{ot_a : OakTypable A}
: OakTypable (list A) :=
let 'build_oak_typable ty_a _ := ot_a in
{| oak_typable_type := oak_list ty_a; |}.
Set Printing Implicit.
Instance oak_typable_set
{A : Type}
{ot_a : OakTypable A}
: (let 'build_oak_typable ty_a _ := ot_a in
let order := interp_order ty_a in
let _ : OrderedType A := ltac:(subst; exact order) in
OakTypable (set A)).
Proof.
destruct ot_a as [ty interps_ty].
subst.
simpl.
refine {| oak_typable_type := oak_set ty |}.
reflexivity.
Qed.
Definition oak_value_extract_auto
(A : Type)
{ot : OakTypable A}
(value : OakValue) : option A.
Proof.
destruct value as [ty val].
destruct ot as [oak_ty oak_ty_interps].
destruct (eq_oak_type_dec oak_ty ty).
- subst. exact (Some val).
- exact None.
Defined.
Definition oak_value_extract (oak_ty : OakType) (value : OakValue) : option (interp_type oak_ty).
Proof.
destruct value as [ty val].
destruct (eq_oak_type_dec t ty); subst.
- apply (Some val).
- apply None.
destruct (eq_oak_type_dec oak_ty ty).
- subst. exact (Some val).
- exact None.
Defined.
Definition test_bool : OakValue := build_oak_value oak_bool true.
Definition test_int : OakValue := build_oak_value oak_int 5%Z.
Definition test_int_list : OakValue
:= build_oak_value (oak_list oak_int) (cons 5%Z (cons 6%Z (cons 7%Z nil))).
Definition test_int_set : OakValue
:= build_oak_value (oak_set oak_int) {5%Z; {6%Z; {}}}.
Set Typeclasses Debug.
Compute (oak_value_extract_auto Z test_int).
Compute (oak_value_extract_auto (list Z) test_int_list) : option (list Z).
Compute (oak_value_extract (oak_list oak_int) test_int_list) : option (list Z).
Compute (option_map SetInterface.elements (oak_value_extract (oak_set oak_int) test_int_set)).
Compute (option_map SetInterface.elements (oak_value_extract_auto (set Z) test_int_set)).
Definition oak_value_build
{A : Type}
{order : OrderedType A}
{ot : OakTypable (existT OrderedType A order)}
(value : A) : OakValue :=
build_oak_value (@oak_typable_type (exi
Definition oak_value {A : Type} {
Definition test_bool : OakValue := build_oak_value oak_bool true.
Definition test_int : OakValue := build_oak_value oak_int 5%Z.
Instance oak_typable_set
{A : {T : Type & OrderedType T}}
{ot_a : OakTypable A}
: OakTypable (existT OrderedType (@set (projT1 A) (projT2 A)) _).
Proof.
destruct A as [ty_A order_A].
destruct ot_a as [oak_ty_a oak_ty_a_interps].
simpl.
replace (existT _ _ _) with (interp_type_with_ordering (oak_list oak_ty_a)).
- apply make_typable.
- unfold interp_type_with_ordering; fold interp_type_with_ordering.
destruct (interp_type_with_ordering oak_ty_a).
inversion oak_ty_a_interps.
subst.
reflexivity.
Qed.
Instance oak_typable_pair
{A B : Type}
{ot_a : OakTypable A}
{ot_b : OakTypable B}
: OakTypable (A * B).
Proof.
destruct ot_a as [oak_ty_a oak_ty_a_interps],
ot_b as [oak_ty_b oak_ty_b_interps].
subst.
replace (interp_type oak_ty_a * interp_type oak_ty_b)%type
with (interp_type (oak_pair oak_ty_a oak_ty_b)).
- apply make_typable.
- unfold interp_type.
simpl.
destruct (interp_type_with_ordering oak_ty_a), (interp_type_with_ordering oak_ty_b).
reflexivity.
Qed.
Instance oak_typable_list
{A : Type}
{ot_a : OakTypable A}
: OakTypable (list A).
Proof.
destruct ot_a as [oak_ty_a oak_ty_a_interps].
subst.
replace (list (interp_type oak_ty_a)) with (interp_type (oak_list oak_ty_a)).
- apply make_typable.
- unfold interp_type.
simpl.
destruct (interp_type_with_ordering oak_ty_a).
reflexivity.
Qed.
Instance oak_typable_set
{A : Type}
{ot_a : OakTypable A}
: OakTypable (@set A (projT2 (interp_type_with_ordering oak_typable_type))).
Proof.
destruct ot_a as [oak_ty_a oak_ty_a_interps].
subst.
replace (list (interp_type oak_ty_a)) with (interp_type (oak_list oak_ty_a)).
- apply make_typable.
- unfold interp_type.
simpl.
destruct (interp_type_with_ordering oak_ty_a).
reflexivity.
Qed.
Definition oak_value_extract_auto (A : Type) `{OT : OakTypable A} (value : OakValue) : option A.
Proof.
destruct value as [ty val].
destruct OT as [oak_ty oak_ty_interps].
destruct (eq_oak_type_dec oak_ty ty).
- subst. apply (Some val).
- apply None.
Defined.
(*
Examples:
......@@ -73,11 +284,10 @@ 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 (oak_value_extract_auto bool test_bool) : option bool.
Compute (oak_value_extract_auto Z test_bool) : option Z.
Compute (oak_value_extract_auto bool test_int) : option bool.
Compute (oak_value_extract_auto Z test_int) : option 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)).
*)
\ 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