Commit 180e9317 authored by Pietro Abate's avatar Pietro Abate

More work on delayed evaluation

parent 54af7c3b
......@@ -3,7 +3,7 @@ open Lambda
type env = {
cu: Compunit.t option; (* None: toplevel *)
vars: var_loc Env.t;
vars: var_loc Env.t; (* Id.t to var_loc *)
sigma : sigma; (* symbolic substitutions (Lambda.sigma) *)
gamma : Types.Node.t IdMap.map; (* map of type variables to types *)
stack_size: int;
......@@ -59,10 +59,18 @@ let enter_global_cu cu env x =
global_size = env.global_size + 1 }
let rec domain = function
|Identity -> []
|Identity -> Var.Set.empty
|List l -> Types.Tallying.domain l
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Sel(_,sigma) -> (domain sigma)
|Sel(_,_,sigma) -> (domain sigma)
let fresharg =
let count = ref 0 in
function () ->
let s = Printf.sprintf "__ARG%d" !count in
incr count;
(0,U.mk s)
;;
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
(* Typed -> Lambda *)
......@@ -130,9 +138,12 @@ and compile_abstr env a =
| None -> Env.empty, []
in
(* we add a nameless empty slot for the argument *)
let fun_env = Env.add (0,U.mk "") (Env 1) fun_env in
let argvar = fresharg () in
let argloc = Env 1 in
let fun_env = Env.add argvar argloc fun_env in
let (slots,nb_slots,fun_env) =
(* here deburin indexes are reshuffled *)
List.fold_left
(fun (slots,nb_slots,fun_env) x ->
match find x env with
......@@ -157,7 +168,7 @@ and compile_abstr env a =
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let sigma = Sel(List.map snd a.Typed.fun_iface,env.sigma) in
let sigma = Sel(argloc,a.Typed.fun_iface,env.sigma) in
let polyvars =
let vs =
List.fold_left (fun acc (t1,t2) ->
......@@ -168,10 +179,8 @@ and compile_abstr env a =
in
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)
else
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
let flag = Var.Set.is_empty polyvars in
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), flag, sigma, argloc)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
......
......@@ -22,20 +22,22 @@ type var_loc =
(* Only for the toplevel *)
| Dummy
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
type iface = (Types.descr * Types.descr) list
type sigma =
| Identity
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (Types.t list * sigma)
| Sel of (var_loc * iface * sigma)
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
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
(* environment, interface, branches, size of locals *)
| Abstraction of var_loc array * iface * branches * int * bool * sigma * var_loc
(* environment, interface, branches, size of locals, sigma, x *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
......@@ -22,19 +22,21 @@ type var_loc =
(* Only for the toplevel *)
| Dummy
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
let iface = (Types.t * Types.t) list
type sigma =
| Identity
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (Types.t list * sigma)
| Sel of (var_loc * iface * sigma)
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
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
| Abstraction of var_loc array * iface * branches * int * bool * sigma * var_loc
(* 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(sI,f,sigma') -> Value.Abstraction(sI,f,Value.Comp(sigma,sigma'))
|Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,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'))
......@@ -76,19 +76,16 @@ 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(sI,sigma) -> Value.Sel(sI,eval_sigma env locals sigma)
|Lambda.Sel(x,iface,sigma) -> Value.Sel(1,iface,eval_sigma env locals sigma)
(* env is an array implementing de bruines indexes *)
(* Evaluation rules : Lamda -> Value *)
(* Evaluation rules : Lambda -> Value *)
let rec eval env locals = function
| Var ((Global _ | Ext _ | External _ | Builtin _) as x) as e ->
let v = eval_var env locals x in
Obj.set_field (Obj.repr e) 0 (Obj.repr v);
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 *)
| Var x -> eval_var env locals x
| TVar (x,sigma) -> (* delayed sigma application *)
let sigma' = eval_sigma env locals sigma in
......@@ -97,7 +94,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) ->
| Abstraction (slots,iface,body,lsize,flag,sigma,x) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
| Const c -> c
......@@ -141,13 +138,13 @@ let rec eval env locals = function
| Check (e,d) -> eval_check env locals e d
and eval_check env locals e d =
Explain.do_check d (eval env locals e)
Explain.do_check env d (eval env locals e)
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 env = Array.map (eval_var env locals) slots in
let f arg = eval_branches env (Array.create lsize Value.Absent) body arg in
let a = Value.Abstraction (Some iface,f,sigma) in
clousure.(0) <- a;
env.(0) <- a;
a
and eval_apply f arg = match f with
......@@ -155,13 +152,13 @@ and eval_apply f arg = match f with
| _ -> 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
let (code, bindings) = Run_dispatch.run_dispatcher env brs.brs_disp arg in
match brs.brs_rhs.(code) with
| Auto_pat.Match (n,e) ->
Array.blit bindings 0 locals brs.brs_stack_pos n;
eval env locals e
(* copy n elements from bindings into locals starting
* from position brs.brs_stack_pos *)
Array.blit bindings 0 locals brs.brs_stack_pos n;
eval env locals e
| Auto_pat.Fail -> Value.Absent
and eval_ref env locals e t =
......@@ -271,7 +268,8 @@ let eval_toplevel = function
| Eval (e,lsize) -> ignore (expr e lsize)
| LetDecls (e,lsize,disp,n) ->
let v = expr e lsize in
let (_, bindings) = Run_dispatch.run_dispatcher disp v in
(* XXX Env.empty ??? *)
let (_, bindings) = Run_dispatch.run_dispatcher Env.empty disp v in
ensure globs (!nglobs + n);
Array.blit bindings 0 !globs !nglobs n;
nglobs := !nglobs + n
......@@ -294,7 +292,8 @@ let eval_unit globs nglobs = function
| Eval (e,lsize) -> ignore (expr e lsize)
| LetDecls (e,lsize,disp,n) ->
let v = expr e lsize in
let (_, bindings) = Run_dispatch.run_dispatcher disp v in
(* XXX Env.empty ??? *)
let (_, bindings) = Run_dispatch.run_dispatcher Env.empty disp v in
Array.blit bindings 0 globs !nglobs n;
nglobs := !nglobs + n
| LetDecl (e,lsize) ->
......
......@@ -18,7 +18,4 @@ val eval_var: var_loc -> t
val eval_unit: Value.t array -> code_item list -> unit
val eval_apply: Value.t -> Value.t -> Value.t
......@@ -125,25 +125,25 @@ let rec simplify = function
| x :: l -> (try [ x; List.find is_xml l ] with Not_found -> [ x ])
| [] -> assert false
let check d v =
let check env d v =
if (d.fail_code < 0) then ()
else
let (code,_) = Run_dispatch.run_dispatcher d v in
let (code,_) = Run_dispatch.run_dispatcher env d v in
if code == d.fail_code then (ignore (run_disp [] d v); assert false)
let explain d v =
try check d v; None
let explain env d v =
try check env d v; None
with Failed p -> Some p
let do_check d v =
try check d v; v
let do_check env d v =
try check env d v; v
with Failed p ->
let p = simplify p in
let s = print_to_string print p in
raise (CDuceExn (string_latin1 s))
let check_failure d v =
try check d v; v
let check_failure env d v =
try check env d v; v
with Failed p ->
let p = simplify p in
let s = print_to_string print p in
......
This diff is collapsed.
open Ident
open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (Types.t list * sigma)
| Sel of (int * iface * sigma)
| Identity
and t =
......
open Ident
open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (Types.t list * sigma)
| Sel of (int * iface * sigma)
| Identity
and t =
......
......@@ -22,8 +22,8 @@ INEXTFILES = misc/custom.ml misc/encodings.ml misc/upool.ml misc/ns.ml\
EXTFILES = $(INEXTFILES:%=$(ROOTDIR)/%)
RM ?= rm -f
OUT ?= lambdaTests.native typedTests.native
OUTDEBUG ?= lambdaTests.byte typedTests.byte
OUT ?= valueTests.native lambdaTests.native typedTests.native
OUTDEBUG ?= valueTests.native lambdaTests.byte typedTests.byte
.PHONY: clean _import tests
......
open OUnit2
open Camlp4.PreCast
(* Typed -> Lamda *)
(* Typed -> Lambda *)
let run_test_compile msg expected totest =
let aux str =
try
let expr = Parse.ExprParser.of_string_no_file str in
let env, texpr = Compute.to_typed expr in
Format.printf "Compted Typed -> %s%!@." (Printer.typed_to_string texpr);
let lambdaexpr = Compile.compile env texpr in
Printer.lambda_to_string lambdaexpr
with
......@@ -63,6 +64,12 @@ Int
]
let tests_poly_abstr = [
"Test CDuce.lambda.const_abstr failed",
"Abstraction(Dummy,,,,Sel((Int -> Int),{}))",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2";
];;
let tests_compile = "CDuce compile tests (Typed -> Lambda )" >:::
List.map (fun (m,e,f) -> f >:: run_test_compile m e f) tests_poly_abstr
......@@ -463,7 +470,7 @@ let _ =
run_test_tt_main (
test_list
[ tests_compile;
tests_eval
(* tests_eval *)
]
)
;;
......@@ -4,7 +4,7 @@ let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a" f h
|h::t -> Format.fprintf ppf "%a ,%a" f h aux t
|h::t -> Format.fprintf ppf "%a,%a" f h aux t
in
match l with
|[] -> Format.fprintf ppf ""
......@@ -27,10 +27,10 @@ let rec pp_typed ppf e =
and pp_typedsigma ppf =
let rec aux ppf s = Types.Tallying.CS.E.iter
(fun k v -> Format.fprintf ppf "(%a, %a)" Var.dump k Types.Print.print v) s
(fun k v -> Format.fprintf ppf "(%a,%a)" Var.print k Types.Print.print v) s
in
function
| s :: rest -> Format.fprintf ppf "[%a, %a]" aux s pp_typedsigma rest
| s :: rest -> Format.fprintf ppf "[%a,%a]" aux s pp_typedsigma rest
| [] -> ()
and pp_typed_aux ppf e =
......@@ -66,7 +66,7 @@ and pp_typed_aux ppf e =
| _ -> assert false
and pp_abst ppf abstr =
Format.fprintf ppf "%a,\niface:[%a],\nbody:[%a], typ:%a, fv:[%a]"
Format.fprintf ppf "%a,\niface:[%a],\nbody:[%a],typ:%a,fv:[%a]"
pp_fun_name abstr.Typed.fun_name
pp_iface abstr.Typed.fun_iface
pp_branches abstr.Typed.fun_body
......@@ -75,14 +75,14 @@ and pp_abst ppf abstr =
and pp_fun_name ppf = function
|Some (id, name) ->
Format.fprintf ppf "name:(%s, %s)"
Format.fprintf ppf "name:(%s,%s)"
(string_of_int (Upool.int id))
(Encodings.Utf8.to_string name)
|None -> Format.fprintf ppf "name:<none>"
and pp_iface ppf l =
let f ppf (t1,t2) =
Format.fprintf ppf "(%a, %a)"
Format.fprintf ppf "(%a,%a)"
Types.Print.print t1
Types.Print.print t2
in
......@@ -143,7 +143,7 @@ and pp_pattern ppf = function
*)
and pp_v ppf (id, name) =
Format.fprintf ppf "(%d, %s)" (Upool.int id) (Encodings.Utf8.to_string 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
......@@ -160,7 +160,7 @@ let pp_vloc_array ppf a =
print_lst pp_vloc ppf (Array.to_list a)
let pp_binding ppf (id, name) value =
Format.fprintf ppf "((%d, %s),%a)\n"
Format.fprintf ppf "((%d,%s),%a)\n"
(Upool.int id)
(Encodings.Utf8.to_string name)
pp_vloc value
......@@ -180,12 +180,12 @@ 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_v x pp_aux tl pp_sigma s
|Value.Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Value.Identity -> Format.fprintf ppf "Id"
and pp_value ppf = function
| Value.Pair(v1, v2, sigma) ->
Format.fprintf ppf "(%a, %a, %a)"
Format.fprintf ppf "(%a,%a,%a)"
pp_value v1
pp_value v2
pp_sigma sigma
......@@ -221,15 +221,18 @@ 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_v x pp_aux tl pp_lambda_sigma s
|Lambda.Sel(x,iface,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_vloc x pp_aux iface pp_lambda_sigma s
|Lambda.Identity -> Format.fprintf ppf "Id"
and pp_lambda ppf =
let open Lambda in function
| Var v -> Format.fprintf ppf "Var(%a)" pp_vloc v
| TVar (v,sigma) -> Format.fprintf ppf "TVar(%a,%a)" pp_vloc v pp_lambda_sigma sigma
| Apply (e1,e2) -> Format.fprintf ppf "Apply(%a,%a)" pp_lambda e1 pp_lambda e2
| Abstraction (va, l, b, i, true, sigma) -> Format.fprintf ppf "PolyAbstraction(%a,,,,%a)" pp_vloc_array va pp_sigma sigma
| Abstraction (va, l, b, i, false, sigma) -> Format.fprintf ppf "Abstraction(%a,,,,%a)" pp_vloc_array va pp_sigma sigma
| Abstraction (va, l, b, i, true, sigma,x) ->
Format.fprintf ppf "PolyAbstraction(%a,,,,%a,%a)" pp_vloc_array va pp_lambda_sigma sigma pp_vloc x
| Abstraction (va, l, b, i, false, sigma,x) ->
Format.fprintf ppf "Abstraction(%a,,,,%a,%a)" pp_vloc_array va pp_lambda_sigma sigma pp_vloc x
| Check(_) -> Format.fprintf ppf "Check"
| Const(v) -> Format.fprintf ppf "Const(%a)" pp_value v
| Pair(e1, e2) -> Format.fprintf ppf "Pair(%a, %a)" pp_lambda e1 pp_lambda e2
......
......@@ -74,14 +74,19 @@ let tests_typer_list = [
"Test CDuce.typed.fun.const",
"fun f x : Int : Int -> x",
"fun f (Int -> Int) x&Int -> x";
"Test CDuce.typed.fun.identity",
"fun f x : 'A[{}] : 'A[{}] -> x",
"fun f (`$A -> `$A) x -> x";
"Test CDuce.typed.fun.identity.int",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2",
"fun f (`$A -> `$A) x -> x";
"Test CDuce.typed.fun.match",
"fun f x : ('A[{}] | Int) : ('A[{}] | Int) -> x",
"fun f (`$A -> `$A) x & Int -> x | x -> x";
]
let tests_typer = "CDuce type tests (Ast -> Typed)" >:::
......
open OUnit2
open Camlp4.PreCast
(* Typed -> Lambda *)
let run_test_compile msg expected totest =
let aux str =
try
let expr = Parse.ExprParser.of_string_no_file str in
let env, texpr = Compute.to_typed expr in
Format.printf "Compted Typed -> %s%!@." (Printer.typed_to_string texpr);
let lambdaexpr = Compile.compile env texpr in
Printer.lambda_to_string lambdaexpr
with
| Compute.Error -> exit 3
| Loc.Exc_located (loc, exn) ->
let l = Loc.start_line loc in
let cbegin = Loc.start_off loc - Loc.start_bol loc in
let cend = Loc.stop_off loc - Loc.start_bol loc in
Printf.eprintf "File %s, line %d, characters %d-%d:\n" (Loc.file_name loc) l
cbegin cend; raise exn
| e -> Printf.eprintf "Runtime error.\n"; raise e
in
fun _ -> assert_equal ~msg:msg ~printer:(fun x -> x) expected (aux totest)
let tests_poly_abstr = [
"Test CDuce.lambda.const_abstr failed",
"Abstraction(Dummy,,,,Sel((Int -> Int),{}))",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2";
];;
let tests_compile = "CDuce compile tests (Typed -> Lambda )" >:::
List.map (fun (m,e,f) -> f >:: run_test_compile m e f) tests_poly_abstr
(* Typed -> Lambda -> Value *)
let run_test_eval msg expected totest =
let aux str =
try
let expr = Parse.ExprParser.of_string_no_file str in
let env, texpr = Compute.to_typed expr in
Format.printf "Compted Typed -> %s%!@." (Printer.typed_to_string texpr);
let evalexpr = Compile.compile_eval_expr env texpr in
Printer.value_to_string evalexpr
with
| Compute.Error -> exit 3
| Loc.Exc_located (loc, exn) ->
let l = Loc.start_line loc in
let cbegin = Loc.start_off loc - Loc.start_bol loc in
let cend = Loc.stop_off loc - Loc.start_bol loc in
Printf.eprintf "File %s, line %d, characters %d-%d:\n" (Loc.file_name loc) l
cbegin cend; raise exn
| e -> Printf.eprintf "Runtime error.\n"; raise e
in
fun _ -> assert_equal ~msg:msg ~printer:(fun x -> x) expected (aux totest)
let tests_eval = "CDuce evaluation tests (Typed -> Lambda -> Value )" >:::
List.map (fun (m,e,f) -> f >:: run_test_eval m e f) tests_poly_abstr
let _ =
run_test_tt_main (
test_list
[ tests_compile;
tests_eval
]
)
;;
......@@ -370,6 +370,11 @@ x=(1,2)
| Cup ((a1,_,_) as p1,p2) ->
approx_var seen p2 (Types.diff t a1)
(approx_var seen p1 (Types.cap t a1) xs)
| Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
IdSet.cup
(approx_var seen p1 t (IdSet.cap fv1 xs))
(approx_var seen p2 t (IdSet.cap fv2 xs))
(*
| Cap ((_,fv1,d1) as p1,((_,fv2,d2) as p2)) ->
(match d1 with
| Capture(_, name) when Str.string_match (Str.regexp "pat[0-9]+:") name 0 ->
......@@ -377,6 +382,7 @@ x=(1,2)
| _ -> IdSet.cup
(approx_var seen p1 t (IdSet.cap fv1 xs))
(approx_var seen p2 t (IdSet.cap fv2 xs)))
*)
| Capture _ ->
xs
| Constant (_,c) ->
......
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