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

Add lifting mechanism for sigma in lambda abstractions

parent 8d294687
......@@ -214,12 +214,17 @@ and compile_abstr env a =
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let rec lift = function
|Sel(Env i, iface, s) -> Sel(Env (i+nb_slots),iface,lift s)
|Comp(s1,s2) -> Comp(lift s1,lift s2)
|s -> s
in
if is_mono then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack))
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)
let sigma = Sel(Env 1,a.Typed.fun_iface,lift(env.sigma)) in
PolyAbstraction(slots, a.Typed.fun_iface, body, !(env.max_stack), sigma)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
......
......@@ -37,8 +37,8 @@ type expr =
| TVar of (var_loc * sigma)
| Apply of expr * expr
| 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 *)
| PolyAbstraction of var_loc array * iface * branches * int * sigma
(* environment, interface, branches, size of locals, sigma *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
......@@ -37,8 +37,8 @@ type expr =
| TVar of (var_loc * sigma)
| Apply of expr * expr
| 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 *)
| PolyAbstraction of var_loc array * iface * branches * int * sigma
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
......@@ -172,7 +172,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
| PolyAbstraction (slots,iface,body,lsize,sigma,x) ->
| PolyAbstraction (slots,iface,body,lsize,sigma) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
| Abstraction (slots,iface,body,lsize) ->
......
......@@ -237,8 +237,8 @@ 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
| 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
| PolyAbstraction (va, l, b, i, sigma) ->
Format.fprintf ppf "PolyAbstraction(%a,,,,%a)" pp_vloc_array va pp_lambda_sigma sigma
| Abstraction (va, l, b, i) ->
Format.fprintf ppf "Abstraction(%a,,,,)" pp_vloc_array va
| Check(_) -> Format.fprintf ppf "Check"
......
......@@ -41,36 +41,55 @@ module BIN = struct
types
end
let run_test_typer msg expected totest =
let parse_expr s =
let astexpr = Parser.expr (Stream.of_string s) in
let texpr = fst (Typer.type_expr BIN.env astexpr) in
Format.printf "Cduce Typed -> %s%!@." (Printer.typed_to_string texpr);
texpr
in
let parse_typed s =
try
let expr = Parse.ExprParser.of_string_no_file s in
let env, texpr = Compute.to_typed expr in
Format.printf "Expected Typed -> %s%!@." (Printer.typed_to_string texpr);
texpr
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 _ ->
let expected = (parse_typed expected) in
let totest = (parse_expr totest) in
assert_equal ~msg:msg ~printer:(fun x -> Printer.typed_to_string x) expected totest
let wrap f s =
try f s
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
let parse_cduce s =
let astexpr = Parser.expr (Stream.of_string s) in
let texpr = fst (Typer.type_expr BIN.env astexpr) in
Format.printf "Cduce Typed %s ====> \n %s\n%!@." s (Printer.typed_to_string texpr);
texpr
let parse_texpr s =
let expr = Parse.ExprParser.of_string_no_file s in
let env, texpr = Compute.to_typed expr in
Format.printf "Computed Typed %s ====> \n %s\n%!@." s (Printer.typed_to_string texpr);
texpr
let parse_lexpr f s =
let texpr = wrap f s in
let lambdaexpr,lsize = Compile.compile_expr Compile.empty_toplevel texpr in
Format.printf "Lambda : %s\n" (Printer.lambda_to_string lambdaexpr);
lambdaexpr, lsize
let parse_vexpr f s =
let lambdaexpr,lsize = parse_lexpr f s in
let evalexpr = Eval.expr lambdaexpr lsize in
Format.printf "Value : %s\n" (Printer.value_to_string evalexpr);
evalexpr
let run_test_typer msg expected totest _ =
let expected = wrap parse_texpr expected in
let totest = wrap parse_cduce totest in
assert_equal ~msg:msg ~printer:(fun x -> Printer.typed_to_string x) expected totest
let run_test_compile msg expected totest _ =
let expected,_ = parse_lexpr parse_texpr expected in
let totest,_ = parse_lexpr parse_cduce totest in
assert_equal ~msg:msg ~printer:(fun x -> Printer.lambda_to_string x) expected totest
(* (message, typed expr - expected, cduce expr) *)
let tests_typer_list = [
(*
"Test CDuce.typed.fun.const",
"fun f x : Int : Int -> x",
"fun f (Int -> Int) x&Int -> x";
......@@ -90,11 +109,10 @@ let tests_typer_list = [
"Test CDuce.typed.fun.partial 1",
"fun f x : 'A : 'A -> 2",
"fun f ( `$A -> `$A -> `$A) x -> fun g -> g x";
*)
"Test CDuce.typed.fun.partial 2",
"fun f x : 'A : 'A -> 2",
"fun f ( `$A -> `$A -> `$A) g -> fun (`$A -> `$A) x -> g x";
"fun f ( g : `$A -> `$B ) ( x : `$A) : `$B = g x";
]
......@@ -104,11 +122,18 @@ let tests_typer = "CDuce type tests (Ast -> Typed)" >:::
msg >:: run_test_typer msg expected cduce
) tests_typer_list
let tests_compile = "CDuce compile tests (Ast -> Typed -> Lambda)" >:::
List.map (fun (msg,expected,cduce) ->
msg >:: run_test_compile msg expected cduce
) tests_typer_list
let _ =
run_test_tt_main (
test_list
[
tests_typer
tests_typer;
tests_compile;
]
)
;;
......
......@@ -23,7 +23,6 @@ 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";
......@@ -36,8 +35,6 @@ let tests_poly_abstr = [
"",
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
*)
"Test CDuce.runtime.misc.partial",
"",
"fun applier x : 'A f : ('A -> 'A) : 'A -> f.x";
......
......@@ -3212,6 +3212,7 @@ module Tallying = struct
exception Step1Fail
exception Step2Fail
(* XXX add delta here !!! *)
let tallying l =
let n = List.fold_left (fun acc (s,t) ->
let d = diff s t in
......@@ -3324,3 +3325,11 @@ let abstr s t =
let e1 = Tallying.CS.E.filter (fun v _ -> Var.Set.mem v delta) e in
e1 :: acc
) [] sl
(** square subtype *)
let subsqtype s t (sigma,delta) =
List.exists (fun si ->
let si =Tallying.CS.E.filter (fun v _ -> Var.Set.mem v delta) si in
subtype Tallying.(s @@ si) t
) sigma
......@@ -428,6 +428,7 @@ module Tallying : sig
end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
(** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
......@@ -435,5 +436,8 @@ val apply_full : t -> t -> t
and res is the type of the result of the application
*)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(** tallying sigma s < t *)
val abstr : t -> t -> Tallying.CS.sl
val subsqtype : t -> t -> (Tallying.CS.sl * Var.Set.t) -> bool
......@@ -822,7 +822,10 @@ let require loc t s =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
let verify loc t s =
require loc t s; t
Format.printf "VERIFY %a < %a\n" Types.Print.print t Types.Print.print s;
require loc t s;
Format.printf "VERIFY TRUE \n";
t
let verify_noloc t s =
if not (Types.subtype t s) then raise (Constraint (t, s));
......
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