compute.ml 8.51 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
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
  | Subst (_, e, s) ->
    let _, _, e = _to_typed env l e in
    (env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=(Subst (e, make_sigma s)) })
  | Apply (_, 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=Types.empty; exp_descr=Apply(e1, e2) }
  | Abstr (_, fun_name, params, rtype, body) ->
    parse_abstr env l [] loc (Some(0, fun_name)) params rtype body
  | Match (_, e, t, b) ->
    let b = parse_branches env l t [] b in
    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
    (env, l, { exp_loc=loc; exp_typ=t; exp_descr=Match(exp_descr, brs) })
  | Pair (_, e1, e2) ->
    let _, _, exp_descr1 = _to_typed env l e1 in
    let _, _, exp_descr2 = _to_typed env l e2 in
    (env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Pair(exp_descr1, exp_descr2) })
  | Var (origloc, vname) ->
    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 (Types.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
48
49
50
      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
51
52
          (Loc.file_name origloc) line cbegin cend vname; raise Error)
      in
53
54
55
      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
56
57
58
59
60
61
62
  | Int (_, i) ->
    let i = Big_int.big_int_of_int i in
    (env, l, { exp_loc=loc; exp_typ=(type_of_string "Int"); exp_descr=Cst(Types.Integer i) })
  | 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
      (env, l, { exp_loc=loc; exp_typ=(type_of_string "String"); exp_descr=Cst s })
63

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

and type_of_sigma x s =
73
74
  let rec aux x acc = function
    | [] -> acc
75
    | (id, t2) :: rest when id = x -> aux x (Types.cup acc (type_of_ptype t2)) rest
76
    | _ :: rest -> aux x acc rest
77
  in
78
  aux x Types.empty s
79

80
81
and type_of_ptype = 
  let open Types in function
82
83
84
85
86
87
88
89
90
91
92
  | 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 =
93
  let open Types in
94
95
96
97
98
99
100
101
102
103
104
105
  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
106

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

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

138
and parse_iface env l params fv nb iface rtype = match params with
139
140
141
142
143
144
145
146
  | (_, 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
147
  | [] -> true, env, l, fv, iface, []
148

149
150
151
152
and itype acc =
  let open Types in function
  | (_, _, t) :: rest -> itype (arrow (cons acc) (cons (type_of_ptype t))) rest
  | [] -> acc
153

Pietro Abate's avatar
Pietro Abate committed
154
and parse_branches env l toptype acc = function
155
  | (loc, p, e) :: rest ->
Pietro Abate's avatar
Pietro Abate committed
156
    let t, d, fv, br_locals, br_used = parse_match_value env l [] toptype p in
157
158
159
160
    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
161
    let fname = Loc.file_name loc in
Pietro Abate's avatar
Pietro Abate committed
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
    let tpat =
      if not br_used then begin 
        Printf.eprintf 
        "File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
	  fname line cbegin cend; 
        make_patterns t [] d
       end else 
         make_patterns t fv d
    in
    let b = { 
      Typed.br_loc = caml_loc_to_cduce loc; 
      br_used = br_used; 
      br_ghost = false; 
      br_vars_empty = []; 
      br_pat = tpat; 
      br_body = br_body}
    in
    parse_branches env l toptype (acc @ [b]) rest
  | [] -> acc
181

Pietro Abate's avatar
Pietro Abate committed
182
183
and make_patterns t fv d = 
  incr Patterns.counter;
184
  { Patterns.id=(!Patterns.counter);
Pietro Abate's avatar
Pietro Abate committed
185
186
187
188
    descr=(t, fv, d);
    accept=(Types.cons t); 
    fv=fv 
  }
189

Pietro Abate's avatar
Pietro Abate committed
190
and parse_match_value env l list toptype = function
Julien Lopez's avatar
Julien Lopez committed
191
  | MPair (_, m1, m2) ->
192
    let top1, top2 =
Julien Lopez's avatar
Julien Lopez committed
193
194
      (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
195
196
    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
197
    Types.times (Types.cons t1) (Types.cons t2),
198
199
    Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
    (list1 @ list2), l, b1 && b2;
200
201
  | MVar (_, mname, mtype) ->
    let lsize = Locals.cardinal l in
202
    let l = Locals.add mname (lsize, type_of_ptype mtype) l in
203
    let list = list @ [lsize, mname] in
204
    let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
205
    let t2 = type_of_ptype mtype in
206
    let d2 = t2, [], Patterns.Constr(t2) in
207
208
    let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
    (t2, Patterns.Cap(d1, d2), list, l, is_subtype)
209
  | MInt (_, i) ->
210
211
212
    let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
    let is_subtype = Types.subtype (type_of_string "Int") (type_of_ptype toptype) in
    (t, Patterns.Constr(t), list, l, is_subtype)
213
  | MString (_, s) ->
214
215
216
    let t = Types.constant (Types.String(0, String.length s - 1, s, Types.Integer(Big_int.big_int_of_int 0))) in
    let is_subtype = Types.subtype (type_of_string "String") (type_of_ptype toptype) in
    (t, Patterns.Constr(t), list, l, is_subtype)
217

218
let to_typed expr =
219
  let env, l, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
220
  env, expr