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

Legend:
Removed from v.23  
changed lines
  Added in v.24

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