Commit 99542d60 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2002-10-20 19:07:35 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-20 19:08:05+00:00
parent 46cc4f61
......@@ -17,13 +17,18 @@ let rec print_exn ppf = function
| Location ((i,j), exn) ->
Format.fprintf ppf "Error at chars %i-%i@\n" i j;
print_exn ppf exn
| Typer.ShouldHave (t,msg) ->
Format.fprintf ppf "This expression should have type %a@\n%s@\n"
Types.Print.print_descr t
msg
| Typer.Constraint (s,t,msg) ->
Format.fprintf ppf "%s@\n" msg;
Format.fprintf ppf "%a is not a subtype of %a@\n"
Types.Print.print_descr s
Types.Print.print_descr t;
Format.fprintf ppf "as shown by %a@\n"
Types.Print.print_sample (Types.Sample.get (Types.diff s t))
Format.fprintf ppf "This expression should have type %a@\n"
Types.Print.print_descr t;
Format.fprintf ppf "but its infered type is: %a@\n"
Types.Print.print_descr s;
Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n"
Types.Print.print_sample (Types.Sample.get (Types.diff s t));
Format.fprintf ppf "%s@\n" msg
| Typer.NonExhaustive t ->
Format.fprintf ppf "This pattern matching is not exhaustive@\n";
Format.fprintf ppf "Residual type: %a@\n"
......@@ -37,7 +42,7 @@ let phrase ph =
match ph.descr with
| Ast.EvalStatement e ->
let (fv,e) = Typer.expr e in
let t = Typer.compute_type Typer.Env.empty e in
let t = Typer.type_check Typer.Env.empty e Types.any true in
Format.fprintf ppf "%a@\n" Types.Print.print_descr t;
| Ast.TypeDecl _ -> ()
| _ -> assert false
......
......@@ -15,7 +15,7 @@ open Ast
let rec tuple loc = function
| [ x ] -> x
| x :: l -> mk loc (Pair (x, tuple loc l))
| x :: l -> mk (x.loc) (Pair (x, tuple loc l))
| [] -> assert false
let char = mk noloc (Internal (Types.char Chars.any))
......@@ -157,6 +157,8 @@ open Ast
let i = Big_int.big_int_of_string i
and j = Big_int.big_int_of_string j in
mk loc (Internal (Types.interval i j))
| i = char ->
mk loc (Internal (Types.char (Chars.char_class i i)))
| i = char ; "--"; j = char ->
mk loc (Internal (Types.char (Chars.char_class i j)))
| c = const -> mk loc (Internal (Types.constant c))
......
type Content = [(Name Addr Tel?)*];;
type Addrbook = <addrbook>Content;;
type Name = <name>[String];;
type Addr = <addr>[String];;
type Tel = <tel>[String];;
(*
<addrbook>[
<name>["Haruo Hosoya"]
<addr>["Tokyo"]
<name>["Benjamin Pierce"]
<addr>["Philadelphia"]
<tel>["123-456-789"]
<name>["Peter Buneman"]
<addr>["Scotland"]
];;
*)
(* converting an address book into a telephone list *)
(*
fun mkTelList ([ (Name Addr Tel?)* ] -> [ (Name Tel)* ])
| [ <name>n <addr>a <tel>t ; rest] -> [ <name>n <tel>t ; mkTelList rest]
| [ <name>n <addr>a; rest] -> mkTelList rest
| [ ] -> [ ]
;;
fun mkTelList (Addrbook -> [ (Name Tel)* ])
<_>[ ( ( (x::Name) Addr (x::Tel) ) | _ )* ] -> x
;;
*)
(*
fun (Int -> Addrbook) x ->
<addrbook>[
<name>["Haruo Hosoya"]
<addr>["Tokyo"]
<name>["Benjamin Pierce"]
<addr>["Philadelphia"]
<tel>["123-456-789"]
<name>["Peter Buneman"]
<addr>["Scotland"]
]
;;
*)
match <addrbook>[
<name>["Haruo Hosoya"]
<addr>["Tokyo"]
<name>["Benjamin Pierce"]
<addr>["Philadelphia"]
<tel>["123-456-789"]
<name>["Peter Buneman"]
<addr>["Scotland"]
] with
<_>[ ( ( (x::Name) Addr (x::Tel) ) | _ )* ] -> x;;
(*
(* the pattern extract the full sequence of subelements *)
match ex with addrbook:[;a] -> mkTelList a;;
*)
......@@ -706,13 +706,15 @@ test_filter "[ (1 2 3?)* ]" "[ (x::(1 2) 3?)* ]";;
*)
(*
let pat s = Patterns.descr (Syntax.make_pat (Syntax.parse s));;
let typ s = Types.descr (Syntax.make_type (Syntax.parse s));;
let pat s = Patterns.descr (Typer.pat (Parser.From_string.pat s));;
let typ s = Types.descr (Typer.typ (Parser.From_string.pat s));;
let f s = Patterns.NF.nf (pat s);;
let show' t l = Patterns.NF.show Format.std_formatter t (List.map f l);;
let show l = show' Types.any l;;
let showt t l = show' (typ t) l;;
showt " [(`A `B `C?)*] " [" [ (((x::`A) `B (x::`C))|_)* ] "];;
show ["{x=2;y=3}"];;
show [" [((x::1)|(y::2))*] "];;
......
......@@ -382,6 +382,8 @@ struct
let other d = { d with times = empty.times }
let is_product d = is_empty (other d)
let need_second = function _::_::_ -> true | _ -> false
let get d =
let line accu (left,right) =
let rec aux accu d1 d2 = function
......@@ -437,6 +439,7 @@ struct
List.map (!) !res
let any = { empty with times = any.times }
let is_empty d = d = []
end
......@@ -701,6 +704,31 @@ end
module Arrow =
struct
let check_simple left s1 s2 =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
if not (empty_rec accu1') then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if not (empty_rec accu2') then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_strenghten t s =
let left = match t.arrow with [ (p,[]) ] -> p | _ -> assert false in
let rec aux = function
| [] -> raise Not_found
| (p,n) :: rem ->
if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
(List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
{ empty with arrow = [ (SortedList.cup left p, n) ] }
else aux rem
in
aux s.arrow
type t = descr * (descr * descr) list list
let get t =
......@@ -742,7 +770,20 @@ struct
let apply (_,arr) t =
List.fold_left (apply_simple t) empty arr
let need_arg (dom, arr) =
List.exists (function [_] -> false | _ -> true) arr
let apply_noarg (_,arr) =
List.fold_left
(fun accu ->
function
| [(t,s)] -> cup accu s
| _ -> assert false
)
empty arr
let any = { empty with arrow = any.arrow }
let is_empty (_,arr) = arr = []
end
......
......@@ -72,6 +72,7 @@ module Product : sig
(* List of non-empty rectangles *)
type t = (descr * descr) list
val is_empty: t -> bool
val get: descr -> t
val pi1: t -> descr
val pi2: t -> descr
......@@ -82,7 +83,10 @@ module Product : sig
(* List of non-empty rectangles whose first projection
are pair-wise disjunct *)
type normal = t
val normal: descr -> t
val normal: descr -> normal
val need_second: t -> bool
(* Is there more than a single rectangle ? *)
end
module Record : sig
......@@ -110,13 +114,28 @@ end
module Arrow : sig
val any : descr
val check_strenghten: descr -> descr -> descr
(* [check_strenghten t s]
Assume that [t] is an intersection of arrow types
representing the interface of an abstraction;
check that this abstraction has type [s] (otherwise raise Not_found)
and returns a refined type for this abstraction.
*)
type t
val is_empty: t -> bool
val get: descr -> t
(* Always succeed; no check <= Arrow.any *)
val domain: t -> descr
val apply: t -> descr -> descr
(* Always succeed; no check on the domain *)
val need_arg : t -> bool
(* True if the type of the argument is needed to obtain
the type of the result (must use [apply]; otherwise,
[apply_noarg] is enough *)
val apply_noarg : t -> descr
end
......
......@@ -46,6 +46,7 @@ and abstr = {
and branches = {
mutable br_typ : Types.descr;
br_accept : Types.descr;
br_branches: branch list
}
and branch = {
......
......@@ -7,6 +7,7 @@ open Ast
exception Pattern of string
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr * string
exception ShouldHave of Types.descr * string
let raise_loc loc exn = raise (Location (loc,exn))
......@@ -357,15 +358,24 @@ let rec expr { loc = loc; descr = d } =
and branches b =
let fv = ref Fv.empty in
let accept = ref Types.empty in
let b = List.map
(fun (p,e) ->
let (fv2,e) = expr e in
fv := Fv.union !fv fv2;
let p = pat p in
accept := Types.cup !accept (Types.descr (Patterns.accept p));
{ Typed.br_used = false;
Typed.br_pat = pat p;
Typed.br_pat = p;
Typed.br_body = e }
) b in
(!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )
(!fv,
{
Typed.br_typ = Types.empty;
Typed.br_branches = b;
Typed.br_accept = !accept
}
)
module Env = StringMap
......@@ -375,48 +385,68 @@ open Typed
let check loc t s msg =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
let rec compute_type env e =
let d = compute_type' e.exp_loc env e.exp_descr in
let rec type_check env e constr precise =
(* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
Types.Print.print_descr constr precise; *)
let d = type_check' e.exp_loc env e.exp_descr constr precise in
e.exp_typ <- Types.cup e.exp_typ d;
d
and compute_type' loc env = function
| DebugTyper t -> Types.descr t
| Var s -> Env.find s env
| Apply (e1,e2) ->
let t1 = compute_type env e1 and t2 = compute_type env e2 in
if Types.is_empty t2
then Types.empty
else
if Types.subtype t1 Types.Arrow.any
then
let t1 = Types.Arrow.get t1 in
let dom = Types.Arrow.domain t1 in
if Types.subtype t2 dom
then Types.Arrow.apply t1 t2
else
raise_loc loc
(Constraint
(t2,dom,"The argument is not in the domain of the function"))
else
raise_loc loc
(Constraint
(t1,Types.Arrow.any,"The expression in function position is not necessarily a function"))
and type_check' loc env e constr precise = match e with
| Abstraction a ->
let t =
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
raise_loc loc
(ShouldHave
(constr, "but the interface of the abstraction is not compatible"))
in
let env = match a.fun_name with
| None -> env
| Some f -> Env.add f a.fun_typ env in
List.iter (fun (t1,t2) ->
let t = type_branches loc env t1 a.fun_body in
if not (Types.subtype t t2) then
raise_loc loc (Constraint (t,t2,"Constraint not satisfied in interface"))
) a.fun_iface;
a.fun_typ
| Cst c -> Types.constant c
List.iter
(fun (t1,t2) ->
ignore (type_check_branches loc env t1 a.fun_body t2 false)
) a.fun_iface;
t
| Match (e,b) ->
let t = type_check env e b.br_accept true in
type_check_branches loc env t b constr precise
| Pair (e1,e2) ->
let t1 = compute_type env e1 and t2 = compute_type env e2 in
let t1 = Types.cons t1 and t2 = Types.cons t2 in
Types.times t1 t2
let rects = Types.Product.get constr in
if Types.Product.is_empty rects then
raise_loc loc (ShouldHave (constr,"but it is a pair."));
let pi1 = Types.Product.pi1 rects in
let t1 = type_check env e1 (Types.Product.pi1 rects)
(precise || (Types.Product.need_second rects))in
let rects = Types.Product.restrict_1 rects t1 in
let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
if precise then
Types.times (Types.cons t1) (Types.cons t2)
else
constr
| _ ->
let t : Types.descr = compute_type' loc env e in
check loc t constr "";
t
and compute_type env e =
type_check env e Types.any true
and compute_type' loc env = function
| DebugTyper t -> Types.descr t
| Var s -> Env.find s env
| Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in
let t1 = Types.Arrow.get t1 in
let dom = Types.Arrow.domain t1 in
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)
| Cst c -> Types.constant c
| RecordLitt r ->
List.fold_left
(fun accu (l,e) ->
......@@ -427,21 +457,21 @@ and compute_type' loc env = function
| Op (op, el) ->
let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
type_op loc op args
| Match (e,b) ->
let t = compute_type env e in
type_branches loc env t b
| Map (e,b) ->
let t = compute_type env e in
Sequence.map (fun t -> type_branches loc env t b) t
Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
| _ -> assert false
and type_branches loc env targ brs =
and type_check_branches loc env targ brs constr precise =
if Types.is_empty targ then Types.empty
else (
brs.br_typ <- Types.cup brs.br_typ targ;
branches_aux loc env targ Types.empty brs.br_branches
branches_aux loc env targ
(if precise then Types.empty else constr)
constr precise brs.br_branches
)
and branches_aux loc env targ tres = function
and branches_aux loc env targ tres constr precise = function
| [] -> raise_loc loc (NonExhaustive targ)
| b :: rem ->
let p = b.br_pat in
......@@ -449,18 +479,18 @@ and branches_aux loc env targ tres = function
let targ' = Types.cap targ acc in
if Types.is_empty targ'
then branches_aux loc env targ tres rem
then branches_aux loc env targ tres constr precise rem
else
( b.br_used <- true;
let res = Patterns.filter targ' p in
let env' = List.fold_left
(fun env (x,t) -> Env.add x (Types.descr t) env)
env res in
let t = compute_type env' b.br_body in
let tres = Types.cup t tres in
let t = type_check env' b.br_body constr precise in
let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc in
if (Types.non_empty targ'') then
branches_aux loc env targ'' (Types.cup t tres) rem
branches_aux loc env targ'' tres constr precise rem
else
tres
)
......
exception Pattern of string
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr * string
exception ShouldHave of Types.descr * string
val compile_regexp : Ast.regexp -> Ast.ppat -> Ast.ppat
......@@ -15,4 +16,10 @@ module Env : Map.S with type key = string
val expr: Ast.pexpr -> Fv.t * Typed.texpr
val compute_type: Types.descr Env.t -> Typed.texpr -> Types.descr
val type_check:
Types.descr Env.t -> Typed.texpr -> Types.descr -> bool -> Types.descr
(* [compute_type env e t precise] checks that expression [e]
has type [t] under typing environment [env]; if [precise=true],
also returns a possible more precise type for [e].
*)
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