Commit 2c10a6aa authored by Pietro Abate's avatar Pietro Abate

More work on the Typer

Remove sigma annotations from pairs in lambda
parent e7a14bb5
......@@ -73,7 +73,11 @@ and compile_aux env = function
| Typed.Var x -> Var (find x env)
| Typed.TVar x ->
let v = find x env in
let polyvars = Var.Set.inter (domain(env.sigma)) (Types.all_vars(Types.descr (IdMap.assoc x env.gamma))) in
let polyvars =
Var.Set.inter
(domain(env.sigma))
(Types.all_vars(Types.descr (IdMap.assoc x env.gamma)))
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
......
......@@ -193,11 +193,10 @@ let norm_tests () = [
"(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
];
(*
"(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
"(`$A -> `$B) -> [ `$A ] -> [ `$B ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$Gamma", mk_s [
[P(V "A","Empty")]
];
*)
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
......@@ -307,7 +306,8 @@ let tallying_tests = [
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
(* map even *)
[("(`$A -> `$B) -> [`$A] -> [`$B]","(Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int))")], [[]];
[("(`$A -> `$B) -> [`$A* ] -> [`$B* ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
[("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e []
]
let test_tallying =
......
......@@ -298,11 +298,12 @@ let memo_filter = ref MemoFilter.empty
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
(* TODO: avoid is_empty t when t is not changing (Cap) *)
if Types.is_empty t
then empty_res fv
if Types.is_empty t then empty_res fv
else
match d with
| Constr _ -> IdMap.empty
| Constr t0 ->
if Types.subtype t t0 then IdMap.empty
else (empty_res fv) (* omega *)
| Cup ((a,_,_) as d1,d2) ->
IdMap.merge cup_res
(filter_descr (Types.cap t a) d1)
......@@ -330,7 +331,6 @@ and filter_prod ?kind fv p1 p2 t =
(empty_res fv)
(Types.Product.normal ?kind t)
and filter_node t p : Types.Positive.v id_map =
try MemoFilter.find (t,p) !memo_filter
with Not_found ->
......@@ -345,12 +345,12 @@ let filter t p =
let r = filter_node t p in
memo_filter := MemoFilter.empty;
IdMap.map Types.Positive.solve r
let filter_descr t p =
let r = filter_descr t p in
memo_filter := MemoFilter.empty;
IdMap.get (IdMap.map Types.Positive.solve r)
(* Factorization of capture variables and constant patterns *)
module Factorize = struct
......
......@@ -36,7 +36,6 @@ end
val accept : node -> Types.Node.t
val filter : Types.t -> node -> Types.Node.t id_map
(* Pattern matching: compilation *)
module Compile: sig
......@@ -44,5 +43,3 @@ module Compile: sig
val make_branches : Types.t -> (node * 'a) list -> state * 'a rhs array
val make_checker : Types.t -> Types.t -> state
end
......@@ -193,7 +193,7 @@ module TLV = struct
let print ppf x = if x.b then Set.print ";" ppf x.s
let dump ppf x =
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
x.b Var.Set.dump x.f (Set.print ";") x.s
x.b Var.Set.print x.f (Set.print ";") x.s
let mem v x = Set.mem v x.s
end
......
......@@ -50,6 +50,8 @@ type item =
type t = {
ids : item Env.t;
delta : Var.Set.t;
gamma : Var.var Env.t;
ns: Ns.table;
keep_ns: bool
}
......@@ -105,6 +107,8 @@ let type_schema env loc name uri =
let empty_env = {
ids = Env.empty;
delta = Var.Set.empty; (* set of bounded type variables *)
gamma = Env.empty; (* map from expression variables to types *)
ns = Ns.def_table;
keep_ns = false
}
......@@ -478,7 +482,7 @@ type branch = Branch of Typed.branch * branch list
let cur_branch : branch list ref = ref []
let exp' loc e =
{ Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e; }
{ Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e }
let exp loc fv e = fv, exp' loc e
......@@ -725,7 +729,8 @@ and branches env b =
let x = Ident.to_string x in
warning br_loc
("The capture variable " ^ x ^
" is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
" is declared in the pattern but not used in the body of this branch." ^
" It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
let fv2 = Fv.diff fv2 fvp in
fv := Fv.cup !fv fv2;
accept := Types.cup !accept (Types.descr (Patterns.accept p));
......@@ -818,10 +823,10 @@ let let_decl env p e =
open Typed
let localize loc f x =
try f x
with
| (Error _ | Constraint (_,_)) as exn -> raise (Cduce_loc.Location (loc,`Full,exn))
| Warning (s,t) -> warning loc s; t
try f x with
| (Error _ | Constraint (_,_)) as exn ->
raise (Cduce_loc.Location (loc,`Full,exn))
| Warning (s,t) -> warning loc s; t
let require loc t s =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
......@@ -857,116 +862,124 @@ let flatten arg constr precise =
let rec type_check env e constr precise =
let d = type_check' e.exp_loc env e.exp_descr constr precise in
let (ed,d) = type_check' e.exp_loc env e.exp_descr constr precise in
let d = if precise then d else constr in
e.exp_typ <- Types.cup e.exp_typ d;
e.exp_descr <- ed;
d
and type_check' loc env e constr precise = match e with
and type_check' loc env ed constr precise = match ed with
| Forget (e,t) ->
let t = Types.descr t in
ignore (type_check env e t false);
verify loc t constr
(ed,verify loc t constr)
(* TODO: Fix this branch *)
| Subst (e, sigma) -> type_check env e constr precise
| Subst (e, sigma) -> (ed,type_check env e constr precise)
| Check (t0,e,t) ->
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
verify loc (Types.cap te (Types.descr t)) constr
(ed,verify loc (Types.cap te (Types.descr t)) constr)
| Abstraction a ->
let t =
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
should_have loc constr
"but the interface of the abstraction is not compatible"
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
should_have loc constr
"but the interface of the abstraction is not compatible"
in
let env = match a.fun_name with
| None -> env
| Some f -> enter_value f a.fun_typ env in
List.iter
(fun (t1,t2) ->
let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then
raise_loc loc (NonExhaustive (Types.diff t1 acc));
ignore (type_check_branches loc env t1 a.fun_body t2 false)
| None -> env
| Some f -> enter_value f a.fun_typ env
in
List.iter (fun (t1,t2) ->
let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then
raise_loc loc (NonExhaustive (Types.diff t1 acc));
ignore (type_check_branches loc env t1 a.fun_body t2 false)
) a.fun_iface;
t
(Subst(exp' noloc (Abstraction a),[]),t)
| Match (e,b) ->
let t = type_check env e b.br_accept true in
type_check_branches loc env t b constr precise
(Match(e,b),type_check_branches loc env t b constr precise)
| Try (e,b) ->
let te = type_check env e constr precise in
let tb = type_check_branches loc env Types.any b constr precise in
Types.cup te tb
(ed,Types.cup te tb)
| Pair (e1,e2) ->
type_check_pair loc env e1 e2 constr precise
(ed,type_check_pair loc env e1 e2 constr precise)
| Xml (e1,e2,_) ->
type_check_pair ~kind:`XML loc env e1 e2 constr precise
(ed,type_check_pair ~kind:`XML loc env e1 e2 constr precise)
| RecordLitt r ->
type_record loc env r constr precise
(ed,type_record loc env r constr precise)
| Map (e,b) ->
type_map loc env false e b constr precise
(ed,type_map loc env false e b constr precise)
| Transform (e,b) ->
localize loc (flatten (type_map loc env true e b) constr) precise
(ed,localize loc (flatten (type_map loc env true e b) constr) precise)
| Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in
let t1 = Types.Arrow.get t1 in
let t1_t = type_check env e1 Types.Arrow.any true in
let t1 = Types.Arrow.get t1_t in
let dom = Types.Arrow.domain t1 in
let res =
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
else
(ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
in
verify loc res constr
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
let sigma = Types.apply t1_t t2 in
let t = Types.Arrow.apply t1 t2 in
let e1 = exp' noloc (Subst(e1,sigma)) in
let e2 = exp' noloc (Subst(e2,sigma)) in
(Apply(e1,e2),verify loc t constr)
else begin
ignore (type_check env e2 dom false);
let t = Types.Arrow.apply_noarg t1 in
(Apply(e1,e2),verify loc t constr)
end
| Var s ->
verify loc (find_value s env) constr
(ed,verify loc (find_value s env) constr)
| TVar s ->
verify loc (find_value s env) constr
(ed,verify loc (find_value s env) constr)
| ExtVar (cu,s,t) ->
verify loc t constr
(ed,verify loc t constr)
| Cst c ->
verify loc (Types.constant c) constr
(ed,verify loc (Types.constant c) constr)
| String (i,j,s,e) ->
type_check_string loc env 0 s i j e constr precise
(ed,type_check_string loc env 0 s i j e constr precise)
| Dot (e,l) ->
let expect_rec = Types.record l (Types.cons constr) in
let expect_elt =
Types.xml
Types.any_node
(Types.cons (Types.times (Types.cons expect_rec) Types.any_node)) in
(Types.cons (Types.times (Types.cons expect_rec) Types.any_node))
in
let t = type_check env e (Types.cup expect_rec expect_elt) precise in
let t_elt =
let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
let t = Types.Product.pi1 (Types.Product.get t) in
t in
if not precise then constr
else
(try Types.Record.project (Types.cup t t_elt) l
with Not_found -> assert false)
let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
let t = Types.Product.pi1 (Types.Product.get t)
in t
in
let t' =
if not precise then constr else
(try Types.Record.project (Types.cup t t_elt) l
with Not_found -> assert false)
in (ed,t')
| RemoveField (e,l) ->
let t = type_check env e Types.Record.any true in
let t = Types.Record.remove_field t l in
verify loc t constr
(ed,verify loc t constr)
| Xtrans (e,b) ->
let t = type_check env e Sequence.any true in
......@@ -992,24 +1005,24 @@ and type_check' loc env e constr precise = match e with
raise (Cduce_loc.Location (loc,precise,exn))
with Not_found ->
raise_loc loc exn
in
verify loc t constr
in
(ed,verify loc t constr)
| Validate (e, t, _) ->
ignore (type_check env e Types.any false);
verify loc t constr
(ed,verify loc t constr)
| Ref (e,t) ->
ignore (type_check env e (Types.descr t) false);
verify loc (Builtin_defs.ref_type t) constr
(ed,verify loc (Builtin_defs.ref_type t) constr)
| External (t,_) ->
verify loc t constr
(ed,verify loc t constr)
| Op (op,_,args) ->
let args = List.map (type_check env) args in
let t = localize loc (typ_op op args constr) precise in
verify loc t constr
(ed,verify loc t constr)
| NsTable (ns,e) ->
type_check' loc env e constr precise
......@@ -1097,10 +1110,10 @@ and branches_aux loc env targ tres constr precise = function
let acc = Types.descr (Patterns.accept p) in
let targ' = Types.cap targ acc in
if Types.is_empty targ'
then branches_aux loc env targ tres constr precise rem
else
( b.br_used <- true;
if Types.is_empty targ' then
branches_aux loc env targ tres constr precise rem
else begin
b.br_used <- true;
let res = Patterns.filter targ' p in
let res = IdMap.map Types.descr res in
......@@ -1117,7 +1130,7 @@ and branches_aux loc env targ tres constr precise = function
branches_aux loc env targ'' tres constr precise rem
else
tres
)
end
and type_map loc env def e b constr precise =
let acc = if def then Sequence.any else Sequence.star b.br_accept in
......
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