typed.ml 6.73 KB
Newer Older
1
(* Typed abstract syntax *)
2

3 4
(*  Some sub-expression may have to be type-checked several times.
    We first build the ``skeleton'' of the typed ast
5
    (basically the parsed ast with types and patterns replaced with their
6 7 8 9 10 11
    internal representation), then type check it.

    The exp_typ and br_typ fields are updated to capture all the possible
    values than can result from the expression or flow to the branch
*)

12
open Cduce_loc
13
open Ident
14 15

type tpat = Patterns.node
16
type ttyp = Types.Node.t
17

18
type sigma = Types.Subst.t list
19

20 21 22
type texpr  =
    { exp_loc : loc;
      mutable exp_typ : Types.t;
23
      (* Currently exp_typ is not used. It will be used for compilation ! *)
24
      mutable exp_descr : texpr';
25
    }
26

27
and  texpr' =
28
  | Forget of texpr * ttyp
29
  | Check of (Types.t ref) * texpr * ttyp
30
  (* CDuce is a Lambda-calculus ... *)
31
  | Var of id
32 33
  (* polymorphic variable *)
  | TVar of id
34 35
  (* lazy substutiutions *)
  | Subst of (texpr * sigma)
36
  | ExtVar of Compunit.t * id * Types.t
37 38
  | Apply of texpr * texpr
  | Abstraction of abstr
39

40 41 42
  (* Data constructors *)
  | Cst of Types.const
  | Pair of texpr * texpr
43
  | Xml of texpr * texpr * Ns.table option
44
  | RecordLitt of texpr label_map
45
  | String of U.uindex * U.uindex * U.t * texpr
46

47 48
  (* Data destructors *)
  | Match of texpr * branches
49 50
  | Map of texpr * branches
  | Transform of texpr * branches
51
  | Xtrans of texpr * branches
52
  | Validate of texpr * Types.t * Schema_validator.t
53
  | RemoveField of texpr * label
54
  | Dot of texpr * label
55

56 57
  (* Exception *)
  | Try of texpr * branches
58

59
  | Ref of texpr * ttyp
60
  | External of Types.t * [ `Builtin of string | `Ext of int ]
61
  | Op of string * int * texpr list
62
  | NsTable of Ns.table * texpr'
63

64 65
and abstr = {
  fun_name : id option;
66
  fun_iface : (Types.t * Types.t) list;
67
  fun_body : branches;
68
  fun_typ  : Types.t;
69
  fun_fv   : fv
70 71
}

72 73 74 75 76
and let_decl = {
  let_pat : tpat;
  let_body : texpr;
}

77
and branches = {
78
  mutable br_typ : Types.t; (* Type of values that can flow to branches *)
79
  br_accept : Types.t;      (* Type accepted by all branches *)
80
  br_branches: branch list;
81
}
82
and branch = {
83
  br_loc : loc;
84
  mutable br_used : bool;
85
  br_ghost : bool;
86
  mutable br_vars_empty : fv;
87
  mutable br_vars_poly : Var.Set.t IdMap.map;
88
  br_pat : tpat;
89
  (* this field is mutable because we need to add substitutions *)
90
  mutable br_body : texpr
91
}
92

93

94 95
let pat_list_of_expr e =
  let max_occ = ref ~-1 in
96
  let open Typepat in
97
  let module HashId = Hashtbl.Make(Id) in
98
  let any_pat = mk_type Types.any in
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
  let mk_pat i e =
    let map = HashId.create 17 in
    let rec loop e =
      match e.exp_descr with
	Var id ->
	  let occ =
	    try
	      HashId.find map id
	    with Not_found -> 1
	  in
	  if occ > !max_occ then max_occ := occ;
	  HashId.replace map id (occ + 1);
	  if i = occ then
	    mk_capture id
	  else
	    any_pat
      | Pair (e1, e2) -> mk_prod (loop e1) (loop e2)
      | Xml (e1, e2, None) -> mk_xml (loop e1) (loop e2) (* TODO : check the inpact of Ns.table *)
      | RecordLitt emap -> mk_record false (LabelMap.map (fun e -> loop e, None) emap)
      | _ -> any_pat
    in
    pat_node (loop e)
121
  in
122 123 124 125 126 127 128 129 130
  let rec loop i acc =
    let acc = (mk_pat i e) :: acc in
    if !max_occ == 0 then [] else
      if i < !max_occ then loop (i+1) acc
      else acc
  in
  List.rev (loop 1 [])


131

132 133 134 135 136 137 138 139
module Print = struct

  let rec pp_const ppf cst =
    match cst with
      | Types.Integer(i) -> Format.fprintf ppf "Integer(%s)" (Intervals.V.to_string i)
      | Types.Atom(a) -> Format.fprintf ppf "Atom(%s)" (Atoms.V.to_string a)
      | Types.Char(c) -> Format.fprintf ppf "Char(%d)" (Chars.V.to_int c)
      | Types.Pair(c1, c2) -> Format.fprintf ppf "(%a,%a)" pp_const c1 pp_const c2
Pietro Abate's avatar
Pietro Abate committed
140
      | Types.String(_, _, s, _) -> Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
141 142
      | _ -> assert false

143
  let rec pp ppf e =
144
    Format.fprintf ppf "{typ: %a; descr= %a}"
145
      Types.Print.pp_type e.exp_typ
146
      pp_aux e
147

148
  and pp_aux ppf e =
149
    match e.exp_descr with
150
      | Subst(e,sl) -> Format.fprintf ppf "%a @@ %a" pp e Type_tallying.pp_sl sl
151 152
      | Forget(e, _) -> Format.fprintf ppf "Forget(%a)" pp e
      | Check(_, e, _) -> Format.fprintf ppf "Check(%a)" pp e
153
      | TVar(id, name) ->
Pietro Abate's avatar
Pietro Abate committed
154 155 156
          Format.fprintf ppf "TVar(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
157
      | Var(id, name) ->
Pietro Abate's avatar
Pietro Abate committed
158 159 160
          Format.fprintf ppf "Var(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
161
      | ExtVar(_, (id, name), _) ->
Pietro Abate's avatar
Pietro Abate committed
162 163 164
          Format.fprintf ppf "ExtVar(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
165
      | Apply(e1, e2) ->
166
          Format.fprintf ppf "(%a).(%a)" pp e1 pp e2
167
      | Abstraction(abstr) ->
Pietro Abate's avatar
Pietro Abate committed
168
          Format.fprintf ppf "Abstraction(%a)" pp_abst abstr
169 170
      | Cst(cst) -> pp_const ppf cst
      | Pair(e1, e2) ->
171
          Format.fprintf ppf "(%a, %a)" pp e1 pp e2
172
      | String(_, _, s, _) ->
Pietro Abate's avatar
Pietro Abate committed
173
          Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
174
      | Match(e, b) ->
175
          Format.fprintf ppf "Match(%a,%a)" pp e pp_branches b
Pietro Abate's avatar
Pietro Abate committed
176
      | Op(s, i, l) ->
177
          Format.fprintf ppf "(%s, %d, %a)" s i (Utils.pp_list pp) l
178 179 180
      | _ -> assert false

  and pp_abst ppf abstr =
181
    Format.fprintf ppf "%a, iface:[%a], body:[%a], typ:%a, fv:[%a]"
182 183 184
      pp_fun_name abstr.fun_name
      pp_iface abstr.fun_iface
      pp_branches abstr.fun_body
185
      Types.Print.pp_type abstr.fun_typ
186 187 188 189
      pp_fv abstr.fun_fv

  and pp_fun_name ppf = function
    |Some (id, name) ->
Pietro Abate's avatar
Pietro Abate committed
190 191 192
        Format.fprintf ppf "name:(%s,%s)"
        (string_of_int (Upool.int id))
        (Encodings.Utf8.to_string name)
193 194 195 196 197
    |None -> Format.fprintf ppf "name:<none>"

  and pp_iface ppf l =
    let f ppf (t1,t2) =
      Format.fprintf ppf "(%a,%a)"
198 199
        Types.Print.pp_type t1
        Types.Print.pp_type t2
200
    in
Pietro Abate's avatar
Pietro Abate committed
201
    Utils.pp_list f ppf l
202 203 204

  and pp_branches ppf brs =
    Format.fprintf ppf "typ:%a, accept:%a, branches:%a"
205 206
      Types.Print.pp_type brs.br_typ
      Types.Print.pp_type brs.br_accept
207 208 209 210 211
      pp_branch brs.br_branches

  and pp_branch ppf brs =
    let f ppf br =
      Format.fprintf ppf
212
      "{used:%b; ghost:%b; br_vars_poly:{%a}; br_vars_empty:[%a]; pat:{%a}; body:{typ:%a, descr:%a}}"
213 214
	br.br_used
	br.br_ghost
215
	pp_vars_poly br.br_vars_poly
216
	pp_fv br.br_vars_empty
Julien Lopez's avatar
Julien Lopez committed
217
	Patterns.pp_node br.br_pat
218
	Types.Print.pp_type br.br_body.exp_typ
219
	pp br.br_body
220
    in
Pietro Abate's avatar
Pietro Abate committed
221
    Utils.pp_list f ppf brs
222 223 224 225

  and pp_v ppf (id, name) =
    Format.fprintf ppf "(%d,%s)" (Upool.int id) (Encodings.Utf8.to_string name)

226
  and pp_fv ppf fv = Utils.pp_list pp_v ppf (IdSet.get fv)
227

228
  and pp_vars_poly ppf m =
229
    let pp_aux ppf (x,s) = Format.fprintf ppf "%a : %a" Ident.print x  Var.Set.print s in
Pietro Abate's avatar
Pietro Abate committed
230 231
    Utils.pp_list ~sep:";" pp_aux ppf (Ident.IdMap.get m)

232
  let string_of_typed = Utils.string_of_formatter pp
233
end