| 1 | val toString = Int.toString |
| 2 | |
| 3 | (* Ported to kit 23/4/97 by Mads. |
| 4 | Commented out module phrases and changed a couple of sml/nj things (like makestring) |
| 5 | No rewriting to please region inference. |
| 6 | Still it uses less that 100Kb when it runs (see region.ps) |
| 7 | *) |
| 8 | |
| 9 | (* This is a quickly written type checker for subtyping, using the |
| 10 | MATCH and TYPE algorithms from the Fuh and Mishra paper. |
| 11 | |
| 12 | The code is ugly at places, and no consideration has been given to |
| 13 | effeciency -- please accept my apologies |
| 14 | |
| 15 | -- Mads*) |
| 16 | |
| 17 | (* |
| 18 | structure List = (* list utilities *) |
| 19 | struct |
| 20 | *) |
| 21 | type 'a set = 'a list; (* sets are represented by lists without repeated |
| 22 | elements *) |
| 23 | val emptyset = [] |
| 24 | |
| 25 | fun isin(x,[])=false |
| 26 | | isin(x,(y::rest)) = x=y orelse isin(x,rest) |
| 27 | |
| 28 | fun union([],l) = l |
| 29 | | union((x::rest),l) = if isin(x,l) then union(rest,l) |
| 30 | else x:: union(rest,l); |
| 31 | fun intersect([],l) = [] |
| 32 | | intersect((x::rest),l) = if isin(x,l) then x:: intersect(rest,l) |
| 33 | else intersect(rest,l); |
| 34 | fun setminus([],l) = [] |
| 35 | | setminus(x::l,l') = if isin(x,l') then setminus(l,l') |
| 36 | else x:: setminus(l,l'); |
| 37 | fun foldr f b [] = b |
| 38 | | foldr f b (x::rest) = f(x,foldr f b rest); |
| 39 | |
| 40 | fun foldl f base [] = base |
| 41 | | foldl f base (x::xs) = foldl f (f(x, base)) xs |
| 42 | |
| 43 | (* function for finding transitive closure. |
| 44 | Culled from other application. |
| 45 | DO NOT READ (CRUDE AND INEFFICIENT) *) |
| 46 | |
| 47 | fun transClos (eq: 'a * 'a -> bool) |
| 48 | (insert_when_eq: bool) |
| 49 | (newsets: 'a set list, |
| 50 | oldsets: 'a set list): bool * 'a set list = |
| 51 | (* The lists in oldsets are pairwise disjoint, but nothing is known about the |
| 52 | lists in newsets. The resulting sets are pairwise disjoint, |
| 53 | and moreover, the resulting boolean is true if and only if |
| 54 | every member (i.e. list) of newsets, is contained in some member (i.e., list) |
| 55 | of oldsets *) |
| 56 | let |
| 57 | val any: bool = true (* could be false, for that matter *) |
| 58 | |
| 59 | fun isin(x,[]) = false |
| 60 | | isin(x,x'::rest) = eq(x,x') orelse isin(x,rest) |
| 61 | |
| 62 | (* In the following function, L is a list of pairwise disjoint |
| 63 | sets. S' is the set currently under construction; |
| 64 | it is also disjoint from the sets in L. x |
| 65 | will be added to S' if x is not in any set in L. *) |
| 66 | |
| 67 | fun add(x:'a, |
| 68 | (found_fixpt: bool, found_class: bool, L as [], S')): |
| 69 | bool * bool * 'a list list * 'a list = |
| 70 | if isin(x,S') |
| 71 | then if insert_when_eq |
| 72 | then |
| 73 | (found_fixpt andalso found_class, found_class,[],x::S') |
| 74 | else |
| 75 | (found_fixpt andalso found_class, found_class,[],S') |
| 76 | else |
| 77 | (false, any, [], x::S') |
| 78 | |
| 79 | | add(x,(found_fixpt,found_class,(S::L), S')) = |
| 80 | if isin(x,S) |
| 81 | then |
| 82 | if insert_when_eq |
| 83 | then |
| 84 | (found_fixpt andalso not found_class,true, L, x::(S @ S')) |
| 85 | else |
| 86 | (found_fixpt andalso not found_class,true, L, S @ S') |
| 87 | else |
| 88 | let val (found_fixpt1, found_class1, L1, S1)= |
| 89 | add(x,(found_fixpt,found_class,L,S')) |
| 90 | in |
| 91 | (found_fixpt andalso found_fixpt1, |
| 92 | found_class orelse found_class1, |
| 93 | S::L1, |
| 94 | S1 |
| 95 | ) |
| 96 | end |
| 97 | |
| 98 | fun add_S (S,(found_fixpt, oldsets)) : bool * 'a set list = |
| 99 | let |
| 100 | val (found_fixpt1, _, L1, S1) = |
| 101 | foldl add (found_fixpt, false, oldsets, emptyset) S |
| 102 | in |
| 103 | case S1 of |
| 104 | [] => (found_fixpt andalso found_fixpt1, L1) |
| 105 | | _ => (found_fixpt andalso found_fixpt1, S1::L1) |
| 106 | end |
| 107 | |
| 108 | in |
| 109 | foldl add_S (true, oldsets) newsets |
| 110 | end |
| 111 | (* |
| 112 | end; |
| 113 | *) |
| 114 | (* |
| 115 | structure Variables = (* program variables *) |
| 116 | struct |
| 117 | *) |
| 118 | type var = string |
| 119 | (* |
| 120 | end; |
| 121 | *) |
| 122 | (*structure Type = (* Types, substitutions and matching *) |
| 123 | struct |
| 124 | local |
| 125 | (* open List Variables*) |
| 126 | in |
| 127 | *) datatype ty = INT | REAL | ARROW of ty * ty | PROD of ty * ty | TYVAR of int |
| 128 | |
| 129 | type subst = ty -> ty |
| 130 | |
| 131 | fun mk_subst_ty(i: int,ty:ty):subst = |
| 132 | let |
| 133 | fun S(INT) = INT |
| 134 | | S(REAL) = REAL |
| 135 | | S(ARROW(ty1,ty2)) = ARROW(S ty1, S ty2) |
| 136 | | S(PROD(ty1,ty2)) = PROD(S ty1, S ty2) |
| 137 | | S(tv as TYVAR j) = if i=j then ty else tv |
| 138 | in |
| 139 | S |
| 140 | end; |
| 141 | |
| 142 | val Id = fn x => x; |
| 143 | |
| 144 | val r = ref 0; (* counter for fresh type variables *) |
| 145 | fun fresh() = (r:= !r + 1; ! r); |
| 146 | fun fresh_ty() = TYVAR(fresh()); |
| 147 | |
| 148 | (* free variables *) |
| 149 | |
| 150 | fun fv_ty (INT,acc) = acc |
| 151 | | fv_ty (REAL,acc) = acc |
| 152 | | fv_ty(ARROW(t1,t2), acc) = fv_ty(t1,fv_ty(t2,acc)) |
| 153 | | fv_ty(PROD(t1,t2), acc) = fv_ty(t1,fv_ty(t2,acc)) |
| 154 | | fv_ty((TYVAR i),acc) = if isin(i,acc) then acc else i :: acc; |
| 155 | |
| 156 | fun tyvars(t:ty) = fv_ty(t,[]) |
| 157 | |
| 158 | fun fv_tyenv TE = |
| 159 | foldr (fn((i,tau),acc)=> fv_ty(tau,acc)) [] TE |
| 160 | |
| 161 | (* ALLNEW, page 168: create a fresh copy of a type, using type variables |
| 162 | at the leaves of the type *) |
| 163 | |
| 164 | fun allnew(INT) = fresh_ty() |
| 165 | | allnew(REAL) = fresh_ty() |
| 166 | | allnew(ARROW(t1,t2)) = ARROW(allnew(t1),allnew(t2)) |
| 167 | | allnew(PROD(t1,t2)) = PROD(allnew(t1),allnew(t2)) |
| 168 | | allnew(TYVAR _) = fresh_ty(); |
| 169 | |
| 170 | (* PAIR, page 168: create list of atomic types that occur in the same |
| 171 | places of t1 and t2 *) |
| 172 | |
| 173 | fun pair(ARROW(t1,t2),ARROW(t1',t2')) = pair(t1,t1') @ pair (t2,t2') |
| 174 | | pair(PROD(t1,t2),PROD(t1',t2')) = pair(t1,t1') @ pair (t2,t2') |
| 175 | | pair(t1,t2) = [[t1,t2]] |
| 176 | |
| 177 | (* dealing with equivalence classes of atomic types -- for algorithm MATCH *) |
| 178 | |
| 179 | (* M_v, page 168: removing that equivalence class containing v from M *) |
| 180 | |
| 181 | fun remove([], v) = [] |
| 182 | | remove((class::rest), v) = |
| 183 | if isin(v,class) then rest else class:: remove(rest,v); |
| 184 | |
| 185 | (* [a]_M, page 168: the equivalence class containing a *) |
| 186 | |
| 187 | exception ClassOff |
| 188 | |
| 189 | fun class_of([],a) = raise ClassOff |
| 190 | | class_of((class::rest), a) = |
| 191 | if isin(a,class) then class else class_of(rest,a); |
| 192 | |
| 193 | (* [t]^M, page 168: the set of type variables eqivalent to some type variable |
| 194 | occurring in non-atomic type t *) |
| 195 | |
| 196 | fun equiv_tyvars(t,M): ty list = |
| 197 | foldr union [] ((map (fn a=> class_of(M,TYVAR a)) (tyvars(t))): ty list list) ; |
| 198 | |
| 199 | fun transitive_closure(oldsets,newsets) = |
| 200 | #2(transClos(op = : ty*ty-> bool)(false)(newsets,oldsets)) |
| 201 | |
| 202 | (* Coercion sets *) |
| 203 | |
| 204 | type coercion = ty * ty |
| 205 | |
| 206 | type coercion_set = coercion list |
| 207 | |
| 208 | fun on_C(S,C) = map (fn(t1,t2) => (S t1, S t2)) C |
| 209 | |
| 210 | fun atomic t = |
| 211 | case t of |
| 212 | INT => true |
| 213 | | REAL => true |
| 214 | | TYVAR _ => true |
| 215 | | _ => false; |
| 216 | |
| 217 | (* diagonal is used in match to create initial equivalence relation*) |
| 218 | |
| 219 | |
| 220 | fun diagonal(C: coercion_set) = |
| 221 | let |
| 222 | fun diag(t,acc) = |
| 223 | case t of |
| 224 | INT => union([INT],acc) |
| 225 | | REAL => union([REAL],acc) |
| 226 | | PROD(t1,t2) => diag(t1,diag(t2,acc)) |
| 227 | | ARROW(t1,t2) => diag(t1,diag(t2,acc)) |
| 228 | | TYVAR _ => union([t],acc) |
| 229 | |
| 230 | fun diag2((t1,t2),acc) = diag(t1,diag(t2,acc)) |
| 231 | |
| 232 | val atomics = foldr diag2 [] C |
| 233 | in |
| 234 | map (fn atomic => [atomic,atomic]) atomics |
| 235 | end |
| 236 | |
| 237 | fun ground_atomic t = |
| 238 | case t of |
| 239 | INT => true |
| 240 | | REAL => true |
| 241 | | _ => false; |
| 242 | |
| 243 | fun contains_no_type_constant [] = true |
| 244 | | contains_no_type_constant (t::rest) = |
| 245 | not (ground_atomic t) andalso contains_no_type_constant rest; |
| 246 | |
| 247 | exception MATCH |
| 248 | |
| 249 | local |
| 250 | fun match1([]:coercion_set,S:subst,M) = S |
| 251 | | match1((t1,t2)::C, S, M) = |
| 252 | if atomic t1 andalso atomic t2 then atomicElimination(t1,t2,C,S,M) |
| 253 | else if atomic t1 then expansion(t1,t2,C,S,M) |
| 254 | else if atomic t2 then expansion(t2,t1,C,S,M) |
| 255 | else decomposition(t1,t2,C,S,M) |
| 256 | |
| 257 | and atomicElimination(t1,t2,C,S,M) = |
| 258 | match1(C,S,transitive_closure(M,[[t1,t2]])) |
| 259 | |
| 260 | and decomposition(ARROW(t1,t2),ARROW(t1',t2'),C,S,M)= |
| 261 | match1((t1',t1)::(t2,t2')::C, S, M) |
| 262 | | decomposition(PROD(t1,t2),PROD(t1',t2'),C,S,M)= |
| 263 | match1((t1,t1')::(t2,t2')::C, S, M) |
| 264 | | decomposition(_) = raise MATCH |
| 265 | |
| 266 | and expansion(t1:ty,t2:ty,C,S,M) = |
| 267 | case intersect(class_of(M,t1), equiv_tyvars(t2,M)) (* occurs check *) |
| 268 | of |
| 269 | []=> if contains_no_type_constant(class_of(M,t1)) |
| 270 | then |
| 271 | (* not matching of int or real with arrow or prod *) |
| 272 | let |
| 273 | fun loop([],C,S,M) = match1(C,S,M) |
| 274 | | loop((TYVAR alpha)::tyvars, C, S, M) = |
| 275 | let val t' = allnew t2 |
| 276 | val delta = mk_subst_ty(alpha,t') |
| 277 | in |
| 278 | loop(tyvars, on_C(delta,C), delta o S, |
| 279 | transitive_closure(M,pair(t2,t'))) |
| 280 | end |
| 281 | | loop((_::tyvars), C, S, M) = |
| 282 | (* skip atomic types, that are not variables *) |
| 283 | loop(tyvars, C, S, M) |
| 284 | in |
| 285 | loop(class_of(M,t1),C,S,M) |
| 286 | end |
| 287 | |
| 288 | else (* matching of int or real with arrow or prod *) |
| 289 | raise MATCH |
| 290 | |
| 291 | | _ => (* occurs check failed *) |
| 292 | raise MATCH |
| 293 | in |
| 294 | |
| 295 | fun match(C) = match1(C,Id,diagonal C); |
| 296 | |
| 297 | end |
| 298 | |
| 299 | (* Type Environments *) |
| 300 | |
| 301 | type tyenv = (var * ty)list (* no polymorphism! *) |
| 302 | |
| 303 | (* looking up variables in the type environement *) |
| 304 | |
| 305 | exception Lookup; |
| 306 | |
| 307 | fun lookup(i,[]) = raise Lookup |
| 308 | | lookup(i,((j,sigma)::rest)) = if i=j then sigma else lookup(i,rest); |
| 309 | |
| 310 | fun on_tyenv(S:subst,TE:tyenv) = |
| 311 | map (fn(i,tau) => (i, S tau)) TE |
| 312 | |
| 313 | (* pretty printing -- actually not very pretty, but it will do *) |
| 314 | |
| 315 | (* precedences: -> : 1 |
| 316 | * : 2 *) |
| 317 | |
| 318 | fun pp_ty' (context:int,INT) = "INT" |
| 319 | | pp_ty'(_,REAL) = "REAL" |
| 320 | | pp_ty'(context,ARROW(ty1, ty2)) = |
| 321 | let val s = pp_ty'(2,ty1) ^ "->" ^ |
| 322 | pp_ty'(1, ty2) |
| 323 | in |
| 324 | if context > 1 then "(" ^ s ^ ")" else s |
| 325 | end |
| 326 | | pp_ty'(context,PROD(ty1, ty2)) = |
| 327 | let val s = pp_ty'(3,ty1) ^ "*" ^ pp_ty'(3,ty2) |
| 328 | in |
| 329 | if context > 2 then "(" ^ s ^ ")" |
| 330 | else s |
| 331 | end |
| 332 | | pp_ty'(context,(TYVAR i)) = "'a" ^ toString i; |
| 333 | |
| 334 | fun pp_ty ty = pp_ty'(0,ty) |
| 335 | |
| 336 | local |
| 337 | fun filter [] = [] |
| 338 | | filter ((x,sigma)::rest) = |
| 339 | if isin(x,["fst","snd","floor"]) |
| 340 | (* hack to avoid printing of built-in variables fst, snd and floor *) |
| 341 | then filter rest |
| 342 | else (x,sigma)::filter rest |
| 343 | |
| 344 | fun pp_tyenv [] = "" |
| 345 | | pp_tyenv ([(x,sigma)]) = |
| 346 | x ^ ":" ^ pp_ty sigma ^ " " |
| 347 | | pp_tyenv ((x,sigma)::rest) = |
| 348 | x ^ ":" ^ pp_ty sigma ^ "," ^ pp_tyenv rest; |
| 349 | in |
| 350 | val pp_tyenv = pp_tyenv o filter |
| 351 | end |
| 352 | |
| 353 | fun pp_coercion(tau1,tau2) = "\n " ^ pp_ty tau1 ^ " |> " ^ pp_ty tau2 |
| 354 | |
| 355 | fun pp_coercion_set [] = "" |
| 356 | | pp_coercion_set[coercion] = pp_coercion coercion |
| 357 | | pp_coercion_set(coercion::rest) = |
| 358 | pp_coercion coercion ^ ", " ^ pp_coercion_set rest |
| 359 | |
| 360 | (* |
| 361 | end (* local *) |
| 362 | end; |
| 363 | *) |
| 364 | |
| 365 | (*structure Expressions = |
| 366 | struct |
| 367 | local |
| 368 | open List Variables |
| 369 | in |
| 370 | *) datatype exp = VAR of var |
| 371 | | INTCON of int |
| 372 | | REALCON of real |
| 373 | | LAM of var * exp |
| 374 | | APP of exp * exp |
| 375 | | LET of var * exp * exp |
| 376 | | PLUS of exp |
| 377 | | MINUS of exp |
| 378 | | PAIR of exp * exp; |
| 379 | |
| 380 | (* pretty printing *) |
| 381 | |
| 382 | fun pp_exp(VAR x) = x |
| 383 | | pp_exp(LAM(x,e')) = "(fn " ^ x ^ " =>" ^ pp_exp e' ^ ")" |
| 384 | | pp_exp(APP(e1,e2)) = "(" ^ pp_exp e1 ^ " @ " ^ pp_exp e2 ^ ")" |
| 385 | | pp_exp(LET(x,e1,e2)) = "let " ^ x ^ "=" ^ pp_exp e1 ^ " in " ^ pp_exp e2 ^ "end" |
| 386 | | pp_exp(INTCON i) = toString i |
| 387 | | pp_exp(REALCON r) = toString(floor r) ^ ".?" |
| 388 | | pp_exp(PLUS(e1)) = "(+" ^ pp_exp e1 ^ ")" |
| 389 | | pp_exp(MINUS(e1)) = "(-" ^ pp_exp e1 ^ ")" |
| 390 | | pp_exp(PAIR(e1,e2)) = "(" ^ pp_exp e1 ^ "," ^ pp_exp e2 ^ ")" |
| 391 | (* |
| 392 | end (* local *) |
| 393 | end; |
| 394 | *) |
| 395 | |
| 396 | |
| 397 | (*structure TypeChecker= |
| 398 | struct |
| 399 | local |
| 400 | open List Variables Type Expressions |
| 401 | in |
| 402 | *) |
| 403 | type job = tyenv * exp * ty |
| 404 | |
| 405 | fun TYPE(TE:tyenv,e:exp) : ty * coercion_set = |
| 406 | let val alpha0 = fresh_ty() |
| 407 | val C = TY([(TE,e,alpha0)],[]) |
| 408 | in (alpha0, C) |
| 409 | end |
| 410 | |
| 411 | and TY([]: job list, C: coercion_set)= C |
| 412 | | TY((job as (TE,e,tau)) :: rest, C: coercion_set)= |
| 413 | case e of |
| 414 | VAR x => TY(rest, (lookup(x,TE),tau)::C) |
| 415 | | LAM(x,e') => |
| 416 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); |
| 417 | val TE' = (x,(new_ty1))::TE |
| 418 | in |
| 419 | TY((TE',e',new_ty2)::rest, (ARROW(new_ty1,new_ty2), tau):: C) |
| 420 | end |
| 421 | | APP(e1,e2) => |
| 422 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); |
| 423 | in |
| 424 | TY((TE,e1,ARROW(new_ty1,new_ty2))::(TE,e2,new_ty1)::rest, |
| 425 | (new_ty2,tau)::C) |
| 426 | end |
| 427 | | LET(x,e1,e2) => |
| 428 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); |
| 429 | in |
| 430 | TY((TE,e1,new_ty1)::((x,new_ty1)::TE,e2,new_ty2)::rest, |
| 431 | (new_ty2,tau)::C) |
| 432 | end |
| 433 | | INTCON i => TY(rest, (INT, tau):: C) |
| 434 | | REALCON i => TY(rest, (REAL, tau):: C) |
| 435 | |
| 436 | | PLUS e1 => TY((TE,e1, PROD(INT,INT))::rest, (PROD(INT,INT),tau):: C) |
| 437 | | MINUS e1 => TY((TE,e1, PROD(INT,INT))::rest, (PROD(INT,INT),tau):: C) |
| 438 | | PAIR(e1,e2) => |
| 439 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); |
| 440 | in |
| 441 | TY((TE,e1,new_ty1)::(TE,e2,new_ty2)::rest, |
| 442 | (PROD(new_ty1,new_ty2),tau)::C) |
| 443 | end |
| 444 | |
| 445 | type judgement = coercion_set * tyenv * exp * ty |
| 446 | |
| 447 | fun pp_judgement(C,TE,e,tau) = |
| 448 | "\nCoersion set: " ^ pp_coercion_set C ^ |
| 449 | "\nType environment: " ^ pp_tyenv TE ^ |
| 450 | "\nExpression: " ^ pp_exp e ^ |
| 451 | "\nType: " ^ pp_ty tau; |
| 452 | |
| 453 | (* |
| 454 | end (* local *) |
| 455 | end; |
| 456 | *) |
| 457 | |
| 458 | |
| 459 | (*structure Run = |
| 460 | struct |
| 461 | local |
| 462 | open List Variables Type Expressions TypeChecker |
| 463 | in |
| 464 | *) val e0 = (* let val Id = fn x => x in (Id 3, Id 4.0) end *) |
| 465 | let |
| 466 | val Id = LAM("x",VAR "x") |
| 467 | val pair = PAIR(APP(VAR "Id", INTCON 3), APP(VAR "Id", REALCON 4.0)) |
| 468 | in |
| 469 | LET("Id",Id, pair) |
| 470 | end; |
| 471 | |
| 472 | val e1 = (* let val makepair = fn x => (x,x) in makepair 3.14 *) |
| 473 | let |
| 474 | val makepair = LAM("x",PAIR(VAR "x", VAR "x")) |
| 475 | in |
| 476 | LET("makepair", makepair, APP(VAR "makepair", REALCON 3.14)) |
| 477 | end |
| 478 | |
| 479 | val e2 = (* let fun mappair = fn f => fn x => (f (fst x), f (snd x)) |
| 480 | in mappair floor (3.14,2.18) end *) |
| 481 | |
| 482 | let |
| 483 | val mappair = LAM("f",LAM("x", |
| 484 | PAIR(APP(VAR "f",APP(VAR "fst", VAR "x")), |
| 485 | APP(VAR "f",APP(VAR "snd", VAR "x"))))) |
| 486 | in |
| 487 | LET("mappair",mappair, APP(APP(VAR "mappair", VAR "floor"), |
| 488 | PAIR(REALCON 3.14, REALCON 2.18))) |
| 489 | end; |
| 490 | |
| 491 | val e3 = (* fn x => x *) |
| 492 | LAM("x",VAR "x") |
| 493 | val e4 = (* fn f => fn x => f x *) |
| 494 | LAM("f",LAM("x",APP(VAR "f", VAR "x"))); |
| 495 | val e5 = (* fn f => fn x => f(f x) *) |
| 496 | LAM("f",LAM("x",APP(VAR "f", APP(VAR "f", VAR "x")))); |
| 497 | |
| 498 | |
| 499 | fun run(e: exp, outfilename: string) = |
| 500 | let |
| 501 | val _ = r:= 5; (* reset counter for type variables *) |
| 502 | val _ = print("\nprocessing " ^ outfilename ^ "...") |
| 503 | val TE0 = |
| 504 | [("fst", (ARROW(PROD(TYVAR 0,TYVAR 1),TYVAR 0))), (* the type of fst *) |
| 505 | ("snd", (ARROW(PROD(TYVAR 0,TYVAR 1),TYVAR 1))), (* the type of snd *) |
| 506 | ("floor", (ARROW(REAL,INT)))] (* the type of floor *) |
| 507 | val _ = print("running TYPE...") |
| 508 | val (ty,C) = TYPE(TE0,e) ; |
| 509 | val os = TextIO.openOut outfilename; |
| 510 | val _ = TextIO.output(os, "\nResult of TYPE:\n\n\n " ^ pp_judgement(C,TE0,e,ty)); |
| 511 | val _ = print("running MATCH...") |
| 512 | val S = match C |
| 513 | val judgem' as (C',TE',e',ty') = (on_C(S,C),on_tyenv(S,TE0),e,S ty) |
| 514 | val _ = TextIO.output(os, "\n\n\nResult of MATCH:\n\n\n " ^ pp_judgement judgem'); |
| 515 | in |
| 516 | TextIO.closeOut os |
| 517 | end; |
| 518 | |
| 519 | val _ = run(e0,"outFuhMishra0"); |
| 520 | val _ = run(e1,"outFuhMishra1"); |
| 521 | val _ = run(e2,"outFuhMishra2"); |
| 522 | val _ = run(e3,"outFuhMishra3"); |
| 523 | val _ = run(e4,"outFuhMishra4"); |
| 524 | val _ = run(e5,"outFuhMishra5"); |
| 525 | |
| 526 | (* |
| 527 | end (* local *) |
| 528 | end (*struct*); |
| 529 | *) |
| 530 | |
| 531 | val _ = print "\n" |