Commit b51c79e8 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add Empty slot in the enviroment to implement delayed evaluation

parent 6dce4b88
......@@ -16,7 +16,7 @@ let global_size env = env.global_size
let mk cu = {
cu = cu;
vars = Env.empty;
sigma = List [];
sigma = Lambda.Identity;
gamma = IdMap.empty;
stack_size = 0;
max_stack = ref 0;
......@@ -59,17 +59,13 @@ let enter_global_cu cu env x =
global_size = env.global_size + 1 }
let rec domain = function
|Identity -> []
|List l -> Types.Tallying.domain l
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Sel(_,_,s) -> (domain s)
let count_name = ref 0
let fresh_arg () =
incr count_name;
let s = ("__abstr_arg" ^ (string_of_int !count_name)) in
(0,Ns.U.mk s)
|Sel(_,sigma) -> (domain sigma)
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
(* Typed -> Lambda *)
let rec compile env e = compile_aux env e.Typed.exp_descr
and compile_aux env = function
| Typed.Forget (e,_) -> compile env e
......@@ -133,9 +129,8 @@ and compile_abstr env a =
| Some x -> Env.add x (Env 0) Env.empty, [x, Types.cons a.Typed.fun_typ]
| None -> Env.empty, []
in
(* here is were we add a fresh variable to compture the argument of an abstraction *)
let fun_env = Env.add (fresh_arg ()) (Env 1) fun_env in
(* we add a nameless empty slot for the argument *)
let fun_env = Env.add (0,U.mk "") (Env 1) fun_env in
let (slots,nb_slots,fun_env) =
List.fold_left
......@@ -151,20 +146,18 @@ and compile_abstr env a =
Env.add x p fun_env
| Dummy -> assert false
)
([Dummy],2,fun_env) (IdSet.get a.Typed.fun_fv)
([Dummy;Dummy],2,fun_env) (IdSet.get a.Typed.fun_fv)
in
let slots = Array.of_list (List.rev slots) in
let env =
let env =
{ env with vars = fun_env;
gamma = IdMap.merge (fun _ v2 -> v2) env.gamma fun_name;
stack_size = 0;
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
(* we add a fresh variable to this abstraction *)
let argvar = Local 1 in
let sigma = Sel(argvar,a.Typed.fun_iface,env.sigma) in
let sigma = Sel(List.map snd a.Typed.fun_iface,env.sigma) in
let polyvars =
let vs =
List.fold_left (fun acc (t1,t2) ->
......@@ -176,9 +169,9 @@ and compile_abstr env a =
Var.Set.inter (domain(env.sigma)) vs
in
if Var.Set.is_empty polyvars then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma, argvar)
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
else
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma, argvar)
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
......
......@@ -25,16 +25,17 @@ type var_loc =
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
type sigma =
| Identity
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * (Types.t * Types.t) list * sigma)
| Sel of (Types.t list * sigma)
type expr =
| Var of var_loc
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma * var_loc
(* environment, interface, branches, size of locals, eval flag, substitutions, variable *)
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......@@ -69,5 +70,4 @@ type code_item =
(* expression, size of locals, dispatcher, number of globals to set *)
| LetDecl of expr * int
type code = code_item list
......@@ -25,15 +25,16 @@ type var_loc =
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
type sigma =
| Identity
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * (Types.t * Types.t) list * sigma)
| Sel of (Types.t list * sigma)
type expr =
| Var of var_loc
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma * var_loc
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
| Check of expr * Auto_pat.state
| Const of Value.t
......
......@@ -65,7 +65,7 @@ let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
let apply_sigma sigma = function
|Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,Value.Comp(sigma,sigma'))
|Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,Value.Comp(sigma,sigma'))
|Value.Abstraction(sI,f,sigma') -> Value.Abstraction(sI,f,Value.Comp(sigma,sigma'))
|Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.Comp(sigma,sigma'))
|Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.Comp(sigma,sigma'))
|Value.Record(m,sigma') -> Value.Record(m,Value.Comp(sigma,sigma'))
......@@ -74,8 +74,9 @@ let apply_sigma sigma = function
let rec eval_sigma env locals = function
|Lambda.Comp(s1,s2) -> Value.Comp(eval_sigma env locals s1,eval_sigma env locals s2)
|Lambda.Identity -> Value.Identity
|Lambda.List l -> Value.List l
|Lambda.Sel(x,iface,sigma) -> Value.Sel(eval_var env locals x,iface,eval_sigma env locals sigma)
|Lambda.Sel(sI,sigma) -> Value.Sel(sI,eval_sigma env locals sigma)
(* env is an array implementing de bruines indexes *)
(* Evaluation rules : Lamda -> Value *)
......@@ -86,8 +87,8 @@ let rec eval env locals = function
Obj.set_tag (Obj.repr e) tag_const;
v
(* variable evaluation will be split in PEnv and Env.
* PEnv and Env belong to the runtime lambda language
* from the parsing ast + typing information *)
* PEnv and Env belong to the runtime lambda language
* from the parsing ast + typing information *)
| Var x -> eval_var env locals x
| TVar (x,sigma) -> (* delayed sigma application *)
let sigma' = eval_sigma env locals sigma in
......@@ -96,7 +97,7 @@ let rec eval env locals = function
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
eval_apply v1 v2
| Abstraction (slots,iface,body,lsize,flag,sigma,var) ->
| Abstraction (slots,iface,body,lsize,flag,sigma) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
| Const c -> c
......@@ -145,15 +146,17 @@ and eval_check env locals e d =
and eval_abstraction env locals slots iface body lsize sigma =
let clousure = Array.map (eval_var env locals) slots in
let f arg = eval_branches clousure (Array.create lsize Value.Absent) body arg in
let a = Value.Abstraction (Some iface,f,sigma) in
let a = Value.Abstraction (Some iface,f,sigma) in
clousure.(0) <- a;
a
and eval_apply f arg = match f with
| Value.Abstraction (_,f,sigma) -> f arg
| Value.Abstraction (_,f,_) -> f arg
| _ -> assert false
and eval_branches env locals brs arg =
(* \Epsilon, x -> v0 *)
env.(1) <- arg;
let (code, bindings) = Run_dispatch.run_dispatcher brs.brs_disp arg in
match brs.brs_rhs.(code) with
| Auto_pat.Match (n,e) ->
......
......@@ -82,7 +82,6 @@ let make_result_basic v (code,r,_) =
done);
code
let make_result_char ch (code,r,_) =
let n = Array.length r in
if n > 0 then (
......@@ -196,9 +195,38 @@ let (@@) v sigma =
|Abstraction (iface,t,s) -> Value.Abstraction (iface,t,Value.Comp(sigma,s))
|_ -> v
let rec eval_sigma env = function
|Value.Identity -> []
|Value.List l -> l
|Value.Comp(s1,s2) -> (eval_sigma env s1) @ (eval_sigma env s2)
|Value.Sel(sI,sigma) ->
List.fold_left (fun acc sigma_j ->
(* we always put the argument in env(1) and we call eval only with
* a clousure from an abstraction *)
if List.exists (fun s_i ->
inzero env env.(1) (Types.Tallying.(s_i @@ sigma_j))
) sI
then sigma_j::acc
else acc
) [] (eval_sigma env sigma)
and inzero env v t = match v with (* XXX I should chech p1(t) and p2(t) or \Omega *)
| Value.Pair (v1,v2,sigma) -> (inzero env (v1 @@ sigma) t) && (inzero env (v2 @@ sigma) t)
| XmlNs (v1,v2,v3,_,sigma)
| Xml (v1,v2,v3,sigma) -> (inzero env (v1 @@ sigma) t) && (inzero env ((Pair (v2,v3,sigma)) @@ sigma) t)
| Record (r,sigma) -> true (* XXX !!!! apply sigma here *)
| Abstraction (None,_,_) -> failwith "Run-time inspection of external abstraction"
| Abstraction (Some iface,_,Value.Identity) -> Types.Arrow.check_iface iface t
| Abstraction (Some iface,_,sigma) ->
let s = List.fold_left (fun acc t -> Types.cap acc (snd t)) Types.any iface in
List.for_all (fun si ->
Types.subtype (Types.Tallying.(s @@ si)) t
) (eval_sigma env sigma)
| _ -> true
let rec run_dispatcher d v =
(* Format.fprintf Format.std_formatter "Matching (%a) with:@." Value.print v;
Patterns.Compile.print_dispatcher Format.std_formatter d; *)
(* Format.fprintf Format.std_formatter "Matching (%a) with:@." Value.print v;
Patterns.Compile.print_dispatcher Format.std_formatter d; *)
match d.actions with
| AIgnore r -> make_result_basic v r
| AKind k -> run_disp_kind k v
......@@ -209,11 +237,9 @@ and run_disp_kind actions v =
| Xml (v1,v2,v3,sigma)
| XmlNs (v1,v2,v3,_,sigma) -> run_disp_prod v (v1 @@ sigma) ((Pair (v2,v3,sigma)) @@ sigma) actions.xml
| Record (r,sigma) -> run_disp_record 0 v r actions.record (* XXX !!!! apply sigma here *)
| String_latin1 (i,j,s,q) ->
(* run_disp_kind actions (Value.normalize v) *)
| String_latin1 (i,j,s,q) -> (* run_disp_kind actions (Value.normalize v) *)
run_disp_string_latin1 i j s q actions
| String_utf8 (i,j,s,q) ->
(* run_disp_kind actions (Value.normalize v) *)
| String_utf8 (i,j,s,q) -> (* run_disp_kind actions (Value.normalize v) *)
run_disp_string_utf8 i j s q actions
| Atom q -> make_result_basic v (Atoms.get_map q actions.atoms)
| Char c -> make_result_basic v (Chars.get_map c actions.chars)
......@@ -227,7 +253,7 @@ and run_disp_kind actions v =
actions.basic
| Abstract (abs,_) ->
run_disp_basic v (fun t -> Types.Abstract.contains abs (Types.get_abstract t))
actions.basic
actions.basic
| Absent ->
run_disp_basic v (fun t -> Types.Record.has_absent t) actions.basic
| Concat (_,_) as v -> run_disp_kind actions (Value.normalize v)
......@@ -239,7 +265,6 @@ and run_disp_prod v v1 v2 = function
| Dispatch (d1,b1) ->
let code1 = run_dispatcher d1 v1 in
run_disp_prod2 v1 v v2 b1.(code1)
and run_disp_prod2 v1 v v2 = function
| Impossible -> assert false
| Ignore r -> make_result_prod v1 v2 v r
......@@ -259,7 +284,6 @@ and run_disp_record n v fields = function
match r with
| Some r -> make_result_basic v r
| None -> assert false
and run_disp_record1 v n v1 rem = function
| Impossible -> assert false
| TailCall d1 -> run_dispatcher d1 v1
......@@ -267,7 +291,6 @@ and run_disp_record1 v n v1 rem = function
| Dispatch (d1,b1) ->
let code1 = run_dispatcher d1 v1 in
run_disp_record2 v n v1 rem b1.(code1)
and run_disp_record2 v n v1 rem = function
| Impossible -> assert false
| Ignore r -> make_result_prod v1 Absent v r
......@@ -275,13 +298,11 @@ and run_disp_record2 v n v1 rem = function
| Dispatch (d2,b2) ->
let code2 = run_disp_record_loop v n rem d2 in
make_result_prod v1 Absent v b2.(code2)
and run_disp_record_loop v n rem d =
match d.actions with
| AIgnore r -> make_result_basic v r
| AKind k -> run_disp_record n v rem k.record
and run_disp_string_latin1 i j s q actions =
if i == j then run_disp_kind actions q
else match actions.prod with
......
......@@ -4,7 +4,7 @@ open Encodings
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (t * (Types.t * Types.t) list * sigma)
| Sel of (Types.t list * sigma)
| Identity
and t =
......
......@@ -4,7 +4,7 @@ open Encodings
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (t * (Types.t * Types.t) list * sigma)
| Sel of (Types.t list * sigma)
| Identity
and t =
......
......@@ -142,11 +142,10 @@ and pp_pattern ppf = function
*)
and pp_fv ppf fv =
let f ppf (id, name) =
Format.fprintf ppf "(%d, %s)" (Upool.int id) (Encodings.Utf8.to_string name)
in
print_lst f ppf fv
and pp_v ppf (id, name) =
Format.fprintf ppf "(%d, %s)" (Upool.int id) (Encodings.Utf8.to_string name)
and pp_fv ppf fv = print_lst pp_v ppf fv
let pp_vloc ppf = function
| Lambda.Local(i) -> Format.fprintf ppf "Local(%d)" i
......@@ -181,7 +180,7 @@ let rec pp_sigma ppf =
function
|Value.List ll -> Types.Tallying.CS.pp_sl ppf ll
|Value.Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Value.Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_value x pp_aux tl pp_sigma s
|Value.Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_v x pp_aux tl pp_sigma s
|Value.Identity -> Format.fprintf ppf "Id"
and pp_value ppf = function
......@@ -222,7 +221,7 @@ let rec pp_lambda_sigma ppf =
function
|Lambda.List ll -> Types.Tallying.CS.pp_sl ppf ll
|Lambda.Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_lambda_sigma s1 pp_lambda_sigma s2
|Lambda.Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_vloc x pp_aux tl pp_lambda_sigma s
|Lambda.Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_v x pp_aux tl pp_lambda_sigma s
and pp_lambda ppf =
let open Lambda in function
......
......@@ -322,16 +322,16 @@ let test_tallying =
(print_test l) >:: (fun _ ->
try
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let result = Tallying.tallying l in
let sigma = Tallying.tallying l in
List.iter (fun (s,t) ->
List.iter (fun sigma ->
let s_sigma = Tallying.apply_subst s sigma in
let t_sigma = Tallying.apply_subst t sigma in
List.iter (fun si ->
let s_sigma = Tallying.(s @@ si) in
let t_sigma = Tallying.(t @@ si) in
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
) (Types.subtype s_sigma t_sigma) true
) result
) sigma
) l
(*
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
......
......@@ -35,7 +35,6 @@ module Make(X : Custom.T) = struct
let exists = List.exists
let fold = List.fold_left
external get: t -> elem list = "%identity"
let singleton x = [ x ]
......@@ -46,335 +45,333 @@ module Make(X : Custom.T) = struct
let empty = []
let is_empty l = l = []
let rec disjoint l1 l2 =
if l1 == l2 then l1 == [] else
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c < 0 then disjoint q1 l2
else if c > 0 then disjoint l1 q2
else false
| _ -> true
let rec cup l1 l2 =
if l1 == l2 then l1 else
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c = 0 then t1::(cup q1 q2)
else if c < 0 then t1::(cup q1 l2)
else t2::(cup l1 q2)
| ([],l2) -> l2
| (l1,[]) -> l1
let add x l = cup [x] l
let rec split l1 l2 =
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c = 0 then let (l1,i,l2) = split q1 q2 in (l1,t1::i,l2)
else if c < 0 then let (l1,i,l2) = split q1 l2 in (t1::l1,i,l2)
else let (l1,i,l2) = split l1 q2 in (l1,i,t2::l2)
| _ -> (l1,[],l2)
let rec diff l1 l2 =
if l1 == l2 then [] else
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c = 0 then diff q1 q2
else if c < 0 then t1::(diff q1 l2)
else diff l1 q2
| _ -> l1
let remove x l = diff l [x]
let rec cap l1 l2 =
if l1 == l2 then l1 else
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c = 0 then t1::(cap q1 q2)
else if c < 0 then cap q1 l2
else cap l1 q2
| _ -> []
let rec subset l1 l2 =
(l1 == l2) ||
match (l1,l2) with
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c = 0 then (
(* inlined: subset q1 q2 *)
(q1 == q2) || match (q1,q2) with
| (t1::qq1, t2::qq2) ->
let c = X.compare t1 t2 in
if c = 0 then subset qq1 qq2
else if c < 0 then false
else subset q1 qq2
| [],_ -> true | _ -> false
)
else if c < 0 then false
else subset l1 q2
| [],_ -> true | _ -> false
let from_list l =
let rec initlist = function
| [] -> []
| e::rest -> [e] :: initlist rest in
let rec merge2 = function
| l1::l2::rest -> cup l1 l2 :: merge2 rest
| x -> x in
let rec mergeall = function
| [] -> []
| [l] -> l
| llist -> mergeall (merge2 llist) in
mergeall (initlist l)
let map f l =
from_list (List.map f l)
let rec mem l x =
match l with
| [] -> false
| t::q ->
let c = X.compare x t in
(c = 0) || ((c > 0) && (mem q x))
module Map = struct
type 'a map = (X.t * 'a) list
external get: 'a map -> (elem * 'a) list = "%identity"
let empty = []
let is_empty l = l = []
let singleton x y = [ (x,y) ]
let fold f l acc = List.fold_left (fun tacc (k,v) -> f k v tacc) acc l
let length = List.length
let domain l = List.map fst l
let rec iter f = function
| (_,y)::l -> f y; iter f l
| [] -> ()
let rec iteri f = function
| (x,y)::l -> f x y; iteri f l
| [] -> ()
let rec filter f = function
| ((x,y) as c)::l -> if f x y then c::(filter f l) else filter f l
| [] -> []
let rec assoc_remove_aux v r = function
| ((x,y) as a)::l ->
let c = X.compare x v in
if c = 0 then (r := Some y; l)
else if c < 0 then a :: (assoc_remove_aux v r l)
else raise Not_found
| [] -> raise Not_found
let assoc_remove v l =
let r = ref None in
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
original list ? *)
let rec remove v = function
| (((x,y) as a)::rem) as l->
let c = X.compare x v in
if c = 0 then rem
else if c < 0 then a :: (remove v rem)
else l
| [] -> []
let rec merge f l1 l2 =
let rec disjoint l1 l2 =
if l1 == l2 then l1 == [] else
match (l1,l2) with
| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
let c = X.compare x1 x2 in
if c = 0 then (x1,(f y1 y2))::(merge f q1 q2)
else if c < 0 then t1::(merge f q1 l2)
else t2::(merge f l1 q2)
| ([],l2) -> l2
| (l1,[]) -> l1
let rec combine f1 f2 f12 l1 l2 =
match (l1,l2) with
| (x1,y1)::q1, (x2,y2)::q2 ->
let c = X.compare x1 x2 in
if c = 0 then (x1,(f12 y1 y2))::(combine f1 f2 f12 q1 q2)
else if c < 0 then (x1,f1 y1)::(combine f1 f2 f12 q1 l2)
else (x2, f2 y2)::(combine f1 f2 f12 l1 q2)
| [], l2 -> List.map (fun (x2,y2) -> (x2,f2 y2)) l2
| l1, [] -> List.map (fun (x1,y1) -> (x1,f1 y1)) l1
let rec cap f l1 l2 =
match (l1,l2) with
| (x1,y1)::q1, (x2,y2)::q2 ->
let c = X.compare x1 x2 in
if c = 0 then (x1,(f y1 y2))::(cap f q1 q2)
else if c < 0 then cap f q1 l2
else cap f l1 q2
| _ -> []
let rec sub f l1 l2 =
match (l1,l2) with
| ((x1,y1) as t1)::q1, (x2,y2)::q2 ->
let c = X.compare x1 x2 in
if c = 0 then (x1,(f y1 y2))::(sub f q1 q2)
else if c < 0 then t1::(sub f q1 l2)
else sub f l1 q2
| (l1,_) -> l1
let merge_elem x l1 l2 = merge (fun _ _ -> x) l1 l2
(* TODO: optimize this ? *)
let rec union_disj l1 l2 =
| (t1::q1, t2::q2) ->
let c = X.compare t1 t2 in
if c < 0 then disjoint q1 l2
else if c > 0 then disjoint l1 q2
else false
| _ -> true
let rec cup l1 l2 =
if l1 == l2 then l1 else
match (l1,l2) with
| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
let c = X.compare x1 x2 in