Commit 70043fc7 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add a runtime check to fail pattern-matching on polymorphic arrows.

parent 99357a17
Pipeline #158 failed with stages
in 36 seconds
......@@ -52,7 +52,7 @@ let load_xml_html mimetype open_cb close_cb text_cb txt =
in
loop (Js.Opt.return (root :> Dom.node Js.t))
let get_fun = function Value.Abstraction (_, f) -> f | _ -> assert false
let get_fun = function Value.Abstraction (_, f, _) -> f | _ -> assert false
let load_url async url cb_ok cb_err =
let xhr = XmlHttpRequest.create () in
......
......@@ -122,7 +122,7 @@ and compile_abstr env a =
let slots = Array.of_list (List.rev slots) in
let env = { env with vars = fun_env; stack_size = 0; max_stack = ref 0 } in
let body = compile_branches env a.Typed.fun_body in
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack))
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), a.Typed.fun_is_poly)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been
......
......@@ -26,7 +26,7 @@ type var_loc =
type expr =
| Var of { loc : var_loc ; mutable value : Value.t }
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool
(* environment, interface, branches, size of locals *)
| Check of expr * Auto_pat.state
| Const of Value.t
......
......@@ -26,8 +26,8 @@ type var_loc =
type expr =
| Var of { loc : var_loc ; mutable value : Value.t }
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int
(* environment, interface, branches, size of locals *)
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool
(* environment, interface, branches, size of locals, is_poly *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
......@@ -32,17 +32,22 @@ let register_cst op t v =
(function [] -> v | _ -> assert false)
let register_fun op dom codom eval =
register_cst op
(Types.arrow (Types.cons dom) (Types.cons codom))
(Value.Abstraction (Some [ (dom, codom) ], eval))
let t = Types.arrow (Types.cons dom) (Types.cons codom) in
register_cst op t
(Value.Abstraction
(Some [ (dom, codom) ], eval, not (Var.Set.is_empty (Types.Subst.vars t))))
let register_fun2 op dom1 dom2 codom eval =
let t2 = Types.arrow (Types.cons dom2) (Types.cons codom) in
let iface2 = Some [ (dom2, codom) ] in
register_cst op
(Types.arrow (Types.cons dom1) (Types.cons t2))
let t = Types.arrow (Types.cons dom1) (Types.cons t2) in
let poly = not (Var.Set.is_empty (Types.Subst.vars t)) in
let poly2 = not (Var.Set.is_empty (Types.Subst.vars t2)) in
register_cst op t
(Value.Abstraction
(Some [ (dom1, t2) ], fun v1 -> Value.Abstraction (iface2, eval v1)))
( Some [ (dom1, t2) ],
(fun v1 -> Value.Abstraction (iface2, eval v1, poly)),
poly2 ))
let register_fun3 op dom1 dom2 dom3 codom eval =
let t3 = Types.arrow (Types.cons dom3) (Types.cons codom) in
......@@ -51,12 +56,18 @@ let register_fun3 op dom1 dom2 dom3 codom eval =
let iface3 = Some [ (dom3, codom) ] in
let iface2 = Some [ (dom2, t3) ] in
let iface1 = Some [ (dom1, t2) ] in
let poly1 = not (Var.Set.is_empty (Types.Subst.vars t1)) in
let poly2 = not (Var.Set.is_empty (Types.Subst.vars t2)) in
let poly3 = not (Var.Set.is_empty (Types.Subst.vars t3)) in
register_cst op t1
(Value.Abstraction
( iface1,
fun x1 ->
(fun x1 ->
Value.Abstraction
(iface2, fun x2 -> Value.Abstraction (iface3, eval x1 x2)) ))
( iface2,
(fun x2 -> Value.Abstraction (iface3, eval x1 x2, poly3)),
poly2 )),
poly1 ))
let register_op op ?(expect = Types.any) typ eval =
register_unary op
......
......@@ -77,8 +77,8 @@ 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) ->
eval_abstraction env locals slots iface body lsize
| Abstraction (slots,iface,body,lsize, is_poly) ->
eval_abstraction env locals slots iface body lsize is_poly
| Const c -> c
| Pair (e1,e2) ->
let v1 = eval env locals e1 in
......@@ -117,17 +117,17 @@ let rec eval env locals = function
and eval_check env locals e d =
Explain.do_check d (eval env locals e)
and eval_abstraction env locals slots iface body lsize =
and eval_abstraction env locals slots iface body lsize is_poly=
let local_env = Array.map (eval_var env locals) slots in
let f arg =
eval_branches local_env (Array.make lsize Value.Absent) body arg
in
let a = Value.Abstraction (Some iface,f) in
let a = Value.Abstraction (Some iface,f,is_poly) in
local_env.(0) <- a;
a
and eval_apply f arg = match f with
| Value.Abstraction (_,f) -> f arg
| Value.Abstraction (_,f, _) -> f arg
| _ -> assert false
and eval_branches env locals brs arg =
......
......@@ -3,17 +3,14 @@ open Ident
open Auto_pat
open Encodings
type t = (Value.t * string) list
let rec print ppf = function
| [] -> ()
| [] -> ()
| (v, t) :: l ->
print ppf l;
Format.fprintf ppf
"Value @[%a@] does not match type @[%s@]@."
Value.print v
t
Format.fprintf ppf "Value @[%a@] does not match type @[%s@]@." Value.print
v t
let print_to_string f x =
let b = Buffer.create 1024 in
......@@ -22,130 +19,139 @@ let print_to_string f x =
Format.pp_print_flush ppf ();
Buffer.contents b
let to_string e =
print_to_string print e
let to_string e = print_to_string print e
exception Failed of t
let make_result pt d (code,_,_) =
let make_result pt d (code, _, _) =
if d.fail_code == code then raise (Failed pt);
code
let rec run_disp_basic pt d f = function
| [(_,r)] -> make_result pt d r
| (t,r)::rem ->
if f t then make_result pt d r
else run_disp_basic pt d f rem
| _ -> assert false
let rec run_disp_basic pt d f = function
| [ (_, r) ] -> make_result pt d r
| (t, r) :: rem ->
if f t then make_result pt d r else run_disp_basic pt d f rem
| _ -> assert false
let rec run_dispatcher pt d v =
let rec run_dispatcher pt d v =
match d.actions with
| AIgnore r -> make_result pt d r
| AKind k -> run_disp_kind pt d k v
| AIgnore r -> make_result pt d r
| AKind k -> run_disp_kind pt d k v
and run_disp pt d v =
run_dispatcher ((v, d.expected_type)::pt) d v
and run_disp pt d v = run_dispatcher ((v, d.expected_type) :: pt) d v
and run_disp_kind pt d actions = function
| Pair { fst=v1; snd=v2; concat=false } -> run_disp_prod pt d v1 v2 actions.prod
| Xml (v1,v2,v3) | XmlNs (v1,v2,v3,_) -> run_disp_prod pt d v1 (pair v2 v3) actions.xml
| Pair { fst = v1; snd = v2; concat = false } ->
run_disp_prod pt d v1 v2 actions.prod
| Xml (v1, v2, v3) | XmlNs (v1, v2, v3, _) ->
run_disp_prod pt d v1 (pair v2 v3) actions.xml
| Record r -> run_disp_record pt d 0 r actions.record
| Atom q -> make_result pt d (AtomSet.get_map q actions.atoms)
| Char c -> make_result pt d (CharSet.get_map c actions.chars)
| Atom q -> make_result pt d (AtomSet.get_map q actions.atoms)
| Char c -> make_result pt d (CharSet.get_map c actions.chars)
| Integer i ->
run_disp_basic pt d (fun t -> Intervals.contains i (Types.Int.get t)) actions.basic
| Abstraction (None,_) ->
run_disp_basic pt d
(fun t -> failwith "Run-time inspection of external abstraction")
(fun t -> Intervals.contains i (Types.Int.get t))
actions.basic
| Abstraction (None, _, _) ->
run_disp_basic pt d
(fun t -> failwith "Run-time inspection of external abstraction")
actions.basic
| Abstraction (Some iface,_) ->
run_disp_basic pt d (fun t -> Types.Arrow.check_iface iface t)
| Abstraction (Some iface, _, is_poly) ->
run_disp_basic pt d
(fun t ->
if is_poly && not Types.(subtype Function.any t) then
failwith "Run-time inspection of polymorphic function"
else Types.Arrow.check_iface iface t)
actions.basic
| Absent ->
run_disp_basic pt d (fun t -> Types.Record.has_absent t) actions.basic
| v ->
run_disp_kind pt d actions (normalize v)
| v -> run_disp_kind pt d actions (normalize v)
and run_disp_prod pt d v1 v2 = function
| Impossible -> assert false
| TailCall d1 -> run_disp pt d1 v1
| Ignore d2 -> run_disp_prod2 pt d v2 d2
| Dispatch (d1,b1) ->
| Impossible -> assert false
| TailCall d1 -> run_disp pt d1 v1
| Ignore d2 -> run_disp_prod2 pt d v2 d2
| Dispatch (d1, b1) ->
let code1 = run_disp pt d1 v1 in
run_disp_prod2 pt d v2 b1.(code1)
and run_disp_prod2 pt d v2 = function
| Impossible -> assert false
| Ignore r -> make_result pt d r
| TailCall d2 -> run_disp pt d2 v2
| Dispatch (d2,b2) ->
| Impossible -> assert false
| Ignore r -> make_result pt d r
| TailCall d2 -> run_disp pt d2 v2
| Dispatch (d2, b2) ->
let code2 = run_disp pt d2 v2 in
make_result pt d b2.(code2)
and run_disp_record pt d n fields = function
| None -> assert false
| Some (RecLabel (l,r)) ->
| Some (RecLabel (l, r)) -> (
(* TODO: get rid of this exception... *)
(try run_disp_record1 pt d l (succ n)
(Imap.find fields (Upool.int l)) fields r
with Not_found ->
run_disp_record1 pt d l n Absent fields r)
| Some (RecNolabel (some,none)) ->
let r = if (n < Imap.cardinal fields) then some else none in
match r with
| Some r -> make_result pt d r
| None -> assert false
try
run_disp_record1 pt d l (succ n)
(Imap.find fields (Upool.int l))
fields r
with Not_found -> run_disp_record1 pt d l n Absent fields r)
| Some (RecNolabel (some, none)) -> (
let r = if n < Imap.cardinal fields then some else none in
match r with Some r -> make_result pt d r | None -> assert false)
and run_disp_record1 pt d l n v1 rem = function
| Impossible -> assert false
| TailCall d1 -> run_disp pt d1 v1
| Ignore d2 -> run_disp_record2 pt d n rem d2
| Dispatch (d1,b1) ->
| Impossible -> assert false
| TailCall d1 -> run_disp pt d1 v1
| Ignore d2 -> run_disp_record2 pt d n rem d2
| Dispatch (d1, b1) ->
let code1 = run_disp pt d1 v1 in
run_disp_record2 pt d n rem b1.(code1)
and run_disp_record2 pt d n rem = function
| Impossible -> assert false
| Ignore r -> make_result pt d r
| TailCall d2 -> run_disp_record_loop pt n rem d2
| Dispatch (d2,b2) ->
| Impossible -> assert false
| Ignore r -> make_result pt d r
| TailCall d2 -> run_disp_record_loop pt n rem d2
| Dispatch (d2, b2) ->
let code2 = run_disp_record_loop pt n rem d2 in
make_result pt d b2.(code2)
and run_disp_record_loop pt n rem d =
match d.actions with
| AIgnore r -> make_result pt d r
| AKind k -> run_disp_record pt d n rem k.record
| AIgnore r -> make_result pt d r
| AKind k -> run_disp_record pt d n rem k.record
let is_xml = function ((Xml _ | XmlNs _),_) -> true | _ -> false
let is_xml = function (Xml _ | XmlNs _), _ -> true | _ -> false
let rec simplify = function
| (Absent, _) :: l -> simplify l
| x :: l -> (try [ x; List.find is_xml l ] with Not_found -> [ x ])
| [] -> assert false
| x :: l -> ( try [ x; List.find is_xml l ] with Not_found -> [ x ])
| [] -> assert false
let check d v =
if (d.fail_code < 0) then ()
if d.fail_code < 0 then ()
else
let (code,_) = Run_dispatch.run_dispatcher d v in
if code == d.fail_code then (ignore (run_disp [] d v); assert false)
let code, _ = Run_dispatch.run_dispatcher d v in
if code == d.fail_code then (
ignore (run_disp [] d v);
assert false)
let explain d v =
try check d v; None
try
check d v;
None
with Failed p -> Some p
let do_check d v =
try check d v; v
try
check d v;
v
with Failed p ->
let p = simplify p in
let s = print_to_string print p in
raise (CDuceExn (string_latin1 s))
let check_failure d v =
try check d v; v
try
check d v;
v
with Failed p ->
let p = simplify p in
let s = print_to_string print p in
failwith s
......@@ -17,6 +17,7 @@ open Auto_pat
open Encodings
let buffer = ref (Array.make 127 Absent)
let cursor = ref 0
let blit a1 ofs1 a2 ofs2 len =
......@@ -25,304 +26,321 @@ let blit a1 ofs1 a2 ofs2 len =
done
(* important to do this in the increasing order ... *)
let ensure_room n =
let l = Array.length !buffer in
if !cursor + n > l then
let buffer' = Array.make (l * 2 + n) Absent in
if !cursor + n > l then (
let buffer' = Array.make ((l * 2) + n) Absent in
blit !buffer 0 buffer' 0 !cursor;
buffer := buffer'
buffer := buffer')
let push v =
ensure_room 1;
!buffer.(!cursor) <- v;
incr cursor
let make_result_prod v1 v2 v (code,r,pop) =
let make_result_prod v1 v2 v (code, r, pop) =
let n = Array.length r in
if n > 0 then (
ensure_room n;
let buf = !buffer in
let c = !cursor in
for a = 0 to n - 1 do
let x = match Array.unsafe_get r a with
| Catch -> v
| Const c -> const c
| Nil -> nil
| Left -> v1
| Right -> v2
| Stack i -> buf.(c - i)
| Recompose (i,j) ->
pair
(match i with (-1) -> v1 | (-2) -> nil | _ -> buf.(c - i))
(match j with (-1) -> v2 | (-2) -> nil | _ -> buf.(c - j))
in
buf.(c + a) <- x
done;
if pop != 0 then blit buf c buf (c - pop) n);
cursor := !cursor - pop + n; (* clean space for GC ? *)
ensure_room n;
let buf = !buffer in
let c = !cursor in
for a = 0 to n - 1 do
let x =
match Array.unsafe_get r a with
| Catch -> v
| Const c -> const c
| Nil -> nil
| Left -> v1
| Right -> v2
| Stack i -> buf.(c - i)
| Recompose (i, j) ->
pair
(match i with -1 -> v1 | -2 -> nil | _ -> buf.(c - i))
(match j with -1 -> v2 | -2 -> nil | _ -> buf.(c - j))
in
buf.(c + a) <- x
done;
if pop != 0 then blit buf c buf (c - pop) n);
cursor := !cursor - pop + n;
(* clean space for GC ? *)
code
let make_result_basic v (code,r,_) =
let make_result_basic v (code, r, _) =
let n = Array.length r in
if n > 0 then (
ensure_room n;
let buf = !buffer in
for a = 0 to n - 1 do
let x = match Array.unsafe_get r a with
| Catch -> v
| Const c -> const c
| _ -> assert false
in
buf.(!cursor) <- x;
incr cursor
done);
ensure_room n;
let buf = !buffer in
for a = 0 to n - 1 do
let x =
match Array.unsafe_get r a with
| Catch -> v
| Const c -> const c
| _ -> assert false
in
buf.(!cursor) <- x;
incr cursor
done);
code
let make_result_char ch (code,r,_) =
let make_result_char ch (code, r, _) =
let n = Array.length r in
if n > 0 then (
ensure_room n;
let buf = !buffer in
for a = 0 to n - 1 do
let x = match Array.unsafe_get r a with
| Catch -> Char ch
| Const c -> const c
| _ -> assert false
in
buf.(!cursor + a) <- x
done;
cursor := !cursor + n);
ensure_room n;
let buf = !buffer in
for a = 0 to n - 1 do
let x =
match Array.unsafe_get r a with
| Catch -> Char ch
| Const c -> const c
| _ -> assert false
in
buf.(!cursor + a) <- x
done;
cursor := !cursor + n);
code
let tail_string_latin1 i j s q =
if i + 1 == j then q else String_latin1 {i=i + 1;j;str=s;tl=q}
if i + 1 == j then q else String_latin1 { i = i + 1; j; str = s; tl = q }
let make_result_string_latin1 i j s q (code,r,pop) =
let make_result_string_latin1 i j s q (code, r, pop) =
let n = Array.length r in
if n > 0 then (
ensure_room n;
let c = !cursor in
let buf = !buffer in
for a = 0 to n - 1 do
let x = match Array.unsafe_get r a with
| Catch -> String_latin1 {i;j;str=s;tl=q}
| Const c -> const c
| Nil -> nil
| Left -> Char (CharSet.V.mk_char s.[i])
| Right -> tail_string_latin1 i j s q
| Stack n -> buf.(c - n)
| Recompose (n,m) ->
pair
(match n with
| (-1) -> Char (CharSet.V.mk_char s.[i])
| (-2) -> nil
| _ -> buf.(c - n))
(match m with
| (-1) -> tail_string_latin1 i j s q
| (-2) -> nil
| _ -> buf.(c - m))
in
buf.(c + a) <- x
done;
if pop != 0 then blit buf c buf (c - pop) n);
ensure_room n;
let c = !cursor in
let buf = !buffer in
for a = 0 to n - 1 do
let x =
match Array.unsafe_get r a with
| Catch -> String_latin1 { i; j; str = s; tl = q }
| Const c -> const c
| Nil -> nil
| Left -> Char (CharSet.V.mk_char s.[i])
| Right -> tail_string_latin1 i j s q
| Stack n -> buf.(c - n)
| Recompose (n, m) ->
pair
(match n with
| -1 -> Char (CharSet.V.mk_char s.[i])
| -2 -> nil
| _ -> buf.(c - n))
(match m with
| -1 -> tail_string_latin1 i j s q
| -2 -> nil
| _ -> buf.(c - m))
in
buf.(c + a) <- x
done;
if pop != 0 then blit buf c buf (c - pop) n);
cursor := !cursor - pop + n;
code
let tail_string_utf8 i j s q =
let i = Utf8.advance s i in
if Utf8.equal_index i j then q else String_utf8 {i;j;str=s;tl=q}
if Utf8.equal_index i j then q else String_utf8 { i; j; str = s; tl = q }
let make_result_string_utf8 i j s q (code,r,pop) =
let make_result_string_utf8 i j s q (code, r, pop) =
let n = Array.length r in
if n > 0 then (
ensure_room n;
let c = !cursor in
let buf = !buffer in
for a = 0 to n - 1 do
let x = match Array.unsafe_get r a with
| Catch -> String_utf8 {i;j;str=s;tl=q}
| Const c -> const c
| Nil -> nil
| Left -> Char (CharSet.V.mk_int (Utf8.get s i))
| Right -> tail_string_utf8 i j s q
| Stack n -> buf.(c - n)
| Recompose (n,m) ->
pair
(match n with
| (-1) -> Char (CharSet.V.mk_int (