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/plambda/chkplexp.sml
ViewVC logotype

Diff of /sml/branches/primop-branch-2/src/compiler/FLINT/plambda/chkplexp.sml

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

revision 1935, Mon Jun 5 18:21:55 2006 UTC revision 2038, Mon Aug 21 23:07:07 2006 UTC
# Line 107  Line 107 
107     else LT.ltd_pfct lt) handle _ => raise LtyArrow     else LT.ltd_pfct lt) handle _ => raise LtyArrow
108    
109  val lt_inst_chk = LT.lt_inst_chk_gen()  val lt_inst_chk = LT.lt_inst_chk_gen()
110    (* kind checker for ltys *)
111    val ltyChk = LT.ltyChkGen ()
112    (* kind checker for tycs *)
113    val tycChk = LT.tkTycGen ()
114    
115  fun ltAppChk (lt, ts, kenv) =  fun ltAppChk (lt, ts, kenv) : LT.lty =
116    (case lt_inst_chk(lt, ts, kenv)    (case lt_inst_chk(lt, ts, kenv)
117      of [b] => b      of [b] => b
118       | _ => bug "unexpected ase in ltAppChk")       | _ => bug "unexpected arg in ltAppChk")
119    
120  (** utility functions for type checking *)  (** utility functions for type checking *)
121  fun ltTyApp le s (lt, ts, kenv) =  fun ltTyApp le s (lt, ts, kenv) =
# Line 120  Line 124 
124         (clickerror ();         (clickerror ();
125          say (s ^ "  **** Kind conflicting in lexp =====> \n    ");          say (s ^ "  **** Kind conflicting in lexp =====> \n    ");
126          case zz of LT.LtyAppChk => say "      exception LtyAppChk raised! \n"          case zz of LT.LtyAppChk => say "      exception LtyAppChk raised! \n"
127                   | LT.TkTycChk =>  say "      exception TkTycChk raised! \n"                   | LT.TkTycChk _ =>  say "      exception TkTycChk raised! \n"
128                   | _ => say "   other weird exception raised! \n";                   | _ => say "   other weird exception raised! \n";
129          say "\n \n"; lePrint le; say "\n For Types: \n";          say "\n \n"; lePrint le; say "\n For Types: \n";
130          ltPrint lt; say "\n and   \n    ";          ltPrint lt; say "\n and   \n    ";
# Line 149  Line 153 
153              (clickerror ();              (clickerror ();
154               say (s ^ "  **** Applying Non-Arrow Type in lexp =====> \n    ");               say (s ^ "  **** Applying Non-Arrow Type in lexp =====> \n    ");
155               case zz of LtyArrow => say "exception LtyArrow raised. \n"               case zz of LtyArrow => say "exception LtyArrow raised. \n"
156                        | LT.tcUnbound => say "exception tcUnbound raised. \n"                        | LT.TeUnbound => say "exception TeUnbound raised. \n"
157                        | _ => say "other weird exceptions raised\n";                        | _ => say "other weird exceptions raised\n";
158               say "\n \n";  lePrint le; say "\n For Types \n";               say "\n \n";  lePrint le; say "\n For Types \n";
159               ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";               ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";
# Line 165  Line 169 
169              (clickerror ();              (clickerror ();
170               say (s ^ "  **** Rev-Apply Non-Arrow Type in lexp =====> \n    ");               say (s ^ "  **** Rev-Apply Non-Arrow Type in lexp =====> \n    ");
171               case zz of LtyArrow => say "exception LtyArrow raised. \n"               case zz of LtyArrow => say "exception LtyArrow raised. \n"
172                        | LT.tcUnbound => say "exception tcUnbound raised. \n"                        | LT.TeUnbound => say "exception TeUnbound raised. \n"
173                        | _ => say "other weird exceptions raised\n";                        | _ => say "other weird exceptions raised\n";
174               say "\n \n";  lePrint le; say "\n For Types \n";               say "\n \n";  lePrint le; say "\n For Types \n";
175               ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";               ltPrint t1; say "\n and   \n    "; ltPrint t2; say "\n \n";
# Line 181  Line 185 
185         (clickerror ();         (clickerror ();
186          say (s ^ "  **** Select from a wrong-type lexp  =====> \n    ");          say (s ^ "  **** Select from a wrong-type lexp  =====> \n    ");
187          case zz of LtySelect => say "exception LtyArrow raised. \n"          case zz of LtySelect => say "exception LtyArrow raised. \n"
188                   | LT.tcUnbound => say "exception tcUnbound raised. \n"                   | LT.TeUnbound => say "exception TeUnbound raised. \n"
189                   | _ => say "other weird exceptions raised\n";                   | _ => say "other weird exceptions raised\n";
190          say "\n \n";  lePrint le; say "\n \n";          say "\n \n";  lePrint le; say "\n \n";
191          say "Selecting "; say (Int.toString i);          say "Selecting "; say (Int.toString i);
# Line 206  Line 210 
210         in ltMatch le s (nt, root); venv         in ltMatch le s (nt, root); venv
211        end        end
212    
   
213  (** check : tkindEnv * ltyEnv * DI.depth -> lexp -> lty *)  (** check : tkindEnv * ltyEnv * DI.depth -> lexp -> lty *)
214  fun check (kenv, venv, d) =  fun check (kenv, venv, d) =
215    let fun loop le =    let val ltyChkenv = ltyChk kenv
216          fun loop le =
217         (case le         (case le
218           of VAR v =>           of VAR v =>
219                (LT.ltLookup(venv, v, d)                (LT.ltLookup(venv, v, d)
# Line 220  Line 224 
224            | (INT32 _ | WORD32 _) => LT.ltc_int32            | (INT32 _ | WORD32 _) => LT.ltc_int32
225            | REAL _ => LT.ltc_real            | REAL _ => LT.ltc_real
226            | STRING _ => ltString            | STRING _ => ltString
227            | PRIM(p, t, ts) => ltTyApp le "PRIM" (t, ts, kenv)            | PRIM(p, t, ts) =>
228                 (* kind check t and ts *)
229                  ((* ltyChkenv t; map (tycChk kenv) ts; *)
230                   ltTyApp le "PRIM" (t, ts, kenv))
231    
232            | FN(v, t, e1) =>            | FN(v, t, e1) =>
233                let val venv' = LT.ltInsert(venv, v, t, d)                let val _ = ltyChkenv t (* kind check bound variable type *)
234                      val venv' = LT.ltInsert(venv, v, t, d)
235                    val res = check (kenv, venv', d) e1                    val res = check (kenv, venv', d) e1
236    (*                  val _ = ltyChkenv res *)
237                 in ltFun(t, res) (* handle both functions and functors *)                 in ltFun(t, res) (* handle both functions and functors *)
238                end                end
239    
240            | FIX(vs, ts, es, eb) =>            | FIX(vs, ts, es, eb) =>
241                let fun h (env, v::r, x::z) = h(LT.ltInsert(env, v, x, d), r, z)                let val _ = map ltyChkenv ts  (* kind check bound variable types *)
242                      fun h (env, v::r, x::z) = h(LT.ltInsert(env, v, x, d), r, z)
243                      | h (env, [], []) = env                      | h (env, [], []) = env
244                      | h _ = bug "unexpected FIX bindings in checkLty."                      | h _ = bug "unexpected FIX bindings in checkLty."
245                    val venv' = h(venv, vs, ts)                    val venv' = h(venv, vs, ts)
246    
247                    val nts = map (check (kenv, venv', d)) es                    val nts = map (check (kenv, venv', d)) es
248    (*                   val _ = map ltyChkenv nts *)
249                    val _ = app2(ltMatch le "FIX1", ts, nts)                    val _ = app2(ltMatch le "FIX1", ts, nts)
250    
251                 in check (kenv, venv', d) eb                 in check (kenv, venv', d) eb
252                end                end
253    
254            | APP(e1, e2) => ltFnApp le "APP" (loop e1, loop e2)            | APP(e1, e2) =>
255                  let val top = loop e1
256                      val targ = loop e2
257                  in (* ltyChkenv top; ltyChkenv targ; *)
258                     ltFnApp le "APP" (top, targ)
259                  end
260    
261            | LET(v, e1, e2) =>            | LET(v, e1, e2) =>
262                let val venv' = LT.ltInsert(venv, v, loop e1, d)                let val t1 = loop e1
263    (*                  val _ = ltyChkenv t1 *)
264                      val venv' = LT.ltInsert(venv, v, t1, d)
265                 in check (kenv, venv', d) e2                 in check (kenv, venv', d) e2
266                end                end
267    
268            | TFN(ks, e) =>            | TFN(ks, e) =>
269                let val kenv' = LT.tkInsert(kenv, ks)                let val kenv' = LT.tkInsert(kenv, ks)
270                    val lt = check (kenv', venv, DI.next d) e                    val lt = check (kenv', venv, DI.next d) e
271    (*                  val _ = ltyChkenv lt *)
272                 in LT.ltc_poly(ks, [lt])                 in LT.ltc_poly(ks, [lt])
273                end                end
274    
275            | TAPP(e, ts) => ltTyApp le "TAPP" (loop e, ts, kenv)            | TAPP(e, ts) =>
276                  let val lt = loop e
277    (*                  val _ = ltyChkenv lt *)
278                  in  ltTyApp le "TAPP" (lt, ts, kenv)
279                  end
280    
281            | GENOP(dict, p, t, ts) =>            | GENOP(dict, p, t, ts) =>
282                ((* should type check dict also *)                ((* should type check dict also *)
283                 ltTyApp le "GENOP" (t, ts, kenv))                 ltTyApp le "GENOP" (t, ts, kenv))
# Line 266  Line 290 
290    
291            | CON((_, rep, lt), ts, e) =>            | CON((_, rep, lt), ts, e) =>
292                let val t1 = ltTyApp le "CON" (lt, ts, kenv)                let val t1 = ltTyApp le "CON" (lt, ts, kenv)
293    (*                  val _ = ltyChkenv t1 *)
294                    val t2 = loop e                    val t2 = loop e
295    (*                  val _ = ltyChkenv t2 *)
296                 in ltFnApp le "CON-A" (t1, t2)                 in ltFnApp le "CON-A" (t1, t2)
297                end                end
298  (*  (*
# Line 330  Line 356 
356                    val nt = LT.ltc_tyc ntc                    val nt = LT.ltc_tyc ntc
357                 in (ltMatch le "UNWRAP" (loop e, nt); LT.ltc_tyc t)                 in (ltMatch le "UNWRAP" (loop e, nt); LT.ltc_tyc t)
358                end)                end)
359      in (* wrap loop with kind check of result *)
360         fn x => let val y = loop x in ltyChkenv y; y end
   in loop  
361   end (* end-of-fn-check *)   end (* end-of-fn-check *)
362    
363  in  in
# Line 342  Line 367 
367    
368  end (* toplevel local *)  end (* toplevel local *)
369  end (* structure CheckLty *)  end (* structure CheckLty *)
   

Legend:
Removed from v.1935  
changed lines
  Added in v.2038

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