Commit 74646857 authored by Gaspard Ferey's avatar Gaspard Ferey

Fixed flags

parent 0146527e
(; plus_ACU, lift_0, confluent, max_err
(; plus_ACU, lift_1, confluent, max_err
Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
Maude joins all critical pairs.
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
;)
(;-------------------------------;)
......
(; plus_AC, lift_0, confluent, max_err
(; plus_AC, lift_1, confluent, max_err
System derived from original.
......@@ -8,8 +8,8 @@ This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
......
(; plus_AC, lift_0
(; plus_AC, lift_1
System derived from original.
......@@ -12,9 +12,8 @@ This variant implements :
- Added the i + (max j k) --> max (i+j) (i+k)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
;)
(;-------------------------------;)
......
......@@ -8,9 +8,8 @@ This variant implements :
- Use of ACU for max (not for plus)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
;)
(;-------------------------------;)
......
(; max_AC, lift_0, WIP ;)
Sort : Type.
......
(; This is not a CiC implementation : nocic ;)
def Cstr := cc.Cstr.
def s := cc.s.
def Sort := cc.N.
......
# All supported flags
FLAGS=max_AC plus_AC plus_ACU cast lift lift_0 max_err confluent WIP constraints
FLAGS=max_AC plus_AC plus_ACU cast lift lift_1 max_err confluent WIP constraints
DKS=$(shell find ./ -type f -name '*.dk')
......@@ -16,14 +16,16 @@ all:
@for fg in $(FLAGS) ; do echo -n " --- |" >> README.md ; done
@echo -n "\n" >> README.md
@for dk in $(DKS) ; do \
echo -n "| [$$dk]($$dk) |" >> README.md ; \
for fg in $(FLAGS) ; do \
if [ -z $$(head -q -n 1 $$dk | grep "$$fg") ]; then \
echo -n " |" >> README.md ; \
else \
echo -n " X |" >> README.md ; \
fi ; \
done ; \
echo -n "\n" >> README.md ; \
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 \
echo -n " |" >> README.md ; \
else \
echo -n " X |" >> README.md ; \
fi ; \
done ; \
echo -n "\n" >> README.md ; \
fi ; \
done
@cat post.txt >> README.md
This project contains various implementations of cic.dk
| File | max_AC | plus_AC | plus_ACU | cast | lift | lift_0 | max_err | confluent | WIP | constraints |
| 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) | | | | | | | | | | |
| [./old_to_ACU/translation.dk](./old_to_ACU/translation.dk) | | | | | | | | | | |
| [./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 |
| [./Constraints/idcic.dk](./Constraints/idcic.dk) | | | | | | | | | | |
| [./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 | 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 | | | | |
| [./example_id.dk](./example_id.dk) | | | | | | | | | | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | | | | | | | | | | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | X | | | | X | | | | X | |
## Flags
* **max_AC**: `max` on universe levels is AC
* **plus_AC**: `plus` on universe levels is AC
* **plus_ACU**: `plus` on universe levels is ACU
* **cast**: `cast` term from subtype to supertype is implemented
* **lift**: `lift` type from any universe to higher universe
* **lift_0**: `lift` type from `Type0` to higher universe
* **lift**: `lift` type from any universe i to any higher universe j
* **lift_1**: `lift` type from any universe i to (i+1)
* **max_err**: `1 + max(i,j)` is not convertible with `max(1+i, 1+j)`
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
......
#NAME idic.
(; This is not a CiC implementation : nocic ;)
def Top_3 := cc.1.
def Top_48 := cc.2.
......
(; plus_AC, lift_0
(; plus_AC, lift_1
System derived from original.
This variant implements :
......
#NAME cic.
(; This is not a CiC implementation : nocic ;)
def Nat : Type := cc.Sort.
......
#NAME cic.
(; max_AC, lift, WIP ;)
(; Natural numbers ;)
......
......@@ -4,8 +4,8 @@
* **plus_AC**: `plus` on universe levels is AC
* **plus_ACU**: `plus` on universe levels is ACU
* **cast**: `cast` term from subtype to supertype is implemented
* **lift**: `lift` type from any universe to higher universe
* **lift_0**: `lift` type from `Type0` to higher universe
* **lift**: `lift` type from any universe i to any higher universe j
* **lift_1**: `lift` type from any universe i to (i+1)
* **max_err**: `1 + max(i,j)` is not convertible with `max(1+i, 1+j)`
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
......
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