1: # 25 "./lpsrc/flx_overload.ipk"
2: open Flx_util
3: open Flx_ast
4: open Flx_types
5: open Flx_mtypes1
6: open Flx_mtypes2
7: open Flx_print
8: open Flx_exceptions
9: open Flx_typing
10: open Flx_typing2
11: open List
12: open Flx_srcref
13: open Flx_unify
14: open Flx_beta
15: open Flx_generic
16: open Flx_name
17: open Flx_tconstraint
18: open Flx_tpat
19:
20: type overload_result =
21: int * (* index of function *)
22: btypecode_t * (* type of function signature *)
23: (int * btypecode_t) list * (* mgu *)
24: btypecode_t list (* ts *)
25:
26: type result =
27: | Unique of overload_result
28: | Fail
29:
30:
31: let get_data table index : symbol_data_t =
32: try Hashtbl.find table index
33: with Not_found ->
34: failwith ("[Flx_lookup.get_data] No definition of <" ^ string_of_int index ^ ">")
35:
36: let sig_of_symdef symdef sr name i = match symdef with
37: | `SYMDEF_match_check (_)
38: -> `TYP_tuple[],`TYP_sum [`TYP_tuple[];`TYP_tuple[]] (* bool *)
39:
40: (* primitives *)
41: | `SYMDEF_fun (_,ps,r,_,_,_)
42: -> typeof_list ps,r
43:
44: | `SYMDEF_callback (_,ts_orig,r,_)
45: ->
46: let ts_f =
47: filter
48: (function
49: | `AST_name (_,id,[]) when id = name -> false
50: | t -> true
51: )
52: ts_orig
53: in
54: let tf_args = match ts_f with
55: | [x] -> x
56: | lst -> `TYP_tuple lst
57: in
58: let tf = `TYP_function (tf_args, r) in
59:
60: (* The type of the arguments Felix thinks the raw
61: C function has on a call. A closure of this
62: function is a Felix function .. NOT the raw
63: C function.
64: *)
65: let ts_cf =
66: map
67: (function
68: | `AST_name (_,id,[]) when id = name -> tf
69: | t -> t
70: )
71: ts_orig
72: in
73: typeof_list ts_cf,r
74:
75: | `SYMDEF_function (ps,r,_,_)
76: -> paramtype (fst ps),r
77:
78: | `SYMDEF_cstruct ls
79: | `SYMDEF_struct ls ->
80: typeof_list (map snd ls),`AST_index (sr,name,i)
81:
82: | `SYMDEF_const_ctor (_,r,_) -> `AST_void sr,r
83: | `SYMDEF_nonconst_ctor (_,r,_,t) -> t,r
84: | `SYMDEF_type_alias t ->
85: begin match t with
86: | `TYP_typefun (ps,r,b) -> typeof_list (map snd ps),r
87: | symdef ->
88: clierr sr (
89: "[sig_of_symdef] Expected "^
90: name
91: ^" to be a type function, got " ^
92: string_of_typecode t
93: )
94: end
95:
96: | symdef ->
97: clierr sr (
98: "[sig_of_symdef] Expected "^
99: name
100: ^" to be function or procedure, got " ^
101: string_of_symdef symdef name []
102: )
103:
104: let resolve syms i =
105: match get_data syms.dfns i with
106: {id=id; sr=sr;parent=parent;privmap=table;dirs=dirs;symdef=symdef} ->
107: let pvs,vs = find_split_vs syms i in
108: let t,r = sig_of_symdef symdef sr id i in
109: id,sr,parent,vs,pvs,t,r
110:
111: let rec unravel_ret tin dts =
112: match tin with
113: | `BTYP_function (a,b) -> unravel_ret b (a::dts)
114: | _ -> rev dts
115:
116: let consider syms bt i ts signs call_sr =
117: let bt sr t = bt sr i t in
118: let id,sr,p,vs,pvs,t,r = resolve syms i in
119: (*
120: print_endline ("Candidate "^si i^" sig is " ^ string_of_typecode t);
121: *)
122: let t = bt sr t in
123: let dms =
124: try unravel_ret (bt sr r) []
125: with _ -> print_endline "Failed to bind candidate return type!"; []
126: in
127: let tdms = t :: dms in
128:
129: (*
130: print_endline ("Argument sigs= " ^ catmap "->" (sbt syms.dfns) signs);
131: print_endline ("Candidate sigs= " ^ catmap "->" (sbt syms.dfns) tdms);
132: print_endline ("pvs = " ^ catmap ", " (fun (s,i,_) ->s ^ "=" ^ si i) pvs);
133: print_endline ("vs = " ^ catmap ", " (fun (s,i,_) ->s ^ "=" ^ si i) vs);
134: print_endline ("type constraint = " ^ sbt syms.dfns type_constraint);
135: *)
136: (* Here we have a parameter list vs of m type variables,
137: a signature type t, containing these variables,
138: and a list ts of type expressions of length n which are
139: bindings to first n of the m type variables.
140:
141: Because of recursion, it is possible the ts also
142: contain the type variables in vs, however, these
143: are quite distinct.
144:
145: To fix this problem we must 'alpha convert'
146: the type expression by replacing the vs variables
147: in t with fresh variables, and also assigning the
148: first n of these to the ts values.
149:
150: Matching requires a solution for all the fresh variables.
151: The return type must be converted to use the fresh variables,
152: and then the solution plugged in to eliminate them: any
153: remaining variables from the original vs list are actually
154: from the environment of a recursive function call
155: *)
156: (* Step1: make equations for the ts *)
157:
158: let k = length pvs in
159: let m = length vs in
160: let n = length ts in
161: (* This is actually NOT an error .. it should just
162: cause this candidate to be rejected
163: *)
164: (*
165: if n>m then clierr sr
166: (
167: "[overload] Overloading " ^ name ^
168: "\nToo many type subscripts for index "^si i^", expected " ^
169: si m ^ ", got:\n" ^
170: catmap "," (sbt syms.dfns) ts
171: )
172: ;
173: *)
174: if n>m then None else
175:
176: (* Currently, vs lists can only specify TYPE variables *)
177: let base = !(syms.counter) in
178: syms.counter := base + k + m;
179: let lhs = map (fun i -> `BTYP_var ((i+base),`BTYP_type)) (nlist (k + m)) in
180: let rhs = (map (fun (_,i,_) -> `BTYP_var (i,`BTYP_type)) pvs) @ ts in
181: let eqns = combine (list_prefix lhs (k+n)) rhs in
182:
183: (* Step 2: convert t to use variables 0 to m-1
184: instead of those in vs
185: *)
186: let bvs = map (fun (s,i,tp) -> s,i) (pvs @ vs) in
187: let tdms' = map (tsubst bvs lhs) tdms in
188: let rec rfld res x y = match x,y with
189: | [],_ | _,[] -> res
190: | h::t,h'::t' -> rfld ((h,h'):: res) t t'
191: in
192: let eqns = rfld eqns tdms' signs in
193: (*
194: let eqns = (t',sign) :: eqns in
195: *)
196: (*
197: print_endline "EQUATIONS ARE:";
198: iter (fun (t1,t2) -> print_endline (sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2))
199: eqns
200: ;
201: print_endline "...";
202: *)
203: let mgu = maybe_specialisation syms.dfns eqns in
204: (match mgu with
205: | Some mgu ->
206: let mgu = ref mgu in
207: (*
208: print_endline "Specialisation detected";
209: print_endline (" .. mgu = " ^ string_of_varlist syms.dfns mgu);
210: *)
211: (* each universally quantified variable must be fixed
212: by the mgu .. if it doesn't its an error .. hmmm
213:
214: THIS CANNOT HAPPEN NOW!
215: JS: 13/3/2006 .. oh yes it can!
216:
217: *)
218: (* Below algorithm is changed! We now make list
219: of unresolved dependent variables, and see
220: if the constraint resolution can help.
221: Actually, at this point, we can even try
222: to see if the return type can help
223: *)
224:
225: let unresolved = ref (
226: fold_left2
227: (fun acc (s,i,tp) k ->
228: if not (mem_assoc (k+base) !mgu) then (s,i,tp,k)::acc else acc
229: )
230: [] vs (nlist m)
231: )
232: in
233:
234: let th i = match i with
235: | 0 -> "first"
236: | 1 -> "second"
237: | 2 -> "third"
238: | _ -> si (i+1) ^ "'th"
239: in
240:
241: let report_unresolved =
242: let maybe_tp tp = match tp with
243: | `TPAT_any -> ""
244: | tp -> ": " ^ string_of_tpattern tp
245: in
246: fold_left (fun acc (s,i,tp,k) -> acc ^
247: " The " ^th k ^" subscript " ^ s ^ "["^si i^"]" ^
248: maybe_tp tp ^ "\n"
249: ) "" !unresolved
250: in
251: (*
252: if length !unresolved > 0 then
253: print_endline (
254: "WARNING: experimental feature coming up\n" ^
255: "Below would be an error, but we try now to do more work\n" ^
256: (* clierr call_sr ( *)
257: "[resolve_overload] In application of " ^ id ^
258: " cannot resolve:\n" ^
259: report_unresolved ^
260: "Try using explicit subscript" ^
261: "\nMost General Unifier(mgu)=\n" ^ string_of_varlist syms.dfns !mgu
262: )
263: ;
264: *)
265:
266: (* HACKERY to try to get more values from type patterns*)
267: if length !unresolved > 0 then
268: begin
269: let extra_eqns = ref [] in
270: let dvars = ref IntSet.empty in
271: (*
272: print_endline ("BASE=" ^ si base);
273: *)
274: let counter = ref 0 in
275: iter (fun (s,j',tp) ->
276: let et,explicit_vars1,any_vars1, as_vars1, eqns1 =
277: type_of_tpattern syms tp
278: in
279: let et = bt sr et in
280: let j = !counter + base in
281: incr counter;
282: (*
283: print_endline ("Analysing "^s^"<"^si j^">: " ^ string_of_tpattern tp);
284: print_endline (si j ^ (if mem_assoc j !mgu then " IS IN MGU" else " IS NOT IN MGU"));
285: *)
286: if mem_assoc j !mgu then begin
287: let t1 = assoc j !mgu in
288: let t2 = et in
289: (*
290: print_endline ("Adding equation " ^ sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2);
291: *)
292: extra_eqns := (t1,t2) :: !extra_eqns
293: end
294: ;
295: (*
296: print_endline ("Equivalen type is:\n " ^ sbt syms.dfns et);
297: *)
298:
299: let et = list_subst !mgu et in
300: let et = beta_reduce syms [] et in
301: (*
302: print_endline ("After substitution of mgu, Reduced type is:\n " ^
303: sbt syms.dfns et)
304: ;
305: *)
306: (*
307: if length explicit_vars1 > 0 then
308: print_endline ("Explicit ?variables: " ^
309: catmap "," (fun (i,s) -> s ^ "<" ^ si i ^ ">") explicit_vars1)
310: ;
311: *)
312: let pos_ix vs k =
313: let rec aux vs i = match vs with
314: | (_,k',_) :: tl -> if k = k' then i else aux tl (i+1)
315: | _ -> failwith "WOOPS not in vs list??"
316: in
317: aux vs 0
318: in
319: iter
320: (fun (i,s) ->
321: let coupled = filter (fun (s',_,_) -> s = s') vs in
322: match coupled with
323: | [] -> ()
324: | [s',k,pat] ->
325: (*
326: print_endline (
327: "Coupled " ^ s ^ ": " ^ si k ^ "(vs var) <--> " ^ si i ^" (pat var)" ^
328: " pat=" ^ string_of_tpattern pat);
329: *)
330: let q = pos_ix vs k in
331: (*
332: print_endline ("Position in vs list is " ^ si q);
333: *)
334: let q = q+base in
335: (*
336: print_endline ("Alpha converted index is " ^ si q);
337: *)
338: let t1 = `BTYP_var (i,`BTYP_type) in
339: let t2 = `BTYP_var (q,`BTYP_type) in
340: (*
341: print_endline ("Adding equation " ^ sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2);
342: *)
343: extra_eqns := (t1,t2) :: !extra_eqns;
344: dvars := IntSet.add i !dvars;
345: dvars := IntSet.add q !dvars;
346:
347: | _ -> assert false (* vs should have distinct names *)
348: )
349: explicit_vars1
350: ;
351: (*
352: if length as_vars1 > 0 then
353: print_endline ("As variables: " ^
354: catmap "," (fun (i,s) -> s ^ "<" ^ si i ^ ">") as_vars1)
355: ;
356: if length any_vars1 > 0 then
357: print_endline ("Wildcard variables: " ^
358: catmap "," (fun i -> "<" ^ si i ^ ">") any_vars1)
359: ;
360: if length eqns1 > 0 then
361: print_endline ("Equations for as terms (unbound): " ^
362: catmap "\n" (fun (i,t) -> si i ^ " -> " ^ string_of_typecode t) eqns1)
363: ;
364: *)
365: )
366: vs
367: ;
368: let maybe_extra_mgu =
369: try Some (unification false syms.dfns !extra_eqns !dvars)
370: with Not_found -> None
371: in
372: match maybe_extra_mgu with
373: | None -> () (* print_endline "COULDN'T RESOLVE EQUATIONS" *)
374: | Some extra_mgu ->
375: (*
376: print_endline ("Resolved equations with mgu:\n " ^
377: string_of_varlist syms.dfns extra_mgu)
378: ;
379: *)
380: let ur = !unresolved in
381: unresolved := [];
382: iter (fun ((s,i,_,k) as u) ->
383: let j = base + k in
384: if mem_assoc j extra_mgu
385: then begin
386: let t = assoc j extra_mgu in
387: (*
388: print_endline ("CAN NOW RESOLVE " ^
389: th k ^ " vs term " ^ s ^ "<"^ si i^"> ---> " ^ sbt syms.dfns t)
390: ;
391: *)
392: mgu := (j,t) :: !mgu
393: end
394: else begin
395: (*
396: print_endline ("STILL CANNOT RESOLVE " ^ th k ^ " vs term " ^ s ^ "<"^si i^">");
397: *)
398: unresolved := u :: !unresolved
399: end
400: )
401: ur
402: end
403: ;
404:
405:
406: if length !unresolved > 0 then None else begin
407:
408:
409:
410: iter
411: (fun sign ->
412: if sign <> list_subst !mgu sign then
413: clierr call_sr
414: (
415: "[resolve_overload] Unification of function " ^
416: id ^ "<" ^ si i ^ "> signature " ^
417: sbt syms.dfns t ^
418: "\nwith argument type " ^ sbt syms.dfns sign ^
419: "\nhas mgu " ^ string_of_varlist syms.dfns !mgu ^
420: "\nwhich specialises a variable of the argument type"
421: )
422: )
423: signs
424: ;
425: (*
426: print_endline ("Matched with mgu = " ^ string_of_varlist syms.dfns !mgu);
427: *)
428: (* RIGHT! *)
429: let ts = map (fun i -> assoc (base+i) !mgu) (nlist (m+k)) in
430:
431: (*
432: print_endline ("Matched candidate " ^ si i ^
433: " mgu=" ^ string_of_varlist syms.dfns !mgu ^
434: ", ts=" ^ catmap ", " (sbt syms.dfns) ts
435: );
436: *)
437:
438: (* we need to check the type constraint, it uses the
439: raw vs type variable indicies. We need to substitute
440: in the corresponding ts values. First we need to build
441: a map of the correspondence
442: *)
443:
444: assert (length bvs = length ts);
445: let type_constraint = build_type_constraints syms (bt sr) sr vs in
446: let type_constraint = tsubst bvs ts type_constraint in
447: (*
448: print_endline ("Substituted type constraint " ^ sbt syms.dfns type_constraint);
449: *)
450: let reduced_constraint = beta_reduce syms [] type_constraint in
451: (*
452: print_endline ("Reduced type constraint " ^ sbt syms.dfns reduced_constraint);
453: *)
454: begin match reduced_constraint with
455: | `BTYP_void ->
456: (*
457: print_endline "Constraint failure, rejecting candidate";
458: *)
459: None
460: | `BTYP_tuple [] -> Some (i,t,!mgu,ts)
461: | _ ->
462: clierr sr
463: ("[overload] Cannot resolve type constraint! " ^
464: sbt syms.dfns type_constraint
465: )
466: end
467: end
468:
469: | None ->
470: (*
471: print_endline "No match";
472: *)
473: None
474: )
475:
476: let overload
477: syms
478: bt
479: call_sr
480: (fs : entry_kind_t list)
481: (name: string)
482: (sufs : btypecode_t list)
483: (ts:btypecode_t list)
484: : (entry_kind_t * btypecode_t * (int * btypecode_t) list * btypecode_t list) option =
485:
486: (*
487: print_endline ("Argument sigs are " ^ catmap ", " (sbt syms.dfns) sufs);
488: print_endline ("Candidates are " ^ catmap "," (string_of_entry_kind) fs);
489: print_endline ("Input ts = " ^ catmap ", " (sbt syms.dfns) ts);
490: *)
491: (* HACK for the moment *)
492: let rec aux i =
493: match consider syms bt i ts sufs call_sr with
494: | Some x -> Unique x
495: | None -> Fail
496: in
497: let fun_defs = List.map aux fs in
498: let candidates =
499: List.filter
500: (fun result -> match result with
501: | Unique _ -> true
502: | Fail -> false
503: )
504: fun_defs
505: in
506: (*
507: print_endline "Got matching candidates .. ";
508: *)
509: (* start with an empty list, and fold one result
510: at a time into it, as follows: if one element
511: of the list is greater (more general) than the candidate,
512: then add the candidate to the list and remove all
513: element greater than the candidate,
514:
515: otherwise, if one element of the list is less then
516: the candidate, keep the list and discard the candidate.
517:
518: The list starts off empty, so that all elements in
519: it are vacuously incomparable. It follows either
520: the candidate is not less than all the list,
521: or not less than all the list: that is, there cannot
522: be two element a,b such that a < c < b, since by
523: transitivity a < c would follow, contradicting
524: the assumption the list contains no ordered pairs.
525:
526: If in case 1, all the greater element are removed and c added,
527: all the elements must be less or not comparable to c,
528: thus the list remains without comparable pairs,
529: otherwise in case 2, the list is retained and c discarded
530: and so trivially remains unordered.
531:
532: *)
533:
534: let candidates = fold_left
535: (fun oc r ->
536: match r with Unique (j,c,_,_) ->
537: (*
538: print_endline ("Considering candidate sig " ^ sbt syms.dfns c);
539: *)
540: let rec aux lhs rhs =
541: match rhs with
542: | [] ->
543: (*
544: print_endline "return elements plus candidate";
545: *)
546: r::lhs (* return all non-greater elements plus candidate *)
547: | (Unique(i,typ,mgu,ts) as x)::t
548: ->
549: (*
550: print_endline (" .. comparing with " ^ sbt syms.dfns typ);
551: *)
552: begin match compare_sigs syms.dfns typ c with
553: | `Less ->
554: (*
555: print_endline "Candidate is more general, discard it, retain whole list";
556: *)
557: lhs @ rhs (* keep whole list, discard c *)
558: | `Equal ->
559: let sr = match Hashtbl.find syms.dfns i with {sr=sr} -> sr in
560: let sr2 = match Hashtbl.find syms.dfns j with {sr=sr} -> sr in
561: clierrn [call_sr; sr2; sr]
562: (
563: "[resolve_overload] Ambiguous call: Not expecting equal signatures" ^
564: "\n(1) " ^ sbt syms.dfns typ ^
565: "\n(2) " ^ sbt syms.dfns c
566: )
567:
568: | `Greater ->
569: (*
570: print_endline "Candidate is less general: discard this element";
571: *)
572: aux lhs t (* discard greater element *)
573: | `Incomparable ->
574: (*
575: print_endline "Candidate is comparable, retail element";
576: *)
577: aux (x::lhs) t (* keep element *)
578: end
579: | Fail::_ -> assert false
580: in aux [] oc
581: | Fail -> assert false
582: )
583: []
584: candidates in
585: match candidates with
586: | [Unique (i,t,mgu,ts)] ->
587: (*
588: print_endline ("[overload] Got unique result " ^ si i);
589: *)
590: Some (i,t,mgu,ts)
591:
592: | [] -> None
593: | _ ->
594: clierr call_sr
595: (
596: "Too many candidates match in overloading " ^ name ^
597: " with argument types " ^ catmap "," (sbt syms.dfns) sufs ^
598: "\nOf the matching candidates, the following are most specialised ones are incomparable\n" ^
599: catmap "\n" (function
600: | Unique (i,t,_,_) ->
601: qualified_name_of_index syms.dfns i ^ "<" ^ si i ^ "> sig " ^
602: sbt syms.dfns t
603: | Fail -> assert false
604: )
605: candidates
606: ^
607: "\nPerhaps you need to define a function more specialised than all these?"
608: )
609:
610: (* FINAL NOTE: THIS STILL WON'T BE ENOUGH: THE SEARCH ALGORITHM
611: NEEDS TO BE MODIFIED TO FIND **ALL** FUNCTIONS .. alternatively,
612: keep the results from overload resolution for each scope, and resubmit
613: in a deeper scope: then if there is a conflict between signatures
614: (equal or unordered) the closest is taken if that resolves the
615: conflict
616: *)
617:
618: