Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
P
PleinDeDk
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
2
Issues
2
List
Board
Labels
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Guillaume GENESTIER
PleinDeDk
Commits
0146527e
Commit
0146527e
authored
Apr 11, 2018
by
Gaspard Ferey
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Updated flags.
parent
10add8ef
Hide whitespace changes
Inline
Side-by-side
Showing
13 changed files
with
60 additions
and
31 deletions
+60
-31
cicup.dk
CoqModels/AC/cicup.dk
+1
-1
cc.dk
CoqModels/AC_Gilles/1-original/cc.dk
+3
-1
cicup_0elim.dk
CoqModels/AC_Gilles/cicup_0elim.dk
+2
-2
cicup_0elim_maxplus.dk
CoqModels/AC_Gilles/cicup_0elim_maxplus.dk
+2
-2
cicup_maxAC.dk
CoqModels/AC_Gilles/cicup_maxAC.dk
+2
-2
cc.dk
CoqModels/Constraints/cc.dk
+2
-0
HOAS_to_DBAC.dk
CoqModels/HOAS/HOAS_to_DBAC.dk
+1
-1
Makefile
CoqModels/Makefile
+2
-1
README.md
CoqModels/README.md
+29
-17
cicup_v2.dk
CoqModels/old_to_ACU/cicup_v2.dk
+2
-2
cic.dk
CoqModels/orig/cic.dk
+1
-1
cic_coqine.dk
CoqModels/orig/cic_coqine.dk
+1
-1
post.txt
CoqModels/post.txt
+12
-0
No files found.
CoqModels/AC/cicup.dk
View file @
0146527e
(; max_AC, plus_AC,
experiment
;)
(; max_AC, plus_AC,
WIP
;)
Sort : Type.
...
...
CoqModels/AC_Gilles/1-original/cc.dk
View file @
0146527e
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
(; plus_ACU, lift_0, confluent, max_err
Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
Maude joins all critical pairs.
...
...
CoqModels/AC_Gilles/cicup_0elim.dk
View file @
0146527e
#NAME cc.
(; plus_AC, lift_0, confluent, max_err
(;
System derived from original.
System derived from original.
Maude joins all critical pairs.
...
...
CoqModels/AC_Gilles/cicup_0elim_maxplus.dk
View file @
0146527e
#NAME cc.
(; plus_AC, lift_0
(;
System derived from original.
System derived from original.
Maude requires 23 critical pairs to be joined.
rule(i,k) <-> max(k,rule(i,k))
...
...
CoqModels/AC_Gilles/cicup_maxAC.dk
View file @
0146527e
#NAME cc.
(; max_ACU, lift_0
(;
System derived from original.
System derived from original.
No Maude test performed.
...
...
CoqModels/Constraints/cc.dk
View file @
0146527e
(; WIP, constraints ;)
(; Natural numbers ;)
N : Type.
...
...
CoqModels/HOAS/HOAS_to_DBAC.dk
View file @
0146527e
#NAME HOASDB.
(; WIP ;)
N : Type.
0 : N.
...
...
CoqModels/Makefile
View file @
0146527e
# All supported flags
FLAGS
=
max_AC plus_AC
experiment
FLAGS
=
max_AC plus_AC
plus_ACU cast lift lift_0 max_err confluent WIP constraints
DKS
=
$(
shell
find ./
-type
f
-name
'*.dk'
)
...
...
@@ -26,3 +26,4 @@ all:
done
;
\
echo
-n
"
\n
"
>>
README.md
;
\
done
@
cat
post.txt
>>
README.md
CoqModels/README.md
View file @
0146527e
This project contains various implementations of cic.dk
| File | max_AC | plus_AC | experiment |
| --- | --- | --- | --- |
|
[
./AC/cicup.dk
](
./AC/cicup.dk
)
| X | X | X |
|
[
./HOAS/HOAS_to_DBAC.dk
](
./HOAS/HOAS_to_DBAC.dk
)
| | | |
|
[
./orig/cic_coqine.dk
](
./orig/cic_coqine.dk
)
| | | |
|
[
./orig/cic.dk
](
./orig/cic.dk
)
| | | |
|
[
./orig/cic_v2.dk
](
./orig/cic_v2.dk
)
| | | |
|
[
./old_to_ACU/translation.dk
](
./old_to_ACU/translation.dk
)
| | | |
|
[
./old_to_ACU/cicup_v2.dk
](
./old_to_ACU/cicup_v2.dk
)
| | | |
|
[
./Constraints/cc.dk
](
./Constraints/cc.dk
)
| | | |
|
[
./Constraints/idcic.dk
](
./Constraints/idcic.dk
)
| | | |
|
[
./AC_Gilles/1-original/cc.dk
](
./AC_Gilles/1-original/cc.dk
)
| | | |
|
[
./AC_Gilles/cicup_maxAC.dk
](
./AC_Gilles/cicup_maxAC.dk
)
| | | |
|
[
./AC_Gilles/cicup_0elim.dk
](
./AC_Gilles/cicup_0elim.dk
)
| | | |
|
[
./AC_Gilles/cicup_0elim_maxplus.dk
](
./AC_Gilles/cicup_0elim_maxplus.dk
)
| | | |
|
[
./example_id.dk
](
./example_id.dk
)
| | | |
|
[
./AC_with_constraints/cic.dk
](
./AC_with_constraints/cic.dk
)
| | | |
| File | max_AC | plus_AC | plus_ACU | cast | lift | lift_0 | 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
)
| | | | | | | | | | |
|
[
./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_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
)
| | | | | | | | | | |
## 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
*
**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)
*
**constraints**
: Implementation is relying on Coq-like constraints mechanisms
CoqModels/old_to_ACU/cicup_v2.dk
View file @
0146527e
#NAME cc.
(; plus_AC, lift_0
(;
System derived from original.
System derived from original.
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
;)
...
...
CoqModels/orig/cic.dk
View file @
0146527e
#NAME cic.
(; lift ;)
(; Natural numbers ;)
...
...
CoqModels/orig/cic_coqine.dk
View file @
0146527e
(; ;)
(;
cast, lift
;)
(; Natural numbers ;)
...
...
CoqModels/post.txt
0 → 100644
View file @
0146527e
## 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
* **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)
* **constraints**: Implementation is relying on Coq-like constraints mechanisms
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment