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

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 = Type_tallying.Constr.sl
19

20 21
type texpr  = 
    { exp_loc : loc; 
22 23
      mutable exp_typ : Types.t;  
      (* 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 39 40 41 42
  | Apply of texpr * texpr
  | Abstraction of abstr
      
  (* 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
and abstr = { 
65
  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 90
  (* this field is mutable because we need to add substitutions *)
  mutable br_body : texpr 
91
}
92

93 94 95 96 97 98 99 100
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
101
      | Types.String(_, _, s, _) -> Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
102 103
      | _ -> assert false

104
  let rec pp ppf e =
105
    Format.fprintf ppf "{typ: %a; descr= %a}"
106
      Types.Print.pp_type e.exp_typ
107
      pp_aux e
108

109
  and pp_aux ppf e =
110
    match e.exp_descr with
111
      | Subst(e,sl) -> Format.fprintf ppf "%a @@ %a" pp e Type_tallying.Constr.pp_sl sl
112 113
      | Forget(e, _) -> Format.fprintf ppf "Forget(%a)" pp e
      | Check(_, e, _) -> Format.fprintf ppf "Check(%a)" pp e
114
      | TVar(id, name) ->
115 116 117
          Format.fprintf ppf "TVar(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
118
      | Var(id, name) ->
119 120 121
          Format.fprintf ppf "Var(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
122
      | ExtVar(_, (id, name), _) ->
123 124 125
          Format.fprintf ppf "ExtVar(%s,%s)"
            (string_of_int (Upool.int id))
            (Encodings.Utf8.to_string name)
126
      | Apply(e1, e2) ->
127
          Format.fprintf ppf "(%a).(%a)" pp e1 pp e2
128
      | Abstraction(abstr) ->
129
          Format.fprintf ppf "Abstraction(%a)" pp_abst abstr
130 131
      | Cst(cst) -> pp_const ppf cst
      | Pair(e1, e2) ->
132
          Format.fprintf ppf "(%a, %a)" pp e1 pp e2
133
      | String(_, _, s, _) ->
134
          Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
135
      | Match(e, b) ->
136
          Format.fprintf ppf "Match(%a,%a)" pp e pp_branches b
137
      | Op(s, i, l) ->
138
          Format.fprintf ppf "(%s, %d, %a)" s i (Utils.pp_list pp) l
139 140 141
      | _ -> assert false

  and pp_abst ppf abstr =
142
    Format.fprintf ppf "%a, iface:[%a], body:[%a], typ:%a, fv:[%a]"
143 144 145
      pp_fun_name abstr.fun_name
      pp_iface abstr.fun_iface
      pp_branches abstr.fun_body
146
      Types.Print.pp_type abstr.fun_typ
147 148 149 150
      pp_fv abstr.fun_fv

  and pp_fun_name ppf = function
    |Some (id, name) ->
151 152 153
        Format.fprintf ppf "name:(%s,%s)"
        (string_of_int (Upool.int id))
        (Encodings.Utf8.to_string name)
154 155 156 157 158
    |None -> Format.fprintf ppf "name:<none>"

  and pp_iface ppf l =
    let f ppf (t1,t2) =
      Format.fprintf ppf "(%a,%a)"
159 160
        Types.Print.pp_type t1
        Types.Print.pp_type t2
161
    in
162
    Utils.pp_list f ppf l
163 164 165

  and pp_branches ppf brs =
    Format.fprintf ppf "typ:%a, accept:%a, branches:%a"
166 167
      Types.Print.pp_type brs.br_typ
      Types.Print.pp_type brs.br_accept
168 169 170 171 172
      pp_branch brs.br_branches

  and pp_branch ppf brs =
    let f ppf br =
      Format.fprintf ppf
173
      "{used:%b; ghost:%b; br_vars_poly:{%a}; br_vars_empty:[%a]; pat:{%a}; body:{typ:%a, descr:%a}}"
174 175
	br.br_used
	br.br_ghost
176
	pp_vars_poly br.br_vars_poly
177
	pp_fv br.br_vars_empty
Julien Lopez's avatar
Julien Lopez committed
178
	Patterns.pp_node br.br_pat
179
	Types.Print.pp_type br.br_body.exp_typ
180
	pp br.br_body
181
    in
182
    Utils.pp_list f ppf brs
183 184 185 186

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

187
  and pp_fv ppf fv = Utils.pp_list pp_v ppf (IdSet.get fv)
188

189
  and pp_vars_poly ppf m =
190
    let pp_aux ppf (x,s) = Format.fprintf ppf "%a : %a" Ident.print x  Var.Set.print s in
191 192
    Utils.pp_list ~sep:";" pp_aux ppf (Ident.IdMap.get m)

193
  let string_of_typed = Utils.string_of_formatter pp
194
end