Commit 56e2d0ee authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Add automatic checking of confluence.

Comment hard to check rules and fix a confluence bug in dk_machine_int.
parent 1ec3632f
......@@ -6,21 +6,29 @@ DKDEPENDS = $(DKS:.dk=.dk.depend)
DKDEP = dkdep
DKCHECK = dkcheck
DKCHECK_OPTIONS =
DKCHECK_CONFLUENCE_OPTION = -cc $(shell locate csiho.sh)
.PHONY: clean depend
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) $<
# dk_monads and dk_monads_coc use non-linear rules so we deactivate
# confluence checking for those files and activate the relevant options
dk_monads.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) -nl $<
dk_monads_coc.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) -nl -coc $<
# dk_binary_nat is too hard for the confluence checker
dk_binary_nat.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
......
......@@ -35,16 +35,20 @@ def simple_match : A : cc.uT ->
(; Append ;)
def append : A : cc.uT -> List A -> List A -> List A.
[l] append _ (nil _) l --> l
[A,a1,l1,l2] append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2)
[A,l1,l2,l3] append A l1 (append _ l2 l3) --> append A (append A l1 l2) l3.
[A,a1,l1,l2] append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2).
(; Associativity rule, breaks confluence automatic verification. ;)
(; [A,l1,l2,l3] append A (append _ l1 l2) l3 --> append A l1 (append A l2 l3). ;)
(; Map ;)
def map : A : cc.uT ->
B : cc.uT ->
(cc.eT A -> cc.eT B) -> List A -> List B.
[B] map _ B _ (nil _) --> nil B
[A,B,f,a,l] map A B f (cons _ a l) --> cons B (f a) (map A B f l)
[A,B,C,f,g,l] map B C g (map A _ f l) --> map A C (x : cc.eT A => g (f x)) l.
[A,B,f,a,l] map A B f (cons _ a l) --> cons B (f a) (map A B f l).
(; Composition rule, breaks confluence automatic verification. ;)
(; [A,B,C,f,g,l] map B C g (map A _ f l) --> map A C (x : cc.eT A => g (f x)) l. ;)
def mem : A : cc.uT ->
(cc.eT A -> cc.eT A -> cc.eT dk_bool.bool) ->
......
......@@ -145,8 +145,8 @@ def positive : N : UNat -> MInt N -> Bool.
[] positive dk_nat.O O --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S0 dk_nat.O O) --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S1 dk_nat.O O) --> dk_bool.false
[N,n] positive (dk_nat.S N) (S0 _ n) --> positive N n
[N,n] positive (dk_nat.S N) (S1 _ n) --> positive N n.
[N,n] positive (dk_nat.S (dk_nat.S N)) (S0 _ n) --> positive (US N) n
[N,n] positive (dk_nat.S (dk_nat.S N)) (S1 _ n) --> positive (US N) n.
def signed_leq : N : UNat ->
n : MInt N ->
......
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