compute.ml 8.85 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) }
Pietro Abate's avatar
Pietro Abate committed
48
49
50
  | Var (origloc, vname) ->
    if vname = "`nil" then
      let nil_atom = Atoms.V.mk_ascii "nil" in
51
52
      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
53
54
55
56
    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
Pietro Abate's avatar
Pietro Abate committed
57
      let index, vtype =
58
        try Locals.find vname l
Pietro Abate's avatar
Pietro Abate committed
59
        with Not_found -> Printf.eprintf
60
          "File %s, line %d, characters %d-%d:\nError: Unbound identifier %s\n"
61
          (Loc.file_name origloc) line cbegin cend vname;
Pietro Abate's avatar
Pietro Abate committed
62
          raise Error
Pietro Abate's avatar
Pietro Abate committed
63
      in
Pietro Abate's avatar
Pietro Abate committed
64
      let v = if Types.no_var vtype then Var(index, vname) else TVar(index, vname)
Pietro Abate's avatar
Pietro Abate committed
65
      in env, l, { exp_loc=loc; exp_typ=vtype; exp_descr=v }
Pietro Abate's avatar
Pietro Abate committed
66
67
  | Int (_, i) ->
    let i = Big_int.big_int_of_int i in
68
69
    env, l, { exp_loc=loc; exp_typ=(type_of_string "Int");
	      exp_descr=Cst(Types.Integer i) }
Pietro Abate's avatar
Pietro Abate committed
70
71
72
  | 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
73
74
      env, l, { exp_loc=loc; exp_typ=(type_of_string "String");
		exp_descr=Cst s }
75
76
77
78
79
80
81
82
83
84
85
86
87
  | 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;
			    exp_descr=Cst (Types.Atom 1) }
      | "false" -> env, l, { exp_loc=loc; exp_typ=f;
			     exp_descr=Cst (Types.Atom 0) }
      | _ ->
	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
88
          "File %s, line %d, characters %d-%d:\nError: Unknown special term %s\n"
89
90
          (Loc.file_name origloc) line cbegin cend b;
        raise Error
91

92
and make_sigma s =
93
  let rec aux acc = function
94
    | (name, ptype) :: rest ->
95
96
      aux ([`Var (Var.make_id name), type_of_ptype ptype] :: acc) rest
    | [] -> acc
97
  in
98
  aux [] s
99
100

and type_of_sigma x s =
101
102
  let rec aux x acc = function
    | [] -> acc
103
104
    | (id, t2) :: rest when id = x ->
      aux x (Types.cup acc (type_of_ptype t2)) rest
105
    | _ :: rest -> aux x acc rest
106
  in
107
  aux x Types.empty s
108

109
and type_of_ptype =
110
  let open Types in function
111
112
113
114
115
116
117
118
119
120
  | 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)

121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
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
140
  in
141
  _first_param loc [] iface
142

143
and parse_abstr env l loc fun_name iface fv body =
144
145
146
147
148
149
  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
150
151
  let brs = { Typed.br_typ=type_of_ptype ptype; br_accept=Types.any;
	      br_branches=b } in
152
  let abstr = { Typed.fun_name=fun_name; fun_iface=iface; fun_body=brs;
153
                fun_typ=fun_typ; fun_fv=fv } in
154
155
  env, l, { Typed.exp_loc=caml_loc_to_cduce loc; exp_typ=fun_typ;
	    exp_descr=Typed.Abstraction(abstr) }
156

157
158
159
160
161
162
163
and make_patterns t fv d =
  incr Patterns.counter;
  { Patterns.id=(!Patterns.counter);
    descr=(t, fv, d);
    accept=(Types.cons t);
    fv=fv
  }
164

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

194
195
196
197
198
199
200
201
202
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
203

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

235
let to_typed expr =
236
  let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
237
  env, expr