compute.ml 9.99 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
  | "Char" -> Types.char Chars.any
14
15
  | "Bool" -> Types.atom (Atoms.cup (Atoms.atom (Atoms.V.mk_ascii "false"))
			    (Atoms.atom (Atoms.V.mk_ascii "true")))
16
  | "Any" -> Types.any
17
  | _ -> Types.empty
18

19
let rec _to_typed env l expr =
20
  let open Typed in
21
22
  (* From Camlp4 locations to CDuce locations *)
  let loc = caml_loc_to_cduce (get_loc expr) in
23
  match expr with
Pietro Abate's avatar
Pietro Abate committed
24
25
  | Subst (_, e, s) ->
    let _, _, e = _to_typed env l e in
26
27
    env, l, { exp_loc=loc; exp_typ=e.exp_typ;
	      exp_descr=(Subst (e, make_sigma s)) }
Pietro Abate's avatar
Pietro Abate committed
28
29
30
  | Apply (_, e1, e2) ->
    let _, _, e1 = _to_typed env l e1 in
    let _, _, e2 = _to_typed env l e2 in
31
32
33
    env, l, { exp_loc=loc;
	      exp_typ=(Types.Arrow.apply (Types.Arrow.get e1.exp_typ) e2.exp_typ);
	      exp_descr=Apply(e1, e2) }
34
  | Abstr (origloc, fun_name, iface, fv, body) ->
35
    let fname = match fun_name with | "_" -> None | _ -> Some(0, fun_name) in
36
    parse_abstr env l origloc fname iface fv body
Pietro Abate's avatar
Pietro Abate committed
37
  | Match (_, e, t, b) ->
38
    let b, btype = parse_branches env l t [] Types.empty b in
Pietro Abate's avatar
Pietro Abate committed
39
40
41
    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
42
    env, l, { exp_loc=loc; exp_typ=btype; exp_descr=Match(exp_descr, brs) }
Pietro Abate's avatar
Pietro Abate committed
43
  | Pair (_, e1, e2) ->
44
45
46
47
    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) }
48
49
50
51
52
  | Op (_, op, e1, e2) ->
    let _, _, e1 = _to_typed env l e1 in
    let _, _, e2 = _to_typed env l e2 in
    env, l, { exp_loc=loc; exp_typ=type_of_string "Int";
	      exp_descr=Op(op, 0, [e1; e2]) }
Pietro Abate's avatar
Pietro Abate committed
53
  | Var (origloc, vname) ->
54
55
56
    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
Pietro Abate's avatar
Pietro Abate committed
57
58
    if vname = "`nil" then
      let nil_atom = Atoms.V.mk_ascii "nil" in
59
60
      env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom));
		exp_descr=(Cst (Types.Atom nil_atom)) }
61
62
63
64
    else if vname = "_" then
      (Printf.eprintf
	 "File %s, line %d, characters %d-%d:\nError: Invalid reference to special variable %s\n"
	 (Loc.file_name origloc) line cbegin cend vname; raise Error)
Pietro Abate's avatar
Pietro Abate committed
65
    else
Pietro Abate's avatar
Pietro Abate committed
66
      let index, vtype =
67
        try Locals.find vname l
Pietro Abate's avatar
Pietro Abate committed
68
        with Not_found -> Printf.eprintf
69
          "File %s, line %d, characters %d-%d:\nError: Unbound identifier %s\n"
70
          (Loc.file_name origloc) line cbegin cend vname;
Pietro Abate's avatar
Pietro Abate committed
71
          raise Error
Pietro Abate's avatar
Pietro Abate committed
72
      in
Pietro Abate's avatar
Pietro Abate committed
73
      let v = if Types.no_var vtype then Var(index, vname) else TVar(index, vname)
Pietro Abate's avatar
Pietro Abate committed
74
      in env, l, { exp_loc=loc; exp_typ=vtype; exp_descr=v }
Pietro Abate's avatar
Pietro Abate committed
75
76
  | Int (_, i) ->
    let i = Big_int.big_int_of_int i in
77
78
    env, l, { exp_loc=loc; exp_typ=(type_of_string "Int");
	      exp_descr=Cst(Types.Integer i) }
Pietro Abate's avatar
Pietro Abate committed
79
80
81
  | 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
82
83
      env, l, { exp_loc=loc; exp_typ=(type_of_string "String");
		exp_descr=Cst s }
84
85
86
87
88
  | Bool (origloc, b) ->
    let t = Types.atom (Atoms.atom (Atoms.V.mk_ascii "true")) in
    let f = Types.atom (Atoms.atom (Atoms.V.mk_ascii "false")) in
    match b with
      | "true" -> env, l, { exp_loc=loc; exp_typ=t;
89
			    exp_descr=Cst (Types.Atom (Atoms.V.mk_ascii "true")) }
90
      | "false" -> env, l, { exp_loc=loc; exp_typ=f;
91
			     exp_descr=Cst (Types.Atom (Atoms.V.mk_ascii "false")) }
92
93
94
95
96
      | _ ->
	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
	Printf.eprintf
97
          "File %s, line %d, characters %d-%d:\nError: Unknown special term %s\n"
98
99
          (Loc.file_name origloc) line cbegin cend b;
        raise Error
100

101
and make_sigma s =
102
  let rec aux acc = function
103
    | (name, ptype) :: rest ->
104
105
      aux ([`Var (Var.make_id name), type_of_ptype ptype] :: acc) rest
    | [] -> acc
106
  in
107
  aux [] s
108
109

and type_of_sigma x s =
110
111
  let rec aux x acc = function
    | [] -> acc
112
113
    | (id, t2) :: rest when id = x ->
      aux x (Types.cup acc (type_of_ptype t2)) rest
114
    | _ :: rest -> aux x acc rest
115
  in
116
  aux x Types.empty s
117

118
and type_of_ptype =
119
  let open Types in function
120
121
122
123
124
125
126
127
128
129
  | 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)

130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
and first_param loc iface =
  let rec _first_param loc accu = function
    | TArrow(t1, t2) -> t1, accu @ [type_of_ptype t1, type_of_ptype t2]
    | TUnion(t1, t2) ->
      let t1, acc1 = first_param loc t1 in
      let t2, acc2 = first_param loc t2 in
      TInter(t1, t2), acc1 @ acc2
    | TInter(t1, t2) ->
      let t1, acc1 = first_param loc t1 in
      let t2, acc2 = first_param loc t2 in
      TUnion(t1, t2), acc1 @ acc2
    | _ ->
      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 fname = Loc.file_name loc in
      Printf.eprintf
	"File %s, line %d, characters %d-%d:\nError: This type should be an arrow type\n"
	fname line cbegin cend; raise Error
149
  in
150
  _first_param loc [] iface
151

152
and parse_abstr env l loc fun_name iface fv body =
153
154
155
156
157
158
  let fun_typ = type_of_ptype iface in
  let ptype, iface = first_param loc iface in
  let l = (match fun_name with
    | None -> l
    | Some (id, name) -> Locals.add name (id,fun_typ) l) in
  let b, btype = parse_branches env l ptype [] Types.empty body in
159
160
  let brs = { Typed.br_typ=type_of_ptype ptype; br_accept=Types.any;
	      br_branches=b } in
161
  let abstr = { Typed.fun_name=fun_name; fun_iface=iface; fun_body=brs;
162
                fun_typ=fun_typ; fun_fv=fv } in
163
164
  env, l, { Typed.exp_loc=caml_loc_to_cduce loc; exp_typ=fun_typ;
	    exp_descr=Typed.Abstraction(abstr) }
165

166
167
168
169
170
171
172
and make_patterns t fv d =
  incr Patterns.counter;
  { Patterns.id=(!Patterns.counter);
    descr=(t, fv, d);
    accept=(Types.cons t);
    fv=fv
  }
173

174
and parse_branches env l toptype acc btype = function
175
  | (loc, p, e) :: rest ->
Pietro Abate's avatar
Pietro Abate committed
176
    let t, d, fv, br_locals, br_used = parse_match_value env l [] toptype p in
177
178
179
180
    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
181
    let fname = Loc.file_name loc in
Pietro Abate's avatar
Pietro Abate committed
182
    let tpat =
183
184
      if not br_used then begin
        Printf.eprintf
Pietro Abate's avatar
Pietro Abate committed
185
        "File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
186
	  fname line cbegin cend;
Pietro Abate's avatar
Pietro Abate committed
187
        make_patterns t [] d
188
       end else
Pietro Abate's avatar
Pietro Abate committed
189
190
         make_patterns t fv d
    in
191
192
193
194
195
196
    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
197
198
      br_body = br_body}
    in
199
200
201
    parse_branches env l toptype (acc @ [b])
      (Types.cup btype br_body.Typed.exp_typ) rest
  | [] -> acc, btype
202

203
204
205
206
207
208
209
210
211
and get_fv brs =
  let rec _fv_of_patt = function
    | MPair (_, m1, m2) -> (_fv_of_patt m1) @ (_fv_of_patt m2)
    | MVar (_, mname, _) -> [0, mname]
    | _ -> [] in
  let rec _get_fv accu = function
    | (_, p, _) :: rest -> _get_fv (accu @ (_fv_of_patt p)) rest
    | [] -> accu in
  _get_fv [] brs
212

Pietro Abate's avatar
Pietro Abate committed
213
and parse_match_value env l list toptype = function
Julien Lopez's avatar
Julien Lopez committed
214
  | MPair (_, m1, m2) ->
215
    let top1, top2 =
Julien Lopez's avatar
Julien Lopez committed
216
217
      (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
218
219
    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
220
    Types.times (Types.cons t1) (Types.cons t2),
221
222
    Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
    (list1 @ list2), l, b1 && b2;
223
  | MVar (_, mname, mtype) ->
224
225
226
227
    if mname = "`nil" then
      let nil_atom = Atoms.V.mk_ascii "nil" in
      let t = Types.atom (Atoms.atom nil_atom) in
      (t, Patterns.Constr(t), list, l, true)
228
    else if mname = "_" then
229
230
      let t = type_of_ptype mtype in
      (t, Patterns.Constr(t), list, l, true)
231
232
233
234
235
236
237
238
239
    else
      let lsize = Locals.cardinal l in
      let l = Locals.add mname (lsize, type_of_ptype mtype) l in
      let list = list @ [lsize, mname] in
      let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
      let t2 = type_of_ptype mtype in
      let d2 = t2, [], Patterns.Constr(t2) in
      let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
      (t2, Patterns.Cap(d1, d2), list, l, is_subtype)
240
  | MInt (_, i) ->
241
    let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
242
243
    let is_subtype = Types.subtype (type_of_string "Int")
      (type_of_ptype toptype) in
244
    (t, Patterns.Constr(t), list, l, is_subtype)
245
  | MString (_, s) ->
246
247
248
249
    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
250
    (t, Patterns.Constr(t), list, l, is_subtype)
251

252
let rec arith_op f = function
253
  | Value.Integer(x) :: Value.Integer(y) :: [] ->
254
255
    Value.Integer(Big_int.big_int_of_int (f (Big_int.int_of_big_int x)
					    (Big_int.int_of_big_int y)))
256
257
  | _ -> raise Error

258
let to_typed expr =
259
260
261
262
263
  Eval.register_op "+" (arith_op ( + ));
  Eval.register_op "-" (arith_op ( - ));
  Eval.register_op "*" (arith_op ( * ));
  Eval.register_op "/" (arith_op ( / ));
  Eval.register_op "%" (arith_op ( mod ));
264
  let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
265
  env, expr