| 1 |
abate |
1 |
type capture = string
|
| 2 |
|
|
type fv = capture SortedList.t
|
| 3 |
|
|
|
| 4 |
|
|
exception IllFormedCup of fv * fv
|
| 5 |
|
|
exception IllFormedCap of fv * fv
|
| 6 |
|
|
|
| 7 |
|
|
(* Syntactic algebra *)
|
| 8 |
|
|
|
| 9 |
|
|
type d =
|
| 10 |
|
|
| Constr of Types.node
|
| 11 |
|
|
| Cup of descr * descr
|
| 12 |
|
|
| Cap of descr * descr
|
| 13 |
|
|
| Times of node * node
|
| 14 |
|
|
| Record of Types.label * node
|
| 15 |
|
|
| Capture of capture
|
| 16 |
|
|
| Constant of capture * Types.const
|
| 17 |
|
|
and node = {
|
| 18 |
|
|
id : int;
|
| 19 |
|
|
mutable descr : descr option;
|
| 20 |
|
|
accept : Types.node;
|
| 21 |
|
|
fv : fv
|
| 22 |
|
|
} and descr = Types.descr * fv * d
|
| 23 |
|
|
|
| 24 |
|
|
let make =
|
| 25 |
|
|
let counter = ref 0 in
|
| 26 |
|
|
fun fv ->
|
| 27 |
|
|
incr counter;
|
| 28 |
|
|
{ id = !counter; descr = None; accept = Types.make (); fv = fv }
|
| 29 |
|
|
|
| 30 |
|
|
let define x ((accept,fv,_) as d) =
|
| 31 |
|
|
assert (x.fv = fv);
|
| 32 |
|
|
Types.define x.accept accept;
|
| 33 |
|
|
x.descr <- Some d
|
| 34 |
|
|
|
| 35 |
|
|
let constr x = (Types.descr x,[],Constr x)
|
| 36 |
|
|
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) =
|
| 37 |
|
|
if fv1 <> fv2 then raise (IllFormedCup (fv1,fv2));
|
| 38 |
|
|
(Types.cup acc1 acc2, SortedList.cup fv1 fv2, Cup (x1,x2))
|
| 39 |
|
|
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) =
|
| 40 |
|
|
if not (SortedList.disjoint fv1 fv2) then raise (IllFormedCap (fv1,fv2));
|
| 41 |
|
|
(Types.cap acc1 acc2, SortedList.cup fv1 fv2, Cap (x1,x2))
|
| 42 |
|
|
let times x y =
|
| 43 |
|
|
(Types.times x.accept y.accept, SortedList.cup x.fv y.fv, Times (x,y))
|
| 44 |
|
|
let record l x =
|
| 45 |
|
|
(Types.record l false x.accept, x.fv, Record (l,x))
|
| 46 |
|
|
let capture x = (Types.any, [x], Capture x)
|
| 47 |
|
|
let constant x c = (Types.any, [x], Constant (x,c))
|
| 48 |
|
|
|
| 49 |
|
|
|
| 50 |
|
|
let id x = x.id
|
| 51 |
|
|
let descr x = match x.descr with Some d -> d | None -> failwith "Patterns.descr"
|
| 52 |
|
|
let fv x = x.fv
|
| 53 |
|
|
let accept x = Types.internalize x.accept
|
| 54 |
|
|
|
| 55 |
|
|
|
| 56 |
|
|
(* Static semantics *)
|
| 57 |
|
|
|
| 58 |
|
|
let cup_res v1 v2 = Types.Positive.cup [v1;v2]
|
| 59 |
|
|
let empty_res fv = List.map (fun v -> (v, Types.Positive.ty Types.empty)) fv
|
| 60 |
|
|
let times_res v1 v2 = Types.Positive.times v1 v2
|
| 61 |
|
|
|
| 62 |
|
|
module MemoFilter = Map.Make
|
| 63 |
|
|
(struct type t = Types.descr * node let compare = compare end)
|
| 64 |
|
|
|
| 65 |
|
|
let memo_filter = ref MemoFilter.empty
|
| 66 |
|
|
|
| 67 |
|
|
let rec filter_descr t (_,fv,d) : (capture, Types.Positive.v) SortedMap.t =
|
| 68 |
|
|
if Types.is_empty t
|
| 69 |
|
|
then empty_res fv
|
| 70 |
|
|
else
|
| 71 |
|
|
match d with
|
| 72 |
|
|
| Constr _ -> []
|
| 73 |
|
|
| Cup ((a,_,_) as d1,d2) ->
|
| 74 |
|
|
SortedMap.union cup_res
|
| 75 |
|
|
(filter_descr (Types.cap t a) d1)
|
| 76 |
|
|
(filter_descr (Types.diff t a) d2)
|
| 77 |
|
|
| Cap (d1,d2) ->
|
| 78 |
|
|
SortedMap.union cup_res (filter_descr t d1) (filter_descr t d2)
|
| 79 |
|
|
| Times (p1,p2) ->
|
| 80 |
|
|
List.fold_left
|
| 81 |
|
|
(fun accu (d1,d2) ->
|
| 82 |
|
|
let term =
|
| 83 |
|
|
SortedMap.union times_res
|
| 84 |
|
|
(filter_node d1 p1)
|
| 85 |
|
|
(filter_node d2 p2)
|
| 86 |
|
|
in
|
| 87 |
|
|
SortedMap.union cup_res accu term
|
| 88 |
|
|
)
|
| 89 |
|
|
(empty_res fv)
|
| 90 |
|
|
(Types.Product.normal t)
|
| 91 |
|
|
| Record (l,p) ->
|
| 92 |
|
|
filter_node (Types.Record.project t l) p
|
| 93 |
|
|
| Capture c ->
|
| 94 |
|
|
[(c, Types.Positive.ty t)]
|
| 95 |
|
|
| Constant (c, cst) ->
|
| 96 |
|
|
[(c, Types.Positive.ty (Types.constant cst))]
|
| 97 |
|
|
|
| 98 |
|
|
and filter_node t p : (capture, Types.Positive.v) SortedMap.t =
|
| 99 |
|
|
try MemoFilter.find (t,p) !memo_filter
|
| 100 |
|
|
with Not_found ->
|
| 101 |
|
|
let (_,fv,_) as d = descr p in
|
| 102 |
|
|
let res = List.map (fun v -> (v,Types.Positive.forward ())) fv in
|
| 103 |
|
|
memo_filter := MemoFilter.add (t,p) res !memo_filter;
|
| 104 |
|
|
let r = filter_descr t (descr p) in
|
| 105 |
|
|
List.iter2 (fun (_,r) (_,v) -> Types.Positive.define v r) r res;
|
| 106 |
|
|
r
|
| 107 |
|
|
|
| 108 |
|
|
let filter t p =
|
| 109 |
|
|
let r = filter_node t p in
|
| 110 |
|
|
memo_filter := MemoFilter.empty;
|
| 111 |
|
|
List.map (fun (c,v) -> (c,Types.Positive.solve v)) r
|
| 112 |
|
|
|
| 113 |
|
|
|
| 114 |
|
|
|
| 115 |
|
|
(* Normal forms for patterns and compilation *)
|
| 116 |
|
|
|
| 117 |
|
|
module NF =
|
| 118 |
|
|
struct
|
| 119 |
|
|
|
| 120 |
|
|
type 'a sl = 'a SortedList.t
|
| 121 |
|
|
type ('a,'b) sm = ('a,'b) SortedMap.t
|
| 122 |
|
|
|
| 123 |
|
|
type source =
|
| 124 |
|
|
[ `Catch | `Const of Types.const
|
| 125 |
|
|
| `Left | `Right | `Recompose
|
| 126 |
|
|
| `Field of Types.label
|
| 127 |
|
|
]
|
| 128 |
|
|
type result = (capture, source) sm
|
| 129 |
|
|
|
| 130 |
abate |
39 |
type 'a line = (result * 'a, Types.descr) sm
|
| 131 |
abate |
1 |
type nf = {
|
| 132 |
|
|
v : fv;
|
| 133 |
|
|
a : Types.descr;
|
| 134 |
abate |
39 |
basic : unit line;
|
| 135 |
|
|
prod : (node sl * node sl) line;
|
| 136 |
|
|
record: ((Types.label, node sl) sm) line
|
| 137 |
abate |
1 |
}
|
| 138 |
|
|
|
| 139 |
abate |
39 |
type 'a nline = (result * 'a) list
|
| 140 |
|
|
type record =
|
| 141 |
|
|
[ `Success
|
| 142 |
|
|
| `Fail
|
| 143 |
|
|
| `Dispatch of (nf * record) list
|
| 144 |
|
|
| `Label of Types.label * (nf * record) list * record ]
|
| 145 |
|
|
type normal = {
|
| 146 |
|
|
nbasic : Types.descr nline;
|
| 147 |
|
|
nprod : (nf * nf) nline;
|
| 148 |
|
|
nrecord: record nline
|
| 149 |
|
|
}
|
| 150 |
|
|
|
| 151 |
abate |
1 |
let empty = { v = []; a = Types.empty; basic = []; prod = []; record = [] }
|
| 152 |
|
|
let any_basic = Types.neg (Types.cup Types.Product.any Types.Record.any)
|
| 153 |
|
|
|
| 154 |
|
|
|
| 155 |
|
|
let restrict t nf =
|
| 156 |
abate |
39 |
let rec filter = function
|
| 157 |
|
|
| (key,acc) :: rem ->
|
| 158 |
|
|
let acc = Types.cap t acc in
|
| 159 |
|
|
if Types.is_empty acc then filter rem else (key,acc) :: (filter rem)
|
| 160 |
|
|
| [] -> []
|
| 161 |
|
|
in
|
| 162 |
abate |
1 |
{ v = nf.v;
|
| 163 |
|
|
a = Types.cap t nf.a;
|
| 164 |
abate |
39 |
basic = filter nf.basic;
|
| 165 |
|
|
prod = filter nf.prod;
|
| 166 |
|
|
record = filter nf.record;
|
| 167 |
abate |
1 |
}
|
| 168 |
|
|
|
| 169 |
|
|
let fus = SortedMap.union_disj
|
| 170 |
|
|
let slcup = SortedList.cup
|
| 171 |
|
|
|
| 172 |
|
|
let cap nf1 nf2 =
|
| 173 |
abate |
39 |
let merge f lines1 lines2 =
|
| 174 |
|
|
let m =
|
| 175 |
|
|
List.fold_left
|
| 176 |
|
|
(fun accu ((res1,x1),acc1) ->
|
| 177 |
|
|
List.fold_left
|
| 178 |
|
|
(fun accu ((res2,x2),acc2) ->
|
| 179 |
|
|
let acc = Types.cap acc1 acc2 in
|
| 180 |
|
|
if Types.is_empty acc then accu
|
| 181 |
|
|
else ((fus res1 res2, f x1 x2),acc) :: accu
|
| 182 |
|
|
) accu lines2
|
| 183 |
|
|
) [] lines1 in
|
| 184 |
|
|
SortedMap.from_list Types.cup m
|
| 185 |
|
|
in
|
| 186 |
|
|
let merge_basic () () = ()
|
| 187 |
|
|
and merge_prod (p1,q1) (p2,q2) = slcup p1 p1, slcup q1 q2
|
| 188 |
|
|
and merge_record r1 r2 = SortedMap.union slcup r1 r2 in
|
| 189 |
abate |
1 |
{ v = SortedList.cup nf1.v nf2.v;
|
| 190 |
|
|
a = Types.cap nf1.a nf2.a;
|
| 191 |
abate |
39 |
basic = merge merge_basic nf1.basic nf2.basic;
|
| 192 |
|
|
prod = merge merge_prod nf1.prod nf2.prod;
|
| 193 |
|
|
record = merge merge_record nf1.record nf2.record;
|
| 194 |
abate |
1 |
}
|
| 195 |
|
|
|
| 196 |
|
|
|
| 197 |
|
|
|
| 198 |
|
|
let cup acc1 nf1 nf2 =
|
| 199 |
|
|
let nf2 = restrict (Types.neg acc1) nf2 in
|
| 200 |
abate |
39 |
{ v = nf1.v; (* = nf2.v *)
|
| 201 |
abate |
1 |
a = Types.cup nf1.a nf2.a;
|
| 202 |
|
|
basic = SortedMap.union Types.cup nf1.basic nf2.basic;
|
| 203 |
abate |
39 |
prod = SortedMap.union Types.cup nf1.prod nf2.prod;
|
| 204 |
|
|
record = SortedMap.union Types.cup nf1.record nf2.record;
|
| 205 |
abate |
1 |
}
|
| 206 |
|
|
|
| 207 |
|
|
let times acc p q =
|
| 208 |
|
|
let src_p = List.map (fun v -> (v,`Left)) p.fv
|
| 209 |
|
|
and src_q = List.map (fun v -> (v,`Right)) q.fv in
|
| 210 |
|
|
let src = SortedMap.union (fun _ _ -> `Recompose) src_p src_q in
|
| 211 |
|
|
{ empty with
|
| 212 |
|
|
v = SortedList.cup p.fv q.fv;
|
| 213 |
|
|
a = acc;
|
| 214 |
abate |
39 |
prod = [ (src, ([p], [q])), acc ] }
|
| 215 |
abate |
1 |
|
| 216 |
|
|
let record acc l p =
|
| 217 |
|
|
let src = List.map (fun v -> (v, `Field l)) p.fv in
|
| 218 |
|
|
{ empty with
|
| 219 |
|
|
v = p.fv;
|
| 220 |
|
|
a = acc;
|
| 221 |
abate |
39 |
record = [ (src, [l,[p]]), acc ] }
|
| 222 |
abate |
1 |
|
| 223 |
|
|
let any =
|
| 224 |
|
|
{ v = [];
|
| 225 |
|
|
a = Types.any;
|
| 226 |
abate |
39 |
basic = [ ([],()), any_basic ];
|
| 227 |
|
|
prod = [ ([],([],[])), Types.Product.any ];
|
| 228 |
|
|
record = [ ([],[]), Types.Record.any ];
|
| 229 |
abate |
1 |
}
|
| 230 |
|
|
|
| 231 |
|
|
let capture x =
|
| 232 |
|
|
let l = [x,`Catch] in
|
| 233 |
|
|
{ v = [x];
|
| 234 |
|
|
a = Types.any;
|
| 235 |
abate |
39 |
basic = [ (l,()), any_basic ];
|
| 236 |
|
|
prod = [ (l,([],[])), Types.Product.any ];
|
| 237 |
|
|
record = [ (l,[]), Types.Record.any ];
|
| 238 |
abate |
1 |
}
|
| 239 |
|
|
|
| 240 |
|
|
let constant x c =
|
| 241 |
|
|
let l = [x,`Const c] in
|
| 242 |
|
|
{ v = [x];
|
| 243 |
|
|
a = Types.any;
|
| 244 |
abate |
39 |
basic = [ (l,()), any_basic ];
|
| 245 |
|
|
prod = [ (l,([],[])), Types.Product.any ];
|
| 246 |
|
|
record = [ (l,[]), Types.Record.any ];
|
| 247 |
abate |
1 |
}
|
| 248 |
|
|
|
| 249 |
|
|
let constr t =
|
| 250 |
|
|
{ v = [];
|
| 251 |
|
|
a = t;
|
| 252 |
abate |
39 |
basic = [ ([],()), Types.cap t any_basic ];
|
| 253 |
|
|
prod = [ ([],([],[])), Types.cap t Types.Product.any ];
|
| 254 |
|
|
record = [ ([],[]), Types.cap t Types.Record.any ];
|
| 255 |
abate |
1 |
}
|
| 256 |
|
|
|
| 257 |
|
|
(* Put a pattern in normal form *)
|
| 258 |
|
|
let rec nf (acc,fv,d) =
|
| 259 |
|
|
if Types.is_empty acc
|
| 260 |
|
|
then empty
|
| 261 |
|
|
else match d with
|
| 262 |
|
|
| Constr t -> constr (Types.descr t)
|
| 263 |
|
|
| Cap (p,q) -> cap (nf p) (nf q)
|
| 264 |
|
|
| Cup ((acc1,_,_) as p,q) -> cup acc1 (nf p) (nf q)
|
| 265 |
|
|
| Times (p,q) -> times acc p q
|
| 266 |
|
|
| Capture x -> capture x
|
| 267 |
|
|
| Constant (x,c) -> constant x c
|
| 268 |
|
|
| Record (l,p) -> record acc l p
|
| 269 |
|
|
|
| 270 |
|
|
let bigcap = List.fold_left (fun a p -> cap a (nf (descr p))) any
|
| 271 |
|
|
|
| 272 |
|
|
let rec num i = function [] -> [] | h::t -> (h,i)::(num (i+1) t)
|
| 273 |
|
|
|
| 274 |
|
|
|
| 275 |
|
|
module Dispatch = struct
|
| 276 |
|
|
type t = {
|
| 277 |
|
|
fv : fv list;
|
| 278 |
|
|
masks : (mask * int) list;
|
| 279 |
|
|
basic : (Types.descr * (result option list)) list;
|
| 280 |
|
|
prod : prod;
|
| 281 |
abate |
39 |
record: record option;
|
| 282 |
abate |
1 |
}
|
| 283 |
|
|
and prod = disp * (mask * disp * (mask * prod_result) list) list
|
| 284 |
|
|
and prod_result = (result * (int * int)) option list
|
| 285 |
|
|
|
| 286 |
|
|
and record =
|
| 287 |
|
|
[ `Label of Types.label * disp * (mask * record) list * record option
|
| 288 |
|
|
| `Result of record_result ]
|
| 289 |
|
|
and record_result = (result * (Types.label * int) list) option list
|
| 290 |
|
|
|
| 291 |
|
|
and mask = bool list
|
| 292 |
|
|
and disp = Types.descr * nf SortedList.t
|
| 293 |
|
|
end
|
| 294 |
abate |
39 |
|
| 295 |
|
|
let normal nf =
|
| 296 |
|
|
let basic =
|
| 297 |
|
|
List.map (fun ((res,()),acc) -> (res,acc))
|
| 298 |
|
|
|
| 299 |
|
|
and prod =
|
| 300 |
|
|
let line accu (((res,(pl,ql)),acc)) =
|
| 301 |
|
|
let p = bigcap pl and q = bigcap ql in
|
| 302 |
|
|
let aux accu (t1,t2) = (res,(restrict t1 p,restrict t2 q))::accu in
|
| 303 |
|
|
List.fold_left aux accu (Types.Product.normal acc) in
|
| 304 |
|
|
List.fold_left line []
|
| 305 |
|
|
|
| 306 |
|
|
and record =
|
| 307 |
|
|
let rec aux nr fields =
|
| 308 |
|
|
match (nr,fields) with
|
| 309 |
|
|
| (`Success, []) -> `Success
|
| 310 |
|
|
| (`Fail,_) -> `Fail
|
| 311 |
|
|
| (`Success, (l2,pl)::fields) ->
|
| 312 |
|
|
`Label (l2, [bigcap pl, aux nr fields], `Fail)
|
| 313 |
|
|
| (`Label (l1, _, _), (l2,pl)::fields) when l2 < l1 ->
|
| 314 |
|
|
`Label (l2, [bigcap pl, aux nr fields], `Fail)
|
| 315 |
|
|
| (`Label (l1, pr, _), (l2,pl)::fields) when l1 = l2 ->
|
| 316 |
|
|
let p = bigcap pl in
|
| 317 |
|
|
let pr =
|
| 318 |
|
|
List.map (fun (t,x) -> (restrict t p, aux x fields)) pr in
|
| 319 |
|
|
`Label (l1, pr, `Fail)
|
| 320 |
|
|
| (`Label (l1, pr, ab),_) ->
|
| 321 |
|
|
let pr =
|
| 322 |
|
|
List.map (fun (t,x) -> (constr t, aux x fields)) pr in
|
| 323 |
|
|
`Label (l1, pr, aux ab fields)
|
| 324 |
|
|
in
|
| 325 |
|
|
|
| 326 |
|
|
let line accu ((res,fields),acc) =
|
| 327 |
|
|
let nr = Types.Record.normal acc in
|
| 328 |
|
|
let x = aux nr fields in
|
| 329 |
|
|
match x with
|
| 330 |
|
|
| `Fail -> accu
|
| 331 |
|
|
| x -> (res,x) :: accu in
|
| 332 |
|
|
List.fold_left line []
|
| 333 |
|
|
in
|
| 334 |
|
|
{ nbasic = basic nf.basic;
|
| 335 |
|
|
nprod = prod nf.prod;
|
| 336 |
|
|
nrecord = record nf.record;
|
| 337 |
|
|
}
|
| 338 |
|
|
|
| 339 |
abate |
1 |
let collect f pp =
|
| 340 |
|
|
let aux accu (res,x) = (f x) :: accu in
|
| 341 |
|
|
SortedList.from_list (List.fold_left (List.fold_left aux) [] pp)
|
| 342 |
|
|
|
| 343 |
|
|
let rec map_map f = function
|
| 344 |
|
|
| [] -> []
|
| 345 |
|
|
| x::l ->
|
| 346 |
|
|
try let y = f x in y::(map_map f l)
|
| 347 |
|
|
with Not_found -> map_map f l
|
| 348 |
|
|
|
| 349 |
|
|
let get_option = function [x] -> Some x | [] -> None | _ -> assert false
|
| 350 |
|
|
let extract_unique f l = get_option (map_map f l)
|
| 351 |
|
|
(* Could optimize to extract directly the first (and single) *)
|
| 352 |
|
|
|
| 353 |
|
|
(* Basic (and arrow) types *)
|
| 354 |
|
|
|
| 355 |
|
|
let filter_basic ty =
|
| 356 |
|
|
let aux (k,t) = if Types.subtype ty t then k else raise Not_found in
|
| 357 |
|
|
List.map (extract_unique aux)
|
| 358 |
|
|
|
| 359 |
|
|
let dispatch_basic t pl =
|
| 360 |
|
|
let rec aux pl accu t l =
|
| 361 |
|
|
if Types.is_empty t then accu
|
| 362 |
|
|
else match l with
|
| 363 |
|
|
| [] ->
|
| 364 |
|
|
let pl = filter_basic t pl in
|
| 365 |
|
|
(t, pl) :: accu
|
| 366 |
|
|
| ty :: rem ->
|
| 367 |
|
|
let accu = aux pl accu (Types.cap t ty) rem in
|
| 368 |
|
|
let accu = aux pl accu (Types.diff t ty) rem in
|
| 369 |
|
|
accu
|
| 370 |
|
|
in
|
| 371 |
abate |
39 |
let pl = List.map (fun p -> p.nbasic) pl in
|
| 372 |
abate |
1 |
let tests = collect (fun x -> x) pl in
|
| 373 |
|
|
let t = Types.cap any_basic t in
|
| 374 |
|
|
aux pl [] t tests
|
| 375 |
|
|
|
| 376 |
|
|
(* Product types *)
|
| 377 |
|
|
|
| 378 |
|
|
let filter_prod1 success =
|
| 379 |
|
|
let aux (res,(p,q)) = (res,(List.assoc p success,q)) in
|
| 380 |
|
|
List.map (map_map aux)
|
| 381 |
|
|
|
| 382 |
|
|
let filter_prod2 success =
|
| 383 |
|
|
let aux (res,(i,q)) = (res,(i,List.assoc q success)) in
|
| 384 |
|
|
List.map (extract_unique aux)
|
| 385 |
|
|
|
| 386 |
|
|
let rec dispatch_prod t pl =
|
| 387 |
abate |
39 |
let pl = List.map (fun p -> p.nprod) pl in
|
| 388 |
abate |
1 |
let tests = collect (fun (p,_) -> p) pl in
|
| 389 |
|
|
let t = Types.Product.get t in
|
| 390 |
|
|
let disp = aux_prod1 t pl [] [] [] 0 tests in
|
| 391 |
|
|
let pi1 = Types.Product.pi1 t in
|
| 392 |
|
|
((pi1,tests),disp)
|
| 393 |
|
|
|
| 394 |
|
|
and aux_prod2 t pl accu mask success j tests =
|
| 395 |
|
|
if Types.is_empty t then accu
|
| 396 |
|
|
else match tests with
|
| 397 |
|
|
| [] ->
|
| 398 |
|
|
let pl = filter_prod2 success pl in
|
| 399 |
|
|
(List.rev mask, pl) :: accu
|
| 400 |
|
|
| p :: rem ->
|
| 401 |
|
|
let accu =
|
| 402 |
|
|
let t = Types.cap t p.a in
|
| 403 |
|
|
aux_prod2 t pl accu (true::mask) ((p,j)::success) (j+1) rem in
|
| 404 |
|
|
let accu =
|
| 405 |
|
|
let t = Types.diff t p.a in
|
| 406 |
|
|
aux_prod2 t pl accu (false::mask) success (j+1) rem in
|
| 407 |
|
|
accu
|
| 408 |
|
|
|
| 409 |
|
|
and aux_prod1 t pl accu mask success i tests =
|
| 410 |
|
|
if t = [] then accu
|
| 411 |
|
|
else match tests with
|
| 412 |
|
|
| [] ->
|
| 413 |
|
|
let pl = filter_prod1 success pl in
|
| 414 |
|
|
let t = Types.Product.pi2 t in
|
| 415 |
|
|
let tests = collect (fun (_,q)-> q) pl in
|
| 416 |
|
|
let disp = aux_prod2 t pl [] [] [] 0 tests in
|
| 417 |
|
|
let mask = List.rev mask in
|
| 418 |
|
|
(mask, (t,tests), disp) :: accu
|
| 419 |
|
|
| p :: rem ->
|
| 420 |
|
|
let accu =
|
| 421 |
|
|
let t = Types.Product.restrict_1 t p.a in
|
| 422 |
|
|
aux_prod1 t pl accu (true::mask) ((p,i)::success) (i+1) rem in
|
| 423 |
|
|
let accu =
|
| 424 |
|
|
let t = Types.Product.restrict_1 t (Types.neg p.a) in
|
| 425 |
|
|
aux_prod1 t pl accu (false::mask) success (i+1) rem in
|
| 426 |
|
|
accu
|
| 427 |
|
|
|
| 428 |
|
|
(* Record types *)
|
| 429 |
|
|
|
| 430 |
|
|
|
| 431 |
|
|
let map_record f =
|
| 432 |
|
|
let rec aux = function
|
| 433 |
|
|
| [] -> []
|
| 434 |
|
|
| h::t -> (match f h with (_,_,`Fail) -> aux t | x -> x :: (aux t)) in
|
| 435 |
|
|
List.map aux
|
| 436 |
|
|
|
| 437 |
|
|
let label_found l =
|
| 438 |
|
|
map_record
|
| 439 |
|
|
(function
|
| 440 |
|
|
| (res, catch, `Label (l1, pr, _)) when l1 = l ->
|
| 441 |
|
|
(res, catch, `Dispatch pr)
|
| 442 |
|
|
| x -> x)
|
| 443 |
|
|
|
| 444 |
|
|
let label_disp l success =
|
| 445 |
|
|
map_record
|
| 446 |
|
|
(function
|
| 447 |
|
|
| (res, catch, `Dispatch disp) ->
|
| 448 |
|
|
let aux (p,rem) = (List.assoc p success, rem) in
|
| 449 |
|
|
(match extract_unique aux disp with
|
| 450 |
|
|
| None -> (res, catch, `Fail)
|
| 451 |
|
|
| Some (i,rem) -> (res, (l, i)::catch, rem))
|
| 452 |
|
|
| x -> x)
|
| 453 |
|
|
|
| 454 |
|
|
let label_not_found l =
|
| 455 |
|
|
map_record
|
| 456 |
|
|
(function
|
| 457 |
|
|
| (res, catch, `Label (l1, _, ab)) when l1 = l -> (res, catch, ab)
|
| 458 |
|
|
| x -> x)
|
| 459 |
|
|
|
| 460 |
|
|
|
| 461 |
|
|
let dummy_label = Types.label ""
|
| 462 |
|
|
|
| 463 |
|
|
let collect_first_label pp =
|
| 464 |
|
|
let f = ref true and m = ref dummy_label in
|
| 465 |
|
|
let aux = function
|
| 466 |
|
|
| (_, _, `Label (l, _, _)) ->
|
| 467 |
|
|
if (!f) then (f := false; m := l) else if (l < !m) then m:= l;
|
| 468 |
|
|
| _ -> () in
|
| 469 |
|
|
List.iter (List.iter aux) pp;
|
| 470 |
|
|
if !f then None else Some !m
|
| 471 |
|
|
|
| 472 |
|
|
let collect_record pp =
|
| 473 |
|
|
let aux accu = function
|
| 474 |
|
|
| (res,catch,`Dispatch disp) ->
|
| 475 |
|
|
List.fold_left (fun accu (p,_) -> p :: accu) accu disp
|
| 476 |
|
|
| _ -> accu in
|
| 477 |
|
|
SortedList.from_list (List.fold_left (List.fold_left aux) [] pp)
|
| 478 |
|
|
|
| 479 |
|
|
let final_record =
|
| 480 |
|
|
let aux = function
|
| 481 |
|
|
| [(res, catch, `Success)] -> Some (res, catch)
|
| 482 |
|
|
| [] -> None
|
| 483 |
|
|
| _ -> assert false in
|
| 484 |
|
|
List.map aux
|
| 485 |
|
|
|
| 486 |
|
|
(* combiner les restrict field, ... *)
|
| 487 |
|
|
let rec dispatch_record t pl =
|
| 488 |
abate |
39 |
let pl = List.map
|
| 489 |
|
|
(fun p -> List.map (fun (res,r) -> (res,[],r)) p.nrecord
|
| 490 |
|
|
) pl in
|
| 491 |
abate |
1 |
let t = Types.Record.get t in
|
| 492 |
abate |
39 |
if Types.Record.is_empty t then None else Some (aux_record1 t pl)
|
| 493 |
abate |
1 |
|
| 494 |
|
|
and aux_record1 t pl =
|
| 495 |
|
|
match collect_first_label pl with
|
| 496 |
|
|
| None -> `Result (final_record pl)
|
| 497 |
|
|
| Some l ->
|
| 498 |
|
|
let (disp,pr) =
|
| 499 |
|
|
let pl = label_found l pl in
|
| 500 |
|
|
let tests = collect_record pl in
|
| 501 |
|
|
let t = Types.Record.restrict_label_present t l in
|
| 502 |
|
|
let disp = aux_record2 t pl l [] [] [] 0 tests in
|
| 503 |
|
|
((Types.Record.project_field t l, tests),disp)
|
| 504 |
|
|
in
|
| 505 |
|
|
let ab =
|
| 506 |
|
|
let pl = label_not_found l pl in
|
| 507 |
|
|
let t = Types.Record.restrict_label_absent t l in
|
| 508 |
|
|
if Types.Record.is_empty t then None
|
| 509 |
|
|
else Some (aux_record1 t pl)
|
| 510 |
|
|
in
|
| 511 |
|
|
`Label (l, disp, pr, ab)
|
| 512 |
|
|
|
| 513 |
|
|
and aux_record2 t pl l accu mask success i tests =
|
| 514 |
|
|
if Types.Record.is_empty t then accu
|
| 515 |
|
|
else match tests with
|
| 516 |
|
|
| [] ->
|
| 517 |
|
|
let pl = label_disp l success pl in
|
| 518 |
|
|
let disp = aux_record1 t pl in
|
| 519 |
|
|
(List.rev mask, disp) :: accu
|
| 520 |
|
|
| p :: rem ->
|
| 521 |
|
|
let accu =
|
| 522 |
|
|
let t = Types.Record.restrict_field t l p.a in
|
| 523 |
|
|
aux_record2 t pl l accu (true::mask) ((p,i)::success) (i+1) rem in
|
| 524 |
|
|
let accu =
|
| 525 |
|
|
let t = Types.Record.restrict_field t l (Types.neg p.a) in
|
| 526 |
|
|
aux_record2 t pl l accu (false::mask) success (i+1) rem in
|
| 527 |
|
|
accu
|
| 528 |
abate |
39 |
|
| 529 |
abate |
1 |
let mask l = List.map (function None -> false | Some _ -> true) l
|
| 530 |
|
|
|
| 531 |
|
|
let rec dispatch (t : Types.descr) (pl : nf list) =
|
| 532 |
abate |
39 |
let fv = List.map (fun p -> p.v) pl in
|
| 533 |
|
|
let pl = List.map (fun p -> normal (restrict t p)) pl in
|
| 534 |
abate |
1 |
let basic = dispatch_basic t pl
|
| 535 |
|
|
and prod = dispatch_prod t pl
|
| 536 |
|
|
and record = dispatch_record t pl in
|
| 537 |
|
|
|
| 538 |
|
|
let masks =
|
| 539 |
|
|
let accu = ref [] in
|
| 540 |
|
|
let acc r = accu := (mask r) :: !accu in
|
| 541 |
|
|
List.iter (fun (_,r) -> acc r) basic;
|
| 542 |
|
|
List.iter (fun (_,_,l) -> List.iter (fun (_,r) -> acc r) l) (snd prod);
|
| 543 |
|
|
num 0 (SortedList.from_list !accu) in
|
| 544 |
|
|
|
| 545 |
|
|
{
|
| 546 |
abate |
39 |
Dispatch.fv = fv;
|
| 547 |
abate |
1 |
Dispatch.masks = masks;
|
| 548 |
|
|
Dispatch.basic = basic;
|
| 549 |
|
|
Dispatch.prod = prod;
|
| 550 |
|
|
Dispatch.record = record;
|
| 551 |
|
|
}
|
| 552 |
|
|
|
| 553 |
|
|
|
| 554 |
|
|
let to_print = ref []
|
| 555 |
|
|
let memo = ref []
|
| 556 |
|
|
let count = ref 0
|
| 557 |
|
|
|
| 558 |
|
|
let print_fv ppf fv =
|
| 559 |
|
|
List.iter (fun x -> Format.fprintf ppf "{%s}" x) fv
|
| 560 |
|
|
|
| 561 |
|
|
let res_basic x = function
|
| 562 |
|
|
| `Catch -> "v"
|
| 563 |
|
|
| `Const c -> "const"
|
| 564 |
|
|
| _ -> assert false
|
| 565 |
|
|
|
| 566 |
|
|
let res_prod i j x res =
|
| 567 |
|
|
match res with
|
| 568 |
|
|
| `Left -> Printf.sprintf "l%i_%s" i x
|
| 569 |
|
|
| `Right -> Printf.sprintf "r%i_%s" j x
|
| 570 |
|
|
| `Recompose -> Printf.sprintf "(l%i_%s,r%i_%s)" i x j x
|
| 571 |
|
|
| _ -> res_basic x res
|
| 572 |
|
|
|
| 573 |
|
|
let res_record m x res =
|
| 574 |
|
|
match res with
|
| 575 |
|
|
| `Field l ->
|
| 576 |
|
|
Printf.sprintf "f%s_%i_%s" (Types.label_name l) (List.assoc l m) x
|
| 577 |
|
|
| _ -> res_basic x res
|
| 578 |
|
|
|
| 579 |
|
|
|
| 580 |
|
|
let print_mask ppf =
|
| 581 |
|
|
List.iter (fun b -> Format.fprintf ppf "%i" (if b then 1 else 0))
|
| 582 |
|
|
|
| 583 |
|
|
let compute_vars mask pl =
|
| 584 |
|
|
List.fold_right2
|
| 585 |
|
|
(fun (b,i) p acc ->
|
| 586 |
|
|
if b then List.fold_right (fun v acc -> (i,v)::acc) p.v acc
|
| 587 |
|
|
else acc
|
| 588 |
|
|
)
|
| 589 |
|
|
(num 0 mask) pl []
|
| 590 |
|
|
|
| 591 |
|
|
let compute_result f result =
|
| 592 |
|
|
List.fold_right
|
| 593 |
|
|
(function
|
| 594 |
|
|
| None -> (fun acc -> acc)
|
| 595 |
|
|
| Some x ->
|
| 596 |
|
|
let (r,res) = f x in
|
| 597 |
|
|
List.fold_right (fun (x,s) acc -> res x s :: acc) r
|
| 598 |
|
|
)
|
| 599 |
|
|
result []
|
| 600 |
|
|
|
| 601 |
|
|
let print_success ppf (mask,pl,pr) =
|
| 602 |
|
|
let vars =
|
| 603 |
|
|
let v = compute_vars mask pl in
|
| 604 |
|
|
if v = [] then "" else
|
| 605 |
|
|
let v = List.map (fun (i,v) -> Format.sprintf "%s%i_%s" pr i v) v in
|
| 606 |
|
|
" (" ^ String.concat ", " v ^ ")" in
|
| 607 |
|
|
Format.fprintf ppf "`S%a%s" print_mask mask vars
|
| 608 |
|
|
|
| 609 |
|
|
let print_result f ppf result =
|
| 610 |
|
|
let res = compute_result f result in
|
| 611 |
|
|
let res = if res = [] then "" else " (" ^ String.concat ", " res ^ ")" in
|
| 612 |
|
|
Format.fprintf ppf "`S%a%s" print_mask (mask result) res
|
| 613 |
|
|
|
| 614 |
|
|
|
| 615 |
|
|
let no t pl =
|
| 616 |
|
|
try List.assoc (t,pl) !memo
|
| 617 |
|
|
with Not_found ->
|
| 618 |
|
|
incr count;
|
| 619 |
|
|
let d = dispatch t pl in
|
| 620 |
|
|
memo := ((t,pl),!count) :: !memo;
|
| 621 |
|
|
to_print := (!count, d) :: !to_print;
|
| 622 |
|
|
!count
|
| 623 |
|
|
|
| 624 |
|
|
let rec show ppf num d =
|
| 625 |
|
|
Format.fprintf ppf "let matcher_%i v = match v with@\n" num;
|
| 626 |
|
|
show_basic ppf d.Dispatch.basic;
|
| 627 |
|
|
show_prod ppf d.Dispatch.prod;
|
| 628 |
|
|
show_record ppf d.Dispatch.record;
|
| 629 |
|
|
Format.fprintf ppf "@\n"
|
| 630 |
|
|
|
| 631 |
|
|
and show_basic ppf =
|
| 632 |
|
|
let pr_basic ppf t =
|
| 633 |
|
|
if Types.subtype any_basic t then Format.fprintf ppf "AnyBasic"
|
| 634 |
|
|
else Types.Print.print_descr ppf t in
|
| 635 |
|
|
let case (t,result) =
|
| 636 |
|
|
Format.fprintf ppf " | @[%a@] -> %a@\n"
|
| 637 |
|
|
pr_basic t
|
| 638 |
|
|
(print_result (fun res -> (res,res_basic))) result in
|
| 639 |
|
|
List.iter case
|
| 640 |
|
|
|
| 641 |
|
|
and show_prod ppf = function
|
| 642 |
|
|
| (_, []) -> ()
|
| 643 |
|
|
| ((t1,pl1), cases1) ->
|
| 644 |
|
|
Format.fprintf ppf
|
| 645 |
|
|
" | (v1,v2) -> match matcher_%i v1 with@\n" (no t1 pl1);
|
| 646 |
|
|
List.iter (case_prod1 ppf pl1) cases1
|
| 647 |
|
|
and case_prod2 ppf pl2 (mask2, result) =
|
| 648 |
|
|
Format.fprintf ppf " | %a -> %a@\n"
|
| 649 |
|
|
print_success (mask2,pl2,"r")
|
| 650 |
|
|
(print_result (fun (res,(i,j)) -> (res,res_prod i j))) result
|
| 651 |
|
|
and case_prod1 ppf pl1 (mask1, (t2,pl2), cases2) =
|
| 652 |
|
|
Format.fprintf ppf " | %a -> match matcher_%i v2 with@\n"
|
| 653 |
|
|
print_success (mask1,pl1,"l")
|
| 654 |
|
|
(no t2 pl2);
|
| 655 |
|
|
List.iter (case_prod2 ppf pl2) cases2
|
| 656 |
|
|
|
| 657 |
abate |
39 |
and show_record ppf = function
|
| 658 |
|
|
| None -> ()
|
| 659 |
|
|
| Some r ->
|
| 660 |
|
|
Format.fprintf ppf " | Record r -> @\n";
|
| 661 |
|
|
Format.fprintf ppf " @[%a@]@\n" show_record_aux r
|
| 662 |
abate |
1 |
|
| 663 |
|
|
and show_record_aux ppf = function
|
| 664 |
|
|
| `Result r ->
|
| 665 |
|
|
print_result (fun (res,m) -> (res, res_record m)) ppf r
|
| 666 |
|
|
| `Label (l, (t,pl), cases, ab) ->
|
| 667 |
|
|
let ln = Types.label_name l in
|
| 668 |
|
|
Format.fprintf ppf "match matcher_%i r.%s with@\n" (no t pl) ln;
|
| 669 |
|
|
if cases <> [] then
|
| 670 |
|
|
(
|
| 671 |
|
|
let case (mask, rem) =
|
| 672 |
|
|
Format.fprintf ppf " | %a -> @\n @[%a@]@\n"
|
| 673 |
|
|
print_success (mask, pl, Printf.sprintf "f%s_" ln)
|
| 674 |
|
|
show_record_aux rem
|
| 675 |
|
|
in
|
| 676 |
|
|
List.iter case cases;
|
| 677 |
|
|
);
|
| 678 |
|
|
(match ab with
|
| 679 |
|
|
| Some ab ->
|
| 680 |
|
|
Format.fprintf ppf
|
| 681 |
|
|
" | absent -> @\n @[%a@]@\n" show_record_aux ab
|
| 682 |
|
|
| None -> ()
|
| 683 |
|
|
)
|
| 684 |
|
|
|
| 685 |
|
|
|
| 686 |
|
|
|
| 687 |
|
|
let show ppf t pl =
|
| 688 |
|
|
ignore (no t pl);
|
| 689 |
|
|
let rec loop () =
|
| 690 |
|
|
match !to_print with
|
| 691 |
|
|
| (n,d)::r -> to_print:=r; show ppf n d; loop ()
|
| 692 |
|
|
| [] -> ()
|
| 693 |
|
|
in
|
| 694 |
|
|
loop ()
|
| 695 |
|
|
|
| 696 |
|
|
let get i =
|
| 697 |
|
|
fst (List.find (fun (_,j) -> i = j) !memo)
|
| 698 |
|
|
|
| 699 |
|
|
end
|
| 700 |
|
|
|
| 701 |
|
|
(*
|
| 702 |
|
|
let test_filter t p =
|
| 703 |
|
|
let t = Syntax.make_type (Syntax.parse t)
|
| 704 |
|
|
and p = Syntax.make_pat (Syntax.parse p) in
|
| 705 |
|
|
let r = Patterns.filter (Types.descr t) p in
|
| 706 |
|
|
List.iter (fun (v,t) ->
|
| 707 |
|
|
let t = Types.normalize t in
|
| 708 |
|
|
Format.fprintf Format.std_formatter "@[%s => %a@]@\n"
|
| 709 |
|
|
v Types.Print.print t) r;;
|
| 710 |
|
|
test_filter "[ (1 2 3?)* ]" "[ (x::(1 2) 3?)* ]";;
|
| 711 |
|
|
*)
|
| 712 |
|
|
|
| 713 |
|
|
(*
|
| 714 |
abate |
19 |
let pat s = Patterns.descr (Typer.pat (Parser.From_string.pat s));;
|
| 715 |
|
|
let typ s = Types.descr (Typer.typ (Parser.From_string.pat s));;
|
| 716 |
abate |
1 |
let f s = Patterns.NF.nf (pat s);;
|
| 717 |
|
|
let show' t l = Patterns.NF.show Format.std_formatter t (List.map f l);;
|
| 718 |
|
|
let show l = show' Types.any l;;
|
| 719 |
|
|
let showt t l = show' (typ t) l;;
|
| 720 |
|
|
|
| 721 |
abate |
19 |
showt " [(`A `B `C?)*] " [" [ (((x::`A) `B (x::`C))|_)* ] "];;
|
| 722 |
|
|
|
| 723 |
abate |
1 |
show ["{x=2;y=3}"];;
|
| 724 |
|
|
show [" [((x::1)|(y::2))*] "];;
|
| 725 |
|
|
|
| 726 |
|
|
let g s =
|
| 727 |
|
|
Patterns.NF.ProdMap.fold (fun k x acc -> (k,x)::acc) (Patterns.NF.left (f s)) [];;
|
| 728 |
|
|
|
| 729 |
|
|
Patterns.NF.dispatch Types.any [ f "(x,y)" ];;
|
| 730 |
|
|
Patterns.NF.show Format.std_formatter 0 Types.any [ f "(x,y)" ];;
|
| 731 |
|
|
Patterns.NF.show Format.std_formatter 0 Types.any [ f "(0--100,x) | (_,(x:=10))" ];;
|
| 732 |
|
|
|
| 733 |
|
|
let t = Types.descr (Syntax.make_type (Syntax.parse "[_*]")) in
|
| 734 |
|
|
Patterns.NF.show Format.std_formatter 0 t [ f "[((x::5)|_)*]" ];;
|
| 735 |
|
|
|
| 736 |
|
|
|
| 737 |
|
|
Patterns.NF.show Format.std_formatter 0 Types.any [ f "(x,y)"; f "(x,y)"];;
|
| 738 |
|
|
Patterns.NF.show Format.std_formatter 0 Types.any [ f "x"; f "y"];;
|
| 739 |
|
|
|
| 740 |
|
|
show [ "((x,_),_)"; "((_,x),_)" ];;
|
| 741 |
|
|
showt " [ (1 3?)* ]" [ " [(x::1 3?)*] " ];;
|
| 742 |
|
|
showt " [ (1 3?)* ]" [ " [(1 (x::3)?)*] " ];;
|
| 743 |
|
|
#install_printer Types.Print.print;;
|
| 744 |
|
|
#install_printer Types.Print.print_descr;;
|
| 745 |
|
|
let (t,[p1;p2]) = Patterns.NF.get 5;;
|
| 746 |
|
|
*)
|
| 747 |
abate |
39 |
|
| 748 |
|
|
|