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

Fix interp_with_ordering for older Coq versions

parent a7c9adc1
Pipeline #10836 failed with stage
in 4 minutes and 22 seconds
......@@ -23,6 +23,22 @@ Program Instance Empty_set_StrictOrder
Solve Obligations with contradiction.
Program Instance Empty_set_OrderedType : UsualOrderedType Empty_set.
Solve Obligations with contradiction.
(* These functions help some old Coq versions with inference *)
Definition make_sum (A B : Type) (_ : OrderedType A) (_ : OrderedType B)
:= existT OrderedType (A + B)%type _.
Definition make_pair (A B : Type) (_ : OrderedType A) (_ : OrderedType B)
:= existT OrderedType (A * B)%type _.
Definition make_list (A : Type) (_ : OrderedType A)
:= existT OrderedType (list A) _.
Definition make_set (A : Type) (_ : OrderedType A)
:= existT OrderedType (set A) _.
Definition make_map (A B : Type) (_ : OrderedType A) (_ : OrderedType B)
:= existT OrderedType Map[A, B] _.
Fixpoint interp_with_ordering (t : OakType) : {T : Type & OrderedType T} :=
match t with
......@@ -31,23 +47,23 @@ Fixpoint interp_with_ordering (t : OakType) : {T : Type & OrderedType T} :=
| 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 _
let 'existT aT aOT := interp_with_ordering a in
let 'existT bT bOT := interp_with_ordering b in
make_sum aT bT aOT bOT
| 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 _
let 'existT aT aOT := interp_with_ordering a in
let 'existT bT bOT := interp_with_ordering b in
make_pair aT bT aOT bOT
| oak_list a =>
let 'existT aT _ := interp_with_ordering a in
existT OrderedType (list aT) _
let 'existT aT aOT := interp_with_ordering a in
make_list aT aOT
| oak_set a =>
let 'existT aT _ := interp_with_ordering a in
existT OrderedType (set aT) _
let 'existT aT aOT := interp_with_ordering a in
make_set aT aOT
| 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] _
let 'existT aT aOT := interp_with_ordering a in
let 'existT bT bOT := interp_with_ordering b in
make_map aT bT aOT bOT
end.
Definition interp (t : OakType) : Type :=
......
Supports Markdown
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