1: # 30 "./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: open Flx_maps
20:
21: exception OverloadKindError of range_srcref * string
22:
23: type overload_result =
24: int * (* index of function *)
25: btypecode_t * (* type of function signature *)
26: btypecode_t * (* type of function return *)
27: (int * btypecode_t) list * (* mgu *)
28: btypecode_t list (* ts *)
29:
30: type result =
31: | Unique of overload_result
32: | Fail
33:
34: let dfltvs_aux = { raw_type_constraint=`TYP_tuple []; raw_typeclass_reqs=[]}
35: let dfltvs = [],dfltvs_aux
36:
37:
38: let get_data table index : symbol_data_t =
39: try Hashtbl.find table index
40: with Not_found ->
41: failwith ("[Flx_lookup.get_data] No definition of <" ^ string_of_int index ^ ">")
42:
43: let sig_of_symdef symdef sr name i = match symdef with
44: | `SYMDEF_match_check (_)
45: -> `TYP_tuple[],`TYP_sum [`TYP_tuple[];`TYP_tuple[]] (* bool *)
46:
47: (* primitives *)
48: | `SYMDEF_fun (_,ps,r,_,_,_)
49: -> typeof_list ps,r
50:
51: | `SYMDEF_callback (_,ts_orig,r,_)
52: ->
53: let ts_f =
54: filter
55: (function
56: | `AST_name (_,id,[]) when id = name -> false
57: | t -> true
58: )
59: ts_orig
60: in
61: let tf_args = match ts_f with
62: | [x] -> x
63: | lst -> `TYP_tuple lst
64: in
65: let tf = `TYP_function (tf_args, r) in
66:
67: (* The type of the arguments Felix thinks the raw
68: C function has on a call. A closure of this
69: function is a Felix function .. NOT the raw
70: C function.
71: *)
72: let ts_cf =
73: map
74: (function
75: | `AST_name (_,id,[]) when id = name -> tf
76: | t -> t
77: )
78: ts_orig
79: in
80: typeof_list ts_cf,r
81:
82: | `SYMDEF_function (ps,r,_,_)
83: ->
84: let p = fst ps in
85: begin match p,r with
86: (*
87: | (`PRef,_, r)::tail,`AST_void _
88: (* | (`PVal,_,`TYP_pointer r)::tail,`AST_void _ *) ->
89: print_endline "Mangled Procedure Overload";
90: paramtype tail,r
91: *)
92:
93: | _ ->
94: paramtype p,r
95: end
96:
97: | `SYMDEF_cstruct ls
98: | `SYMDEF_struct ls ->
99: typeof_list (map snd ls),`AST_index (sr,name,i)
100:
101: | `SYMDEF_const_ctor (_,r,_,_) -> `AST_void sr,r
102: | `SYMDEF_nonconst_ctor (_,r,_,_,t) -> t,r
103: | `SYMDEF_type_alias t ->
104: begin match t with
105: | `TYP_typefun (ps,r,b) -> typeof_list (map snd ps),r
106: | `TYP_case _ -> `TYP_type,`TYP_type
107: | symdef ->
108: raise (OverloadKindError (sr,
109: "[sig_of_symdef] Expected "^
110: name
111: ^" to be a type function, got " ^
112: string_of_typecode t
113: ))
114: end
115:
116: | symdef ->
117: raise (OverloadKindError (sr,
118: "[sig_of_symdef] Expected "^
119: name
120: ^" to be function or procedure, got " ^
121: string_of_symdef symdef name dfltvs
122: ))
123:
124: let resolve syms i =
125: match get_data syms.dfns i with
126: {id=id; sr=sr;parent=parent;privmap=table;dirs=dirs;symdef=symdef} ->
127: let pvs,vs,{raw_type_constraint=con; raw_typeclass_reqs=rtcr} =
128: find_split_vs syms i
129: in
130: let t,r = sig_of_symdef symdef sr id i in
131: id,sr,parent,vs,pvs,con,rtcr,t,r
132:
133: let rec unravel_ret tin dts =
134: match tin with
135: | `BTYP_function (a,b) -> unravel_ret b (a::dts)
136: | _ -> rev dts
137:
138: let hack_name qn = match qn with
139: | `AST_name (sr,name,ts) -> `AST_name (sr,"_inst_"^name,ts)
140: | `AST_lookup (sr,(e,name,ts)) -> `AST_lookup (sr,(e,"_inst_"^name,ts))
141: | _ -> failwith "expected qn .."
142:
143: (* Note this bt must bind types in the base context *)
144: let consider syms bt luqn2 name
145: ({base_sym=i;spec_vs=spec_vs; sub_ts=sub_ts} as eeek)
146: input_ts arg_types call_sr
147: : overload_result option =
148: let bt sr t = bt sr i t in
149: let id,sr,p,base_vs,parent_vs,con,rtcr,base_domain,base_result = resolve syms i in
150:
151: (*
152: if length rtcr > 0 then begin
153: (*
154: print_endline (name ^" TYPECLASS INSTANCES REQUIRED (unbound): " ^
155: catmap "," string_of_qualified_name rtcr);
156: *)
157: iter
158: (fun qn -> let es,ts' = luqn2 i (hack_name qn) in
159: print_endline ("With ts = " ^ catmap "," string_of_typecode ts');
160: match es with
161: | `NonFunctionEntry _ -> print_endline "EXPECTED INSTANCES TO BE FUNCTION SET"
162: | `FunctionEntry es ->
163: print_endline ("Candidates " ^ catmap "," string_of_entry_kind es)
164: )
165: rtcr
166: end
167: ;
168: *)
169: (*
170: print_endline (id ^ "|-> " ^string_of_myentry syms.dfns eeek);
171: begin
172: print_endline ("PARENT VS=" ^ catmap "," (fun (s,i,_)->s^"<"^si i^">") parent_vs);
173: print_endline ("base VS=" ^ catmap "," (fun (s,i,_)->s^"<"^si i^">") base_vs);
174: print_endline ("sub TS=" ^ catmap "," (sbt syms.dfns) sub_ts);
175: print_endline ("spec VS=" ^ catmap "," (fun (s,i)->s^"<"^si i^">") spec_vs);
176: print_endline ("input TS=" ^ catmap "," (sbt syms.dfns) input_ts);
177: end
178: ;
179: *)
180: (* these are wrong .. ? or is it just shitty table?
181: or is the mismatch due to unresolved variables?
182: *)
183: if (length base_vs != length sub_ts) then
184: begin
185: print_endline "WARN: VS != SUB_TS";
186: print_endline (id ^ "|-> " ^string_of_myentry syms.dfns eeek);
187: print_endline ("PARENT VS=" ^ catmap "," (fun (s,i,_)->s^"<"^si i^">") parent_vs);
188: print_endline ("base VS=" ^ catmap "," (fun (s,i,_)->s^"<"^si i^">") base_vs);
189: print_endline ("sub TS=" ^ catmap "," (sbt syms.dfns) sub_ts);
190: print_endline ("spec VS=" ^ catmap "," (fun (s,i)->s^"<"^si i^">") spec_vs);
191: print_endline ("input TS=" ^ catmap "," (sbt syms.dfns) input_ts);
192: end
193: ;
194: (*
195: if (length spec_vs != length input_ts) then print_endline "WARN: SPEC_VS != INPUT_TS";
196: *)
197:
198: (* bind type in base context, then translate it to view context:
199: thus, base type variables are eliminated and specialisation
200: type variables introduced
201: *)
202: let spec t =
203: (*
204: print_endline ("specialise Base type " ^ sbt syms.dfns t);
205: *)
206: let n = length base_vs in
207: let ts = list_prefix sub_ts n in
208: let vs = map (fun (i,n,_) -> i,n) base_vs in
209: let t = tsubst vs ts t in
210: (*
211: print_endline ("to View type " ^ sbt syms.dfns t);
212: *)
213: t
214: in
215: let spec_bt sr t =
216: let t = bt sr t in
217: let t = spec t in
218: t
219: in
220:
221: let con = bt sr con in
222: let domain = bt sr base_domain in
223: let spec_domain = spec domain in
224: let spec_result =
225: try spec_bt sr base_result
226: with _ -> clierr sr "Failed to bind candidate return type!"
227: in
228: (*
229: print_endline ("BASE Return type of function " ^ id^ "<"^si i^">=" ^ sbt syms.dfns spec_result);
230: *)
231:
232: (* unravel function a->b->c->d->..->z into domains a,b,c,..y
233: to match curry argument list
234: *)
235: let curry_domains =
236: try unravel_ret spec_result []
237: with _ -> print_endline "Failed to unravel candidate return type!"; []
238: in
239: let curry_domains = spec_domain :: curry_domains in
240:
241: (*
242: print_endline ("Argument sigs= " ^ catmap "->" (sbt syms.dfns) arg_types);
243: print_endline ("Candidate sigs= " ^ catmap "->" (sbt syms.dfns) curry_domains);
244: *)
245: (*
246: if con <> `BTYP_tuple [] then
247: print_endline ("type constraint (for "^name^") = " ^ sbt syms.dfns con)
248: ;
249: *)
250: (*
251: We need to attempt to find assignments for spec_vs which
252: unify the specialised function signature(s) with arguments.
253:
254: To do this we match up:
255:
256: (a) spec vs variables with input ts values
257: (b) signatures with arguments
258:
259: which hopefully produces mgu with all the spec_vs variables
260:
261: If this succeeds, we plug these into the sub_ts to get
262: assignments for base_vs, eliminating the spec vs and
263: base vs variables. The parent variables must not be
264: eliminated since they act like constants (constructors).
265:
266: The resulting ts is then returned, it may contain variables
267: from the calling context.
268:
269: There is a twist: a polymorphic function calling itself.
270: In that case the variables in the calling context
271: can be the same as the base variables of the called
272: function, but they have to be treated like constants.
273: for example here:
274:
275: fun f[t] ... => .... f[g t]
276:
277: the 't' in f[g t] has to be treated like a constant.
278:
279: So the base_vs variables are renamed in the
280: function signature where they're dependent.
281:
282: The spec vs variables don't need renaming
283: because they're anonymous.
284:
285: Note that the base_vs variables are eliminated
286: from the signature .. so the renaming is pointless!
287:
288:
289: *)
290: (* Step1: make equations for the ts *)
291:
292: let n_parent_vs = length parent_vs in
293: let n_base_vs = length base_vs in
294: let n_spec_vs = length spec_vs in
295: let n_sub_ts = length sub_ts in
296: let n_input_ts = length input_ts in
297:
298: (* equations for user specified assignments *)
299: let lhsi = map (fun (n,i) -> i) spec_vs in
300: let lhs = map (fun (n,i) -> `BTYP_var ((i),`BTYP_type 0)) spec_vs in
301: let n = min n_spec_vs n_input_ts in
302: let eqns = combine (list_prefix lhs n) (list_prefix input_ts n) in
303:
304: (* these are used for early substitution *)
305: let eqnsi = combine (list_prefix lhsi n) (list_prefix input_ts n) in
306:
307: (*
308: print_endline "TS EQUATIONS ARE:";
309: iter (fun (t1,t2) -> print_endline (sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2))
310: eqns
311: ;
312: *)
313:
314: (*
315: print_endline ("Curry domains (presub) = " ^ catmap ", " (sbt syms.dfns) curry_domains);
316: *)
317: let curry_domains = map (fun t -> list_subst eqnsi t) curry_domains in
318:
319: (*
320: print_endline ("Curry domains (postsub) = " ^ catmap ", " (sbt syms.dfns) curry_domains);
321: *)
322:
323: let curry_domains = map (fun t -> reduce_type (beta_reduce syms sr t)) curry_domains in
324:
325: (*
326: print_endline ("Curry domains (postbeta) = " ^ catmap ", " (sbt syms.dfns) curry_domains);
327: *)
328:
329: let n = min (length curry_domains) (length arg_types) in
330: let eqns = eqns @ combine (list_prefix curry_domains n) (list_prefix arg_types n) in
331:
332: let dvars = ref IntSet.empty in
333: iter (fun (_,i)-> dvars := IntSet.add i !dvars) spec_vs;
334:
335: (*
336: print_endline "EQUATIONS ARE:";
337: iter (fun (t1,t2) -> print_endline (sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2))
338: eqns
339: ;
340: *)
341: (*
342: (* WRONG!! dunno why, but it is! *)
343: print_endline ("DEPENDENT VARIABLES ARE " ^ catmap "," si
344: (IntSet.fold (fun i l-> i::l) !dvars [])
345: );
346: print_endline "...";
347: *)
348:
349: let mgu = maybe_specialisation syms.dfns eqns in
350: (*
351: (* doesn't work .. fails to solve for some vars
352: which aren't local vs of the fun .. this case:
353:
354: fun g2[w with Eq[w,w]] (x:int,y:int)=> xeq(x,y);
355:
356: doesn't solve for w checking xeq(x,y) .. not
357: sure why it should tho .. w should be fixed
358: already by the instance match .. hmm ..
359: *)
360: let mgu =
361: try Some (unification true syms.dfns eqns !dvars)
362: with Not_found -> None
363: in
364: *)
365: match mgu with
366: | Some mgu ->
367: (*
368: print_endline "Specialisation detected";
369: print_endline (" .. mgu = " ^ string_of_varlist syms.dfns mgu);
370: *)
371: let mgu = ref mgu in
372: (* each universally quantified variable must be fixed
373: by the mgu .. if it doesn't its an error .. hmmm
374:
375: THIS CANNOT HAPPEN NOW!
376: JS: 13/3/2006 .. oh yes it can!
377:
378: *)
379: (* Below algorithm is changed! We now make list
380: of unresolved dependent variables, and see
381: if the constraint resolution can help.
382: Actually, at this point, we can even try
383: to see if the return type can help
384: *)
385:
386: (*
387: print_endline "Check for unresolved";
388: *)
389: let unresolved = ref (
390: fold_left2
391: (fun acc (s,i) k ->
392: if not (mem_assoc i !mgu) then (s,i,`TYP_type,k)::acc else acc
393: )
394: [] spec_vs (nlist n_spec_vs)
395: )
396: in
397:
398: let th i = match i with
399: | 0 -> "first"
400: | 1 -> "second"
401: | 2 -> "third"
402: | _ -> si (i+1) ^ "'th"
403: in
404:
405: let report_unresolved =
406: (*
407: let maybe_tp tp = match tp with
408: | `TPAT_any -> ""
409: | tp -> ": " ^ string_of_tpattern tp
410: in
411: *)
412: let maybe_tp tp = match tp with
413: | `AST_patany _ -> ""
414: | tp -> ": " ^ string_of_typecode tp
415: in
416: fold_left (fun acc (s,i,tp,k) -> acc ^
417: " The " ^th k ^" subscript " ^ s ^ "["^si i^"]" ^
418: maybe_tp tp ^ "\n"
419: ) "" !unresolved
420: in
421: (*
422: if length !unresolved > 0 then
423: print_endline (
424: "WARNING: experimental feature coming up\n" ^
425: "Below would be an error, but we try now to do more work\n" ^
426: (* clierr call_sr ( *)
427: "[resolve_overload] In application of " ^ id ^
428: " cannot resolve:\n" ^
429: report_unresolved ^
430: "Try using explicit subscript" ^
431: "\nMost General Unifier(mgu)=\n" ^ string_of_varlist syms.dfns !mgu
432: )
433: ;
434: *)
435: (*
436: if length !unresolved > 0 then None else
437: *)
438:
439: (* HACKERY to try to get more values from type patterns*)
440: (*
441: if length !unresolved > 0 then
442: *)
443: begin
444: (* convert mgu from spec vars to base vars *)
445: let basemap = map2 (fun (_,i,_) t -> i,list_subst !mgu t) base_vs sub_ts in
446: (*
447: print_endline ("New basemap: " ^ catmap ","
448: (fun (i,t) -> si i ^ "->" ^ sbt syms.dfns t)
449: basemap
450: );
451: *)
452:
453: let extra_eqns = ref [] in
454: let dvars = ref IntSet.empty in
455: iter (fun (_,i)->
456: if not (mem_assoc i !mgu) then (* mgu vars get eliminated *)
457: dvars := IntSet.add i !dvars
458: )
459: spec_vs;
460:
461: iter (fun (s,j',tp) ->
462: let et,explicit_vars1,any_vars1, as_vars1, eqns1 =
463: type_of_tpattern syms tp
464: in
465: let et = spec_bt sr et in
466: let et = list_subst !mgu et in
467: let et = beta_reduce syms sr et in
468: (*
469: print_endline ("After substitution of mgu, Reduced type is:\n " ^
470: sbt syms.dfns et)
471: ;
472: *)
473:
474: (* tp is a metatype .. it could be a pattern-like thing, which is
475: a constraint. But it could also be an actual meta-type! In that
476: case it is a constraint too, but not the right kind of constraint.
477: EG in
478:
479: j' -> fun (x:TYPE):TYPE=>x : TYPE->TYP
480:
481: the TYPE->TYPE is a constraint only in the sense that it
482: is the type of j'. Felix messes these things up.. you can
483: give an explicit TYPE->TYPE which really amounts only
484: to a typing constraint .. and no additional constraint.
485:
486: So we have to eliminate these from consideration
487:
488: *)
489:
490: (*
491: print_endline ("Analysing "^s^"<"^si j'^">: " ^ string_of_typecode tp);
492: print_endline (si j' ^ (if mem_assoc j' basemap then " IS IN BASEMAP" else " IS NOT IN BASEMAP"));
493: *)
494: (* this check is redundant .. we're SCANNING the base vs! *)
495: match et with
496: | `BTYP_type _
497: | `BTYP_function _ -> () (* print_endline "ignoring whole metatype" *)
498: | _ ->
499: if mem_assoc j' basemap then begin
500: let t1 = assoc j' basemap in
501: let t2 = et in
502: (*
503: print_endline ("CONSTRAINT: Adding equation " ^ sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2);
504: *)
505: extra_eqns := (t1,t2) :: !extra_eqns
506: end
507: ;
508:
509: (* THIS CODE DOES NOT WORK RIGHT YET *)
510: if length explicit_vars1 > 0 then
511: print_endline ("Explicit ?variables: " ^
512: catmap "," (fun (i,s) -> s ^ "<" ^ si i ^ ">") explicit_vars1)
513: ;
514: iter
515: (fun (i,s) ->
516: let coupled = filter (fun (s',_,_) -> s = s') base_vs in
517: match coupled with
518: | [] -> ()
519: | [s',k,pat] ->
520: print_endline (
521: "Coupled " ^ s ^ ": " ^ si k ^ "(vs var) <--> " ^ si i ^" (pat var)" ^
522: " pat=" ^ string_of_typecode pat);
523: let t1 = `BTYP_var (i,`BTYP_type 0) in
524: let t2 = `BTYP_var (k,`BTYP_type 0) in
525: print_endline ("Adding equation " ^ sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2);
526: extra_eqns := (t1,t2) :: !extra_eqns;
527: (*
528: dvars := IntSet.add i !dvars;
529: print_endline ("ADDING DEPENDENT VARIABLE " ^ si i);
530: *)
531:
532: | _ -> assert false (* vs should have distinct names *)
533: )
534: explicit_vars1
535: ;
536:
537: if length as_vars1 > 0 then begin
538: print_endline ("As variables: " ^
539: catmap "," (fun (i,s) -> s ^ "<" ^ si i ^ ">") as_vars1)
540: ;
541: print_endline "RECURSIVE?? AS VARS NOT HANDLED YET"
542: end;
543:
544: (*
545: if length any_vars1 > 0 then
546: print_endline ("Wildcard variables: " ^
547: catmap "," (fun i -> "<" ^ si i ^ ">") any_vars1)
548: ;
549: *)
550:
551: (* add wildcards to dependent variable set ?? *)
552: iter (fun i-> dvars := IntSet.add i !dvars) any_vars1;
553:
554: (* add 'as' equations from patterns like
555: t as v
556: *)
557: iter (fun (i,t) -> let t2 = bt sr t in
558: let t1 = `BTYP_var (i,`BTYP_type 0) in
559: extra_eqns := (t1,t2) :: !extra_eqns
560: ) eqns1;
561:
562: (*
563: if length eqns1 > 0 then
564: print_endline ("Equations for as terms (unbound): " ^
565: catmap "\n" (fun (i,t) -> si i ^ " -> " ^ string_of_typecode t) eqns1)
566: ;
567: *)
568: )
569: base_vs
570: ;
571:
572: (* NOW A SUPER HACK! *)
573: let rec xcons con = match con with
574: | `BTYP_intersect cons -> iter xcons cons
575: | `BTYP_type_match (arg,[{pattern=pat},`BTYP_tuple[]]) ->
576: let arg = spec arg in
577: let arg = list_subst !mgu arg in
578: let arg = beta_reduce syms sr arg in
579: let pat = spec pat in
580: let pat = list_subst !mgu pat in
581: let pat = beta_reduce syms sr pat in
582: extra_eqns := (arg, pat)::!extra_eqns
583: | _ -> ()
584: in
585: xcons con;
586:
587: (*
588: print_endline "UNIFICATION STAGE 2";
589: print_endline "EQUATIONS ARE:";
590: iter (fun (t1,t2) -> print_endline (sbt syms.dfns t1 ^ " = " ^ sbt syms.dfns t2))
591: !extra_eqns
592: ;
593: print_endline "...";
594: print_endline ("DEPENDENT VARIABLES ARE " ^ catmap "," si
595: (IntSet.fold (fun i l-> i::l) !dvars [])
596: );
597: *)
598: let maybe_extra_mgu =
599: try Some (unification false syms.dfns !extra_eqns !dvars)
600: with Not_found -> None
601: in
602: match maybe_extra_mgu with
603: | None -> () (* print_endline "COULDN'T RESOLVE EQUATIONS" *)
604: | Some extra_mgu ->
605: (*
606: print_endline ("Resolved equations with mgu:\n " ^
607: string_of_varlist syms.dfns extra_mgu)
608: ;
609: *)
610: let ur = !unresolved in
611: unresolved := [];
612: iter (fun ((s,i,_,k) as u) ->
613: (*
614: let j = base + k in
615: *)
616: let j = i in
617: if mem_assoc j extra_mgu
618: then begin
619: let t = assoc j extra_mgu in
620: (*
621: print_endline ("CAN NOW RESOLVE " ^
622: th k ^ " vs term " ^ s ^ "<"^ si i^"> ---> " ^ sbt syms.dfns t)
623: ;
624: *)
625: mgu := (j,t) :: !mgu
626: end
627: else begin
628: (*
629: print_endline ("STILL CANNOT RESOLVE " ^ th k ^ " vs term " ^ s ^ "<"^si i^">");
630: *)
631: unresolved := u :: !unresolved
632: end
633: )
634: ur
635: end
636: ;
637:
638:
639: if length !unresolved > 0 then None else begin
640: let ok = ref true in
641: iter
642: (fun sign ->
643: if sign <> list_subst !mgu sign then
644: begin
645: ok := false;
646: (*
647: print_endline ("At " ^ short_string_of_src call_sr);
648: (*
649: clierr call_sr
650: *)
651: print_endline
652: (
653: "[resolve_overload] Unification of function " ^
654: id ^ "<" ^ si i ^ "> signature " ^
655: sbt syms.dfns domain ^
656: "\nwith argument type " ^ sbt syms.dfns sign ^
657: "\nhas mgu " ^ string_of_varlist syms.dfns !mgu ^
658: "\nwhich specialises a variable of the argument type"
659: )
660: *)
661: end
662: )
663: arg_types
664: ;
665: if not (!ok) then None else
666: (*
667: print_endline ("Matched with mgu = " ^ string_of_varlist syms.dfns !mgu);
668: *)
669: (* RIGHT! *)
670: (*
671: let ts = map (fun i -> assoc (base+i) !mgu) (nlist (m+k)) in
672: *)
673: (* The above ts is for plugging into the view, but we
674: have to return the elements to plug into the base
675: vs list, this is the sub_ts with the above ts plugged in,
676: substituting away the view vs
677: *)
678:
679: let base_ts = map (list_subst !mgu) sub_ts in
680:
681: (*
682: print_endline ("Matched candidate " ^ si i ^ "\n" ^
683: ", spec domain=" ^ sbt syms.dfns spec_domain ^"\n" ^
684: ", base domain=" ^ sbt syms.dfns domain ^"\n" ^
685: ", return=" ^ sbt syms.dfns spec_result ^"\n" ^
686: ", mgu=" ^ string_of_varlist syms.dfns !mgu ^ "\n" ^
687: ", ts=" ^ catmap ", " (sbt syms.dfns) base_ts
688: );
689: *)
690:
691: (* we need to check the type constraint, it uses the
692: raw vs type variable indicies. We need to substitute
693: in the corresponding ts values. First we need to build
694: a map of the correspondence
695: *)
696: let parent_ts = map (fun (n,i,_) -> `BTYP_var ((i),`BTYP_type 0)) parent_vs in
697: let type_constraint = build_type_constraints syms (bt sr) sr base_vs in
698: let type_constraint = `BTYP_intersect [type_constraint; con] in
699: (*
700: print_endline ("Raw type constraint " ^ sbt syms.dfns type_constraint);
701: *)
702: let vs = map (fun (s,i,_)-> s,i) base_vs in
703: let type_constraint = tsubst vs base_ts type_constraint in
704: (*
705: print_endline ("Substituted type constraint " ^ sbt syms.dfns type_constraint);
706: *)
707: let reduced_constraint = beta_reduce syms sr type_constraint in
708: (*
709: print_endline ("Reduced type constraint " ^ sbt syms.dfns reduced_constraint);
710: *)
711: begin match reduced_constraint with
712: | `BTYP_void ->
713: (*
714: print_endline "Constraint failure, rejecting candidate";
715: *)
716: None
717: | `BTYP_tuple [] ->
718: let parent_ts = map (fun (n,i,_) -> `BTYP_var ((i),`BTYP_type 0)) parent_vs in
719: Some (i,domain,spec_result,!mgu,parent_ts @ base_ts)
720:
721: | _ ->
722: clierr sr
723: ("[overload] Cannot resolve type constraint! " ^
724: sbt syms.dfns type_constraint
725: )
726: end
727: end
728:
729: | None ->
730: (*
731: print_endline "No match";
732: *)
733: None
734:
735: let overload
736: syms
737: bt
738: luqn2
739: call_sr
740: (fs : entry_kind_t list)
741: (name: string)
742: (sufs : btypecode_t list)
743: (ts:btypecode_t list)
744: :
745: overload_result option
746: =
747: (*
748: print_endline ("Overload " ^ name);
749: print_endline ("Argument sigs are " ^ catmap ", " (sbt syms.dfns) sufs);
750: print_endline ("Candidates are " ^ catmap "," (string_of_entry_kind) fs);
751: print_endline ("Input ts = " ^ catmap ", " (sbt syms.dfns) ts);
752: *)
753: (* HACK for the moment *)
754: let aux i =
755: match consider syms bt luqn2 name i ts sufs call_sr with
756: | Some x -> Unique x
757: | None -> Fail
758: in
759: let fun_defs = List.map aux fs in
760: let candidates =
761: List.filter
762: (fun result -> match result with
763: | Unique _ -> true
764: | Fail -> false
765: )
766: fun_defs
767: in
768: (*
769: print_endline "Got matching candidates .. ";
770: *)
771: (* start with an empty list, and fold one result
772: at a time into it, as follows: if one element
773: of the list is greater (more general) than the candidate,
774: then add the candidate to the list and remove all
775: element greater than the candidate,
776:
777: otherwise, if one element of the list is less then
778: the candidate, keep the list and discard the candidate.
779:
780: The list starts off empty, so that all elements in
781: it are vacuously incomparable. It follows either
782: the candidate is not less than all the list,
783: or not less than all the list: that is, there cannot
784: be two element a,b such that a < c < b, since by
785: transitivity a < c would follow, contradicting
786: the assumption the list contains no ordered pairs.
787:
788: If in case 1, all the greater element are removed and c added,
789: all the elements must be less or not comparable to c,
790: thus the list remains without comparable pairs,
791: otherwise in case 2, the list is retained and c discarded
792: and so trivially remains unordered.
793:
794: *)
795:
796: let candidates = fold_left
797: (fun oc r ->
798: match r with Unique (j,c,_,_,_) ->
799: (*
800: print_endline ("Considering candidate sig " ^ sbt syms.dfns c);
801: *)
802: let rec aux lhs rhs =
803: match rhs with
804: | [] ->
805: (*
806: print_endline "return elements plus candidate";
807: *)
808: r::lhs (* return all non-greater elements plus candidate *)
809: | (Unique(i,typ,rtyp,mgu,ts) as x)::t
810: ->
811: (*
812: print_endline (" .. comparing with " ^ sbt syms.dfns typ);
813: *)
814: begin match compare_sigs syms.dfns typ c with
815: | `Less ->
816: (*
817: print_endline "Candidate is more general, discard it, retain whole list";
818: *)
819: lhs @ rhs (* keep whole list, discard c *)
820: | `Equal ->
821: (* same function .. *)
822: if i = j then aux lhs t else
823: let sr = match Hashtbl.find syms.dfns i with {sr=sr} -> sr in
824: let sr2 = match Hashtbl.find syms.dfns j with {sr=sr} -> sr in
825: clierrn [call_sr; sr2; sr]
826: (
827: "[resolve_overload] Ambiguous call: Not expecting equal signatures" ^
828: "\n(1) fun " ^ si i^ ":" ^ sbt syms.dfns typ ^
829: "\n(2) fun " ^ si j^ ":"^ sbt syms.dfns c
830: )
831:
832: | `Greater ->
833: (*
834: print_endline "Candidate is less general: discard this element";
835: *)
836: aux lhs t (* discard greater element *)
837: | `Incomparable ->
838: (*
839: print_endline "Candidate is comparable, retail element";
840: *)
841: aux (x::lhs) t (* keep element *)
842: end
843: | Fail::_ -> assert false
844: in aux [] oc
845: | Fail -> assert false
846: )
847: []
848: candidates in
849: match candidates with
850: | [Unique (i,t,rtyp,mgu,ts)] ->
851: (*
852: print_endline ("[overload] Got unique result " ^ si i);
853: *)
854: Some (i,t,rtyp,mgu,ts)
855:
856: | [] -> None
857: | _ ->
858: clierr call_sr
859: (
860: "Too many candidates match in overloading " ^ name ^
861: " with argument types " ^ catmap "," (sbt syms.dfns) sufs ^
862: "\nOf the matching candidates, the following are most specialised ones are incomparable\n" ^
863: catmap "\n" (function
864: | Unique (i,t,_,_,_) ->
865: qualified_name_of_index syms.dfns i ^ "<" ^ si i ^ "> sig " ^
866: sbt syms.dfns t
867: | Fail -> assert false
868: )
869: candidates
870: ^
871: "\nPerhaps you need to define a function more specialised than all these?"
872: )
873:
874: (* FINAL NOTE: THIS STILL WON'T BE ENOUGH: THE SEARCH ALGORITHM
875: NEEDS TO BE MODIFIED TO FIND **ALL** FUNCTIONS .. alternatively,
876: keep the results from overload resolution for each scope, and resubmit
877: in a deeper scope: then if there is a conflict between signatures
878: (equal or unordered) the closest is taken if that resolves the
879: conflict
880: *)
881:
882: