regression/FuhMishra.sml

   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"