Commit 45b4e0aa authored by Pietro Abate's avatar Pietro Abate
Browse files

WIP

parent 17335b8d
......@@ -72,6 +72,10 @@ let fresharg =
(0,U.mk s)
;;
let comp = function
|Identity,s | s,Identity -> s
|s1,s2 -> Comp(s1,s2)
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
(* Typed -> Lambda *)
let rec compile env e = compile_aux env e.Typed.exp_descr
......@@ -90,7 +94,7 @@ and compile_aux env = function
in
if Var.Set.is_empty polyvars 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) -> compile { env with sigma = comp(env.sigma,(List sl)) } 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
......@@ -137,13 +141,27 @@ 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
(* we add a nameless empty slot for the argument *)
let argvar = fresharg () in
let argloc = Env 1 in
let fun_env = Env.add argvar argloc fun_env in
let polyvars =
let vs =
List.fold_left (fun acc (t1,t2) ->
let ts1 = Types.all_vars t1 in
let ts2 = Types.all_vars t2 in
(Var.Set.union acc (Var.Set.union ts1 ts2))
) Var.Set.empty a.Typed.fun_iface
in
Var.Set.inter (domain(env.sigma)) vs
in
let (slots,nb_slots,fun_env) =
(* we add a nameless empty slot for the argument *)
if not(Var.Set.is_empty polyvars) then
let argvar = fresharg () in
([Dummy;Dummy],2,Env.add argvar (Env 1) fun_env)
else ([Dummy],1,fun_env)
in
let (slots,nb_slots,fun_env) =
(* here deburin indexes are reshuffled *)
(* here De Bruijn indexes are reshuffled *)
List.fold_left
(fun (slots,nb_slots,fun_env) x ->
match find x env with
......@@ -157,7 +175,7 @@ and compile_abstr env a =
Env.add x p fun_env
| Dummy -> assert false
)
([Dummy;Dummy],2,fun_env) (IdSet.get a.Typed.fun_fv)
(slots,nb_slots,fun_env) (IdSet.get a.Typed.fun_fv)
in
let slots = Array.of_list (List.rev slots) in
......@@ -168,19 +186,12 @@ and compile_abstr env a =
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let sigma = Sel(argloc,a.Typed.fun_iface,env.sigma) in
let polyvars =
let vs =
List.fold_left (fun acc (t1,t2) ->
let ts1 = Types.all_vars t1 in
let ts2 = Types.all_vars t2 in
(Var.Set.union acc (Var.Set.union ts1 ts2))
) Var.Set.empty a.Typed.fun_iface
in
Var.Set.inter (domain(env.sigma)) vs
in
let flag = Var.Set.is_empty polyvars in
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), flag, sigma, argloc)
if Var.Set.is_empty polyvars then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack))
else
let sigma = Sel(Env 1,a.Typed.fun_iface,env.sigma) in
PolyAbstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), sigma, Env 1)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
......@@ -348,7 +359,6 @@ let comp_unit ?(run=false)
let (tenv,cenv,codes) = phrases ~run ~show ~directive (tenv,cenv,[]) phs in
(tenv,cenv,List.rev codes)
let compile_eval_expr env e =
let e,lsize = compile_expr env e in
Eval.expr e lsize
......@@ -36,7 +36,8 @@ type expr =
| Var of var_loc
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * iface * branches * int * bool * sigma * var_loc
| Abstraction of var_loc array * iface * branches * int
| PolyAbstraction of var_loc array * iface * branches * int * sigma * var_loc
(* environment, interface, branches, size of locals, sigma, x *)
| Check of expr * Auto_pat.state
| Const of Value.t
......
......@@ -36,7 +36,8 @@ type expr =
| Var of var_loc
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * iface * branches * int * bool * sigma * var_loc
| Abstraction of var_loc array * iface * branches * int
| PolyAbstraction of var_loc array * iface * branches * int * sigma * var_loc
(* environment, interface, branches, size of locals *)
| Check of expr * Auto_pat.state
| Const of Value.t
......
......@@ -63,6 +63,18 @@ let eval_var env locals = function
let tag_op_resolved = Obj.tag (Obj.repr (OpResolved ((fun _ -> assert false), [])))
let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
let pp_lambda_env ppf env locals =
let aux a =
let l = Array.to_list a in
let sl = List.mapi (fun i v ->
Format.fprintf Format.str_formatter "%d : %a@." i Value.print v;
Format.flush_str_formatter ()
) l
in
String.concat "," sl
in
Format.fprintf ppf "env = {%s}; locals = {%s}" (aux env) (aux locals)
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'))
......@@ -94,9 +106,11 @@ 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,x) ->
| PolyAbstraction (slots,iface,body,lsize,sigma,x) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
| Abstraction (slots,iface,body,lsize) ->
eval_abstraction env locals slots iface body lsize Value.Identity
| Const c -> c
| Pair (e1,e2) ->
let v1 = eval env locals e1 in
......@@ -140,26 +154,31 @@ let rec eval env locals = function
and eval_check env locals e d =
Explain.do_check env d (eval env locals e)
and eval_apply f arg = match f with
| Value.Abstraction (_,f,_) -> f arg
| _ -> assert false
and eval_abstraction env locals slots iface body lsize sigma =
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 f arg =
let v = eval_branches env (Array.create lsize Value.Absent) body arg in
if sigma <> Value.Identity then env.(1) <- arg;
pp_lambda_env Format.std_formatter env locals;
v
in
let a = Value.Abstraction (Some iface,f,sigma) in
env.(0) <- a;
a
and eval_apply f arg = match f with
| Value.Abstraction (_,f,_) -> f arg
| _ -> assert false
and eval_branches env locals brs arg =
let (code, bindings) = Run_dispatch.run_dispatcher env brs.brs_disp arg in
match brs.brs_rhs.(code) with
| Auto_pat.Match (n,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
match brs.brs_rhs.(code) with
| Auto_pat.Match (n,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 =
Value.mk_ref (Types.descr t) (eval env locals e)
......
......@@ -227,8 +227,7 @@ and inzero env v t =
| _ -> true
let rec run_dispatcher env 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; *)
match d.actions with
| AIgnore r -> make_result_basic v r
| AKind k -> run_disp_kind env k v
......@@ -244,14 +243,15 @@ and run_disp_kind env actions v =
| String_utf8 (i,j,s,q) -> run_disp_string_utf8 env 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)
| Integer i ->
run_disp_basic v (fun t -> Types.Int.has_int t i) actions.basic
| Integer i -> run_disp_basic v (fun t -> Types.Int.has_int t i) actions.basic
| Abstraction (None,_,_) ->
run_disp_basic v (fun t -> failwith "Run-time inspection of external abstraction")
actions.basic
| Abstraction (Some iface,_,sigma) ->
| Abstraction (Some iface,_,Value.Identity) ->
run_disp_basic v (fun t -> Types.Arrow.check_iface iface t)
actions.basic
| Abstraction (Some iface,_,sigma) ->
run_disp_basic v (fun t -> inzero env v t) actions.basic
| Abstract (abs,_) ->
run_disp_basic v (fun t -> Types.Abstract.contains abs (Types.get_abstract t))
actions.basic
......
......@@ -265,6 +265,30 @@ let rec is_str = function
| Concat (_,_) as v -> eval_lazy_concat v; is_str v
| _ -> false
let rec pp_sigma ppf =
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
in
match l with
|[] -> Format.fprintf ppf ""
|_ -> Format.fprintf ppf "%a" aux l
in
let pp_aux ppf =
print_lst (fun ppf (t1,t2) ->
Format.fprintf ppf "(%a -> %a)"
Types.Print.print t1
Types.Print.print t2
) ppf
in
function
|List ll -> Types.Tallying.CS.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
let rec print ppf v =
if is_str v then
(Format.fprintf ppf "\"";
......@@ -272,9 +296,9 @@ let rec print ppf v =
Format.fprintf ppf "\"")
else if is_seq v then Format.fprintf ppf "[ @[<hv>%a@]]" print_seq v
else match v with
| Pair (x,y,sigma) -> Format.fprintf ppf "(%a,%a)" print x print y
| Xml (x,y,z,sigma) | XmlNs (x,y,z,_,sigma) -> print_xml ppf x y z
| Record (l,sigma) -> Format.fprintf ppf "@[{%a }@]" print_record (Imap.elements l)
| Pair (x,y,sigma) -> Format.fprintf ppf "(%a,%a,%a)" print x print y pp_sigma sigma
| Xml (x,y,z,sigma) | XmlNs (x,y,z,_,sigma) -> print_xml ppf x y z (* sigma *)
| Record (l,sigma) -> Format.fprintf ppf "@[{%a },%a@]" print_record (Imap.elements l) pp_sigma sigma
| Atom a -> Atoms.V.print_quote ppf a
| Integer i -> Intervals.V.print ppf i
| Char c -> Chars.V.print ppf c
......@@ -298,7 +322,7 @@ let rec print ppf v =
| Absent ->
Format.fprintf ppf "<[absent]>"
and print_quoted_str ppf = function
| Pair (Char c, q,sigma) ->
| Pair (Char c, q,_) ->
Chars.V.print_in_string ppf c;
print_quoted_str ppf q
| String_latin1 (i,j,s, q) ->
......@@ -405,13 +429,14 @@ let dump_xml ppf v =
Format.fprintf ppf "@[<hv1>";
Format.fprintf ppf "<value>@,%a@,</value>@]" aux v
(* XXX here I don't compare sigmas !!! *)
let rec compare x y =
if (x == y) then 0
else
match (x,y) with
| Pair (x1,x2,sigma1), Pair (y1,y2,sigma2) ->
let c = compare x1 y1 in if c <> 0 then c
else compare x2 y2
else compare x2 y2
| (Xml (x1,x2,x3,sigmax1) | XmlNs (x1,x2,x3,_,sigmax1)),
(Xml (y1,y2,y3,sigmay2) | XmlNs(y1,y2,y3,_,sigmay2)) ->
let c = compare x1 y1 in if c <> 0 then c
......
open Value
let print_to_string f x =
let b = Buffer.create 1024 in
let ppf = Format.formatter_of_buffer b in
f ppf x;
Format.pp_print_flush ppf ();
Buffer.contents b
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
......@@ -229,12 +236,12 @@ and pp_lambda ppf =
| 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,x) ->
| PolyAbstraction (va, l, b, i, 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
| Abstraction (va, l, b, i) ->
Format.fprintf ppf "Abstraction(%a,,,,)" pp_vloc_array va
| Check(_) -> Format.fprintf ppf "Check"
| Const(v) -> Format.fprintf ppf "Const(%a)" pp_value v
| Const(v) -> Format.fprintf ppf "Const(%a)" Value.print v
| Pair(e1, e2) -> Format.fprintf ppf "Pair(%a, %a)" pp_lambda e1 pp_lambda e2
| String(_) -> Format.fprintf ppf "String"
| Match(e, brs) -> Format.fprintf ppf "Match(%a, %a)" pp_lambda e pp_lbranches brs
......@@ -247,15 +254,8 @@ and pp_lbranches ppf brs =
and pp_patrhs ppf arr =
Array.iter (function | Auto_pat.Match(i, e) -> Format.fprintf ppf "(%d, %a)" i pp_lambda e | _ -> ()) arr
let print_to_string f x =
let b = Buffer.create 1024 in
let ppf = Format.formatter_of_buffer b in
f ppf x;
Format.pp_print_flush ppf ();
Buffer.contents b
let typed_to_string = print_to_string pp_typed
let print_env = Format.printf "%a" pp_env
let print_value = Format.printf "%a" pp_value
let value_to_string = print_to_string pp_value
let print_value = Format.printf "%a" Value.print
let value_to_string = print_to_string Value.print
let lambda_to_string = print_to_string pp_lambda
......@@ -7,7 +7,7 @@ let run_test_compile msg expected totest =
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);
Format.printf "Computed Typed %s -> %s%!@." str (Printer.typed_to_string texpr);
let lambdaexpr = Compile.compile env texpr in
Printer.lambda_to_string lambdaexpr
with
......@@ -23,24 +23,38 @@ let run_test_compile msg expected totest =
fun _ -> assert_equal ~msg:msg ~printer:(fun x -> x) expected (aux totest)
let tests_poly_abstr = [
(*
"Test CDuce.lambda.const_abstr failed",
"",
"fun f x : 'A : 'A -> 2";
"Test CDuce.lambda.identity",
"",
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
"Test CDuce.lambda.let",
"",
"let x : Int = 3 in x : Int";
*)
"Test CDuce.lambda.identity",
"",
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
(*
"Test CDuce.lambda.apply",
"",
"(fun f x : Int : Int -> x).2";
"Test CDuce.lambda.applier",
"",
"fun applier x : Int f : (Int->Int) : Int -> f.x";
"Test CDuce.runtime.misc.applier_applied failed",
"",
"((fun applier x : Int f : (Int->Int) : Int -> f.x).2).(fun g x : Int : Int -> x)";
"Test CDuce.lambda.applier poly",
"",
"fun applier x : 'A f : ('A -> Int) : Int -> f.x";
*)
];;
let tests_compile = "CDuce compile tests (Typed -> Lambda )" >:::
......@@ -52,8 +66,10 @@ let run_test_eval msg expected totest =
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
Format.printf "Computed Typed %s -> %s%!@." str (Printer.typed_to_string texpr);
let lambdaexpr,lsize = Compile.compile_expr env texpr in
Format.printf "Lambda : %s\n" (Printer.lambda_to_string lambdaexpr);
let evalexpr = Eval.expr lambdaexpr lsize in
Printer.value_to_string evalexpr
with
| Compute.Error -> exit 3
......@@ -73,7 +89,7 @@ let tests_eval = "CDuce evaluation tests (Typed -> Lambda -> Value )" >:::
let _ =
run_test_tt_main (
test_list
[ tests_compile;
[ (* tests_compile; *)
tests_eval
]
)
......
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