Commit f32ff557 authored by Pietro Abate's avatar Pietro Abate

Fix subsitution problem

Now gamma is correctly propagated in the compilation Enviroment
and substitions are correctly applied to abstractions
parent 95f1a9ed
......@@ -62,9 +62,10 @@ let find_ext cu x =
let enter_local env x =
let new_size = env.stack_size + 1 in
if new_size > !(env.max_stack) then (env.max_stack) := new_size;
{ env with
{ env with
vars = Env.add x (Local env.stack_size) env.vars;
stack_size = new_size }
stack_size = new_size;
}
let enter_global_toplevel env x =
{ env with
......@@ -77,7 +78,7 @@ let enter_global_cu cu env x =
global_size = env.global_size + 1 }
let rec domain = function
|Identity -> assert false
|Identity -> Var.Set.empty
|List l -> Types.Tallying.domain l
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Sel(_,_,sigma) -> (domain sigma)
......@@ -101,9 +102,6 @@ let fresharg =
(* Comp for Lambda.sigma but simplify if possible. *)
let rec comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| Comp(s3, s4), List(_) -> (match comp s4 s2 with
| Comp(_) as s5 when s4 = s5 -> s1
| Comp(_) -> Comp(s1, s2)
......@@ -139,14 +137,15 @@ and compile_aux env = function
let v = find x env in
let ts = Types.all_vars (Types.descr (IdMap.assoc x env.gamma)) in
let is_mono x =
if Var.Set.is_empty ts then true else
let from_xi = try IdMap.assoc x env.xi with Not_found -> Var.Set.empty in
let d = Var.Set.inter from_xi (domain(env.sigma)) in
Var.Set.is_empty (Var.Set.inter ts d)
in
if Var.Set.is_empty ts then Var (v) else
if env.sigma = Identity then TVar(v,env.sigma) else
if is_mono x then Var (v) else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = comp env.sigma (List sl) } e
| Typed.Subst(e,sl) ->
let env = { env with sigma = Comp(env.sigma,(List sl)) } in
compile env e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
| Typed.Abstraction a -> compile_abstr env a
......@@ -248,10 +247,7 @@ and compile_abstr env a =
if is_mono then
Abstraction(slots, a.Typed.fun_iface, body, !(env.max_stack))
else
let sigma = match env.sigma with
| Identity -> Identity
| _ -> Sel(Env 1,a.Typed.fun_iface,lift nb_slots (env.sigma))
in
let sigma = Sel(Env 1,a.Typed.fun_iface,lift nb_slots (env.sigma)) in
PolyAbstraction(slots, a.Typed.fun_iface, body, !(env.max_stack), sigma)
and compile_branches env (brs : Typed.branches) =
......@@ -275,7 +271,7 @@ and compile_branch env br =
let m = Patterns.filter (Types.descr (Patterns.accept br.Typed.br_pat)) br.Typed.br_pat in
let env =
{ env with
gamma = IdMap.merge (fun _ v2 -> v2) m env.gamma;
gamma = IdMap.merge (fun _ v2 -> v2) env.gamma m;
xi = IdMap.merge (fun _ v2 -> v2) env.xi br.Typed.br_vars_poly
}
in
......@@ -350,9 +346,9 @@ let let_decl ~run ~show (tenv,cenv,codes) p e =
(* XXX I've the impression I'm duplicating information here
* as cenv.gamma == tenv.gamma *)
let cenv = {cenv with gamma =
List.fold_left (fun acc (id,_) ->
List.fold_left (fun acc (id,t) ->
(* an old binding is showed by a new one *)
IdMap.add id (Types.cons (Typer.find_value id tenv)) (IdMap.remove id acc)
IdMap.add id (Types.cons t) (IdMap.remove id acc)
) cenv.gamma ids;
}
in
......@@ -362,6 +358,13 @@ let let_decl ~run ~show (tenv,cenv,codes) p e =
let let_funs ~run ~show (tenv,cenv,codes) funs =
let (tenv,funs,ids) = Typer.type_let_funs tenv funs in
let (cenv,code) = compile_rec_funs cenv funs in
let cenv = {cenv with gamma =
List.fold_left (fun acc (id,t) ->
(* an old binding is showed by a new one *)
IdMap.add id (Types.cons t) (IdMap.remove id acc)
) cenv.gamma ids;
}
in
run_show ~run ~show tenv cenv code ids;
(tenv,cenv,List.rev_append code codes)
......
......@@ -84,13 +84,12 @@ let apply_sigma sigma = function
|v -> v
;;
let rec eval_sigma env locals = function
|Lambda.Comp(s1,s2) -> Value.Comp(eval_sigma env locals s1,eval_sigma env locals s2)
let rec eval_sigma = function
|Lambda.Comp(s1,s2) -> Value.Comp(eval_sigma s1,eval_sigma s2)
|Lambda.Identity -> Value.Identity
|Lambda.List [] -> Value.Mono
(* |Lambda.List i when i = Types.Tallying.CS.sat -> Value.Identity *)
|Lambda.List l -> Value.List l
|Lambda.Sel(x,iface,sigma) -> Value.Sel(1,iface,eval_sigma env locals sigma)
|Lambda.Sel(x,iface,sigma) -> Value.Sel(1,iface,eval_sigma sigma)
(* env is an array implementing de bruines indexes *)
(* Evaluation rules : Lambda -> Value *)
......@@ -102,15 +101,14 @@ let rec eval env locals = function
v
| Var x -> eval_var env locals x
| TVar (x,sigma) -> (* delayed sigma application *)
let sigma' = eval_sigma env locals sigma in
apply_sigma sigma' (eval_var env locals x)
let v = eval_var env locals x in
apply_sigma (eval_sigma sigma) v
| Apply (e1,e2) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
eval_apply v1 v2
| PolyAbstraction (slots,iface,body,lsize,sigma) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
eval_abstraction env locals slots iface body lsize (eval_sigma sigma)
| Abstraction (slots,iface,body,lsize) ->
eval_abstraction env locals slots iface body lsize Value.Mono
| Const c -> c
......
......@@ -180,7 +180,7 @@ module Make(X : Custom.T) = struct
let l = assoc_remove_aux v r l in
match !r with Some x -> (x,l) | _ -> assert false
(* TODO: is is faster to raise exception Not_found and return
(* TODO: is it faster to raise exception Not_found and return
original list ? *)
let rec remove v = function
| (((x,y) as a)::rem) as l->
......
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