Commit b5b75fba authored by G. GENESTIER's avatar G. GENESTIER

More libraries centralisation oriented directory

parent d82619e6
*~
\#*\#
*.dko
.*
matita/*
sigmaid/*
verine/*
......@@ -8,4 +9,5 @@ zenon_dk/*
focalide_dks/*
holide_lib/*
iProverModulo_dk/*
dklib-master/*
\ No newline at end of file
dklib-master/*
TermChecker/*.txt
\ No newline at end of file
#NAME test.
nat : Type.
0 : nat.
S : nat -> nat.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
defac mset [nat].
#CONV mset 1 0, mset 0 1.
#CONV mset 0 1, mset 1 0.
#CONV mset 1 0, mset 0 0.
#WHNF mset (mset 2 0) (mset 1 ( (x : nat => mset x (mset (S x) x)) 4)).
#SNF mset (mset 2 0) (mset 1 ( (x : nat => mset x (mset (S x) x)) 4)).
#CONV mset (mset 3 4) (mset 0 1), mset (mset (mset 1 4) 0) 3.
defac min [nat].
[] min 0 --> (x : nat => 0)
[x] min 0 x --> 0
[x,y] min (S x) (S y) --> S (min x y).
#GDT min.
#SNF min (S (S 0)) (min 0 (S 0)).
#PRINT "".
#PRINT "----------- plus ------------".
defacu plus [nat,0].
[x,y] plus (S x) y --> S (plus x y).
#GDT plus.
#SNF plus (plus 2 0) (plus 1 ( (x : nat => plus x (plus (S x) x)) 4)).
#PRINT "".
#PRINT "----------- time ------------".
defacu time [nat,S 0].
[] time 0 _ --> 0.
[x,y] time (S x) y --> plus y (time x y).
#GDT time.
#WHNF time 1 2.
#SNF time 1 2.
#SNF time 5 5.
#PRINT "----------- square ------------".
def square := (x : nat => time x x).
#CONV plus (square 3) (square 4), square 5.
#PRINT "----------- tricky ------------".
defac tricky [nat].
[x,y,z] tricky (tricky x z) (tricky y x) --> 0.
#GDT tricky.
#SNF tricky (tricky 1 (tricky 2 3)) (tricky 5 1).
#SNF tricky (tricky 1 (tricky 2 1)) (tricky 5 2).
#SNF tricky (tricky 1 (tricky 2 3)) (tricky 5 4).
#PRINT "------------ vector -------------".
Vect : nat -> Type.
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat (plus n1 n2) (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
[l] concat 0 _ _ l --> l.
\ No newline at end of file
DKS=$(wildcard *.dk)
# DKOS need not have the same name that the corresponding Dedukti
# files (modulogic.dk becomes zen.dko) but for each file f.dk, dkdep
# f.dk outputs the name of the produced dko file before the ':'
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
DKDEP=dkdep
DKCHECK=dkcheck
all: $(DKOS)
%.dko:
$(DKCHECK) -e -nl $<
clean:
rm -f *.dko .depend
depend: .depend
.depend:
$(DKDEP) *.dk > ./.depend
-include .depend
#NAME Church.
type : Type.
arr : type -> type -> type.
def e : type -> Type.
[a : type, b : type] e (arr a b) --> e a -> e b.
def numeral : Type := A : type -> (e A -> e A) -> (e A -> e A).
def zero : numeral := A : type => f : (e A -> e A) => x : e A => x.
def one : numeral := A : type => f : (e A -> e A) => x : e A => f x.
def two : numeral := A : type => f : (e A -> e A) => x : e A => f (f x).
def three : numeral := A : type => f : (e A -> e A) => x : e A => f (f (f x)).
def four : numeral := A : type => f : (e A -> e A) => x : e A => f (f (f (f x))).
def plus : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => f : (e A -> e A) => x : e A => m A f (n A f x).
def times : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => f : (e A -> e A) => x : e A => m A (n A f) x.
def power : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => n (arr A A) (m A).
def test : numeral := power two (plus one (times three four)).
def test_ : numeral := power two (plus (times four four) one).
P : numeral -> Type.
P2: n:numeral -> P n -> Type.
y : P test_.
z: P2 test y.
#NORMALIZE zero.
#NORMALIZE one.
#NORMALIZE two.
#NORMALIZE three.
#NORMALIZE four.
#NORMALIZE plus one (times three four).
#NAME def.
A:Type.
P:A->Type.
def magic (a1:A) (a2:A) (H:P a1) : P a2 := H.
#NAME pouet.
karaté:Type.
#NAME pouet.
id:Type
#NAME rule_name.
nat : Type.
0 : nat.
def plus : nat -> nat -> nat.
{rule_name.plus_0_n} [n] plus 0 n --> n.
\ No newline at end of file
#NAME var.
A:Type.
a:A.
[x:A] x --> a.
#NAME scope.
id:toto.tata.
#NAME abs.
A:Type.
y:A.
P:A->Type.
p:P y.
id: x:A -> P x -> P x.
def T: P y.
(; [ ] T --> (z => id z p) y. ;)
[ ] T --> (z:A => id z p) y.
#NAME omega.
A : Type.
B : A -> Type.
C : B ( (x => x x)(x => x x) ).
#NAME pi.
T:Type.
x:T.
f:x->Type.
#NAME sort.
nat : Type.
x : nat.
y : x.
DKS=$(wildcard *.dk)
# DKOS need not have the same name that the corresponding Dedukti
# files (modulogic.dk becomes zen.dko) but for each file f.dk, dkdep
# f.dk outputs the name of the produced dko file before the ':'
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
DKDEP=dkdep
DKCHECK=dkcheck
all: $(DKOS)
%.dko:
$(DKCHECK) -e -nl $<
clean:
rm -f *.dko .depend
depend: .depend
.depend:
$(DKDEP) *.dk > ./.depend
-include .depend
......@@ -99,7 +99,7 @@ def Bin : Nat -> Nat -> Nat.
[m, n] Bin (s m) (s n) --> plus (Bin m (s n)) (Bin (s m) n).
def ordrec : A : type -> eval A -> (Ord -> eval A -> eval A) -> ((Nat -> Ord) -> (Nat -> eval A) -> eval A) -> Ord -> eval A.
[x, y, z] ordrec _ x y z 0 --> x.
[x, y, z] ordrec _ x y z 0_ord --> x.
[A, x, y, z, n] ordrec A x y z (s_ord n) --> y n (ordrec A x y z n).
[A, x, y, z, f] ordrec A x y z (lim f) --> z f (n => ordrec A x y z (f n)).
......
import sys
toStudy=open("erreur_"+sys.argv[1]+".txt",'r')
current=0
every=[[],[],[],[],[],[],[],[]]
for line in toStudy:
if line.find("SUCCESS The file was proved terminating")==0:
current=0
elif line.find("ERROR The SCT checker did not proved this file terminating")==0:
current=1
elif line.find("ERROR The pattern matching done line")==0:
current=2
elif line.find("ERROR The symbol")==0:
current=3
elif line.find("ERROR The rule declared line")==0:
current=4
elif line.find("ERROR The meaning of external_rules")==0:
current=5
elif line.find("ERROR Comp error")==0:
current=6
elif line.find("ERROR Problem with the Tarjan algorithm")==0:
current=7
elif line.find("ERROR Type level rewriting between")==0:
current=8
elif line.find("ERROR Type level contains")==0:
current=9
elif line.find("ERROR Module dependancy")==0:
current=10
elif line.find("ERROR The caller line")==0:
current=11
elif line.find("ERROR There is a typing error")==0:
current=12
elif line.find("SUCCESS File")==0:
if current<7:
every[current].append(line.split("'")[1])
else:
every[7].append(line.split("'")[1])
else:
print(line)
toStudy.close()
longueur=0
for i in range(8):
a=len(every[i])
if a>longueur:
longueur=a
toFill=open("../../Bureau/TabRes.csv",sys.argv[2])
toFill.write(";;;"+sys.argv[1]+";;;;\n;;;;;;;;\n")
toFill.write("Accepted;Refused;Pattern Matching;Non-positive;Non linearity;Ext_rule;CompError;Autres\n")
for i in range(longueur):
for j in range(8):
if len(every[j])>i:
toFill.write(every[j][i])
if j==7:
toFill.write('\n')
else:
toFill.write(";")
toFill.write(";;;;;;;\n")
toFill.close()
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