compute.ml 7.93 KB
Newer Older
1
2
open Parse
open Typed
3
open Compile
4
open Camlp4.PreCast
5
6
open Types
open Big_int
7

8
(* Gives a unique id for a name *)
9
10
module Locals = Map.Make(String)

11
(* To throw in case of an unbound name *)
12
13
exception Error

14
15
let type_of_string s = match s with
  | "Int" -> interval [Intervals.Any]
16
  | "String" -> Sequence.string
17
18
  | "Char" -> char Chars.any
  | _ -> empty
19

20
let rec _to_typed env l expr =
21
22
  (* From Camlp4 locations to CDuce locations *)
  let loc = caml_loc_to_cduce (get_loc expr) in
23
  match expr with
24
25
26
    | Subst (_, e, s) ->
      let _, _, e = _to_typed env l e in
      env, l, { exp_loc=loc; exp_typ=empty;
27
		exp_descr=(Subst (e, make_sigma s)) }
28
    | Apply (_, e1, e2) ->
29
30
      let _, _, e1 = _to_typed env l e1 in
      let _, _, e2 = _to_typed env l e2 in
31
32
      env, l, { exp_loc=loc; exp_typ=empty; exp_descr=Apply(e1, e2) }
    | Abstr (_, fun_name, params, rtype, body) ->
33
      parse_abstr env l [] loc (Some(0, fun_name)) params rtype body
34
35
    | Match (_, e, t, b) ->
      let b = parse_branches env l t b [] in
36
      let t = type_of_ptype t in
37
      let brs = { br_typ=t; br_accept=t; br_branches=b } in
38
      let _, _, exp_descr = _to_typed env l e in
39
      env, l, { exp_loc=loc; exp_typ=t;
40
		exp_descr=Match(exp_descr, brs) }
41
    | Pair (_, e1, e2) ->
42
43
      let _, _, exp_descr1 = _to_typed env l e1 in
      let _, _, exp_descr2 = _to_typed env l e2 in
44
      env, l, { exp_loc=loc; exp_typ=empty;
45
		exp_descr=Pair(exp_descr1, exp_descr2) }
46
    | Var (origloc, vname) ->
47
48
49
50
51
52
53
54
55
      if vname = "`nil" then
	let nil_atom = Atoms.V.mk_ascii "nil" in
        env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom)); exp_descr=(Cst (Atom nil_atom)) }
      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
	let index = (try Locals.find vname l with Not_found -> Printf.eprintf
	  "File %s, line %d, characters %d-%d:\nUnbound identifier %s\n"
56
          (Loc.file_name origloc) line cbegin cend vname; raise Error) in
57
	env, l, { exp_loc=loc; exp_typ=empty; exp_descr=Var(index, vname) }
58
    | Int (_, i) ->
59
      let i = big_int_of_int i in
60
61
      env, l, { exp_loc=loc; exp_typ=(type_of_string "Int");
		exp_descr=Cst(Integer i) }
62
    | String (_, s) ->
63
      let s = String (0, (String.length s) - 1, s,
64
			    Integer (big_int_of_int 0)) in
65
66
      env, l, { exp_loc=loc; exp_typ=(type_of_string "String");
		exp_descr=Cst s }
67

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

and type_of_sigma x s =
77
78
79
80
  let rec aux x acc = function
    | [] -> acc
    | (id, t2) :: rest when id = x -> aux x (cup acc (type_of_ptype t2)) rest
    | _ :: rest -> aux x acc rest
81
  in
82
  aux x empty s
83

84
and type_of_ptype = function
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
  | 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 =
  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
108

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

133
134
and make_node fv =
  let d = (match fv with
135
136
137
    | el :: rest -> Patterns.Capture(el)
    | [] -> Patterns.Dummy)
  in
138
  make_patterns any fv d
139

140
141
and parse_iface env l params fv nb iface rtype = match params with
  | (_, pname, ptype) :: [] -> true, env, (Locals.add pname nb l),
142
    (fv @ [nb, pname]), (iface @ [type_of_ptype ptype, rtype]), []
143
  | (_, pname, ptype) :: rest -> false, env, (Locals.add pname nb l),
144
145
    (fv @ [nb, pname]),
    (iface @ [type_of_ptype ptype, type_of_iface rest rtype]), rest
146
  | [] -> true, env, l, fv, iface, []
147

148
149
and itype iface res = match iface with
  | (_, _, t) :: rest -> itype rest
150
    (arrow (cons res) (cons (type_of_ptype t)))
151
152
  | [] -> res

153
and parse_branches env l toptype brs res = match brs with
154
  | (loc, p, e) :: rest ->
155
    let brloc = caml_loc_to_cduce loc in
156
157
    let t, d, list, br_locals, br_used =
      parse_match_value env l [] p toptype in
158
159
160
161
    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
162
163
164
165
166
    let fname = Loc.file_name loc in
    let node =
      (if not br_used then
	  (Printf.eprintf
	     "File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
167
168
	     fname line cbegin cend; make_patterns t [] d)
       else make_patterns t list d) in
169
    let b = { br_loc=brloc; br_used=br_used; br_ghost=false; br_vars_empty=[];
170
	      br_pat=node; br_body=br_body} in
171
    parse_branches env l toptype rest (res @ [b])
172
  | [] -> res
173

174
and make_patterns t fv d = incr Patterns.counter;
175
  { Patterns.id=(!Patterns.counter);
176
    Patterns.descr=(t, fv, d);
177
    Patterns.accept=(cons t); fv=fv }
178

179
and parse_match_value env l list p toptype = match p with
Julien Lopez's avatar
Julien Lopez committed
180
  | MPair (_, m1, m2) ->
181
    let top1, top2 =
Julien Lopez's avatar
Julien Lopez committed
182
183
      (match toptype with | TPair(t1, t2) -> t1, t2 | TSeq(t) -> t, TSeq(t)
	| _ -> Type("Empty"), Type("Empty")) in
184
185
    let t1, d1, list1, l, b1 = parse_match_value env l list m1 top1 in
    let t2, d2, list2, l, b2 = parse_match_value env l list m2 top2 in
186
    times (cons t1) (cons t2),
187
188
    Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
    (list1 @ list2), l, b1 && b2;
189
190
  | MVar (_, mname, mtype) ->
    let lsize = Locals.cardinal l in
191
192
    let l = Locals.add mname lsize l in
    let list = list @ [lsize, mname] in
193
    let d1 = any, list, Patterns.Capture(lsize, mname) in
194
    let t2 = type_of_ptype mtype in
195
    let d2 = t2, [], Patterns.Constr(t2) in
196
    t2, Patterns.Cap(d1, d2), list, l, Types.subtype t2 (type_of_ptype toptype)
197
198
  | MInt (_, i) ->
    let t = constant (Integer(big_int_of_int i)) in
199
200
    t, Patterns.Constr(t), list, l, Types.subtype (type_of_string "Int")
      (type_of_ptype toptype)
201
202
203
  | MString (_, s) ->
    let t = constant (String(0, String.length s - 1, s,
			     Integer(big_int_of_int 0))) in
204
205
    t, Patterns.Constr(t), list, l, Types.subtype (type_of_string "String")
      (type_of_ptype toptype)
206

207
let to_typed expr =
208
  let env, l, expr = _to_typed empty_toplevel Locals.empty expr in
209
  env, expr