5.37. overload resolution

Start ocaml section to src/flx_overload.mli[1 /1 ]
     1: # 4 "./lpsrc/flx_overload.ipk"
     2: open Flx_ast
     3: open Flx_types
     4: open Flx_mtypes2
     5: 
     6: type overload_result =
     7:  int *  (* index of function *)
     8:  btypecode_t * (* type of function signature *)
     9:  btypecode_t * (* type of function return *)
    10:  (int * btypecode_t) list * (* mgu *)
    11:  btypecode_t list (* ts *)
    12: 
    13: val overload:
    14:   sym_state_t ->
    15:   (range_srcref  -> int -> typecode_t -> btypecode_t) ->
    16:   (int -> qualified_name_t -> entry_set_t * typecode_t list) ->
    17:   range_srcref ->
    18:   entry_kind_t list ->
    19:   string ->
    20:   btypecode_t list ->
    21:   btypecode_t list ->
    22:   overload_result option
    23: 
    24: exception OverloadKindError of range_srcref * string
    25: 
End ocaml section to src/flx_overload.mli[1]
Start ocaml section to src/flx_overload.ml[1 /1 ]
     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: 
End ocaml section to src/flx_overload.ml[1]