Commit d4f50a90 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Attempts with transports and coercions

parent 53505ab3
Pipeline #11020 failed with stage
in 4 minutes and 22 seconds
......@@ -36,40 +36,23 @@ Local Fixpoint interp_type_with_ordering (t : OakType)
| oak_int => existT OrderedType Z _
| oak_bool => existT OrderedType bool _
| oak_sum a b =>
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)
let 'existT a_t _ := interp_type_with_ordering a in
let 'existT b_t _ := interp_type_with_ordering b in
existT OrderedType (a_t + b_t)%type _
| oak_pair a b =>
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)
let 'existT a_t _ := interp_type_with_ordering a in
let 'existT b_t _ := interp_type_with_ordering b in
existT OrderedType (a_t * b_t)%type _
| oak_list a =>
let 'existT a_t a_ot := interp_type_with_ordering a in
existT OrderedType (list a_t) (list_OrderedType a_ot)
(*
let 'existT a_t _ := interp_type_with_ordering a in
existT OrderedType (list a_t) _
| oak_set a =>
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
let 'existT a_t _ := 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
existT OrderedType Map[aT, bT] _
let 'existT a_t _ := interp_type_with_ordering a in
let 'existT b_t _ := interp_type_with_ordering b in
existT OrderedType Map[a_t, b_t] _
end.
Definition interp_type (t : OakType) : Type :=
......@@ -84,31 +67,22 @@ Record OakValue :=
oak_value : interp_type oak_value_type;
}.
Definition transport {A : Type} {P : A -> Type} {a b : A} (p : a = b) : P a -> P b
:= fun a => match p with eq_refl => a end.
Notation "p # x" := (transport p x) (right associativity, at level 65).
Class OakTypable (A : Type) :=
build_oak_typable {
oak_typable_type : OakType;
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;*)
oak_typable_order :> OrderedType A;
oak_typable_order_proof : oak_typable_proof # interp_order oak_typable_type = oak_typable_order;
}.
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 |}.
......@@ -124,8 +98,8 @@ Program Instance oak_typable_sum
{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
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
......@@ -133,30 +107,26 @@ Program Instance oak_typable_pair
{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
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
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)).
: OakTypable (set A).
Proof.
destruct ot_a as [ty interps_ty].
destruct ot_a as [ty interps_ty order interps_order].
subst.
simpl.
refine {| oak_typable_type := oak_set ty |}.
instantiate (1:=eq_refl).
reflexivity.
Qed.
......@@ -180,19 +150,26 @@ Proof.
- exact None.
Defined.
Definition test_int_set : OakValue
:= build_oak_value (oak_set oak_int) {5%Z; {6%Z; {}}}.
Set Typeclasses Debug.
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 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}
......
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