compute.ml 8.73 KB
Newer Older
1
2
3
open Parse
open Camlp4.PreCast

4
(* Gives a unique id for a name *)
5
6
module Locals = Map.Make(String)

7
(* To throw in case of an unbound name *)
8
9
exception Error

10
let type_of_string s = match s with
11
  | "Int" -> Types.interval [Intervals.Any]
12
  | "String" -> Sequence.string
13
14
  | "Char" -> Types.char Chars.any
  | _ -> Types.empty
15

16
let rec _to_typed env l expr =
17
  let open Typed in
18
19
  (* From Camlp4 locations to CDuce locations *)
  let loc = caml_loc_to_cduce (get_loc expr) in
20
  match expr with
Pietro Abate's avatar
Pietro Abate committed
21
22
  | Subst (_, e, s) ->
    let _, _, e = _to_typed env l e in
23
24
    env, l, { exp_loc=loc; exp_typ=e.exp_typ;
	      exp_descr=(Subst (e, make_sigma s)) }
Pietro Abate's avatar
Pietro Abate committed
25
26
27
  | Apply (_, e1, e2) ->
    let _, _, e1 = _to_typed env l e1 in
    let _, _, e2 = _to_typed env l e2 in
28
29
30
    env, l, { exp_loc=loc;
	      exp_typ=(Types.Arrow.apply (Types.Arrow.get e1.exp_typ) e2.exp_typ);
	      exp_descr=Apply(e1, e2) }
Pietro Abate's avatar
Pietro Abate committed
31
32
33
  | Abstr (_, fun_name, params, rtype, body) ->
    parse_abstr env l [] loc (Some(0, fun_name)) params rtype body
  | Match (_, e, t, b) ->
34
    let b, btype = parse_branches env l t [] Types.empty b in
Pietro Abate's avatar
Pietro Abate committed
35
36
37
    let t = type_of_ptype t in
    let brs = { br_typ=t; br_accept=t; br_branches=b } in
    let _, _, exp_descr = _to_typed env l e in
38
    env, l, { exp_loc=loc; exp_typ=btype; exp_descr=Match(exp_descr, brs) }
Pietro Abate's avatar
Pietro Abate committed
39
  | Pair (_, e1, e2) ->
40
41
42
43
    let _, _, e1 = _to_typed env l e1 in
    let _, _, e2 = _to_typed env l e2 in
    let t = Types.times (Types.cons e1.exp_typ) (Types.cons e2.exp_typ) in
    env, l, { exp_loc=loc; exp_typ=t; exp_descr=Pair(e1, e2) }
Pietro Abate's avatar
Pietro Abate committed
44
45
46
  | Var (origloc, vname) ->
    if vname = "`nil" then
      let nil_atom = Atoms.V.mk_ascii "nil" in
47
48
      env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom));
		exp_descr=(Cst (Types.Atom nil_atom)) }
Pietro Abate's avatar
Pietro Abate committed
49
50
51
52
    else
      let line = Loc.start_line origloc in
      let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
      let cend = Loc.stop_off origloc - Loc.start_bol origloc in
53
54
55
      let index, vtype = (try Locals.find vname l with Not_found ->
	Printf.eprintf
          "File %s, line %d, characters %d-%d:\nUnbound identifier %s\n"
Pietro Abate's avatar
Pietro Abate committed
56
57
          (Loc.file_name origloc) line cbegin cend vname; raise Error)
      in
58
59
60
      let t = (* Ident.Env.find index env.Compile.gamma *) vtype in
      let v = if Types.no_var t then Var(index, vname) else TVar(index, vname)
      in env, l, { exp_loc=loc; exp_typ=t; exp_descr=v }
Pietro Abate's avatar
Pietro Abate committed
61
62
  | Int (_, i) ->
    let i = Big_int.big_int_of_int i in
63
64
    env, l, { exp_loc=loc; exp_typ=(type_of_string "Int");
	      exp_descr=Cst(Types.Integer i) }
Pietro Abate's avatar
Pietro Abate committed
65
66
67
  | String (_, s) ->
      let i = Big_int.big_int_of_int 0 in
      let s = Types.String (0, (String.length s) - 1, s, Types.Integer i) in
68
69
      env, l, { exp_loc=loc; exp_typ=(type_of_string "String");
		exp_descr=Cst s }
70

71
and make_sigma s =
72
  let rec aux acc = function
73
    | (name, ptype) :: rest ->
74
75
      aux ([`Var (Var.make_id name), type_of_ptype ptype] :: acc) rest
    | [] -> acc
76
  in
77
  aux [] s
78
79

and type_of_sigma x s =
80
81
  let rec aux x acc = function
    | [] -> acc
82
83
    | (id, t2) :: rest when id = x ->
      aux x (Types.cup acc (type_of_ptype t2)) rest
84
    | _ :: rest -> aux x acc rest
85
  in
86
  aux x Types.empty s
87

88
and type_of_ptype =
89
  let open Types in function
90
91
92
93
94
95
96
97
98
99
100
  | Type(t) -> type_of_string t
  | PType(t, s) ->
    if s = [] then var (`Var (Var.make_id t)) else type_of_sigma t s
  | TPair(t1, t2) -> times (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
  | TUnion(t1, t2) -> cup (type_of_ptype t1) (type_of_ptype t2)
  | TInter(t1, t2) -> cap (type_of_ptype t1) (type_of_ptype t2)
  | TNot(t) -> neg (type_of_ptype t)
  | TArrow(t1, t2) -> arrow (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
  | TSeq(t) -> Sequence.star (type_of_ptype t)

and type_of_iface iface rtype =
101
  let open Types in
102
103
104
105
106
107
108
109
110
111
112
113
  let rec _type_of_iface iface rtype res =
  match iface with
  | (_, pname, ptype) :: rest -> _type_of_iface rest rtype
    (arrow (cons res) (cons (type_of_ptype ptype)))
  | [] -> arrow (cons res) (cons rtype)
  in
  match iface with
  | (_, pname, ptype) :: [] -> arrow (cons (type_of_ptype ptype)) (cons rtype)
  | (_, pname, ptype) :: (_, pname2, ptype2) :: rest ->
    let res = type_of_ptype ptype2 in
    arrow (cons (type_of_ptype ptype)) (cons (_type_of_iface rest rtype res))
  | [] -> assert false
114

115
116
and parse_abstr env l fv loc fun_name params rtype body =
  let rec _parse_abstr env l oldfv loc fun_name params rtype body nb =
117
    let brloc = caml_loc_to_cduce (get_loc body) in
118
    let empty, env, l, fv, iface, rest =
119
      parse_iface env l params [] nb [] rtype in
120
    let fun_typ = type_of_iface params rtype in
121
    let node = make_node fv in
122
123
    let l = (match fun_name with
      | None -> l
124
      | Some (id, name) -> Locals.add name (id,fun_typ) l) in
125
126
    let env, l, body = if empty
      then let _, _, body = _to_typed env l body in env, l, body
127
128
      else let env, l, body = _parse_abstr env l (oldfv @ fv) loc None rest
	     rtype body (nb + 1) in env, l, body
129
    in
130
131
    let b = { Typed.br_loc=brloc; br_used=true; br_ghost=false;
	      br_vars_empty=[]; br_pat=node; br_body=body } in
132
133
    let brs = { Typed.br_typ=rtype; br_accept=Types.any; br_branches=[b] } in
    let abstr = { Typed.fun_name=fun_name; fun_iface=iface; fun_body=brs;
134
                  fun_typ=fun_typ; fun_fv=oldfv } in
135
136
    env, l, { Typed.exp_loc=loc; exp_typ=fun_typ;
	      exp_descr=Typed.Abstraction(abstr) }
137
  in
138
  _parse_abstr env l fv loc fun_name params (type_of_ptype rtype) body 0
139

140
141
and make_node fv =
  let d = (match fv with
142
143
144
    | el :: rest -> Patterns.Capture(el)
    | [] -> Patterns.Dummy)
  in
145
  make_patterns Types.any fv d
146

147
and parse_iface env l params fv nb iface rtype = match params with
148
149
150
151
152
153
154
155
  | (_, pname, ptype) :: [] ->
    let ptype = type_of_ptype ptype in
    true, env, (Locals.add pname (nb,ptype) l), (fv @ [nb, pname]),
    (iface @ [ptype, rtype]), []
  | (_, pname, ptype) :: rest ->
    let ptype = type_of_ptype ptype in
    false, env, (Locals.add pname (nb,ptype) l), (fv @ [nb, pname]),
    (iface @ [ptype, type_of_iface rest rtype]), rest
156
  | [] -> true, env, l, fv, iface, []
157

158
159
160
161
and itype acc =
  let open Types in function
  | (_, _, t) :: rest -> itype (arrow (cons acc) (cons (type_of_ptype t))) rest
  | [] -> acc
162

163
and parse_branches env l toptype acc btype = function
164
  | (loc, p, e) :: rest ->
Pietro Abate's avatar
Pietro Abate committed
165
    let t, d, fv, br_locals, br_used = parse_match_value env l [] toptype p in
166
167
168
169
    let line = Loc.start_line loc in
    let cbegin = Loc.start_off loc - Loc.start_bol loc in
    let cend = Loc.stop_off loc - Loc.start_bol loc in
    let _, _, br_body = _to_typed env br_locals e in
170
    let fname = Loc.file_name loc in
Pietro Abate's avatar
Pietro Abate committed
171
    let tpat =
172
173
      if not br_used then begin
        Printf.eprintf
Pietro Abate's avatar
Pietro Abate committed
174
        "File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
175
	  fname line cbegin cend;
Pietro Abate's avatar
Pietro Abate committed
176
        make_patterns t [] d
177
       end else
Pietro Abate's avatar
Pietro Abate committed
178
179
         make_patterns t fv d
    in
180
181
182
183
184
185
    let b = {
      Typed.br_loc = caml_loc_to_cduce loc;
      br_used = br_used;
      br_ghost = false;
      br_vars_empty = [];
      br_pat = tpat;
Pietro Abate's avatar
Pietro Abate committed
186
187
      br_body = br_body}
    in
188
189
190
    parse_branches env l toptype (acc @ [b])
      (Types.cup btype br_body.Typed.exp_typ) rest
  | [] -> acc, btype
191

192
and make_patterns t fv d =
Pietro Abate's avatar
Pietro Abate committed
193
  incr Patterns.counter;
194
  { Patterns.id=(!Patterns.counter);
Pietro Abate's avatar
Pietro Abate committed
195
    descr=(t, fv, d);
196
197
    accept=(Types.cons t);
    fv=fv
Pietro Abate's avatar
Pietro Abate committed
198
  }
199

Pietro Abate's avatar
Pietro Abate committed
200
and parse_match_value env l list toptype = function
Julien Lopez's avatar
Julien Lopez committed
201
  | MPair (_, m1, m2) ->
202
    let top1, top2 =
Julien Lopez's avatar
Julien Lopez committed
203
204
      (match toptype with | TPair(t1, t2) -> t1, t2 | TSeq(t) -> t, TSeq(t)
	| _ -> Type("Empty"), Type("Empty")) in
Pietro Abate's avatar
Pietro Abate committed
205
206
    let t1, d1, list1, l, b1 = parse_match_value env l list top1 m1 in
    let t2, d2, list2, l, b2 = parse_match_value env l list top2 m2 in
207
    Types.times (Types.cons t1) (Types.cons t2),
208
209
    Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
    (list1 @ list2), l, b1 && b2;
210
211
  | MVar (_, mname, mtype) ->
    let lsize = Locals.cardinal l in
212
    let l = Locals.add mname (lsize, type_of_ptype mtype) l in
213
    let list = list @ [lsize, mname] in
214
    let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
215
    let t2 = type_of_ptype mtype in
216
    let d2 = t2, [], Patterns.Constr(t2) in
217
218
    let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
    (t2, Patterns.Cap(d1, d2), list, l, is_subtype)
219
  | MInt (_, i) ->
220
    let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
221
222
    let is_subtype = Types.subtype (type_of_string "Int")
      (type_of_ptype toptype) in
223
    (t, Patterns.Constr(t), list, l, is_subtype)
224
  | MString (_, s) ->
225
226
227
228
    let zero = Types.Integer(Big_int.big_int_of_int 0) in
    let t = Types.constant (Types.String(0, String.length s - 1, s, zero)) in
    let is_subtype = Types.subtype (type_of_string "String")
      (type_of_ptype toptype) in
229
    (t, Patterns.Constr(t), list, l, is_subtype)
230

231
let to_typed expr =
232
  let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
233
  env, expr