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/branches/primop-branch-2/src/compiler/FLINT/kernel/lty.sml
ViewVC logotype

Diff of /sml/branches/primop-branch-2/src/compiler/FLINT/kernel/lty.sml

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

revision 2029, Fri Aug 18 16:24:18 2006 UTC revision 2030, Fri Aug 18 17:28:28 2006 UTC
# Line 616  Line 616 
616    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"
617    
618    
619    (********************************************************************
620     *                      KIND-CHECKING ROUTINES                      *
621     ********************************************************************)
622    exception TkTycChk of string
623    exception LtyAppChk
624    
625    (* tkSubkind returns true if k1 is a subkind of k2, or if they are
626     * equivalent kinds.  it is NOT commutative.  tksSubkind is the same
627     * thing, component-wise on lists of kinds.
628     *)
629    fun tksSubkind (ks1, ks2) =
630        ListPair.all tkSubkind (ks1, ks2)   (* component-wise *)
631    and tkSubkind (k1, k2) =
632        tk_eq (k1, k2) orelse              (* reflexive *)
633        case (tk_outX k1, tk_outX k2) of
634            (TK_BOX, TK_MONO) => true (* ground kinds (base case) *)
635          (* this next case is WRONG, but necessary until the
636           * infrastructure is there to give proper boxed kinds to
637           * certain tycons (e.g., ref : Omega -> Omega_b)
638           *)
639          | (TK_MONO, TK_BOX) => true
640          | (TK_SEQ ks1, TK_SEQ ks2) =>
641              tksSubkind (ks1, ks2)
642          | (TK_FUN (ks1, k1'), TK_FUN (ks2, k2')) =>
643              tksSubkind (ks2, ks1) andalso (* contravariant *)
644              tkSubkind (k1', k2')
645          | _ => false
646    
647    local
648    
649    (* TODO
650     * There must be a better factoring of the dependencies
651     * These functions are in either ltydefs or ltybasic *)
652        (** tkind constructors *)
653      val tkc_mono   : tkind = tk_injX (TK_MONO)
654      val tkc_box    : tkind = tk_injX (TK_BOX)
655      val tkc_seq    : tkind list -> tkind = tk_injX o TK_SEQ
656      val tkc_fun    : tkind list * tkind -> tkind = tk_injX o TK_FUN
657    
658    (** utility functions for constructing tkinds *)
659    fun tkc_arg n =
660      let fun h (n, r) = if n < 1 then r else h(n-1, tkc_mono::r)
661       in h(n, [])
662      end
663    
664    val tkc_fn1 = tkc_fun(tkc_arg 1, tkc_mono)
665    val tkc_fn2 = tkc_fun(tkc_arg 2, tkc_mono)
666    val tkc_fn3 = tkc_fun(tkc_arg 3, tkc_mono)
667    
668    fun tkc_int 0 = tkc_mono
669      | tkc_int 1 = tkc_fn1
670      | tkc_int 2 = tkc_fn2
671      | tkc_int 3 = tkc_fn3
672      | tkc_int i = tkc_fun(tkc_arg i, tkc_mono)
673    in
674    (* is a kind monomorphic? *)
675    fun tkIsMono k = tkSubkind (k, tkc_mono)
676    
677    (* assert that k1 is a subkind of k2 *)
678    fun tkAssertSubkind (k1, k2) =
679        if tkSubkind (k1, k2) then ()
680        else raise TkTycChk "Subkind assertion failed!"
681    
682    (* assert that a kind is monomorphic *)
683    fun tkAssertIsMono k =
684        if tkIsMono k then ()
685        else raise TkTycChk "Mono assertion failed!"
686    
687    (* select the ith element from a kind sequence *)
688    fun tkSel (tk, i) =
689      (case (tk_outX tk)
690        of (TK_SEQ ks) =>
691           (List.nth(ks, i)
692            handle Subscript => raise TkTycChk "Invalid TC_SEQ index")
693         | _ => raise TkTycChk "Projecting out of non-tyc sequence")
694    
695    fun tks_eqv (ks1, ks2) = tk_eq(tkc_seq ks1, tkc_seq ks2)
696    
697    fun tkApp (tk, tks) =
698      (case (tk_outX tk)
699        of TK_FUN(a, b) =>
700           if tks_eqv(a, tks) then b
701           else raise TkTycChk "Param/Arg Tyc Kind mismatch"
702         | _ => raise TkTycChk "Application of non-TK_FUN")
703    
704    (* check the application of tycs of kinds `tks' to a type function of
705     * kind `tk'.
706     *)
707    fun tkApp (tk, tks) =
708      (case (tk_outX tk)
709        of TK_FUN(a, b) =>
710           if tksSubkind(tks, a) then b
711           else raise TkTycChk "Param/Arg Tyc Kind mismatch"
712         | _ => raise TkTycChk "Application of non-TK_FUN")
713    
714    (* Kind-checking naturally requires traversing type graphs.  to avoid
715     * re-traversing bits of the dag, we use a dictionary to memoize the
716     * kind of each tyc we process.
717     *
718     * The problem is that a tyc can have different kinds, depending on
719     * the valuations of its free variables.  So this dictionary maps a
720     * tyc to an association list that maps the kinds of the free
721     * variables in the tyc (represented as a TK_SEQ) to the tyc's kind.
722     *)
723    (* structure TcDict = BinaryMapFn
724                         (struct
725                            type ord_key = tyc
726                            val compare = tc_cmp
727                          end) *)
728    
729    structure Memo :> sig
730      type dict
731      val newDict         : unit -> dict
732      val recallOrCompute : dict * tkindEnv * tyc * (unit -> tkind) -> tkind
733    end =
734    struct
735        structure TcDict = RedBlackMapFn
736                               (struct
737                                   type ord_key = tyc
738                                   val compare = tc_cmp
739                               end)
740    
741        type dict = (tkind * tkind) list TcDict.map ref
742        val newDict : unit -> dict = ref o (fn () => TcDict.empty)
743    
744        fun recallOrCompute (dict, kenv, tyc, doit) =
745            (* what are the valuations of tyc's free variables
746             * in kenv? *)
747            (* (might not be available for some tycs) *)
748            case tkLookupFreeVars (kenv, tyc) of
749                SOME ks_fvs => let
750                    (* encode those as a kind sequence *)
751                    val k_fvs = tkc_seq ks_fvs
752                    (* query the dictionary *)
753                    val kci = case TcDict.find(!dict, tyc) of
754                        SOME kci => kci
755                      | NONE => []
756                    (* look for an equivalent environment *)
757                    fun sameEnv (k_fvs',_) = tk_eq(k_fvs, k_fvs')
758                in
759                    case List.find sameEnv kci of
760                        SOME (_,k) => k     (* HIT! *)
761                      | NONE => let
762                            (* not in the list.  we will compute
763                             * the answer and cache it
764                             *)
765                            val k = doit()
766                            val kci' = (k_fvs, k) :: kci
767                        in
768                            dict := TcDict.insert(!dict, tyc, kci');
769                            k
770                        end
771                end
772              | NONE =>
773                (* freevars were not available.  we'll have to
774                 * recompute and cannot cache the result.
775                 *)
776                doit()
777    
778    end (* Memo *)
779    
780    (* return the kind of a given tyc in the given kind environment *)
781    fun tkTycGen() = let
782        val dict = Memo.newDict()
783    
784        fun tkTyc (kenv : tkindEnv) t = let
785            (* default recursive invocation *)
786            val g = tkTyc kenv
787            fun chkKindEnv(env : tycEnv,j,kenv : tkindEnv) : unit =
788                let
789                    fun chkBinder(Lamb _) = ()
790                      | chkBinder(Beta(j',args,ks)) =
791                        let
792                            val kenv' = List.drop(kenv, j-j')
793                            val argks = map (fn t => tkTyc kenv' t) args
794                        in if tksSubkind(ks, argks)
795                           then ()
796                           else bug "chkKindEnv: Beta binder kinds mismatch"
797                        end
798                        handle Subscript =>
799                               bug "tkTyc[Env]: dropping too many frames"
800                in app chkBinder (teToBinders env)
801                end
802            (* how to compute the kind of a tyc *)
803            fun mk() =
804                case tc_outX t of
805                    TC_VAR (i, j) =>
806                    tkLookup (kenv, i, j)
807                  | TC_NVAR _ =>
808                    bug "TC_NVAR not supported yet in tkTyc"
809                  | TC_PRIM pt =>
810                    tkc_int (PrimTyc.pt_arity pt)
811                  | TC_FN(ks, tc) =>
812                    tkc_fun(ks, tkTyc (tkInsert (kenv,ks)) tc)
813                  | TC_APP (tc, tcs) =>
814                    tkApp (g tc, map g tcs)
815                  | TC_SEQ tcs =>
816                    tkc_seq (map g tcs)
817                  | TC_PROJ(tc, i) =>
818                    tkSel(g tc, i)
819                  | TC_SUM tcs =>
820                    (List.app (tkAssertIsMono o g) tcs;
821                     tkc_mono)
822                  | TC_FIX ((n, tc, ts), i) =>
823                    let (* Kind check generator tyc *)
824                        val k = g tc
825                        (* Kind check freetycs *)
826                        val nk =
827                            case ts
828                              of [] => k
829                               | _ => tkApp(k, map g ts)
830                    in
831                        case (tk_outX nk) of
832                            TK_FUN(a, b) =>
833                            let val arg =
834                                    case a
835                                      of [x] => x
836                                       | _ => tkc_seq a
837                            in
838                                (* Kind check recursive tyc app ??*)
839                                if tkSubkind(arg, b) then (* order? *)
840                                    (if n = 1 then b else tkSel(arg, i))
841                                else raise TkTycChk "Recursive app mismatch"
842                            end
843                          | _ => raise TkTycChk "FIX with no generator"
844                    end
845                  | TC_ABS tc =>
846                    (tkAssertIsMono (g tc);
847                     tkc_mono)
848                  | TC_BOX tc =>
849                    (tkAssertIsMono (g tc);
850                     tkc_mono)
851                  | TC_TUPLE (_,tcs) =>
852                    (List.app (tkAssertIsMono o g) tcs;
853                     tkc_mono)
854                  | TC_ARROW (_, ts1, ts2) =>
855                    (List.app (tkAssertIsMono o g) ts1;
856                     List.app (tkAssertIsMono o g) ts2;
857                     tkc_mono)
858                  | TC_TOKEN(_, tc) =>
859                    (tkAssertIsMono (g tc);
860                     tkc_mono)
861                  | TC_PARROW _ => bug "unexpected TC_PARROW in tkTyc"
862               (* | TC_ENV _ => bug "unexpected TC_ENV in tkTyc" *)
863                  | TC_ENV(body, 0, j, teEmpty) =>
864                      (tkTyc (List.drop(kenv,j)) body
865                       handle Subscript =>
866                              bug "[Env]: dropping too many frames")
867                  | TC_ENV(body, i, j, env) =>
868                      (let val kenv' =
869                               List.drop(kenv, j)
870                               handle Subscript =>
871                                      bug "[Env]: dropping too many frames"
872                           fun bindToKinds(Lamb(_,ks)) = ks
873                             | bindToKinds(Beta(_,_,ks)) = ks
874                           fun addBindToKEnv(b,ke) =
875                               bindToKinds b :: ke
876                           val bodyKenv =
877                               foldr addBindToKEnv kenv' (teToBinders env)
878                       in chkKindEnv(env,j,kenv);
879                          tkTyc bodyKenv body
880                       end)
881                  | TC_IND _ => bug "unexpected TC_IND in tkTyc"
882                  | TC_CONT _ => bug "unexpected TC_CONT in tkTyc"
883        in
884            Memo.recallOrCompute (dict, kenv, t, mk)
885        end
886    in
887        tkTyc
888    end (* function tkTycGen *)
889    
890    (* assert that the kind of `tc' is a subkind of `k' in `kenv' *)
891    fun tkChkGen() =
892        let val tkTyc = tkTycGen()
893            fun tkChk kenv (k, tc) =
894                tkAssertSubkind (tkTyc kenv tc, k)
895        in tkChk
896        end
897    end (* local *)
898    
899  end (* structure Lty *)  end (* structure Lty *)

Legend:
Removed from v.2029  
changed lines
  Added in v.2030

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