Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Tracker SCM

SCM Repository

[smlnj] Diff of /sml/trunk/src/compiler/FLINT/flint/chkflint.sml
ViewVC logotype

Diff of /sml/trunk/src/compiler/FLINT/flint/chkflint.sml

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

revision 44, Sun Mar 22 20:10:57 1998 UTC revision 45, Sun Mar 22 20:11:09 1998 UTC
# Line 1  Line 1 
1  (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *)  (* COPYRIGHT (c) 1997, 1998 YALE FLINT PROJECT *)
2  (* chkflint.sml *)  (* chkflint.sml *)
3    
4  (* FLINT Type Checker *)  (* FLINT Type Checker *)
# Line 10  Line 10 
10    
11  val checkTop : FLINT.fundec * typsys -> bool  val checkTop : FLINT.fundec * typsys -> bool
12  val checkExp : FLINT.lexp * typsys -> bool  val checkExp : FLINT.lexp * typsys -> bool
 val fname_ref : string ref  (* a filename hack *)  
13    
14  end (* signature CHKFLINT *)  end (* signature CHKFLINT *)
15    
16  structure ChkFlint : CHKFLINT =  structure ChkFlint : CHKFLINT =
17  struct  struct
18    
19    (** which set of the typing rules to use while doing the typecheck *)
20    type typsys = int (* currently very crude, use int for phases *)
21    
22  local structure LT = LtyExtern  local structure LT = LtyExtern
23        structure LV = LambdaVar        structure LV = LambdaVar
24        structure DA = Access        structure DA = Access
25        structure DI = DebIndex        structure DI = DebIndex
26        structure PP = PPFlint        structure PP = PPFlint
27        open FLINT        open FLINT
 in  
   
 (** which set of the typing rules to use while doing the typecheck *)  
 type typsys = int (* currently very crude, use int for phases *)  
   
 (*** a hack of printing diagnostic output into a separate file ***)  
 val fname_ref : string ref = ref "yyy"  
28    
29  fun bug s = ErrorMsg.impossible ("ChkFlint: "^s)  fun bug s = ErrorMsg.impossible ("ChkFlint: "^s)
30  val say = Control.Print.say  val say = Control.Print.say
31  val anyerror = ref false  val anyerror = ref false
 val clickerror = fn () => (anyerror := true)  
32    
33  (****************************************************************************  (****************************************************************************
34   *                         BASIC UTILITY FUNCTIONS                          *   *                         BASIC UTILITY FUNCTIONS                          *
35   ****************************************************************************)   ****************************************************************************)
 fun app2(f, [], []) = ()  
   | app2(f, a::r, b::z) = (f(a, b); app2(f, r, z))  
   | app2(f, _, _) = bug "unexpected list arguments in function app2"  
36    
37  fun simplify(le,0) = RET [STRING "<-dummy->"]  fun foldl2 (f,a,xs,ys,g) = let
38      val rec loop =
39       fn (a, nil, nil) => a
40        | (a, x::xs, y::ys) => loop (f (x,y,a), xs, ys)
41        | (a, xs', _) => g (a, xs', length xs, length ys)
42      in loop (a,xs,ys) end
43    
44    fun simplify (le,0) = RET [STRING "<...>"]
45    | simplify(le,n) =    | simplify(le,n) =
46        let fun h le = simplify(le, n-1)        let fun h le = simplify(le, n-1)
47            fun h1 (fk,v,args,le) = (fk,v,args,h le)            fun h1 (fk,v,args,le) = (fk,v,args,h le)
# Line 53  Line 51 
51              | FIX(fdecs, b) => FIX(map h1 fdecs, h b)              | FIX(fdecs, b) => FIX(map h1 fdecs, h b)
52              | TFN(tdec, e) => TFN(h2 tdec, h e)              | TFN(tdec, e) => TFN(h2 tdec, h e)
53              | SWITCH(v, l, dc, opp) =>              | SWITCH(v, l, dc, opp) =>
54                 (let fun g(c, x) = (c, h x)                  let fun g (c,x) = (c, h x)
55                      fun f x = case x of SOME y => SOME(h y) | NONE => NONE                      val f = fn SOME y => SOME (h y) | NONE => NONE
56                   in SWITCH(v, l, map g dc, f opp)                   in SWITCH(v, l, map g dc, f opp)
57                  end)                  end
58                | CON (dc,tcs,vs,lv,le) => CON (dc, tcs, vs, lv, h le)
59                | RECORD (rk,vs,lv,le) => RECORD (rk, vs, lv, h le)
60                | SELECT (v,n,lv,le) => SELECT (v, n, lv, h le)
61              | HANDLE(e, v) => HANDLE(h e, v)              | HANDLE(e, v) => HANDLE(h e, v)
62                | PRIMOP (po,vs,lv,le) => PRIMOP (po, vs, lv, h le)
63              | _ => le              | _ => le
64        end (* end of simplify *)        end (* end of simplify *)
65    
# Line 66  Line 68 
68  val tcPrint = say o LT.tc_print  val tcPrint = say o LT.tc_print
69  val ltPrint = say o LT.lt_print  val ltPrint = say o LT.lt_print
70  fun lePrint le = PP.printLexp (simplify(le, 3))  fun lePrint le = PP.printLexp (simplify(le, 3))
71  fun svPrint sv = PP.printSval (sv)  val svPrint = PP.printSval
   
 (*** a hack for type checking ***)  
 fun laterPhase i = (i > 20)  
   
 (****************************************************************************  
  *  MAIN FUNCTION --- val checkTop : Lambda.fundec * typsys -> bool         *  
  ****************************************************************************)  
 fun checkTop ((fk,v,args,lexp), phase) = bug "not implemented"  
 (*  
 let  
 val ltEquiv = LT.lt_eqv_bx  
 val ltAppChk = LT.lt_inst_chk  
 val ltString = if laterPhase(phase) then LT.ltc_void else LT.ltc_string  
 val ltExn = if laterPhase(phase) then LT.ltc_void else LT.ltc_exn  
 fun ltEtag lt = if laterPhase(phase) then LT.ltc_void  
                 else LT.ltc_etag lt  
 fun ltVector t = if laterPhase(phase) then LT.ltc_void  
                  else LT.ltc_tyc(LT.tcc_app(LT.tcc_vector,[t]))  
 exception tcUnbound = LT.tcUnbound  
 exception LtyArrow  
 exception LtySelect  
 fun ltArrow lt =  
   (LT.lt_arrow lt) handle _ => raise LtyArrow  
 fun ltSel (lt, i) =  
   (LT.lt_select(lt, i)) handle _ => raise LtySelect  
 fun ltFun (t1, t2) = LT.ltc_fun(t1, t2)  
   
 (** utility values and functions on ltyEnv *)  
 type ltyEnv = LT.ltyEnv  
 val initLtyEnv : ltyEnv = LT.initLtyEnv  
 val ltLookup = LT.ltLookup  
 val ltInsert = LT.ltInsert  
   
 (** utility functions for type checking *)  
 fun ltTyApp le s (lt, ts, kenv) =  
       ((ltAppChk(lt, ts, kenv))  
        handle zz =>  
        (clickerror ();  
         say (s ^ "  **** Kind conflicting in lexp =====> \n    ");  
         case zz of LT.LtyAppChk => say "      exception LtyAppChk raised! \n"  
                  | LT.TkTycChk =>  say "      exception TkTycChk raised! \n"  
                  | _ => say "   other weird exception raised! \n";  
         say "\n \n"; lePrint le; say "\n For Types: \n";  
         ltPrint lt; say "\n and   \n    ";  
         app (fn x => (tcPrint x; say "\n")) ts;   say "\n \n";  
         say "***************************************************** \n";  
         bug "fatal typing error in ltTyApp"))  
   
 fun ltMatch le s (t1, t2) =  
   (if ltEquiv(t1,t2) then ()  
    else (clickerror();  
          say (s ^ "  **** Lty conflicting in lexp =====> \n    ");  
          ltPrint t1; say "\n and   \n    "; ltPrint t2;  
          say "\n \n";  MCprint.printLexp le;  
          say "***************************************************** \n"))  
   handle zz =>  
   (clickerror();  
    say (s ^ "  **** Lty conflicting in lexp =====> \n    ");  
    say "uncaught exception found ";  
    say "\n \n";  MCprint.printLexp le; say "\n";  
    ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n";  
    say "***************************************************** \n")  
   
 fun ltsMatch le s (ts1, ts2) = app2 (ltMatch le s) (ts1, ts2)  
   
 fun ltFnApp le s (t1, t2) =  
   let val (a1, b1) =  
         ((ltArrow t1) handle zz =>  
             (clickerror ();  
              say (s ^ "  **** Applying Non-Arrow Type in lexp =====> \n    ");  
              case zz of LtyArrow => say "exception LtyArrow raised. \n"  
                       | tcUnbound => say "exception tcUnbound raised. \n"  
                       | _ => say "other weird exceptions raised\n";  
              say "\n \n";  lePrint le; say "\n For Types \n";  
              ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";  
              say "***************************************************** \n";  
              bug "fatal typing error in ltFnApp"))  
   
    in ltMatch le s (a1, t2); b1  
   end  
   
 fun ltFnAppR le s (t1, t2) =  (*** used for DECON lexps ***)  
   let val (a1, b1) =  
         ((ltArrow t1) handle zz =>  
             (clickerror ();  
              say (s ^ "  **** Rev-Apply Non-Arrow Type in lexp =====> \n    ");  
              case zz of LtyArrow => say "exception LtyArrow raised. \n"  
                       | tcUnbound => say "exception tcUnbound raised. \n"  
                       | _ => say "other weird exceptions raised\n";  
              say "\n \n";  lePrint le; say "\n For Types \n";  
              ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";  
              say "***************************************************** \n";  
              bug "fatal typing error in ltFnApp"))  
   
    in ltMatch le s (b1, t2); a1  
   end  
   
 fun ltSelect le s (lt, i) =  
   ((ltSel(lt, i))  
      handle zz =>  
        (clickerror ();  
         say (s ^ "  **** Select from a wrong-type lexp  =====> \n    ");  
         case zz of LtySelect => say "exception LtyArrow raised. \n"  
                  | tcUnbound => say "exception tcUnbound raised. \n"  
                  | _ => say "other weird exceptions raised\n";  
         say "\n \n";  lePrint le; say "\n \n";  
         say "Selecting "; say (Int.toString i);  
         say "-th component from the type: \n     "; ltPrint lt; say "\n \n ";  
         say "***************************************************** \n";  
         bug "fatal typing error in ltSelect"))  
72    
73    fun error (le,g) = (
74        anyerror := true;
75        say "\n************************************************************\
76            \\n**** FLINT type checking failed: ";
77        g () before (say "\n** term:\n"; lePrint le))
78    
79    fun errMsg (le,s,r) = error (le, fn () => (say s; r))
80    
81    fun catchExn f (le,g) =
82      f () handle ex => error
83        (le, fn () => g () before say ("\n** exception " ^ exnName ex ^ " raised"))
84    
85    (*** a hack for type checkng ***)
86    fun laterPhase i = i > 20
87    
88    fun check phase envs lexp = let
89      val ltEquiv = LT.lt_eqv_x (* should be LT.lt_eqv *)
90      fun ltTAppChk (lt, ts, kenv) = LT.lt_inst(lt, ts)
91    
92      fun constVoid _ = LT.ltc_void
93      val (ltString,ltExn,ltEtag,ltVector,ltWrap) =
94        if laterPhase phase then
95          (LT.ltc_void, LT.ltc_void, constVoid, constVoid, constVoid)
96        else
97          (LT.ltc_string, LT.ltc_exn, LT.ltc_etag, LT.ltc_tyc o LT.tcc_vector,
98           LT.ltc_tyc o LT.tcc_box)
99    
100      fun prMsgLt (s,lt) = (say s; ltPrint lt)
101    
102      fun prList f s t = let
103        val rec loop =
104         fn [] => say "<empty list>\n"
105          | [x] => (f x; say "\n")
106          | x::xs => (f x; say "\n* and\n"; loop xs)
107        in say s; loop t end
108    
109      fun print2Lts (s,s',lt,lt') = (prList ltPrint s lt; prList ltPrint s' lt')
110    
111      fun ltMatch (le,s) (t,t') =
112        if ltEquiv (t,t') then ()
113        else error
114          (le, fn () =>
115                  (prMsgLt (s ^ ": Lty conflict\n** types:\n", t);
116                   prMsgLt ("\n** and\n", t')))
117    
118      fun ltsMatch (le,s) (ts,ts') =
119        foldl2 (fn (t,t',_) => ltMatch (le,s) (t,t'),
120                (), ts, ts',
121                fn (_,_,n,n') => error
122                   (le,
123                    fn () => print2Lts
124                      (concat [s, ": type list mismatch (", Int.toString n, " vs ",
125                               Int.toString n', ")\n** expected types:\n"],
126                       "** actual types:\n",
127                       ts, ts')))
128    
129      local
130        fun ltFnAppGen opr (le,s,msg) (t,ts) =
131          catchExn
132            (fn () => let val (xs,ys) = opr (LT.lt_arrowN t)
133                      (*** lt_arrowN may go away soon, and functors and functions
134                           have to be treated differently anyway, using different
135                           algorithms for comparing datatypes (probably)
136                       ***)
137                in ltsMatch (le,s) (xs,ts); ys
138                end)
139            (le, fn () => (prMsgLt (s ^ msg ^ "\n** type:\n", t); []))
140      in
141      fun ltFnApp (le,s) =
142          ltFnAppGen (fn x => x) (le,s,": Applying term of non-arrow type")
143      fun ltFnAppR (le,s) =
144          ltFnAppGen (fn (x,y) => (y,x)) (le,s,": Rev-app term of non-arrow type")
145      end
146    
147      fun ltTyApp (le,s) (lt,ts,kenv) =
148        catchExn
149          (fn () => ltTAppChk (lt,ts,kenv))
150          (le,
151           fn () =>
152              (prMsgLt (s ^ ": Kind conflict\n** function Lty:\n", lt);
153               prList tcPrint "\n** argument Tycs:\n" ts;
154               []))
155    
156      fun ltArrow (le,s) (isfct,alts,rlts) =
157        (case isfct
158          of NONE => LT.ltc_fct (alts,rlts)
159           | SOME raw =>
160               (catchExn
161                 (fn () => LT.ltc_arrow (raw,alts,rlts))
162                 (le,
163                  fn () =>
164                  (print2Lts
165                    (s ^ ": deeply polymorphic non-functor\n** parameter types:\n",
166                     "** result types:\n",
167                     alts, rlts);
168                  LT.ltc_void))))
169    
170    (* typeInEnv : LT.tkindEnv * LT.ltyEnv * DI.depth -> lexp -> lty list *)
171      fun typeInEnv (kenv,venv,d) = let
172        fun extEnv (lv,lt,ve) = LT.ltInsert (ve,lv,lt,d)
173        fun bogusBind (lv,ve) = extEnv (lv,LT.ltc_void,ve)
174        fun typeIn venv' = typeInEnv (kenv,venv',d)
175        fun typeWith (v,t) = typeIn (LT.ltInsert (venv,v,t,d))
176        fun mismatch (le,s) (a,r,n,n') = errMsg
177            (le,
178             concat [s, ": binding/result list mismatch\n** expected ",
179                     Int.toString n, " elements, got ", Int.toString n'],
180             foldl bogusBind a r)
181    
182        fun typeof le = let
183          fun typeofVar lv = LT.ltLookup (venv,lv,d)
184              handle ltUnbound =>
185                  errMsg (le, "Unbound Lvar " ^ LV.lvarName lv, LT.ltc_void)
186          val typeofVal =
187           fn VAR lv => typeofVar lv
188            | (INT _ | WORD _) => LT.ltc_int
189            | (INT32 _ | WORD32 _) => LT.ltc_int32
190            | REAL _ => LT.ltc_real
191            | STRING _ => LT.ltc_string
192          fun typeofFn ve (_,_,vts,eb) = let
193            fun split ((lv,t), (ve,ts)) = (LT.ltInsert (ve,lv,t,d), t::ts)
194            val (ve',ts) = foldr split (ve,[]) vts
195            in (ts, typeIn ve' eb)
196            end
197    
198          fun chkSnglInst (fp as (le,s)) (lt,ts) =
199            if null ts then lt
200            else case ltTyApp fp (lt,ts,kenv)
201               of [] => LT.ltc_unit
202                | [lt] => lt
203                | lts => errMsg
204                    (le,
205                     concat [s, ": inst yields ", Int.toString (length lts),
206                             " results instead of 1"],
207                     LT.ltc_void)
208          fun typeWithBindingToSingleRsltOfInstAndApp (s,lt,ts,vs,lv) e = let
209            val fp = (le,s)
210            val lt = case ltFnApp fp (chkSnglInst fp (lt,ts), map typeofVal vs)
211               of [lt] => lt
212                | _ => errMsg
213                   (le,
214                    concat [s, ": primop/dcon must return single result type "],
215                    LT.ltc_void)
216  (*  (*
217   * Right now, ltConChk does not check the case for DATAcon but this              | [] => LT.ltc_unit
218   * will be fixed soon. (ZHONG)              | lts => LT.ltc_tuple lts
219                        (*** until PRIMOPs start returning multiple results... ***)
220   *)   *)
221  fun ltConChk le s (DATAcon ((_, rep, lt), ts, vs), root, venv, kenv, d) =          in typeWith (lv,lt) e
       let val nt = ltTyApp le "DECON" (lt, ts, kenv)  
           val nts = ltFnAppR le "DECON" (nt, [root])  
           fun h(env, v::r, x::s) =  
                 h(ltInsert(env, v, x, d), r, s)  
             | h(env, [], []) = env  
             | h _ = (say ("** SWI BINDINGS mismatch ** vs=" ^  
                      (Int.toString (length vs)) ^ "  e1s=" ^  
                      (Int.toString (length nts)) ^ " \n");  
                      bug "unexpected lambda code in ltConChk")  
        in h(venv, vs, nts)  
       end  
   | ltConChk le s (c, lt, venv, kenv, d) =  
       let val nt = (case c of INT32con _ => LT.ltc_int32  
                             | WORD32con _ => LT.ltc_int32  
                             | REALcon _ => LT.ltc_real  
                             | STRINGcon _ => ltString  
                             |  _ => LT.ltc_int)  
        in ltMatch le s (nt, lt); venv  
       end  
   
 (** check : tkindEnv * ltyEnv * DI.depth -> lexp -> lty list *)  
 fun check (kenv, venv, d) =  
   let fun lpsv (INT _) = LT.ltc_int  
         | lpsv (WORD _) = LT.ltc_int  
         | lpsv (INT32 _) = LT.ltc_int32  
         | lpsv (WORD32 _) = LT.ltc_int32  
         | lpsv (REAL _) = LT.ltc_real  
         | lpsv (STRING _) = ltString  
         | lpsv (VAR v) =  
             (ltLookup(venv, v, d)  
              handle LT.ltUnbound =>  
               (say ("** Lvar ** " ^ (LV.lvarName(v)) ^ " is unbound *** \n");  
                bug "unexpected lambda code in checkTop"))  
   
       fun loop le =  
        (case le  
          of RET vs => map lpsv sv  
           | APP(v, vs) => ltFnApp le "APP" (lpsv v, map lpsv vs)  
           | TAPP(sv, ts) => ltTyApp le "TAPP" (lpsv sv, ts, kenv)  
           | LET(vs, e1, e2) =>  
               let val ts = loop e1  
                   fun h(env, v::r, t::s) =  
                         h(ltInsert(env,v,t,d), r, s)  
                     | h(env, [], []) = env  
                     | h _ = (say ("** LET BINDINGS mismatch ** vs=" ^  
                                   (Int.toString (length vs)) ^ "  e1s=" ^  
                                   (Int.toString (length ts)) ^ " \n");  
                              bug "unexpected lambda code in checkTop")  
                    val venv1 = h(venv, vs, ts)  
                in check (kenv, venv1, d) e2  
               end  
           | FIX (fs, eb) =>  
               let fun h (env, (_,v,t,_,_)::r) = h(ltInsert(env,v,t,d), r)  
                     | h (env, []) = env  
                   val venv1 = h(venv, fs)  
   
                   fun g (_,_,_,args,e) =  
                     let fun m (env, (v,t)::r) = m(ltInsert(env,v,t,d), r)  
                           | m (env, []) = env  
                         val venv2 = m(venv1, args)  
                         val argts = map #1 args  
                         val rests = check (kenv, venv2, d) e  
                      in LT.ltc_fun(argts, rests)  
                     end  
                   val nts = map g fs  
                   val _ = ltsMatch le "FIX1" (map #3 fs, nts)  
                in check (kenv, venv1, d) eb  
               end  
           | TFN((v,t,tvs,e), eb) =>  
               let val kenv1 = LT.tkInsert(kenv, map #2 tvs)  
                   (*** temporarily using the old format of type variables ***)  
                   val lts = check (kenv1, venv, DI.next d) e  
                   val nt = LT.ltc_poly(ks, lts)  
                   val _ = ltMatch le "TFN" (t, nt)  
                   val venv1 = ltInsert(venv,v,t,d)  
                in check (kenv, venv1, d) eb  
               end  
           | SWITCH(v, _, cl, opp) =>  
               let val root = lpsv v  
                   fun h (c, x) =  
                     let val venv1 = ltConChk le "SWT1" (c, root, venv, kenv, d)  
                      in check (kenv, venv1, d) x  
                     end  
                   val ts = map h cl  
                in (case ts  
                     of [] => bug "empty switch in checkTop"  
                      | a::r =>  
                         (app (fn x => ltsMatch le "SWT2" (x, a)) r;  
                          case opp  
                           of NONE => a  
                            | SOME be => (ltsMatch le "SWT3" (loop be, a); a)))  
               end  
           | CON((_, rep, lt), ts, vs, v, eb) =>  
               let val ts1 = ltTyApp le "CON" (lt, ts, kenv)  
                   val ts2 = map lpsv vs  
                in case ts1  
                    of [t1] =>  
                         let val nt = ltFnApp le "CON-A" (t1, ts2)  
                             val venv1 = ltInsert(venv, v, nt, d)  
                          in check (kenv, venv1, d) eb  
                         end  
                     | _ => bug "unexpected case in check CON"  
               end  
           | RECORD (RK_VECTOR t, vl) =>  
               let val ts = map lpsv vl  
                in app (fn x => ltMatch le "VECTOR" (x, LT.ltc_tyc t)) ts;  
                   ltVector t  
222                end                end
           | RECORD (_, []) => LT.ltc_unit  
           | RECORD (RK_RECORD, vl) => LT.ltc_tuple (map lpsv vl)  
           | RECORD (RK_STRUCT, vl) => LT.ltc_str (map lpsv vl)  
223    
224            | SELECT(u, i, v, eb) =>        fun matchAndTypeWith (s,v,lt,lt',lv,e) =
225                let val t = ltSelect le "SEL" (lpsv u, i)          (ltMatch (le,s) (typeofVal v, lt); typeWith (lv, lt') e)
226                    val venv1 = ltInsert(venv, v, t, d)        in case le
227                 in check (kenv, venv1, d) eb         of RET vs => map typeofVal vs
228            | LET (lvs,e,e') =>
229              typeIn (foldl2 (extEnv, venv, lvs, typeof e, mismatch (le,"LET"))) e'
230            | FIX ([],e) =>
231              (say "\n**** Warning: empty declaration list in FIX\n"; typeof e)
232            | FIX ((fd as ((FK_FUN{isrec=NONE,...} | FK_FCT),
233                           _, _, _)) :: fds', e) => let
234                val (fk, lv, _, _) = fd
235                val isfct = case fk of FK_FCT => NONE
236                                     | FK_FUN{fixed, ...} => SOME fixed
237                val (alts,rlts) = typeofFn venv fd
238                val lt = ltArrow (le,"non-rec FIX") (isfct,alts,rlts)
239                val ve = extEnv (lv,lt,venv)
240                val venv' =
241                  if null fds' then ve
242                  else errMsg
243                    (le,
244                     "multiple bindings in FIX, not all recursive",
245                     foldl (fn ((_,lv,_,_), ve) => bogusBind (lv,ve)) ve fds')
246                in typeIn venv' e
247                end
248            | FIX (fds,e) => let
249                val isfct = false
250                fun extEnv ((FK_FCT, _, _, _), _) =
251                      bug "unexpected case in extEnv"
252                  | extEnv ((FK_FUN {isrec,fixed,...}, lv, vts, _) : fundec, ve) =
253                  case (isrec, isfct)
254                   of (SOME lts, false) => let
255                        val lt = ltArrow (le,"FIX") (SOME fixed,
256                                                     map #2 vts, lts)
257                        in LT.ltInsert (ve,lv,lt,d)
258                        end
259                    | _ => let
260                        val msg =
261                          if isfct then "recursive functor "
262                          else "a non-recursive function "
263                        in errMsg (le, "in FIX: " ^ msg ^ LV.lvarName lv, ve)
264                        end
265                val venv' = foldl extEnv venv fds
266                fun chkDcl ((FK_FUN {isrec = NONE, ...}, _, _, _) : fundec) = ()
267                  | chkDcl (fd as (FK_FUN {isrec = SOME lts, ...}, _, _, _)) = let
268                    in ltsMatch (le,"FIX") (lts, #2 (typeofFn venv' fd))
269                end                end
270                  | chkDcl _ = ()
271            | ETAG(v, t) =>   (* v is string but the result should be eflag[t] *)              in
272                let val z = lpsv v   (* what do we check on e ? *)                app chkDcl fds;
273                    val _ = ltMatch le "ETAG1" (z, LT.ltc_string)                typeIn venv' e
                in ltEtag t  
274                end                end
275            | APP (v,vs) => ltFnApp (le,"APP") (typeofVal v, map typeofVal vs)
276            | RAISE(v,t) =>          | TFN ((lv,tks,e), e') => let
277                (ltMatch le "RAISE" (lpsv v, ltExn); t)              val ks = map #2 tks
278                val lts = typeInEnv (LT.tkInsert (kenv,ks), venv, DI.next d) e
279            | HANDLE(e,sv) =>              in typeWith (lv, LT.ltc_poly (ks,lts)) e'
280               let val ts = loop e              end
281                   val arg = ltFnAppR le "HANDLE" (lpsv sv, ts)          | TAPP (v,ts) => ltTyApp (le,"TAPP") (typeofVal v, ts, kenv)
282                in ts          | SWITCH (_,_,[],_) => errMsg (le,"empty SWITCH",[])
283            | SWITCH (v, _, ce::ces, lo) => let
284                val selLty = typeofVal v
285                fun g lt = (ltMatch (le,"SWITCH branch 1") (lt,selLty); venv)
286                fun brLts (c,e) = let
287                  val venv' = case c
288                     of DATAcon ((_,_,lt), ts, v) => let
289                          val fp = (le,"SWITCH DECON")
290                          val ct = chkSnglInst fp (lt,ts)
291                          val nts = ltFnAppR fp (ct, [selLty])
292                          in foldl2 (extEnv, venv, [v], nts, mismatch fp)
293                          end
294                      | (INTcon _ | WORDcon _) => g LT.ltc_int
295                      | (INT32con _ | WORD32con _) => g LT.ltc_int32
296                      | REALcon _ => g LT.ltc_real
297                      | STRINGcon _ => g ltString
298                      | VLENcon _ => g LT.ltc_int (* ? *)
299                  in typeIn venv' e
300                  end
301                val ts = brLts ce
302                fun chkBranch (ce,n) =
303                  (ltsMatch (le, "SWITCH branch " ^ Int.toString n) (ts, brLts ce);
304                   n+1)
305                in
306                  foldl chkBranch 2 ces;
307                  case lo
308                   of SOME e => ltsMatch (le,"SWITCH else") (ts, typeof e)
309                    | NONE => ();
310                  ts
311                end
312            | CON ((_,_,lt), ts, u, lv, e) =>
313              typeWithBindingToSingleRsltOfInstAndApp ("CON",lt,ts,[u],lv) e
314            | RECORD (rk,vs,lv,e) => let
315                val lt = case rk
316                   of RK_VECTOR t => let
317                        val lt = LT.ltc_tyc t
318                        val match = ltMatch (le,"VECTOR")
319                        in
320                          app (fn v => match (lt, typeofVal v)) vs;
321                          ltVector t
322               end               end
323                    | RK_TUPLE _ =>
324            | PRIM((p, t, ts), vs, v, eb) =>                    if null vs then LT.ltc_unit
325               let val xx = ltTyApp (SVAL sv) "PRIM" (t, ts, kenv)                    else let
326                in check (kenv, ltInsert(venv, v, t, d), d) eb                      fun chkMono v = let val t = typeofVal v
327                            in
328                              if LT.ltp_fct t orelse LT.ltp_poly t then
329                                error (le, fn () =>
330                                    prMsgLt
331                                      ("RECORD: poly type in mono record:\n",t))
332                              else ();
333                              t
334                            end
335                        in LT.ltc_tuple (map chkMono vs)
336                        end
337                    | RK_STRUCT => LT.ltc_str (map typeofVal vs)
338                in typeWith (lv,lt) e
339                end
340            | SELECT (v,n,lv,e) => let
341                val lt = catchExn
342                    (fn () => LT.lt_select (typeofVal v, n))
343                    (le,
344                     fn () =>
345                        (say "SELECT from wrong type or out of range"; LT.ltc_void))
346                in typeWith (lv,lt) e
347                end
348            | RAISE (v,lts) => (ltMatch (le,"RAISE") (typeofVal v, ltExn); lts)
349            | HANDLE (e,v) => let val lts = typeof e
350                in ltFnAppR (le,"HANDLE") (typeofVal v, lts); lts
351                end
352            | BRANCH ((_,_,lt,ts), vs, e1, e2) =>
353                let val fp = (le, "BRANCH")
354                    val lt =
355                      case ltFnApp fp (chkSnglInst fp (lt,ts), map typeofVal vs)
356                       of [lt] => lt
357                        | _ => errMsg
358                                (le,
359                                 "BRANCK : primop must return single result ",
360                                 LT.ltc_void)
361                    val _ = ltMatch fp (lt, LT.ltc_bool)
362                    val lts1 = typeof e1
363                    val lts2 = typeof e2
364                 in ltsMatch fp (lts1, lts2);
365                    lts1
366               end               end
367            | PRIMOP ((_,_,lt,ts), vs, lv, e) =>
368            | GENOP(dict, (p, t, ts), vs, v, eb) =>            typeWithBindingToSingleRsltOfInstAndApp ("PRIMOP",lt,ts,vs,lv) e
369               (* should check the consistency of dict here *)  (*
370               ltTyApp (SVAL sv) "GENOP" (t, ts, kenv)          | GENOP (dict, (_,lt,ts), vs, lv, e) =>
371              (* verify dict ? *)
372            | PACK(lt, ts, nts, sv) =>            typeWithBindingToSingleRsltOfInstAndApp ("GENOP",lt,ts,vs,lv) e
373                let val argTy = ltTyApp le "PACK-A" (lt, ts, kenv)          | ETAG (t,v,lv,e) =>
374                 in ltMatch le "PACK-M" (argTy, lpsv sv);            matchAndTypeWith ("ETAG", v, ltString, ltEtag (LT.ltc_tyc t), lv, e)
375                    ltTyApp le "PACK-R" (lt, nts, kenv)          | WRAP (t,v,lv,e) =>
376              matchAndTypeWith ("WRAP", v, LT.ltc_tyc t, ltWrap t, lv, e)
377            | UNWRAP (t,v,lv,e) =>
378              matchAndTypeWith ("UNWRAP", v, ltWrap t, LT.ltc_tyc t, lv, e)
379    *)
380                end                end
381        in typeof end
382    
383            (** these two cases should never happen before wrapping *)  in
384            | WRAP(t, b, sv, v, eb) =>    anyerror := false;
385                (ltMatch le "WRAP" (lpsv sv, LT.ltc_tyc t);    ignore (typeInEnv envs lexp);
386                 if laterPhase(phase) then LT.ltc_void    !anyerror
                else LT.ltc_tyc(if b then LT.tcc_box t else LT.tcc_abs t))  
   
           | UNWRAP(t, b, sv, v, eb) =>  
               let val ntc = if laterPhase(phase) then LT.tcc_void  
                             else (if b then LT.tcc_box t else LT.tcc_abs t)  
                   val nt = LT.ltc_tyc ntc  
                in (ltMatch le "UNWRAP" (lpsv sv, nt); LT.ltc_tyc t)  
387                end                end
388    
389            | FN(v, t, e1) =>  in (* loplevel local *)
               let val venv' = ltInsert(venv, v, t, d)  
                   val res = check (kenv, venv', d) e1  
                in ltFun(t, res) (* handle both functions and functors *)  
               end)  
390    
391    (****************************************************************************
392     *  MAIN FUNCTION --- val checkTop : FLINT.fundec * typsys -> bool          *
393     ****************************************************************************)
394    fun checkTop ((fkind, v, args, lexp) : fundec, phase) = let
395      val ve =
396        foldl (fn ((v,t), ve) => LT.ltInsert (ve,v,t,DI.top)) LT.initLtyEnv args
397      val err = check phase (LT.initTkEnv, ve, DI.top) lexp
398      val err = case fkind
399         of FK_FCT => err
400          | _ => (say "**** Not a functor at top level\n"; true)
401      in err end
402    
403    in loop  val checkTop =
404   end (* end-of-fn-check *)    Stats.doPhase (Stats.makePhase "Compiler 051 FLINTCheck") checkTop
405    
406  in  (****************************************************************************
407  anyerror := false; check (LT.initTkEnv, initLtyEnv, DI.top) lexp; !anyerror;   *  MAIN FUNCTION --- val checkExp : FLINT.lexp * typsys -> bool            *
408  end (* end of function checkTop *)   *  (currently unused?)                                                     *
409  *)   ****************************************************************************)
410    fun checkExp (le,phase) = check phase (LT.initTkEnv, LT.initLtyEnv, DI.top) le
 fun checkExp  _ = bug "checkExp not implemented yet"  
411    
412  end (* toplevel local *)  end (* toplevel local *)
413  end (* structure ChkFlint *)  end (* structure ChkFlint *)
   

Legend:
Removed from v.44  
changed lines
  Added in v.45

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