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

Remove polymorphic variables from types before generating pattern automata.

parent 97ea82a0
Pipeline #163 passed with stages
in 7 minutes and 29 seconds
......@@ -60,7 +60,14 @@ and run_disp_kind pt d actions = function
run_disp_basic pt d
(fun t ->
if is_poly && not Types.(subtype Function.any t) then
failwith "Run-time inspection of polymorphic function"
failwith (Format.asprintf
"Run-time inspection of polymorphic function %a against type %a"
Types.Print.print
(List.fold_left (fun acc (s, t) ->
Types.(cap acc (arrow (cons s) (cons t))))
Types.any iface)
Types.Print.print t
)
else Types.Arrow.check_iface iface t)
actions.basic
| Absent ->
......
......@@ -212,7 +212,14 @@ and run_disp_kind actions v =
run_disp_basic v
(fun t ->
if is_poly && not Types.(subtype Function.any t) then
failwith "Run-time inspection of polymorphic function"
failwith (Format.asprintf
"Run-time inspection of polymorphic function %a against type %a"
Types.Print.print
(List.fold_left (fun acc (s, t) ->
Types.(cap acc (arrow (cons s) (cons t))))
Types.any iface)
Types.Print.print t
)
else Types.Arrow.check_iface iface t)
actions.basic
| Abstract (abs, _) ->
......
......@@ -339,7 +339,8 @@ let rec filter_descr t (_, fv, d) : Types.Positive.v id_map =
| Xml (p1, p2) -> filter_prod ~kind:`XML fv p1 p2 t
| Record (l, p) -> filter_node (Types.Record.project t l) p
| Capture c -> IdMap.singleton c (Types.Positive.ty t)
| Constant (c, cst) -> IdMap.singleton c (Types.Positive.ty (Types.constant cst))
| Constant (c, cst) ->
IdMap.singleton c (Types.Positive.ty (Types.constant cst))
| Dummy -> assert false
and filter_prod ?kind fv p1 p2 t =
......@@ -518,8 +519,8 @@ module Normal = struct
(NodeSet.get pl)
let print ppf (pl, t, xs) =
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]" NodeSet.dump pl Types.Print.print t
IdSet.dump xs
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]" NodeSet.dump pl
Types.Print.print t IdSet.dump xs
let compare (l1, t1, xs1) (l2, t2, xs2) =
let c = NodeSet.compare l1 l2 in
......@@ -1153,7 +1154,13 @@ module Compile = struct
aux success (Types.diff t ty) rem
in
aux [] t tests;
!accu
List.map
(fun (t, a) ->
let ct = (* TODO CHECK THAT THIS IS CORRECT W.R.T static semantics. *)
Types.Subst.clean_type ~pos:Types.any ~neg:Types.empty Var.Set.empty t
in
(ct, a))
!accu
let get_tests facto pl f t d post =
let pl = Array.map (List.map f) pl in
......
......@@ -199,15 +199,15 @@ let solve_rectype t alpha =
Positive.define x v;
Types.descr (Positive.solve x)
let clean_type delta t =
let clean_type ?(pos=Types.empty) ?(neg=Types.any) delta t =
let polarities = vars_gen true t in
let clean_subst =
Var.Map.fold
(fun v pol acc ->
match pol with
| `Both -> acc
| `Pos -> if Var.Set.mem delta v then acc else Var.Map.add v Types.empty acc
| `Neg -> if Var.Set.mem delta v then acc else Var.Map.add v Types.any acc
| `Pos -> if Var.Set.mem delta v then acc else Var.Map.add v pos acc
| `Neg -> if Var.Set.mem delta v then acc else Var.Map.add v neg acc
)
polarities Var.Map.empty
in
......
......@@ -53,4 +53,4 @@ val refresh : Var.Set.t -> Types.t -> Types.t
val solve_rectype : Types.t -> Var.t -> Types.t
val clean_type : Var.Set.t -> Types.t -> Types.t
val clean_type : ?pos:Types.t -> ?neg:Types.t -> Var.Set.t -> Types.t -> Types.t
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