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: