← Back to branch summary

~ubuntu-branches/ubuntu/hardy/ocaml-doc/hardy

« back to all changes in this revision

Viewing changes to examples/asl/typing.ml

  • Committer: Bazaar Package Importer
  • Author(s): Samuel Mimram
  • Date: 2007-09-08 01:49:22 UTC
  • mfrom: (0.1.3 upstream)
  • Revision ID: james.westby@ubuntu.com-20070908014922-lvihyehz0ndq7suu
Tags: 3.10-1
* New upstream release.
* Removed camlp4 documentation since it is not up-to-date.
* Updated to standards version 3.7.2, no changes needed.
* Updated my email address.

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/asl/typing.ml
1
 
(* $Id: typing.ml,v 1.1.1.1 2002/05/28 15:59:16 weis Exp $ *)
2
 
 
3
 
open Prel;;
4
 
open Parser;;
5
 
 
6
 
let rec nth n = function
7
 
  | []  -> raise (Failure "nth")
8
 
  | x :: l -> if n = 1 then x else nth (n - 1) l;;
9
 
 
10
 
type asl_type =
11
 
   | Unknown
12
 
   | Number
13
 
   | TypeVar of vartype
14
 
   | Arrow of asl_type * asl_type
15
 
 
16
 
and vartype = {
17
 
  index         : int;
18
 
  mutable value : asl_type
19
 
}
20
 
and asl_type_scheme = Forall of int list * asl_type
21
 
;;
22
 
 
23
 
exception TypingBug of string;;
24
 
 
25
 
let new_vartype, reset_vartypes =
26
 
  (* Generating and resetting unknowns *)
27
 
  let counter = ref 0 in
28
 
  (function () -> counter := !counter+1; {index = !counter; value = Unknown}),
29
 
  (function () -> counter := 0)
30
 
;;
31
 
 
32
 
let rec shorten t =
33
 
    match t with
34
 
    | TypeVar {index = _; value = Unknown} -> t
35
 
    | TypeVar ({index = _;
36
 
                value = TypeVar {index = _;
37
 
                                 value = Unknown} as tv}) -> tv
38
 
    | TypeVar ({index = _; value = TypeVar tv1} as tv2)
39
 
             -> tv2.value <- tv1.value; shorten t
40
 
    | TypeVar {index = _; value = t'} -> t'
41
 
    | Unknown -> raise (TypingBug "shorten")
42
 
    | t' -> t';;
43
 
 
44
 
exception TypeClash of asl_type * asl_type;;
45
 
 
46
 
let occurs {index = n;value = _} =
47
 
  let rec occrec = function
48
 
    | TypeVar {index = m; value = Unknown} -> (n = m)
49
 
    | TypeVar {index = m; value = t} -> (n = m) || (occrec t)
50
 
    | Number -> false
51
 
    | Arrow (t1, t2) -> (occrec t1) || (occrec t2)
52
 
    | Unknown -> raise (TypingBug "occurs") in
53
 
 occrec
54
 
;;
55
 
 
56
 
let rec unify (tau1, tau2) =
57
 
  match (shorten tau1, shorten tau2) with
58
 
  | (* type variable n and type variable m *)
59
 
    (TypeVar ({index = n; value = Unknown} as tv1) as t1),
60
 
    (TypeVar ({index = m; value = Unknown} as tv2) as t2)
61
 
      -> if n = m then () else tv1.value <- t2
62
 
  | (* type t1 and type variable *)
63
 
    t1, (TypeVar ({index = _; value = Unknown} as tv) as t2)
64
 
         -> if not(occurs tv t1) then tv.value <- t1
65
 
            else raise (TypeClash (t1, t2))
66
 
  | (* type variable and type t2 *)
67
 
    (TypeVar ({index = _; value = Unknown} as tv) as t1), t2
68
 
         -> if not(occurs tv t2) then tv.value <- t2
69
 
            else raise (TypeClash (t1, t2))
70
 
  | Number, Number -> ()
71
 
  | Arrow (t1, t2), (Arrow (t'1, t'2) as t)
72
 
         -> unify(t1, t'1); unify(t2, t'2)
73
 
  | (t1, t2) -> raise (TypeClash (t1, t2));;
74
 
 
75
 
let init_typing_env =
76
 
    List.map
77
 
     (function s ->
78
 
       Forall([], Arrow(Number, Arrow(Number, Number))))
79
 
     init_env ;;
80
 
 
81
 
let global_typing_env = ref init_typing_env;;
82
 
 
83
 
let vars_of_type tau =
84
 
 let rec vars vs = function
85
 
   | Number -> vs
86
 
   | TypeVar {index = n; value = Unknown} ->
87
 
       if List.mem n vs then vs else n :: vs
88
 
   | TypeVar {index = _; value =  t} -> vars vs t
89
 
   | Arrow(t1, t2) -> vars (vars vs t1) t2
90
 
   | Unknown -> raise (TypingBug "vars_of_type") in
91
 
 vars [] tau;;
92
 
 
93
 
let unknowns_of_type (bv, t) = subtract (vars_of_type t) bv;;
94
 
 
95
 
let unknowns_of_type_env env =
96
 
    flat (List.map (function Forall(gv, t) -> unknowns_of_type (gv, t)) env)
97
 
;;
98
 
 
99
 
let generalise_type (gamma, tau) =
100
 
  let genvars =
101
 
    make_set (subtract (vars_of_type tau) (unknowns_of_type_env gamma))
102
 
  in Forall(genvars, tau)
103
 
;;
104
 
 
105
 
let gen_instance (Forall(gv, tau)) = 
106
 
  (* We associate a new unknown to each generic variable *)
107
 
  let unknowns =
108
 
      List.map (function n -> n, TypeVar(new_vartype())) gv in
109
 
  let rec ginstance = function
110
 
    | (TypeVar {index = n; value = Unknown} as t) ->
111
 
                  (try List.assoc n unknowns
112
 
                   with Not_found -> t)
113
 
    | TypeVar {index = _; value =  t} -> ginstance t
114
 
    | Number -> Number
115
 
    | Arrow (t1, t2) -> Arrow(ginstance t1, ginstance t2)
116
 
    | Unknown -> raise (TypingBug "gen_instance")
117
 
  in ginstance tau
118
 
;;
119
 
 
120
 
let rec asl_typing_expr gamma =
121
 
  let rec type_rec = function
122
 
  | Const _ -> Number
123
 
  | Var n ->
124
 
      let sigma =
125
 
        try nth n gamma
126
 
        with Failure _ -> raise (TypingBug "Unbound")
127
 
      in gen_instance sigma
128
 
  | Cond (e1, e2, e3) ->
129
 
      let t1 = unify(Number, type_rec e1)
130
 
      and t2 = type_rec e2 and t3 = type_rec e3
131
 
      in unify(t2, t3); t3
132
 
  | App((Abs(x, e2) as f), e1) -> (* LET case *)
133
 
      let t1 = type_rec e1 in
134
 
      let sigma = generalise_type (gamma, t1)
135
 
      in asl_typing_expr (sigma :: gamma) e2
136
 
  | App(e1, e2) ->
137
 
      let u = TypeVar(new_vartype())
138
 
      in unify(type_rec e1, Arrow(type_rec e2, u)); u
139
 
  | Abs(x, e) ->
140
 
      let u = TypeVar(new_vartype()) in
141
 
      let s = Forall([], u)
142
 
      in Arrow(u, asl_typing_expr (s :: gamma) e) in
143
 
 type_rec
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 = String.make 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 =
162
 
   let rec names_of = function
163
 
   | (n, []) -> []
164
 
   | (n, (v1 :: lv)) -> tvar_name n :: names_of (n + 1, lv) in
165
 
   names_of (1, gv) in
166
 
 let tvar_names = List.combine (List.rev gv) names in
167
 
 let rec print_rec = function
168
 
   | TypeVar{index = n; value = Unknown} ->
169
 
        let name =
170
 
            try List.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") in
181
 
  print_rec t
182
 
;;
183
 
 
184
 
let typing (Decl(s, e)) =
185
 
  reset_vartypes();
186
 
  let tau =
187
 
    try asl_typing_expr !global_typing_env e
188
 
    with TypeClash(t1, t2) ->
189
 
      let vars = vars_of_type(t1) @ vars_of_type(t2) in
190
 
      print_string "*** ASL Type clash between ";
191
 
      print_type_scheme (Forall(vars, t1));
192
 
      print_string " and ";
193
 
      print_type_scheme (Forall(vars, t2));
194
 
      reset_vartypes();
195
 
      raise (Failure "ASL typing")
196
 
  in                    
197
 
  generalise_type([], tau)
198
 
;;
199
 
 
200
 
(*
201
 
global_env:=init_env;;
202
 
typing (parse_top "x=1;");;
203
 
typing (parse_top "y = + 2 ((\\x.x) 3);");;
204
 
typing (parse_top "z = C (+ 0 1) 1 0;");;
205
 
typing (parse_top "i = \\x.x;");;
206
 
typing (parse_top "t = + (i 1) (i i 2);");;
207
 
typing (parse_top "f = (\\x.x x) (\\x.x);");;
208
 
typing (parse_top "a = + (\\x.x) 1;");;
209
 
typing (parse_top "z = \\f.((\\x.f(\\z.(x x)z)) (\\x.f(\\z.(x x)z)));");;
210
 
global_env := `z`::init_env;
211
 
global_typing_env:=
212
 
    (Forall([1],
213
 
     Arrow(Arrow(TypeVar{index=1;value=Unknown},
214
 
                   TypeVar{index=1;value=Unknown}),
215
 
            TypeVar{index=1;value=Unknown})))
216
 
   ::init_typing_env;
217
 
();;
218
 
typing (parse_top "f = z(\\f.(\\n. C (= n 0) 1 ( * n (f (- n 1)))));");;
219
 
typing (parse_top "x = f 8;");;
220
 
typing (parse_top
221
 
  "b = z(\\b.(\\n. C (= n 1) 1 (C (= n 2) 1 (+ (b(- n 1)) (b(- n 2))))));");;
222
 
typing (parse_top "x = b 9;");;
223
 
*)