Commit 58d96cdb authored by Gaspard Ferey's avatar Gaspard Ferey

Added cc.dk using no lift.

parent 74646857
# All supported flags
FLAGS=max_AC plus_AC plus_ACU cast lift lift_1 max_err confluent WIP constraints
FLAGS=max_AC plus_AC plus_ACU cast lift lift_1 max_err confluent WIP constraints varity
DKS=$(shell find ./ -type f -name '*.dk')
......@@ -19,7 +19,7 @@ all:
if [ -z $$(head -q -n 1 $$dk | grep "nocic") ]; then \
echo -n "| [$$dk]($$dk) |" >> README.md ; \
for fg in $(FLAGS) ; do \
if [ -z $$(head -q -n 1 $$dk | grep "$$fg") ]; then \
if [ -z $$(head -q -n 1 $$dk | grep "[^a-zA-Z0-9]$$fg[^a-zA-Z0-9]") ]; then \
echo -n " |" >> README.md ; \
else \
echo -n " X |" >> README.md ; \
......
This project contains various implementations of cic.dk
| File | max_AC | plus_AC | plus_ACU | cast | lift | lift_1 | max_err | confluent | WIP | constraints |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| [./AC/cicup.dk](./AC/cicup.dk) | X | X | | | | | | | X | |
| [./HOAS/HOAS_to_DBAC.dk](./HOAS/HOAS_to_DBAC.dk) | | | | | | | | | X | |
| [./orig/cic_coqine.dk](./orig/cic_coqine.dk) | | | | X | X | | | | | |
| [./orig/cic.dk](./orig/cic.dk) | | | | | X | | | | | |
| [./orig/cic_v2.dk](./orig/cic_v2.dk) | X | | | | X | | | | X | |
| [./old_to_ACU/cicup_v2.dk](./old_to_ACU/cicup_v2.dk) | | X | | | X | X | | | | |
| [./Constraints/cc.dk](./Constraints/cc.dk) | | | | | | | | | X | X |
| [./AC_Gilles/1-original/cc.dk](./AC_Gilles/1-original/cc.dk) | | X | X | | X | X | X | X | | |
| [./AC_Gilles/cicup_maxAC.dk](./AC_Gilles/cicup_maxAC.dk) | X | | | | X | | | | | |
| [./AC_Gilles/cicup_0elim.dk](./AC_Gilles/cicup_0elim.dk) | | X | | | X | X | X | X | | |
| [./AC_Gilles/cicup_0elim_maxplus.dk](./AC_Gilles/cicup_0elim_maxplus.dk) | | X | | | X | X | | | | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | X | | | | X | | | | X | |
| File | max_AC | plus_AC | plus_ACU | cast | lift | lift_1 | max_err | confluent | WIP | constraints | varity |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| [./AC/cicup.dk](./AC/cicup.dk) | X | X | | | | | | | X | | |
| [./nolift/cc.dk](./nolift/cc.dk) | | | | X | | | | | X | | X |
| [./HOAS/HOAS_to_DBAC.dk](./HOAS/HOAS_to_DBAC.dk) | | | | | | | | | X | | |
| [./orig/cic_coqine.dk](./orig/cic_coqine.dk) | | | | X | X | | | | | | |
| [./orig/cic.dk](./orig/cic.dk) | | | | | X | | | | | | |
| [./orig/cic_v2.dk](./orig/cic_v2.dk) | X | | | | X | | | | X | | |
| [./old_to_ACU/cicup_v2.dk](./old_to_ACU/cicup_v2.dk) | | X | | | X | | | | | | |
| [./Constraints/cc.dk](./Constraints/cc.dk) | | | | | | | | | X | X | |
| [./AC_Gilles/1-original/cc.dk](./AC_Gilles/1-original/cc.dk) | | | X | | X | X | | X | | | |
| [./AC_Gilles/cicup_maxAC.dk](./AC_Gilles/cicup_maxAC.dk) | | | | | X | | | | | | |
| [./AC_Gilles/cicup_0elim.dk](./AC_Gilles/cicup_0elim.dk) | | X | | | X | X | | X | | | |
| [./AC_Gilles/cicup_0elim_maxplus.dk](./AC_Gilles/cicup_0elim_maxplus.dk) | | X | | | X | | | | | | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | X | | | | X | | | | X | | |
## Flags
* **max_AC**: `max` on universe levels is AC
......@@ -26,3 +27,4 @@ This project contains various implementations of cic.dk
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
* **constraints**: Implementation is relying on Coq-like constraints mechanisms
* **varity**: Implementation requires Dedukti to accept rewrite rules of variable arity
(; cast, WIP, varity ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z (s j) --> s j.
[i,j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
set : Sort.
type : Nat -> Sort.
def axiom : Sort -> Sort.
[] axiom prop --> axiom set.
[] axiom set --> type (s z).
[i] axiom (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[] rule _ prop --> prop.
[] rule prop set --> set.
[] rule set set --> set.
[i] rule set (type i) --> type i.
[i] rule (type i) set --> type i.
[i,j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[] sup prop prop --> prop.
[] sup set set --> set.
[] sup prop set --> type z. (; ;)
[] sup set prop --> type z.
[i] sup set (type i) --> type i.
[i] sup prop (type i) --> type i.
[i] sup (type i) set --> type i.
[i] sup (type i) prop --> type i.
[i,j] sup (type i) (type j) --> type (max i j).
(; Canonicity rules ;)
[s1] sup s1 s1 --> s1.
[s1,s2] axiom (sup s1 s2) --> sup (axiom s1) (axiom s2).
[s1,s2,s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1,s2,s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (sup s1 s2) s3 --> sup (rule s1 s3) (rule s2 s3).
(; Primitive ;)
U : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
u : s : Sort -> U (axiom s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
def join : s1 : Sort -> s2 : Sort -> U s1 -> U s2 -> U (sup s1 s2).
def cast : s1 : Sort -> s2 : Sort -> a : U s1 -> b : U s2 -> T s1 a -> T (sup s1 s2) (join s1 s2 a b).
(; Defining code interpretation: T ;)
[s] T _ (u s) --> U s.
[s,a] T _ (cast _ _ (u s) _ a) --> T s a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
(; Defining join ;)
[i] join _ _ i i --> i.
[s1,s2] join _ _ (u s1) (u s2) --> u (sup s1 s2).
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod s1 s3 a c)
--> prod s1 (sup s2 s3) a (x : T s1 a => join s2 s3 (b x) (c x)).
(; Defining cast ;)
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3, m : T s1 a];)
(;cast {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b) m;)
(;--> cast s1 s3 a b m.;)
[s1,s2,s3,a,b,c,m,x]
cast _ _ (prod s1 s2 a b) (prod s1 s3 a c) m x
--> cast s2 s3 (b x) (c x) (m x).
(; Canonicity rules ;)
[t,a] cast _ _ t t a --> a.
[s1,s2,s3,a]
cast (axiom (sup s1 s2)) (axiom s3) (u (sup s1 s2)) (u s3) (cast (axiom s1) (axiom s2) (u s1) (u s2) a)
--> cast (axiom s1) (axiom (sup s2 s3)) (u s1) (u (sup s2 s3)) a.
[s1,s2,s3,a,b]
prod _ s2 (cast _ _ (u s1) (u s3) a) (x => b x)
--> cast
(axiom (rule s1 s2))
(axiom (rule s3 s2))
(u (rule s1 s2))
(u (rule s3 s2))
(prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => cast _ _ (u s2) (u s3) (b x))
--> cast
(axiom (rule s1 s2))
(axiom (rule s1 s3))
(u (rule s1 s2))
(u (rule s1 s3))
(prod s1 s2 a (x => b x)).
(; Alias for universe casting: lift ;)
def lift : s1 : Sort -> s2 : Sort -> U s1 -> U (sup s1 s2).
[s1,s2,m] lift s1 s2 m --> cast (axiom s1) (axiom s2) (u s1) (u s2) m.
(; Aliases for readibility ;)
def 0 := z.
def 1 := s 0.
def 2 := s 1.
def 3 := s 2.
def 4 := s 3.
def 5 := s 4.
def s0 := type 0.
def s1 := type 1.
def s2 := type 2.
def s3 := type 3.
def s4 := type 4.
def s5 := type 5.
def u0 := u s0.
def u1 := u s1.
def u2 := u s2.
def u3 := u s3.
def u4 := u s4.
def u5 := u s5.
def _prop := u prop.
def _set := u set.
def U0 := U s0.
def U1 := U s1.
def U2 := U s2.
def U3 := U s3.
def U4 := U s4.
def U5 := U s5.
def Prop := U prop.
def Set := U set.
......@@ -10,3 +10,4 @@
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
* **constraints**: Implementation is relying on Coq-like constraints mechanisms
* **varity**: Implementation requires Dedukti to accept rewrite rules of variable arity
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