Commit 13e46332 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Use skcheck instead of skindent+dkcheck and fix bugs new in Sukerujo

parent 9521a499
...@@ -46,6 +46,8 @@ INSTALL_DIR = /usr/local/bin ...@@ -46,6 +46,8 @@ INSTALL_DIR = /usr/local/bin
DKCHECK=dkcheck DKCHECK=dkcheck
SKINDENT=skindent SKINDENT=skindent
SKCHECK=skcheck
SKDEP=skdep
DKDEP=dkdep DKDEP=dkdep
CONFLUENCECHECKER=$(shell locate csiho.sh) CONFLUENCECHECKER=$(shell locate csiho.sh)
DKCHECKOPTIONS=-nl -errors-in-snf -v -d # -cc $(CONFLUENCECHECKER) DKCHECKOPTIONS=-nl -errors-in-snf -v -d # -cc $(CONFLUENCECHECKER)
...@@ -56,11 +58,8 @@ all: $(DKOS) sigmaid ...@@ -56,11 +58,8 @@ all: $(DKOS) sigmaid
builtins.dko: builtins.dk builtins.dko: builtins.dk
$(DKCHECK) -e $< $(DKCHECK) -e $<
%.dko: %.dko: %.sk
$(DKCHECK) -e $(DKCHECKOPTIONS) $< $(SKCHECK) -e $(DKCHECKOPTIONS) $<
%.dk: %.sk
$(SKINDENT) $< > $@
.v.vo: .v.vo:
coqc $< coqc $<
...@@ -71,8 +70,8 @@ builtins.dko: builtins.dk ...@@ -71,8 +70,8 @@ builtins.dko: builtins.dk
ocamlbuild -use-menhir $@ ocamlbuild -use-menhir $@
depend: .depend depend: .depend
.depend: $(DKS) .depend: $(SKS)
$(DKDEP) $(DKDEPOPTIONS) $(DKS) > .depend $(SKDEP) $(DKDEPOPTIONS) $(SKS) > .depend
clean: clean:
rm -rf *.dko pts.dk dk_*.dk *.vo *.glob .depend tmp.* \ rm -rf *.dko pts.dk dk_*.dk *.vo *.glob .depend tmp.* \
...@@ -91,7 +90,7 @@ test.sk: sigmaid.$(COMPILE_MODE) ...@@ -91,7 +90,7 @@ test.sk: sigmaid.$(COMPILE_MODE)
test.v: sigmaid.$(COMPILE_MODE) test.v: sigmaid.$(COMPILE_MODE)
./sigmaid.$(COMPILE_MODE) test.sigma ./sigmaid.$(COMPILE_MODE) test.sigma
test.dko: test.dk dk_obj_examples.dko test.dko: test.sk dk_obj_examples.dko
test.vo: test.v coq_obj.vo test.vo: test.v coq_obj.vo
......
...@@ -78,9 +78,9 @@ def Subset : Domain -> Domain -> Type. ...@@ -78,9 +78,9 @@ def Subset : Domain -> Domain -> Type.
[A,B] [A,B]
Subset A B Subset A B
--> -->
l : Label -> (l : Label ->
Position l A -> Position l A ->
Position l B. Position l B).
(; Position and membership ;) (; Position and membership ;)
def mem : l : Label -> d : Domain -> bool. def mem : l : Label -> d : Domain -> bool.
......
...@@ -118,16 +118,16 @@ def preselect : A : ObjType -> ...@@ -118,16 +118,16 @@ def preselect : A : ObjType ->
Expr A -> Expr A ->
Expr (Ot_assoc A l H). Expr (Ot_assoc A l H).
[A,m,D,l,H] [m,H]
preselect A D (Po_cons {A} {D} l H m _) {l} {H} (dk_domain.Position_head _ _) preselect _ _ (Po_cons _ _ _ H m _) _ H (dk_domain.Position_head _ _)
--> -->
m m
[A,D,l,l2,o,H,Htl] [A,D,l,l2,o,H,Htl]
preselect preselect
A _
(dk_domain.dcons l2 D) _
(Po_cons _ _ _ _ _ o) (Po_cons A D _ _ _ o)
l l
H H
(dk_domain.Position_tail _ _ _ Htl) (dk_domain.Position_tail _ _ _ Htl)
...@@ -144,11 +144,11 @@ def preupdate : A : ObjType -> ...@@ -144,11 +144,11 @@ def preupdate : A : ObjType ->
PreObj A D. PreObj A D.
[A,D,l,p,o,m2] [A,D,l,p,o,m2]
preupdate preupdate
A _
(dk_domain.dcons _ D) _
(Po_cons _ _ _ p _ o) (Po_cons A D l p _ o)
l _
{p} p
(dk_domain.Position_head _ _) (dk_domain.Position_head _ _)
m2 m2
--> -->
......
...@@ -43,7 +43,7 @@ def eT : uT -> Type. ...@@ -43,7 +43,7 @@ def eT : uT -> Type.
Pi : X : uT -> ((eT X) -> uT) -> uT. Pi : X : uT -> ((eT X) -> uT) -> uT.
[X,Y] [X,Y]
eT (Pi X Y) --> x : (eT X) -> (eT (Y x)). eT (Pi X Y) --> (x : (eT X) -> (eT (Y x))).
def Arrow : uT -> uT -> uT. def Arrow : uT -> uT -> uT.
[t1,t2] [t1,t2]
......
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