Commit 6529db60 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

A little bit of cleanup

parent 00e1d3aa
signature abs =
a,b,c:type;
d:type;
t,u,v:(a -> a);
w: a -> d;
cst : a;
end
signature obj =
s:type;
tt,uu,vv:s;
infix + : s -> s -> s;
prefix - : s -> s;
w=lambda x. tt+x:s->s;
binder ALL = lambda P . P (w tt):(s -> s) -> s;
z = ALL t.t+tt: s
end
lexicon absobj ( abs ) : obj =
a,b,c:=s;
d:=s=>s;
t:= lambda x.-x;
u:= lambda x.ALL y.x+y ;
v:=w;
cst := tt;
w := lambda x.Lambda y. y + ( tt +x)
end
(* Fichier d'essais d'erreurs de parsing pour les messages *)
(* voir /home/pogodall/import/ocaml/dypgen-20070803/generators/dypgen/dypgen.ml
et dypgen_lexer.mll pour s'inspirer de la mthode.
En particulier, donner le type d'expression attendue *)
signature essai =
a,b: type ;
c: a ;
(* message incomprhensible : dire que + est infix, idem prefix *)
infix + : a -> a -> a;
prefix - : a -> a -> a;
(* OK c = lambda x . x + : a *)
(* OK d = lambda x . x x + x :a; *)
(* OK e = lambda x. x ( + - x) : a ;*)
(**************OK********************)
(* messages incomprhensibles *)
(* infix - : a -> ; *)
(* infix - : -> a ; *)
(****************OK*******************)
(* dire binder expected, pas reconnu *)
(* c = labda x.x : a->a ; *)
end
\ No newline at end of file
signature toto =
a:type ;
t1,t2: a-> a ;
d,e:a;
a: a -> a;
b,c:type ;
prefix * : b -> a;
t,toto,aa,bb,cc :a -> a -> b ;
string = a -> a : type;
u : (b ->c) -> a;
binder All : (a -> a) -> a;
prefix - : a -> a;
infix + : a -> a -> a;
v1 = t : a -> a -> b;
vv = lambda x y . x + y : a -> a -> a;
v3 = Lambda x.x+x: a => a;
v = lambda x y . t (- (t2 x)) y: a -> a -> b ;
vvv = lambda x y . (t1 x) + (t2 y) : a -> a -> a ;
vv1 = t * (bb d d) : (a -> b);
v2 = lambda x . d + (t1 x) + d + e : a -> a;
z = lambda z.All x y . z+ x + y : a -> a ;
nonlinear = a => a : type;
truc = Lambda x. x: a => a;
binder Ex : (a -> a) -> a;
bidule = Ex x y . - (x +x) : a;
c_n_l : a => a;
(* example = lambda x.c_n_l (t1 x):a ->a;*)
(* tugudu = (lambda x.x) a : a -> a; *)
vacuous = lambda x.t1 d : a-> a;
end
signature tutu =
a:type;
t1,t2: a-> a;
b,c:type ;
t,toto,aa,bb,cc :a -> a -> b ;
u : (b ->c) -> a;
binder All = t : a -> a -> b;
prefix - : a -> a;
infix + : a -> a;
(* v = t : a -> a; *)
vv = lambda x . t1 (t2 x) : a -> a ;
v = t1 - t2 : a ;
vvv = t1 + t2 : a ;
(* vv = t bb : a -> a -> a -> a; *)
(* v = t + aa + bb + cc : a -> a; *)
(* c = lambda a b c x.t (lambda uu v t. toto (All x y z .(- - t aa bb cc) (z + v + t)) v) x : a -> a ; *)
end
signature titi =
a:type;
t1,t2: a-> a;
b,c:type ;
t,toto,aa,bb,cc :a -> a -> b ;
u : (b ->c) -> a;
binder All = t : a -> a -> b;
infix - : a -> a;
prefix + : a -> a;
vv = lambda x . t1 (t2 x) : a -> a ;
(* v = t1 - t2 : a ; *)
(* vvv = t1 + t2 : a ; *)
v4 = lambda x . t1 x : a ;
(* vv = t bb : a -> a -> a -> a; *)
(* v = t + aa + bb + cc : a -> a; *)
(* c = lambda a b c x.t (lambda uu v t. toto (All x y z .(- - t aa bb cc) (z + v + t)) v) x : a -> a ; *)
end
\ No newline at end of file
signature toto =
a,b:type;
t1,t2,toto,aa,bb,cc: a-> a;
x:a;
qq = lambda y x1 . x1 t1 t1 : a;
t :a ;
binder All = t : a -> a -> b;
prefix - : (a -> a) -> a ;
infix + : (a -> a) -> (a -> a) -> a -> a;
c = lambda a b c x1.t (lambda uu v t. toto (All x y z z .(- - t aa bb - cc) (z + v + t x)) v) x1 : a -> a ;
string = a->a : type ;
end
signature titi =
a:type;
t1,t2: a-> a;
b,c:type ;
t,toto,aa,bb,cc :a -> a -> b ;
u : (b ->c) -> a;
binder All = t : a -> a -> b;
infix - : a -> a;
prefix + : a -> a;
qqqqq = lambda x . t1 - ( + (t2 x)) : a -> a ;
vv = lambda x . t1 (t2 x) : a -> a ;
v = lambda x. (t1 x) - (t2 x) : a ;
vvv = t1 + t2 : a ;
(* vv = t bb : a -> a -> a -> a; *)
(* v = t + aa + bb + cc : a -> a; *)
(* c = lambda a b c x.t (lambda uu v t. toto (All x y z .(- - t aa bb cc) (z + v + t)) v) x : a -> a ; *)
end
\ No newline at end of file
signature toto =
a:type;
t: a;
x : a ;
infix + : a -> a -> a ;
c = lambda x.t + x : a -> a;
v = c t : a;
ww = lambda x.x : a-> a;
end
\ No newline at end of file
signature toto =
\ No newline at end of file
signature toto =
a:type ;
t1,t2:a;
prefix - : a -> a;
v = t1 - t2 : a ;
infix + : a -> a -> a;
vv = t1 + t2 + - t2 : a;
end
\ No newline at end of file
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