Commit bb5c9bd3 authored by Hector Suzanne's avatar Hector Suzanne
Browse files

Avec des tests en plus et des bugs en moins

parent 7a7b8f13
......@@ -215,7 +215,7 @@ cons:
| LEFT LPAREN a = typed_var RPAREN {left a}
| RIGHT LPAREN b = typed_var RPAREN {right b}
| INJ LPAREN i = NUM SLASH n = NUM COMMA a = typed_var RPAREN { Inj (i,n,a) }
| SHIFT PLUS a = typed_var RPAREN {shift_pos a}
| SHIFT PLUS LPAREN a = typed_var RPAREN {shift_pos a}
(* Méta-langage *)
......
......@@ -96,7 +96,10 @@ let unify_def ?debug env item =
and unify_bind upol (var, typ) loc =
let polvar =
try VarEnv.find var !env.varpols
with Not_found -> fail_undefined_var (Var.to_string var) loc in
with Not_found ->
let polvar = PolVar.fresh () in
env := {!env with varpols = VarEnv.add var polvar !env.varpols};
polvar in
unify upol (Loc (loc, Redirect polvar));
unify_typ upol typ
......@@ -131,12 +134,9 @@ let unify_def ?debug env item =
match stk with
| Ret -> unify (Loc (loc, upol)) final_upol
| CoZero -> unify upol (Loc (loc, Litt positive))
| CoBind {bind=(var,typ); pol; cmd} ->
let polvar = PolVar.fresh () in
env := {!env with varpols = VarEnv.add var polvar !env.varpols};
| CoBind {bind; pol; cmd} ->
unify_bind upol bind loc;
unify upol (Loc (loc, pol));
unify_typ upol typ;
unify upol (Redirect polvar);
unify_cmd final_upol cmd
| CoBox {stk;_} ->
unify upol (Litt positive);
......@@ -249,8 +249,7 @@ let unify_def ?debug env item =
let upol = Redirect (PolVar.fresh ()) in
unify_cmd upol item.content;
unify_typ upol item.typ;
unify upol item.pol;
unify_typ (Litt Negative) item.cont
unify upol item.pol
end;
begin match item with
......
......@@ -2,12 +2,24 @@ Test that reduction works works
$ autobill simplify <<EOF
> cmd do step GOT_TOP into this.bind x -> x.ret() end
> EOF
/* var x<1> : <t12> */
/* tyvar t12 : - */
cmd<-> anon<0> : <t10> = step-
GOT_TOP
: <t13>
into
this.ret()
end
Test reduction with declarations
$ autobill simplify <<EOF
> decl term y : top
> cmd do step y into this.bind x -> x.ret() end
> EOF
/* var x<2> : <t13> */
/* tyvar t13 : - */
decl term<-> y<0> : top
cmd<-> anon<1> : <t10> = y<0>.ret()
Test shifting
$ autobill simplify <<EOF
......@@ -15,3 +27,45 @@ Test shifting
> term x = unit() in
> term y : (shift- unit) = match this.shift-().ret() -> x.ret() in
> y.ret()
> cmd do
> shift+(GOT_TOP).match shift+(x) -> x.ret()
/* var x<1> : <t13> */
/* var y<2> : (shift- unit) */
/* var x<4> : <t26> */
/* tyvar t13 : + */
/* tyvar t16 : + */
/* tyvar t26 : + */
cmd<-> anon<0> : <t10> =
step-
match
case this.shift-().ret() : <t16> -> unit().ret()
end
: <t19>
into
this.ret()
end
cmd<-> anon<3> : <t22> = step-
GOT_TOP
: <t27>
into
this.ret()
end
Test function calls
$ autobill simplify <<EOF
> decl type a : +
> decl type b : +
> decl type c : +
> decl term x : a
> decl term y : b
> decl term z : c
> cmd do
> term f =
> match this.call(x,y,z).ret() ->
> step
> match this.shift-().ret() -> tupple(y,z,x).ret()
> into
> this.ret()
> end
> in
> f.call(x,y,z).ret()
Supports Markdown
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