Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
ViewVC logotype

Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 196, Fri Nov 20 18:16:19 1998 UTC revision 197, Sun Nov 22 01:25:23 1998 UTC
# Line 26  Line 26 
26     in h(xs, [])     in h(xs, [])
27    end    end
28    
29  datatype aux_info = AX_REG of bool * enc_tvar list  (* definitions of named tyc variables.
30                    | AX_NO     for now, these share the same namespace with lvars. *)
31    type tvar = LambdaVar.lvar
32    val mkTvar = LambdaVar.mkLvar
33    
34    (* for lists of free type variables, debruijn indices are collapsed
35       into a single integer using tvEncode/tvDecode, named variables use
36       the tvar as an integer.  The debruijn-indexed list is kept sorted,
37       the named variables are in arbitrary order (for now) --league, 2 July 1998
38     *)
39    datatype aux_info =
40        AX_REG of bool                      (* normalization flag *)
41                * enc_tvar list             (* free debruijn-indexed type vars *)
42                * tvar list                 (* free named type vars *)
43      | AX_NO                               (* no aux_info available *)
44    
45  val mergeTvs = merge  val mergeTvs = merge
46  val fmergeTvs = foldmerge  val fmergeTvs = foldmerge
# Line 49  Line 62 
62    
63  withtype tkind = tkindI hash_cell              (* hash-consing-impl of tkind *)  withtype tkind = tkindI hash_cell              (* hash-consing-impl of tkind *)
64    
 (* definitoins of named tyc variables *)  
 type tvar = LambdaVar.lvar                     (* temporary definitions *)  
 val mkTvar = LambdaVar.mkLvar  
   
65  (* an special extensible token key *)  (* an special extensible token key *)
66  type token = int  type token = int
67    
# Line 65  Line 74 
74  (** definitions of lambda type constructors *)  (** definitions of lambda type constructors *)
75  datatype tycI  datatype tycI
76    = TC_VAR of DebIndex.index * int             (* tyc variables *)    = TC_VAR of DebIndex.index * int             (* tyc variables *)
77    | TC_NVAR of tvar * DebIndex.depth * int     (* named tyc variables *)    | TC_NVAR of tvar                            (* named tyc variables *)
78    | TC_PRIM of PrimTyc.primtyc                 (* primitive tyc *)    | TC_PRIM of PrimTyc.primtyc                 (* primitive tyc *)
79    
80    | TC_FN of tkind list * tyc                  (* tyc abstraction *)    | TC_FN of tkind list * tyc                  (* tyc abstraction *)
# Line 251  Line 260 
260    
261        fun tc_hash tc =        fun tc_hash tc =
262          let fun g (TC_VAR(d, i)) = combine [1, (DI.di_key d)*10, i]          let fun g (TC_VAR(d, i)) = combine [1, (DI.di_key d)*10, i]
263                | g (TC_NVAR(v, d, i)) = combine[15, v, (DI.dp_key d)*13, i]                | g (TC_NVAR v) = combine[15, v]
264                | g (TC_PRIM pt) = combine [2, PT.pt_toint pt]                | g (TC_PRIM pt) = combine [2, PT.pt_toint pt]
265                | g (TC_FN(ks, t)) = combine (3::(getnum t)::(map getnum ks))                | g (TC_FN(ks, t)) = combine (3::(getnum t)::(map getnum ks))
266                | g (TC_APP(t, ts)) = combine (4::(getnum t)::(map getnum ts))                | g (TC_APP(t, ts)) = combine (4::(getnum t)::(map getnum ts))
# Line 302  Line 311 
311        fun ltI_eq {new : ltyI, old=LT_IND(_,s)} = ltI_eq {new=new, old=s}        fun ltI_eq {new : ltyI, old=LT_IND(_,s)} = ltI_eq {new=new, old=s}
312          | ltI_eq {new, old} = (new=old)          | ltI_eq {new, old} = (new=old)
313    
314        val baseAux = AX_REG (true, [])        val baseAux = AX_REG (true, [], [])
315    
316        fun getAux (ref(i : int, _, x)) = x        fun getAux (ref(i : int, _, x)) = x
317    
318        fun mergeAux(AX_NO, _) = AX_NO        fun mergeAux(AX_NO, _) = AX_NO
319          | mergeAux(_, AX_NO) = AX_NO          | mergeAux(_, AX_NO) = AX_NO
320          | mergeAux(AX_REG(b1,vs1), AX_REG(b2,vs2)) =          | mergeAux(AX_REG(b1,vs1,nvs1), AX_REG(b2,vs2,nvs2)) =
321              AX_REG(b2 andalso b1, mergeTvs(vs1, vs2))              AX_REG(b2 andalso b1, mergeTvs(vs1, vs2),
322                       mergeTvs(nvs1, nvs2))
323    
324        fun fsmerge [] = baseAux        fun fsmerge [] = baseAux
325          | fsmerge [x] = getAux x          | fsmerge [x] = getAux x
# Line 320  Line 330 
330               in loop(xs, baseAux)               in loop(xs, baseAux)
331              end              end
332    
333        fun exitAux(AX_REG(b, vs)) = AX_REG(b, exitLevel vs)        fun exitAux(AX_REG(b, vs, nvs)) = AX_REG(b, exitLevel vs, nvs)
334          | exitAux x = x          | exitAux x = x
335    
336        fun tc_aux tc =        fun tc_aux tc =
337          let fun g (TC_VAR(d, i)) = AX_REG(true, [tvEncode(d, i)])          let fun g (TC_VAR(d, i)) = AX_REG(true, [tvEncode(d, i)], [])
338                | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***)                | g (TC_NVAR v) = AX_REG(true, [], [v])
339                | g (TC_PRIM pt) = baseAux                | g (TC_PRIM pt) = baseAux
340                | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO                | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO
341                | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO                | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO
342                | g (TC_APP(ref(_, TC_FN _, AX_REG(_,vs)), ts)) =                | g (TC_APP(ref(_, TC_FN _, AX_REG(_,vs,nvs)), ts)) =
343                       mergeAux(AX_REG(false, vs), fsmerge ts)       (* ? *)                       mergeAux(AX_REG(false, vs, nvs), fsmerge ts) (* ? *)
344                | g (TC_PROJ(ref(_, TC_SEQ _, AX_REG(_,vs)), _)) =                | g (TC_PROJ(ref(_, TC_SEQ _, AX_REG(_,vs,nvs)), _)) =
345                       AX_REG(false, vs)                             (* ? *)                       AX_REG(false, vs, nvs) (* ? *)
346                | g (TC_FN(ks, t)) = exitAux(getAux t)                | g (TC_FN(ks, t)) = exitAux(getAux t)
347                | g (TC_APP(t, ts)) = fsmerge (t::ts)                | g (TC_APP(t, ts)) = fsmerge (t::ts)
348                | g (TC_SEQ ts) = fsmerge ts                | g (TC_SEQ ts) = fsmerge ts
# Line 341  Line 351 
351                | g (TC_FIX((_,t,ts), _)) =                | g (TC_FIX((_,t,ts), _)) =
352                       let val ax = getAux t                       let val ax = getAux t
353                        in case ax                        in case ax
354                            of AX_REG(_,[]) => mergeAux(ax, fsmerge ts)                            of AX_REG(_,[],[]) => mergeAux(ax, fsmerge ts)
355                             | _ => bug "unexpected TC_FIX freevars in tc_aux"                             | AX_REG _ => bug "unexpected TC_FIX freevars in tc_aux"
356                               | AX_NO => AX_NO
357                       end                       end
358                | g (TC_ABS t) = getAux t                | g (TC_ABS t) = getAux t
359                | g (TC_BOX t) = getAux t                | g (TC_BOX t) = getAux t
# Line 350  Line 361 
361                | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2)                | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2)
362                | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2]                | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2]
363                | g (TC_TOKEN (k, (ref(_, t, AX_NO)))) = AX_NO                | g (TC_TOKEN (k, (ref(_, t, AX_NO)))) = AX_NO
364                | g (TC_TOKEN (k, (x as ref(_, t, AX_REG(b,vs))))) =                | g (TC_TOKEN (k, (x as ref(_, t, AX_REG(b,vs,nvs))))) =
365                       AX_REG((token_whnm k x) andalso b, vs)                       AX_REG((token_whnm k x) andalso b, vs, nvs)
366                | g (TC_CONT ts) = fsmerge ts                | g (TC_CONT ts) = fsmerge ts
367                | g (TC_IND _) = bug "unexpected TC_IND in tc_aux"                | g (TC_IND _) = bug "unexpected TC_IND in tc_aux"
368                | g (TC_ENV _) = AX_NO                | g (TC_ENV _) = AX_NO
# Line 376  Line 387 
387  in  in
388    
389  (** a temporary hack on getting the list of free tyvars *)  (** a temporary hack on getting the list of free tyvars *)
390    (* ignores named vars for now.  --CALeague, 1 Jul 1998 *)
391  fun tc_vs (r as ref(_ : int, _ : tycI, AX_NO)) = NONE  fun tc_vs (r as ref(_ : int, _ : tycI, AX_NO)) = NONE
392    | tc_vs (r as ref(_ : int, _ : tycI, AX_REG (_,x))) = SOME x    | tc_vs (r as ref(_ : int, _ : tycI, AX_REG (_,x,_))) = SOME x
393    
394  fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE  fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE
395    | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x    | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x,_))) = SOME x
   
396    
397  (** converting from the hash-consing reps to the standard reps *)  (** converting from the hash-consing reps to the standard reps *)
398  fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t  fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t
# Line 491  Line 502 
502    
503    
504  (** checking if a tyc or an lty is in the normal form *)  (** checking if a tyc or an lty is in the normal form *)
505  fun tcp_norm ((t as ref (i, _, AX_REG(b,_))) : tyc) =  b  fun tcp_norm ((t as ref (i, _, AX_REG(b,_,_))) : tyc) =  b
506    | tcp_norm _ = false    | tcp_norm _ = false
507    
508  fun ltp_norm ((t as ref (i, _, AX_REG(b,_))) : lty) =  b  fun ltp_norm ((t as ref (i, _, AX_REG(b,_,_))) : lty) =  b
509    | ltp_norm _ = false    | ltp_norm _ = false
510    
511    
# Line 550  Line 561 
561  (** utility functions for updating tycs and ltys *)  (** utility functions for updating tycs and ltys *)
562  fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =  fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =
563        (tgt := (i, TC_IND (nt, old), AX_NO))        (tgt := (i, TC_IND (nt, old), AX_NO))
564    | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false, _))), nt) =    | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false,_,_))), nt) =
565        (tgt := (i, TC_IND (nt, old), x))        (tgt := (i, TC_IND (nt, old), x))
566    | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc"    | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc"
567    
568  fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) =  fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) =
569        (tgt := (i, LT_IND (nt, old), AX_NO))        (tgt := (i, LT_IND (nt, old), AX_NO))
570    | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false, _))), nt) =    | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false,_,_))), nt) =
571        (tgt := (i, LT_IND (nt, old), x))        (tgt := (i, LT_IND (nt, old), x))
572    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"
573    
# Line 1163  Line 1174 
1174        | _ => false        | _ => false
1175    
1176  (** general equality for tycs *)  (** general equality for tycs *)
1177  fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)),  fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _, _)),
1178                   y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)                   y as ref (_, _, AX_REG(true, _, _))) = tc_eq(x,y)
1179    | tc_eqv' hyp (x, y) = let    | tc_eqv' hyp (x, y) = let
1180          val t1 = tc_whnm x          val t1 = tc_whnm x
1181          val t2 = tc_whnm y          val t2 = tc_whnm y
# Line 1251  Line 1262 
1262  fun tcs_depth ([], d) = DI.top  fun tcs_depth ([], d) = DI.top
1263    | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))    | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
1264    
1265    (* these return the list of free NAMED tyvars *)
1266    fun tc_nvars (tyc:tyc) =
1267        case getAux (tc_norm tyc) of
1268            AX_REG (_,_,tvs) => tvs
1269          | AX_NO => bug "unexpected case in tc_nvars"
1270    
1271    fun lt_nvars (lty:lty) =
1272        case getAux (lt_norm lty) of
1273            AX_REG (_,_,tvs) => tvs
1274          | AX_NO => bug "unexpected case in lt_nvars"
1275    
1276    
1277  end (* toplevel local *)  end (* toplevel local *)
1278  end (* abstraction LtyKernel *)  end (* abstraction LtyKernel *)
1279    

Legend:
Removed from v.196  
changed lines
  Added in v.197

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0