home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / asl / typing.ml < prev   
Encoding:
Text File  |  1995-06-19  |  7.0 KB  |  225 lines  |  [TEXT/MPS ]
  1. (* $Id: typing.ml,v 1.6 1995/06/19 12:43:40 doligez Exp $ *)
  2.  
  3. #open "parser";;
  4.  
  5. let rec nth n = function
  6.      []  -> raise (Failure "nth")
  7.   | x::l -> if n=1 then x else nth (n-1) l;;
  8.  
  9. type asl_type =
  10.   Unknown
  11. | Number
  12. | TypeVar of vartype
  13. | Arrow of asl_type * asl_type
  14. and vartype = {
  15.   Index         : int;
  16.   mutable Value : asl_type
  17. }
  18. and asl_type_scheme = Forall of int list * asl_type
  19. ;;
  20.  
  21. exception TypingBug of string;;
  22.  
  23. let new_vartype, reset_vartypes =
  24.   (* Generating and resetting unknowns *)
  25.   let counter = ref 0 in
  26.   (function () -> counter := !counter+1; {Index = !counter; Value = Unknown}),
  27.   (function () -> counter := 0)
  28. ;;
  29.  
  30. let rec shorten t =
  31.     match t with
  32.      TypeVar {Index=_; Value=Unknown} -> t
  33.    | TypeVar ({Index=_;
  34.                 Value=TypeVar {Index=_;
  35.                                Value=Unknown} as tv}) -> tv
  36.    | TypeVar ({Index=_; Value=TypeVar tv1} as tv2)
  37.             -> tv2.Value <- tv1.Value; shorten t
  38.    | TypeVar {Index=_; Value=t'} -> t'
  39.    | Unknown -> raise (TypingBug "shorten")
  40.    | t' -> t';;
  41. exception TypeClash of asl_type * asl_type;;
  42.  
  43. let occurs {Index=n;Value=_} = occrec
  44.   where rec occrec =
  45.   function TypeVar{Index=m;Value=Unknown} -> (n=m)
  46.          | TypeVar{Index=m;Value=t} -> (n=m) or (occrec t)
  47.          | Number -> false
  48.          | Arrow(t1,t2) -> (occrec t1) or (occrec t2)
  49.          | Unknown -> raise (TypingBug "occurs")
  50. ;;
  51.  
  52. let rec unify (tau1,tau2) =
  53.   match (shorten tau1, shorten tau2)
  54.   with (* type variable n and type variable m *)
  55.        (TypeVar({Index=n; Value=Unknown} as tv1) as t1),
  56.        (TypeVar({Index=m; Value=Unknown} as tv2) as t2)
  57.            -> if n=m then () else tv1.Value <- t2
  58.      | (* type t1 and type variable *)
  59.       t1, (TypeVar ({Index=_;Value=Unknown} as tv) as t2)
  60.             -> if not(occurs tv t1) then tv.Value <- t1
  61.                else raise (TypeClash (t1,t2))
  62.      | (* type variable and type t2 *)
  63.        (TypeVar ({Index=_;Value=Unknown} as tv) as t1), t2
  64.             -> if not(occurs tv t2) then tv.Value <- t2
  65.                else raise (TypeClash (t1,t2))
  66.      | Number, Number -> ()
  67.      | Arrow(t1,t2), (Arrow(t'1,t'2) as t)
  68.             -> unify(t1,t'1); unify(t2,t'2)
  69.      | (t1,t2) -> raise (TypeClash (t1,t2));;
  70.  
  71. let init_typing_env =
  72.     map (function s ->
  73.             Forall([],Arrow(Number,
  74.                               Arrow(Number,Number))))
  75.          init_env ;;
  76.  
  77. let global_typing_env = ref init_typing_env;;
  78. let vars_of_type tau = vars [] tau
  79.  where rec vars vs =
  80.   function Number -> vs
  81.          | TypeVar {Index=n; Value=Unknown}
  82.                  -> if mem n vs then vs else n::vs
  83.          | TypeVar {Index=_; Value= t} -> vars vs t
  84.          | Arrow(t1,t2) -> vars (vars vs t1) t2
  85.          | Unknown -> raise (TypingBug "vars_of_type");;
  86.  
  87. let unknowns_of_type (bv,t) =
  88.     subtract (vars_of_type t) bv;;
  89. let flat = it_list (prefix @) [];;
  90.  
  91. let unknowns_of_type_env env =
  92.     flat (map (function Forall(gv,t) -> unknowns_of_type (gv,t)) env)
  93. ;;
  94.  
  95. let rec make_set = function
  96.      []  -> []
  97.   | x::l -> if mem x l then make_set l else x::make_set l
  98. ;;
  99.  
  100. let generalise_type (gamma, tau) =
  101.   let genvars =
  102.     make_set (subtract (vars_of_type tau) (unknowns_of_type_env gamma))
  103.   in Forall(genvars, tau)
  104. ;;
  105.  
  106. let gen_instance (Forall(gv,tau)) = 
  107.   (* We associate a new unknown to each generic variable *)
  108.   let unknowns =
  109.       map (function n -> n, TypeVar(new_vartype()))
  110.           gv
  111.   in ginstance tau
  112.   where rec ginstance = function
  113.         (TypeVar {Index=n; Value=Unknown} as t) ->
  114.                     (try assoc n unknowns
  115.                      with Not_found -> t)
  116.       | TypeVar {Index=_; Value= t} -> ginstance t
  117.       | Number -> Number
  118.       | Arrow(t1,t2) -> Arrow(ginstance t1, ginstance t2)
  119.       | Unknown -> raise (TypingBug "gen_instance")
  120. ;;
  121. let rec asl_typing_expr gamma = type_rec
  122. where rec type_rec = function
  123.     Const _ -> Number
  124.   | Var n ->
  125.       let sigma =
  126.         try nth n gamma
  127.         with Failure _ -> raise (TypingBug "Unbound")
  128.       in gen_instance sigma
  129.   | Cond (e1,e2,e3) ->
  130.       let t1 = unify(Number, type_rec e1)
  131.       and t2 = type_rec e2 and t3 = type_rec e3
  132.       in unify(t2, t3); t3
  133.   | App((Abs(x,e2) as f), e1) -> (* LET case *)
  134.       let t1 = type_rec e1 in
  135.       let sigma = generalise_type (gamma,t1)
  136.       in asl_typing_expr (sigma::gamma) e2
  137.   | App(e1,e2) ->
  138.       let u = TypeVar(new_vartype())
  139.       in unify(type_rec e1,Arrow(type_rec e2,u)); u
  140.   | Abs(x,e) ->
  141.       let u = TypeVar(new_vartype()) in
  142.       let s = Forall([],u)
  143.       in Arrow(u,asl_typing_expr (s::gamma) e)
  144. ;;
  145.  
  146. let tvar_name n =
  147.  (* Computes a name "'a", ... for type variables, *)
  148.  (* given an integer n representing the position  *)
  149.  (* of the type variable in the list of generic   *)
  150.  (* type variables                                *)
  151.  let rec name_of n =
  152.     let q,r = (n / 26), (n mod 26) in
  153.     let s = make_string 1 (char_of_int (96+r)) in
  154.     if q=0 then s else (name_of q)^s
  155.  in "'"^(name_of n)
  156. ;;
  157.  
  158. let print_type_scheme (Forall(gv,t)) =
  159.  (* Prints a type scheme.               *)
  160.  (* Fails when it encounters an unknown *)
  161.  let names = (names_of (1,gv)
  162.       where rec names_of = function
  163.              (n,[]) -> []
  164.            | (n,(v1::lv)) -> (tvar_name n)
  165.                            ::(names_of (n+1, lv))) in
  166.  let tvar_names = combine (rev gv,names) in
  167.  let rec print_rec = function
  168.       TypeVar{Index=n; Value=Unknown} ->
  169.          let name =
  170.              try assoc n tvar_names
  171.              with Not_found ->
  172.                raise (TypingBug "Non generic variable")
  173.          in print_string name
  174.     | TypeVar{Index=_;Value=t} -> print_rec t
  175.     | Number -> print_string "Number"
  176.     | Arrow(t1,t2) ->
  177.            print_string "("; print_rec t1;
  178.            print_string " -> "; print_rec t2;
  179.            print_string ")"
  180.     | Unknown -> raise (TypingBug "print_type_scheme")
  181.   in
  182.   print_rec t
  183. ;;
  184.  
  185. let typing (Decl(s,e)) =
  186.   reset_vartypes();
  187.   let tau =
  188.     try asl_typing_expr !global_typing_env e
  189.     with TypeClash(t1,t2) ->
  190.       let vars = vars_of_type(t1) @ vars_of_type(t2) in
  191.       print_string "*** ASL Type clash between ";
  192.       print_type_scheme (Forall(vars, t1));
  193.       print_string " and ";
  194.       print_type_scheme (Forall(vars, t2));
  195.       reset_vartypes();
  196.       raise (Failure "ASL typing")
  197.   in                    
  198.   generalise_type([], tau)
  199. ;;
  200.  
  201. (*
  202. global_env:=init_env;;
  203. typing (parse_top "x=1;");;
  204. typing (parse_top "y = + 2 ((\\x.x) 3);");;
  205. typing (parse_top "z = C (+ 0 1) 1 0;");;
  206. typing (parse_top "i = \\x.x;");;
  207. typing (parse_top "t = + (i 1) (i i 2);");;
  208. typing (parse_top "f = (\\x.x x) (\\x.x);");;
  209. typing (parse_top "a = + (\\x.x) 1;");;
  210. typing (parse_top "z = \\f.((\\x.f(\\z.(x x)z)) (\\x.f(\\z.(x x)z)));");;
  211. global_env := `z`::init_env;
  212. global_typing_env:=
  213.     (Forall([1],
  214.      Arrow(Arrow(TypeVar{Index=1;Value=Unknown},
  215.                    TypeVar{Index=1;Value=Unknown}),
  216.             TypeVar{Index=1;Value=Unknown})))
  217.    ::init_typing_env;
  218. ();;
  219. typing (parse_top "f = z(\\f.(\\n. C (= n 0) 1 ( * n (f (- n 1)))));");;
  220. typing (parse_top "x = f 8;");;
  221. typing (parse_top
  222.   "b = z(\\b.(\\n. C (= n 1) 1 (C (= n 2) 1 (+ (b(- n 1)) (b(- n 2))))));");;
  223. typing (parse_top "x = b 9;");;
  224. *)
  225.