Commit ca94d508 authored by Pietro Abate's avatar Pietro Abate

More work on the typing algorithm

parent 251e2287
......@@ -33,10 +33,6 @@ let xsi_ns = Uri.mk (U.mk "http://www.w3.org/2001/XMLSchema-instance")
module H = Hashtbl.Make(Uri)
module Table = Map.Make(U)
type table = Uri.t Table.t
(* Tables prefix->uri *)
......@@ -230,12 +226,6 @@ module Label = struct
*)
end
let add_prefix pr ns table =
if (U.get_str pr <> "") then Hashtbl.add global_hints ns pr;
Table.add pr ns table
......@@ -302,9 +292,6 @@ let process_start_tag_subst table tag attrs subst_hash =
aux table ((x,U.mk v)::attrs) rest in
aux table [] attrs
module QName = struct
include Custom.Pair(Uri)(U)
let print = InternalPrinter.print_tag
......
......@@ -197,6 +197,7 @@ and parse_branches env l toptype acc btype = function
br_used = br_used;
br_ghost = false;
br_vars_empty = [];
br_vars_poly = [];
br_pat = tpat;
br_body = br_body}
in
......
......@@ -45,15 +45,24 @@ let rec _to_typed env l expr =
let _, _, e2 = _to_typed env l e2 in
let t = Types.times (Types.cons e1.exp_typ) (Types.cons e2.exp_typ) in
env, l, { exp_loc=loc; exp_typ=t; exp_descr=Pair(e1, e2) }
| Op (_, op, e1, e2) ->
let _, _, e1 = _to_typed env l e1 in
let _, _, e2 = _to_typed env l e2 in
env, l, { exp_loc=loc; exp_typ=type_of_string "Int";
exp_descr=Op(op, 0, [e1; e2]) }
| Var (origloc, vname) ->
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
if vname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom));
exp_descr=(Cst (Types.Atom nil_atom)) }
else if vname = "_" then
(Printf.eprintf
"File %s, line %d, characters %d-%d:\nError: Invalid reference to special variable %s\n"
(Loc.file_name origloc) line cbegin cend vname; raise Error)
else
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
let index, vtype =
try Locals.find vname l
with Not_found -> Printf.eprintf
......@@ -90,27 +99,31 @@ let rec _to_typed env l expr =
raise Error
and make_sigma s =
let rec aux acc = function
let rec aux2 acc = function
| (name, ptype) :: rest ->
aux ([`Var (Var.make_id name), type_of_ptype ptype] :: acc) rest
| [] -> acc
in
aux2 (Types.Tallying.CS.E.add (Var.mk name) (type_of_ptype ptype) acc) rest
| [] -> acc in
let rec aux acc = function
| l :: rest -> aux (acc @ [aux2 Types.Tallying.CS.E.empty l]) rest
| [] -> acc in
aux [] s
and type_of_sigma x s =
let rec aux x acc = function
let rec aux2 x acc = function
| [] -> acc
| (id, t2) :: rest when id = x ->
aux x (Types.cup acc (type_of_ptype t2)) rest
| _ :: rest -> aux x acc rest
in
aux2 x (Types.cap acc (type_of_ptype t2)) rest
| _ :: rest -> aux2 x acc rest in
let rec aux x acc = function
| [] -> acc
| l :: rest -> aux x (Types.cup acc (aux2 x Types.any l)) rest in
aux x Types.empty s
and type_of_ptype =
let open Types in function
| Type(t) -> type_of_string t
| PType(t, s) ->
if s = [] then var (`Var (Var.make_id t)) else type_of_sigma t s
if s = [[]] then var (`Var (Var.make_id t)) else type_of_sigma t s
| TPair(t1, t2) -> times (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
| TUnion(t1, t2) -> cup (type_of_ptype t1) (type_of_ptype t2)
| TInter(t1, t2) -> cap (type_of_ptype t1) (type_of_ptype t2)
......@@ -184,6 +197,7 @@ and parse_branches env l toptype acc btype = function
br_used = br_used;
br_ghost = false;
br_vars_empty = [];
br_vars_poly = [];
br_pat = tpat;
br_body = br_body}
in
......@@ -212,14 +226,22 @@ and parse_match_value env l list toptype = function
Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
(list1 @ list2), l, b1 && b2;
| MVar (_, mname, mtype) ->
let lsize = Locals.cardinal l in
let l = Locals.add mname (lsize, type_of_ptype mtype) l in
let list = list @ [lsize, mname] in
let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
let t2 = type_of_ptype mtype in
let d2 = t2, [], Patterns.Constr(t2) in
let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
(t2, Patterns.Cap(d1, d2), list, l, is_subtype)
if mname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
let t = Types.atom (Atoms.atom nil_atom) in
(t, Patterns.Constr(t), list, l, true)
else if mname = "_" then
let t = type_of_ptype mtype in
(t, Patterns.Constr(t), list, l, true)
else
let lsize = Locals.cardinal l in
let l = Locals.add mname (lsize, type_of_ptype mtype) l in
let list = list @ [lsize, mname] in
let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
let t2 = type_of_ptype mtype in
let d2 = t2, [], Patterns.Constr(t2) in
let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
(t2, Patterns.Cap(d1, d2), list, l, is_subtype)
| MInt (_, i) ->
let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
let is_subtype = Types.subtype (type_of_string "Int")
......@@ -231,7 +253,55 @@ and parse_match_value env l list toptype = function
let is_subtype = Types.subtype (type_of_string "String")
(type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
| MBool (origloc, b) ->
let t = match b with
| "true" -> Types.atom (Atoms.atom (Atoms.V.mk_ascii "true"))
| "false" -> Types.atom (Atoms.atom (Atoms.V.mk_ascii "false"))
| _ ->
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
Printf.eprintf
"File %s, line %d, characters %d-%d:\nError: Unknown special term %s\n"
(Loc.file_name origloc) line cbegin cend b;
raise Error in
let is_subtype = Types.subtype t (type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
let arith_op f = function
| Value.Integer(x) :: Value.Integer(y) :: [] ->
Value.Integer(Big_int.big_int_of_int (f (Big_int.int_of_big_int x)
(Big_int.int_of_big_int y)))
| _ -> raise Error
let equal = function
| Value.Integer(x) :: Value.Integer(y) :: [] ->
let b = if Big_int.int_of_big_int x = Big_int.int_of_big_int y then "true"
else "false" in Value.Atom(Atoms.V.mk_ascii b)
| _ -> raise Error
let concat =
let rec add_to_tail y = function
| Value.Pair(x, nil, s) ->
if nil = Value.Atom(Atoms.V.mk_ascii "nil")
then Value.Pair(x, y, s) else Value.Pair(x, add_to_tail y nil, s)
| _ -> raise Error in
function
| (Value.Pair(_, _, _) as x) :: (Value.Pair(_) as y) :: [] ->
add_to_tail y x
| x :: y :: [] ->
if x = Value.Atom(Atoms.V.mk_ascii "nil") then y
else if y = Value.Atom(Atoms.V.mk_ascii "nil") then x
else raise Error
| _ -> raise Error
let to_typed expr =
Eval.register_op "+" (arith_op ( + ));
Eval.register_op "-" (arith_op ( - ));
Eval.register_op "*" (arith_op ( * ));
Eval.register_op "/" (arith_op ( / ));
Eval.register_op "%" (arith_op ( mod ));
Eval.register_op "=" equal;
Eval.register_op "@" concat;
let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
env, expr
......@@ -2,11 +2,12 @@ open Printf
open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Subst of Loc.t * expr * (string * ptype) list list
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * ptype * fv * branches
| Match of Loc.t * expr * ptype * branches
| Pair of Loc.t * expr * expr
| Op of Loc.t * string * expr * expr
| Var of Loc.t * string
| Int of Loc.t * int
| String of Loc.t * string
......@@ -19,9 +20,10 @@ and match_value =
| MVar of Loc.t * string * ptype
| MInt of Loc.t * int
| MString of Loc.t * string
| MBool of Loc.t * string
and ptype =
| Type of string
| PType of string * (string * ptype) list
| PType of string * (string * ptype) list list
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......@@ -52,31 +54,55 @@ module ExprParser = struct
| (loc, pname, ptype) :: rest ->
let t = TArrow(ptype, t) in
let newfv = match fv with | _ :: rest -> rest | [] -> assert false in
aux (Abstr(_loc, x, t, fv, [_loc, MVar(loc, pname, ptype), acc]))
aux (Abstr(_loc, "_", t, fv, [_loc, MVar(loc, pname, ptype), acc]))
t newfv rest
| [] -> acc
in
aux e t (make_fv [] 1 p) (List.rev p)
aux e t (make_fv [0, x] 1 p) (List.rev p)
| "fun"; t = type_id; b = LIST1 branch -> Abstr(_loc, "_", t, [], b)
| "let"; x = LIDENT; ":"; t = type_id; "="; v = SELF; "in"; e = SELF;
":"; te = type_id -> Match(_loc, v, t, [_loc, MVar(_loc, x, t), e])
| "if"; e1 = SELF; "then"; e2 = SELF ->
let b = [(_loc, MBool(_loc, "true"), e2);
(_loc, MBool(_loc, "false"), Var(_loc, "`nil"))] in
Match(_loc, e1, Type("Bool"), b)
| "if"; e1 = SELF; "then"; e2 = SELF; "else"; e3 = SELF ->
let b = [(_loc, MBool(_loc, "true"), e2);
(_loc, MBool(_loc, "false"), e3)] in
Match(_loc, e1, Type("Bool"), b)
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
Match(_loc, e, t, b) ]
| "pair" LEFTA
[ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2)
| e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
| "list" LEFTA [ "["; le = listexpr; "]" -> le ]
| "egal" LEFTA
[ e1 = SELF; "="; e2 = SELF -> Op(_loc, "=", e1, e2) ]
| "add" LEFTA
[ e1 = SELF; "+"; e2 = SELF -> Op(_loc, "+", e1, e2)
| e1 = SELF; "-"; e2 = SELF -> Op(_loc, "-", e1, e2) ]
| "mult" LEFTA
[ e1 = SELF; "*"; e2 = SELF -> Op(_loc, "*", e1, e2)
| e1 = SELF; "/"; e2 = SELF -> Op(_loc, "/", e1, e2)
| e1 = SELF; "%"; e2 = SELF -> Op(_loc, "%", e1, e2) ]
| "concat" LEFTA [ e1 = SELF; "@"; e2 = SELF -> Op(_loc, "@", e1, e2) ]
| "pair" LEFTA [ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2) ]
| "apply" [ e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
| "list" LEFTA
[ "["; le = LIST0 SELF SEP ";"; "]" ->
let rec make_seq res = function
| e :: rest -> make_seq (Pair(_loc, e, res)) rest
| [] -> res in
make_seq (Var(_loc, "`nil")) (List.rev le)
]
| "paren" [ "("; e = SELF; ")" -> e ]
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "int" [ x = INT -> Int(_loc, int_of_string x) ]
| "string" [ x = STRING -> String(_loc, x) ]
| "bool" [ "`"; x = LIDENT -> Bool(_loc, x) ]
| "subst" NONA
[ e = SELF; "{"; s = LIST1 sigma SEP ";"; "}" -> Subst(_loc, e, s) ]
[ e = SELF; "["; s = LIST0 sigma SEP ","; "]" -> Subst(_loc, e, s) ]
];
sigma: [[ x = UIDENT; "/"; t = type_id -> x, t ]];
sigma:[[ "{"; l = LIST0 subst SEP ";"; "}" -> l ]];
listexpr:[ "rec" RIGHTA [ l1=SELF; ";"; l2=SELF -> Pair(_loc, l1, l2) ]
| [ e=expression -> e]];
subst:[[ x = UIDENT; "/"; t = type_id -> x, t ]];
param:[[p = LIDENT; ":"; t = type_id -> _loc, p, t]];
......@@ -92,18 +118,20 @@ module ExprParser = struct
| "var" [ x = LIDENT; ":"; t = type_id -> MVar(_loc, x, t) ]
| "int" [ x = INT -> MInt(_loc, int_of_string x) ]
| "string" [ x = STRING -> MString(_loc, x) ]
| "bool" [ "`"; x = LIDENT -> MBool(_loc, x) ]
| "empty" [ "["; "]" -> MVar(_loc, "`nil", Type("Any")) ]
];
type_id: [ "atom_type"
[ t = UIDENT -> Type(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ "'"; t1 = UIDENT; "["; s = LIST0 sigma SEP ","; "]" -> PType(t1, s) ]
| [ "("; t = complex_type_id; ")" -> t ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]
];
complex_type_id: [ "complex_type" LEFTA
[ t = UIDENT -> Type(t) | "("; t = SELF; ")" -> t ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ "'"; t1 = UIDENT; "["; s = LIST0 sigma SEP ","; "]" -> PType(t1, s) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2) | t1 = SELF; "->"; t2 = SELF -> TArrow(t1, t2) ]
| [ t1 = SELF; "|"; t2 = SELF -> TUnion(t1, t2) | t1 = SELF; "&"; t2 = SELF -> TInter(t1, t2) ]
| [ "!"; t = SELF -> TNot(t) ]
......@@ -122,6 +150,7 @@ let get_loc expr = match expr with
| Abstr (loc, _, _, _, _) -> loc
| Match (loc, _, _, _) -> loc
| Pair (loc, _, _) -> loc
| Op (loc, _, _, _) -> loc
| Var (loc, _) -> loc
| Int (loc, _) -> loc
| String (loc, _) -> loc
......
......@@ -26,12 +26,12 @@ let rec pp_typed ppf e =
pp_typed_aux e
and pp_typedsigma ppf =
let rec aux ppf = function
| (v, t) :: rest -> Format.fprintf ppf "(%a, %a)" Var.dump v Types.Print.print t
| [] -> Format.fprintf ppf "" in
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
in
function
| s :: rest -> Format.fprintf ppf "[%a, %a]" aux s pp_typedsigma rest
| [] -> Format.fprintf ppf ""
| [] -> ()
and pp_typed_aux ppf e =
match e.Typed.exp_descr with
......
......@@ -32,8 +32,6 @@ and node = {
fv : fv
} and descr = Types.t * fv * d
let id x = x.id
let descr x = x.descr
let fv x = x.fv
......
type t = {
fresh : bool;
id : String.t;
id : string;
}
let make_id ?(fresh=false) id =
{ id = id ; fresh = fresh }
......
......@@ -76,7 +76,7 @@ and let_decl = {
and branches = {
mutable br_typ : Types.t; (* Type of values that can flow to branches *)
br_accept : Types.t; (* Type accepted by all branches *)
br_accept : Types.t; (* Type accepted by all branches *)
br_branches: branch list;
}
and branch = {
......@@ -84,7 +84,8 @@ and branch = {
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
mutable br_vars_poly : fv;
br_pat : tpat;
br_body : texpr
br_body : texpr
}
......@@ -50,7 +50,7 @@ type item =
type t = {
ids : item Env.t;
delta : Var.Set.t;
delta : fv;
gamma : Types.Node.t id_map;
ns: Ns.table;
keep_ns: bool
......@@ -107,7 +107,7 @@ let type_schema env loc name uri =
let empty_env = {
ids = Env.empty;
delta = Var.Set.empty; (* set of bounded type variables *)
delta = IdSet.empty; (* set of bounded type variables *)
gamma = IdMap.empty; (* map from expression variables to types *)
ns = Ns.def_table;
keep_ns = false
......@@ -595,12 +595,14 @@ and if_then_else loc cond yes no =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Fv.empty;
Typed.br_pat = pat_true;
Typed.br_body = yes };
{ Typed.br_loc = no.Typed.exp_loc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Fv.empty;
Typed.br_pat = pat_false;
Typed.br_body = no } ];
Typed.br_accept = Builtin_defs.bool;
......@@ -726,6 +728,7 @@ and branches env b =
Typed.br_used = ghost;
Typed.br_ghost = ghost;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Fv.empty;
Typed.br_pat = p;
Typed.br_body = e } in
cur_branch := Branch (br, !cur_branch) :: cur_br;
......@@ -768,6 +771,7 @@ and select_from_where env loc e from where =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Fv.empty;
Typed.br_pat = p;
Typed.br_body = rest } in
cur_branch := [ Branch (br, !cur_branch) ];
......@@ -877,20 +881,18 @@ and type_check' loc env ed constr precise = match ed with
| None -> env
| Some f -> enter_value f a.fun_typ env
in
(* update \delta with all variables in t1 -> t2 *)
(* I check the body with all possible t1 -> t2 types *)
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));
let su = type_check_branches loc env t1 a.fun_body t2 false in
let sigma = (* Tallying. su t2 *) [] in
(* p_j : t_j -> e^j_i sigma_{H_i} *)
()
(*
List.iter (fun br ->
br.br_body.exp_descr <- Subst(br.br_body,sigma)
) a.fun_body.br_branches
*)
let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then
raise_loc loc (NonExhaustive (Types.diff t1 acc));
let t = type_check_branches loc env t1 a.fun_body t2 false in
let sigma = Types.abstr t t2 in (* H_j *)
List.iter (fun br ->
br.br_body.exp_descr <- Subst(br.br_body,sigma);
) a.fun_body.br_branches
) a.fun_iface;
(ed,t)
......@@ -1083,6 +1085,7 @@ and type_record loc env r constr precise =
if precise then Types.record_fields (false, res)
else constr
(* i \in I , \forall j \in J \cup s^i_j *)
and type_check_branches loc env targ brs constr precise =
if Types.is_empty targ then Types.empty
else begin
......@@ -1103,19 +1106,22 @@ and branches_aux loc env targ tres constr precise = function
branches_aux loc env targ tres constr precise rem
else begin
b.br_used <- true;
let res = Patterns.filter targ' p in (* t_i // p_i *)
(* update gamma *)
let res = Patterns.filter targ' p in (* t^i_j // p_j *)
(* update gamma \Gamma, t^i_j // p_j*)
let env = { env with gamma = IdMap.merge (fun _ v2 -> v2) env.gamma res } in
let res = IdMap.map Types.descr res in
b.br_vars_empty <-
IdMap.domain (
IdMap.filter (fun x t -> Types.subtype t Sequence.nil_type)
IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
(IdMap.restrict res b.br_vars_empty));
(* update delta *)
let env' = enter_values (IdMap.get res) env in
let xj = IdMap.domain (IdMap.restrict env'.gamma env'.delta) in (* Xi_j *)
(* all poly variables associated with the pattern p_j that are not in \Delta *)
b.br_vars_poly <- xj;
let t = type_check env' b.br_body constr precise in (* s_i^j *)
let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc 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