5.43. Typeclass checker

Start ocaml section to src/flx_typeclass.mli[1 /1 ]
     1: # 4 "./lpsrc/flx_typeclass.ipk"
     2: open Flx_ast
     3: open Flx_types
     4: open Flx_mtypes1
     5: open Flx_mtypes2
     6: open Flx_child
     7: 
     8: val typeclass_instance_check:
     9:   sym_state_t ->
    10:   fully_bound_symbol_table_t ->
    11:   child_map_t ->
    12:   unit
    13: 
    14: val fixup_typeclass_instance:
    15:   sym_state_t ->
    16:   fully_bound_symbol_table_t ->
    17:   int ->
    18:   btypecode_t list ->
    19:   int * btypecode_t list
    20: 
    21: val maybe_fixup_typeclass_instance:
    22:   sym_state_t ->
    23:   fully_bound_symbol_table_t ->
    24:   int ->
    25:   btypecode_t list ->
    26:   int * btypecode_t list
    27: 
    28: val fixup_typeclass_instances:
    29:   sym_state_t ->
    30:   fully_bound_symbol_table_t ->
    31:   unit
    32: 
    33: val tcinst_chk:
    34:   sym_state_t ->
    35:   bool ->
    36:   int ->
    37:   btypecode_t list ->
    38:   range_srcref ->
    39:   bvs_t * btypecode_t * btypecode_t list * int ->
    40:   (int * btypecode_t list) option
    41: 
End ocaml section to src/flx_typeclass.mli[1]
Start ocaml section to src/flx_typeclass.ml[1 /1 ]
     1: # 46 "./lpsrc/flx_typeclass.ipk"
     2: open Flx_util
     3: open Flx_ast
     4: open Flx_types
     5: open Flx_print
     6: open Flx_mtypes1
     7: open Flx_mtypes2
     8: open Flx_typing
     9: open Flx_mbind
    10: open Flx_srcref
    11: open List
    12: open Flx_unify
    13: open Flx_treg
    14: open Flx_generic
    15: open Flx_maps
    16: open Flx_exceptions
    17: open Flx_use
    18: open Flx_child
    19: open Flx_beta
    20: 
    21: let dummy_sr = "[typeclass] generated",0,0,0,0
    22: 
    23: let vs2ts vs = map (fun (s,i) -> `BTYP_var (i,`BTYP_type 0)) vs
    24: 
    25: (* drop first n elements of list l *)
    26: let rec drop l n =
    27:   if n = 0 then l else drop (tl l) (n-1)
    28: 
    29: let check_instance syms (bbdfns:fully_bound_symbol_table_t) (child_map:child_map_t)
    30:   (inst:int) (inst_id: string) inst_vs inst_constraint inst_sr inst_props tc inst_ts
    31: =
    32:   let tc_id, _, tc_sr, tc_entry = Hashtbl.find bbdfns tc in
    33:   match tc_entry with
    34:   | `BBDCL_typeclass (tc_props, tc_bvs) ->
    35:     (*
    36:     print_endline ("Found " ^ inst_id ^ "<"^si inst ^ ">" ^
    37:     "[" ^ catmap "," (sbt syms.dfns) inst_ts ^ "]" ^
    38:     " to be instance of typeclass " ^ tc_id ^ "<"^si tc^">")
    39:     ;
    40:     print_endline ("Typeclass vs = " ^
    41:       catmap "," (fun (s,j) -> s^"<"^si j^">") tc_bvs
    42:     );
    43:     *)
    44:     if length tc_bvs <> length inst_ts then
    45:       clierr2 inst_sr tc_sr
    46:       (
    47:         "Instance " ^
    48:         "["^catmap "," (fun (s,j) -> s^"<"^si j^">") inst_vs^"] " ^
    49:         inst_id ^"<"^ si inst^">"^
    50:         "[" ^ catmap "," (sbt syms.dfns) inst_ts ^ "]" ^
    51:         "\nsupplies wrong number of type arguments for typeclass parameters\n" ^
    52:         inst_id^"["^catmap "," (fun (s,j) -> s^"<"^si j^">") tc_bvs^"]"
    53:       )
    54:     ;
    55: 
    56:     let tc_kids = try Hashtbl.find child_map tc with Not_found -> [] in
    57:     let inst_kids = try Hashtbl.find child_map inst with Not_found -> [] in
    58:     (*
    59:     print_endline ("Typeclass kids " ^ catmap "," si tc_kids);
    60:     print_endline ("Instance kids " ^ catmap "," si inst_kids);
    61:     *)
    62:     let inst_map = fold_left (fun acc i->
    63:       let id,_,_,entry = Hashtbl.find bbdfns i in
    64:       match entry with
    65:       | `BBDCL_fun (_,bvs,params,ret,_,_,_) ->
    66:         let argt  : btypecode_t= typeoflist params in
    67:         let qt = bvs,`BTYP_function (argt,ret) in
    68:         (id,(i,qt)) :: acc
    69: 
    70:       | `BBDCL_proc (_,bvs,params,_,_) ->
    71:         let argt  : btypecode_t= typeoflist params in
    72:         let qt = bvs,`BTYP_function (argt,`BTYP_void) in
    73:         (id,(i,qt)) :: acc
    74: 
    75:       | `BBDCL_procedure (_,bvs,bps,_) ->
    76:         let argt : btypecode_t = typeoflist (typeofbps_traint bps) in
    77:         let qt = bvs,`BTYP_function (argt,`BTYP_void) in
    78:         (id,(i,qt)) :: acc
    79: 
    80:       | `BBDCL_function (_,bvs,bps,ret,_) ->
    81:         let argt : btypecode_t = typeoflist (typeofbps_traint bps) in
    82:         let qt = bvs,`BTYP_function (argt,ret) in
    83:         (id,(i,qt)) :: acc
    84: 
    85:       | _ -> acc
    86:       ) [] inst_kids
    87:     in
    88:     let check_binding force tck sr id tck_bvs tctype =
    89:       let entries = filter (fun (name,x) -> name = id) inst_map in
    90:       match entries with
    91:       | [] ->
    92:          if force then
    93:          clierr sr ("Cannot find typeclass virtual " ^ id ^ " in instance")
    94: 
    95:       | [_,(i,(inst_funbvs,t))] ->
    96:         let t = reduce_type t in
    97:         (*
    98:         print_endline ("Typeclass " ^ tc_id ^ "<" ^ si tc ^">" ^ print_bvs tc_bvs);
    99:         print_endline ("Typeclass function " ^ id ^ "<" ^ si tck ^ ">" ^
   100:           print_bvs tck_bvs ^ ":" ^ sbt syms.dfns tctype
   101:         );
   102: 
   103:         print_endline ("Instance vs = " ^ print_bvs inst_vs);
   104:         print_endline ("Instance ts = " ^ catmap "," (sbt syms.dfns) inst_ts);
   105:         print_endline ("Instance function " ^ id ^ "<"^si i^">" ^ print_bvs inst_funbvs ^
   106:         ":" ^ sbt syms.dfns t);
   107:         *)
   108: 
   109:         let tc_ptv = length tck_bvs - length tc_bvs in
   110:         (*
   111:         print_endline ("Typeclass fun has " ^ si tc_ptv ^ " private type variables");
   112:         *)
   113: 
   114:         let inst_ptv = length inst_funbvs - length inst_vs in
   115:         (*
   116:         print_endline ("Instance fun has " ^ si inst_ptv ^ " private type variables");
   117:         *)
   118: 
   119:         if inst_ptv <> tc_ptv then
   120:         clierr sr ("Wrong number of type parameters in instance fun!\n" ^
   121:           "Expected " ^ si tc_ptv ^ "\n" ^
   122:           "Got " ^ si inst_ptv
   123:         );
   124: 
   125:         let inst_funts = inst_ts @ vs2ts (drop inst_funbvs (length inst_vs)) in
   126: 
   127:         assert (length tck_bvs = length inst_funts);
   128: 
   129:         let tct = reduce_type (beta_reduce syms sr (tsubst tck_bvs inst_funts tctype)) in
   130:         (*
   131:         print_endline ("Typeclass function (instantiated) " ^ id ^ "<" ^ si tck ^ ">" ^
   132:           ":" ^ sbt syms.dfns tct
   133:         );
   134:         *)
   135: 
   136:         let matches =  tct = t in
   137:         if matches then
   138:           (*
   139:           print_endline "Matches!";
   140:           *)
   141:           ()
   142:         else begin
   143:           print_endline "Warning: Sole instance doesn't match virtual";
   144:           print_endline ("Typeclass " ^ tc_id ^ "<" ^ si tc ^">" ^ print_bvs tc_bvs);
   145:           print_endline ("Typeclass function " ^ id ^ "<" ^ si tck ^ ">" ^
   146:             print_bvs tck_bvs ^ ":" ^ sbt syms.dfns tctype
   147:           );
   148: 
   149:           print_endline ("Instance vs = " ^ print_bvs inst_vs);
   150:           print_endline ("Instance ts = " ^ catmap "," (sbt syms.dfns) inst_ts);
   151:           print_endline ("Instance function " ^ id ^ "<"^si i^">" ^ print_bvs inst_funbvs ^
   152:           ":" ^ sbt syms.dfns t);
   153:           print_endline ("Typeclass function (instantiated) " ^ id ^ "<" ^ si tck ^ ">" ^
   154:             ":" ^ sbt syms.dfns tct
   155:           );
   156:         end
   157:         ;
   158:         let old =
   159:           try Hashtbl.find syms.typeclass_to_instance tck
   160:           with Not_found -> []
   161:         in
   162:         let entry = inst_vs , inst_constraint, inst_ts , i in
   163:         if mem entry old then
   164:           clierr sr "Instance already registered??"
   165:         else
   166:           Hashtbl.replace syms.typeclass_to_instance tck (entry :: old);
   167: 
   168:         (*
   169:         print_endline ("Register mapping " ^ si tck ^ " vs=" ^
   170:           print_bvs inst_vs ^
   171:           " constraint=(" ^ sbt syms.dfns inst_constraint ^
   172:           ") ts=[" ^ catmap "," (sbt syms.dfns) inst_ts ^ "] -----> " ^ si i
   173:         );
   174:         *)
   175: 
   176:       | _ -> clierr sr ("Felix can't handle overloads in typeclass instances yet, " ^ id ^ " is overloaded")
   177:     in
   178:     iter
   179:     (fun tck ->
   180:       let tckid,tckparent,tcksr,tckentry = Hashtbl.find bbdfns tck in
   181:       match tckentry with
   182:       | `BBDCL_fun (props,bvs,params,ret,ct,breq,prec) ->
   183:         if ct == `Virtual then
   184:           let ft = `BTYP_function (typeoflist params,ret) in
   185:           check_binding true tck tcksr tckid bvs ft
   186:         (*
   187:         clierr tcksr "Typeclass requires virtual function";
   188:         *)
   189: 
   190:       | `BBDCL_proc (props,bvs,params,ct,breq) ->
   191:         if ct == `Virtual then
   192:           let ft = `BTYP_function (typeoflist params,`BTYP_void) in
   193:           check_binding true tck tcksr tckid bvs ft
   194:         (*
   195:         clierr tcksr "Typeclass requires virtual procedure";
   196:         *)
   197: 
   198:       | `BBDCL_function (props,bvs,bps,ret,_) when mem `Virtual props ->
   199:         let argt : btypecode_t = typeoflist (typeofbps_traint bps) in
   200:         let ft = `BTYP_function (argt,ret) in
   201:         check_binding false tck tcksr tckid bvs ft
   202: 
   203:       | `BBDCL_procedure (props, bvs, bps,_) when mem `Virtual props ->
   204:         let argt : btypecode_t = typeoflist (typeofbps_traint bps) in
   205:         let ft = `BTYP_function (argt,`BTYP_void) in
   206:         check_binding false tck tcksr tckid bvs ft
   207: 
   208: 
   209:       | `BBDCL_insert _ -> ()
   210:       | _ -> clierr tcksr "Typeclass entry must be virtual function or procedure"
   211:     )
   212:     tc_kids
   213: 
   214: 
   215:   | _ ->
   216:     clierr2 inst_sr tc_sr ("Expected " ^ inst_id ^ "<"^si inst ^ ">" ^
   217:     "[" ^ catmap "," (sbt syms.dfns) inst_ts ^ "]" ^
   218:     " to be typeclass instance, but" ^ tc_id ^ "<"^si tc^">, " ^
   219:     "is not a typeclass"
   220:     )
   221: 
   222: let typeclass_instance_check syms bbdfns child_map =
   223: Hashtbl.iter
   224: (fun i (id,_,sr,entry) -> match entry with
   225:   | `BBDCL_instance (props, vs, cons, tc, ts) ->
   226:      let iss =
   227:        try Hashtbl.find syms.instances_of_typeclass tc
   228:        with Not_found -> []
   229:      in
   230:      let entry = i,(vs,cons,ts) in
   231:      Hashtbl.replace syms.instances_of_typeclass tc (entry::iss);
   232:      check_instance syms bbdfns child_map i id vs cons sr props tc ts
   233: 
   234:   | _ -> ()
   235: )
   236: bbdfns
   237: 
   238: (* Notes.
   239: 
   240:   ts is the virtual function call ts, and generally doesn't
   241:   include any inst_vs (unless the call is INSIDE the instance!)
   242: 
   243:   inst_vs are the type variables of the instance type schema
   244:   They need to be eliminated, since they're arbitrary.
   245: 
   246:   inst_ts are the ts needed to replace the typeclass vs
   247:   to obtain the candidate instance function signature from the
   248:   virtual signature, these will contain variables of the
   249:   instance type schema.
   250: 
   251:   We match up the call ts with the inst_ts first,
   252:   to find values for the instance schema types, so we
   253:   can eliminate them.
   254: 
   255:   But there is a special case: if the call is actually
   256:   inside an instance, the ts may contain schema variables.
   257:   In this context they're fixed variables, not to be
   258:   eliminated. So any such variables have to be alpha converted
   259:   away before the solution for inst_vs is found,
   260:   the put back afterwards: when replacing the inst_vs,
   261:   some of inst_vs type variable will then remain,
   262:   which is correct.
   263: 
   264:   For technical reasons we do this backwards. We alpha convert
   265:   the inst_vs in the inst_ts away, solve for the new set
   266:   of variables, and then modify the solution back to
   267:   the old set .. this is easier because the dependent
   268:   variables are just integers, so the remapping
   269:   doens't penetrate any type terms.
   270: *)
   271: 
   272: 
   273: let tcinst_chk syms allow_fail i ts sr (inst_vs, inst_constraint, inst_ts, j)  =
   274:      (*
   275:      print_endline
   276:      ("virtual " ^ si i ^ "[" ^ catmap "," (sbt syms.dfns) ts ^ "]");
   277:      if length inst_ts > length ts then
   278:        failwith (
   279:          "Not enough ts given, expected at least " ^
   280:          si (length inst_ts) ^ ", got " ^ si (length ts)
   281:        )
   282:      ;
   283:      *)
   284:      (* solve for vs' *)
   285:      let v0 = !(syms.counter) in
   286:      let n = length inst_vs in
   287:      let vis =  (* list of ints from v0 to v0+n-1 *)
   288:        let rec aux i o = match i with
   289:        | 0 -> o
   290:        | _ -> aux (i-1) ((v0+i-1)::o)
   291:        in aux n []
   292:      in
   293:      let nuvs = map (fun i -> `BTYP_var (i,`BTYP_type 0)) vis in
   294:      let inst_ts' = map (tsubst inst_vs nuvs) inst_ts in
   295:      let vset = fold_left (fun acc i -> IntSet.add i acc) IntSet.empty vis in
   296: 
   297:      (*
   298:      let vset = fold_left (fun acc (_,i) -> IntSet.add i acc) IntSet.empty inst_vs' in
   299:      *)
   300:      let eqns = combine (list_prefix ts (length inst_ts)) inst_ts' in
   301:      (*
   302:      print_endline ("Solving equations\n " ^
   303:        catmap "\n" (fun (a,b) -> sbt syms.dfns a ^ " = " ^ sbt syms.dfns b ) eqns
   304:      );
   305:      *)
   306:      let mgu =
   307:        try Some (unification false syms.dfns eqns vset)
   308:        with Not_found -> None
   309:      in
   310:      begin match mgu with
   311:      | None -> None
   312:      | Some mgu ->
   313:        let mgu =
   314:          let goback = combine vis (map (fun (_,i)->i) inst_vs) in
   315:          map (fun (i,t) -> assoc i goback, t) mgu
   316:        in
   317:        let tsv =
   318:          map
   319:          (fun (s,i) ->
   320:            if not (mem_assoc i mgu) then
   321:              failwith ("Didn't solve for instance type variable " ^ s)
   322:            else
   323:            (
   324:              (*
   325:              print_endline ("Solved " ^ s ^"<"^si i^">" ^ "-> " ^ sbt syms.dfns (assoc i mgu));
   326:              *)
   327:              assoc i mgu
   328:            )
   329:          )
   330:          inst_vs
   331:        in
   332:        (*
   333:        print_endline ("instance constraint: " ^ sbt syms.dfns inst_constraint);
   334:        *)
   335:        let con = list_subst mgu inst_constraint in
   336:        let con = reduce_type (Flx_beta.beta_reduce syms sr con) in
   337:        match con with
   338:        | `BTYP_tuple [] ->
   339:          let tail = drop ts (length inst_ts) in
   340:          let ts = tsv @ tail in
   341:          (*
   342:          print_endline ("Remap to " ^ si j ^ "[" ^ catmap "," (sbt syms.dfns) ts ^ "]");
   343:          *)
   344:          Some (j,ts)
   345:        | `BTYP_void -> (* print_endline "constraint reduce failure"; *) None
   346:        | _ ->
   347:          if not allow_fail then
   348:          failwith ("Unable to reduce type constraint: " ^ sbt syms.dfns con)
   349:          else
   350:          (
   351:            (*
   352:            print_endline ("Unable to reduce type constraint! " ^ sbt syms.dfns con);
   353:            *)
   354:            None
   355:          )
   356:      end
   357: 
   358: 
   359: let fixup_typeclass_instance' syms bbdcls allow_fail i ts =
   360:    let entries =
   361:     try Hashtbl.find syms.typeclass_to_instance i
   362:     with Not_found -> (* print_endline ("Symbol " ^ si i ^ " Not instantiated?"); *) []
   363:    in
   364:    let sr =
   365:      try match Hashtbl.find syms.dfns i with {sr=sr} -> sr
   366:      with Not_found -> dummy_sr
   367:    in
   368:    let entries = fold_left (fun acc x -> match tcinst_chk syms allow_fail i ts sr x with
   369:      | None -> acc
   370:      | Some x -> x::acc
   371:      ) [] entries
   372:    in
   373:    match entries with
   374:    | [] -> i,ts
   375:    | [j,ts] ->
   376:      (*
   377:      print_endline ("Found instance " ^ si j ^ "[" ^ catmap "," (sbt syms.dfns) ts ^ "]");
   378:      *)
   379:      j,ts
   380:    | ls ->
   381:      let id,parent,sr,entry =
   382:        try Hashtbl.find bbdcls i
   383:        with Not_found -> failwith ("Woops can't find virtual function index "  ^ si i)
   384:      in
   385:      print_endline
   386:      ("Unimplemented: Multiple matching instances for typeclass virtual instance\n"
   387:      ^id^"<"^ si i^">["^ catmap "," (sbt syms.dfns) ts ^"]"
   388:      )
   389:      ;
   390:      iter
   391:      (fun (j,ts) ->
   392:        let id,parent,sr,entry =
   393:          try Hashtbl.find bbdcls j
   394:          with Not_found -> failwith ("Woops can't find instance function index "  ^ si j)
   395:        in
   396:        let parent = match parent with Some k -> k | None -> assert false in
   397:        print_endline ("Function " ^ si j ^ " instance parent " ^ si parent);
   398:        let id,parent,sr,entry =
   399:          try Hashtbl.find bbdcls parent
   400:          with Not_found -> failwith ("Woops can't find instance "  ^ si parent)
   401:        in
   402:        ()
   403:        (* FINISH ME! *)
   404:      )
   405:      ls
   406:      ;
   407:    failwith "can't handle overlapping instances yet"
   408: 
   409: 
   410: let id x = x
   411: 
   412: let fixup_expr syms bbdfns e =
   413:   (*
   414:   print_endline ("Check expr " ^ sbe syms.dfns e);
   415:   *)
   416:   let rec aux e =  match map_tbexpr id aux id e with
   417:   | `BEXPR_apply_direct (i,ts,a),t ->
   418:     let a = aux a in
   419:     let j,ts = (* print_endline ("Check apply direct " ^ si i);  *)
   420:       fixup_typeclass_instance' syms bbdfns true i ts in
   421:     (*
   422:     if j <> i then print_endline ("[direct] instantiate virtual as " ^ si j);
   423:     *)
   424:     `BEXPR_apply_direct (j,ts,a),t
   425: 
   426:   | `BEXPR_apply_prim (i,ts,a),t ->
   427:     let a = aux a in
   428:     let j,ts = (* print_endline ("Check apply prim " ^ si i^ "[" ^ catmap "," (sbt syms.dfns) ts ^ "]"); *)
   429:       fixup_typeclass_instance' syms bbdfns true i ts in
   430:     (*
   431:     if j <> i then
   432:       print_endline ("[prim] instantiate virtual as " ^
   433:         si j ^ "[" ^ catmap "," (sbt syms.dfns) ts ^ "]"
   434:       )
   435:     ;
   436:     *)
   437:     `BEXPR_apply_direct (j,ts,a),t
   438: 
   439:   | x -> x
   440:   in aux e
   441: 
   442: let fixup_exe syms bbdfns exe = match exe with
   443:   | `BEXE_call_direct (sr,i,ts,a) ->
   444:     let j,ts = fixup_typeclass_instance' syms bbdfns true i ts in
   445:     (*
   446:     if j <> i then print_endline "instantiate virtual ..";
   447:     *)
   448:     let a  = fixup_expr syms bbdfns a in
   449:     `BEXE_call_direct (sr,j,ts,a)
   450:   | x ->
   451:     map_bexe id (fixup_expr syms bbdfns) id id id x
   452: 
   453: let fixup_exes syms bbdfns exes = map (fixup_exe syms bbdfns) exes
   454: 
   455: let fixup_typeclass_instances syms bbdfns =
   456:   Hashtbl.iter (fun i (id,parent,sr,entry) -> match entry with
   457:   | `BBDCL_function (props,bvs,bps,ret,exes) ->
   458:     let exes = fixup_exes syms bbdfns exes in
   459:     let entry = `BBDCL_function (props, bvs, bps, ret, exes) in
   460:     Hashtbl.replace bbdfns i (id,parent,sr,entry)
   461:   | `BBDCL_procedure (props, bvs, bps,exes)  ->
   462:     let exes = fixup_exes syms bbdfns exes in
   463:     let entry = `BBDCL_procedure (props, bvs, bps,exes) in
   464:     Hashtbl.replace bbdfns i (id,parent,sr,entry)
   465:   | _ -> ()
   466:   )
   467:   bbdfns
   468: 
   469: (* this routine doesn't allow constraint reduction failure
   470:   and should only be run at instantiation time
   471: *)
   472: let fixup_typeclass_instance syms bbdcls i ts =
   473:   fixup_typeclass_instance' syms bbdcls false i ts
   474: 
   475: (* this routine allows failure, only use for early
   476:   instantiation for optimisation
   477: *)
   478: let maybe_fixup_typeclass_instance syms bbdcls i ts =
   479:   fixup_typeclass_instance' syms bbdcls true i ts
   480: 
End ocaml section to src/flx_typeclass.ml[1]