hphp/hack/src/typing/tast_typecheck.ml

   1 (**
   2  * Copyright (c) 2017, Facebook, Inc.
   3  * All rights reserved.
   4  *
   5  * This source code is licensed under the MIT license found in the
   6  * LICENSE file in the "hack" directory of this source tree.
   7  *
   8  *)
   9
  10 open Hh_core
  11
  12 open Delta
  13 open Tast_expand
  14 open Typing_defs
  15 open ETast
  16
  17 module C = Typing_continuations
  18 module Cont = Typing_lenv_cont
  19 module Env = Typing_env
  20 module Phase = Typing_phase
  21
  22 (** This happens, for example, when there are unsafe blocks, or gotos *)
  23 exception Cant_check
  24 exception Not_implemented
  25
  26 let expect_ty_equal env (pos, ty:Pos.t * locl ty) (expected_ty:locl ty_) =
  27   let expected_ty = (Reason.none, expected_ty) in
  28   if not @@ ty_equal ~normalize_unresolved:true ty expected_ty then
  29     let actual_ty = Typing_print.debug env ty in
  30     let expected_ty = Typing_print.debug env expected_ty in
  31     Errors.unexpected_ty_in_tast pos ~actual_ty ~expected_ty
  32
  33 let refine ((_p, (_r, cond_ty)), cond_expr) _cond_is_true gamma =
  34   let is_refinement_fun fun_name =
  35     match fun_name with
  36     | "\\is_int" | "\\is_float" | "\\is_string" | "\\is_bool"
  37     | "\\is_array" | "\\is_vec" | "\\is_dict" | "\\is_keyset"
  38     | "\\is_resource" -> true
  39     | _ -> false in
  40   match cond_expr with
  41   | Call (Aast.Cnormal, (_, Id (_, id)), [], _, []) when is_refinement_fun id ->
  42     raise Not_implemented
  43   | Call (
  44       _,
  45       (_, Class_const ((_, CI (_, "\\Shapes")), (_, "keyExists"))),
  46       _,
  47       _,
  48       _) ->
  49     raise Not_implemented
  50   | InstanceOf _
  51   | Is _
  52   | As _
  53   | Binop _
  54   | Unop _
  55   | True
  56   | False ->
  57     raise Not_implemented
  58   | _ when cond_ty = Tprim Nast.Tbool -> gamma
  59   | _ ->
  60     raise Not_implemented
  61
  62 let check_assign (_lty, lvalue) ty gamma =
  63   match lvalue with
  64   | Lvar (_, lid) ->
  65     let gamma_updates = add_to_gamma lid ty empty_gamma in
  66     gamma, gamma_updates
  67   | _ -> raise Not_implemented
  68
  69 (* TODO for now check_expr is done with a visitor to deal more gracefully
  70  * with the unimplemented nodes: implemented nodes will be checked even if
  71  * they are not at the top-level. When all nodes are implemented, check_expr
  72  * might be simply redefined using the definition of on_expr. *)
  73 (* This uses the iter visitor as an accumulator using a mutable variable
  74  * gamma as the accumulator, as showcased in the visitor documentation (fig. 2)
  75  * However, this results in a quite ugly programming style.
  76  * TODO write a proper accumulator visitor `accum` inheriting from iter and
  77  * using an `acc` mutable variable, then here inherit from `accum` instead of
  78  * `iter`. *)
  79 let check_expr env (expr:ETast.expr) (gamma:gamma) : gamma =
  80   let expect_ty_equal = expect_ty_equal env in
  81   let expr_checker = object (self)
  82     inherit [_] ETast.iter as super
  83
  84     val mutable gamma = gamma
  85
  86     method gamma () = gamma
  87
  88     method! on_expr env (ty, expr as texpr) =
  89       match expr with
  90       | True | False ->
  91         expect_ty_equal ty (Tprim Nast.Tbool)
  92       | Int _ ->
  93         expect_ty_equal ty (Tprim Nast.Tint)
  94       | Float _ ->
  95         expect_ty_equal ty (Tprim Nast.Tfloat)
  96       | String _ ->
  97         expect_ty_equal ty (Tprim Nast.Tstring)
  98       | Lvar (_, lid) ->
  99         let expected_ty = match lookup lid gamma with
 100         | None -> Tany
 101         | Some (_p, (_r, ty)) -> ty
 102         in
 103         expect_ty_equal ty expected_ty
 104       | _ -> (* TODO *) super#on_expr env texpr
 105
 106     method! on_Binop env bop expr1 (ty2, _ as expr2) =
 107       match bop with
 108       | Ast.Eq None ->
 109         let gamma_, updates = check_assign expr1 ty2 gamma in
 110         gamma <- gamma_;
 111         self#on_expr env expr2;
 112         gamma <- update_gamma gamma updates
 113       | Ast.Eq _ -> raise Not_implemented
 114       | Ast.Ampamp | Ast.Barbar ->
 115         self#on_expr env expr1;
 116         let gamma_ = gamma in
 117         gamma <- refine expr1 (bop = Ast.Ampamp) gamma;
 118         self#on_expr env expr2;
 119         gamma <- gamma_
 120       | _ -> (* TODO *) super#on_Binop env bop expr1 expr2
 121
 122     method! on_Efun _env _fun _id_list = raise Not_implemented
 123
 124     method! on_Class_const env class_id const_name =
 125       match class_id, const_name with
 126       | (_, CI (_, "\\Shapes")), (_, "removeKey") -> raise Not_implemented
 127       | _ -> super#on_Class_const env class_id const_name
 128
 129     method! on_Eif _env _cond _e1 _e2 = raise Not_implemented
 130
 131     method! on_Pipe _env _lid _e1 _e2 = raise Not_implemented
 132
 133     method! on_As _env _e1 _ty = raise Not_implemented
 134
 135     method! on_Callconv _env param_kind _expr =
 136       match param_kind with
 137       | Ast.Pinout -> raise Not_implemented
 138   end in
 139   expr_checker#on_expr env expr;
 140   expr_checker#gamma ()
 141
 142 let rec check_stmt env (stmt:ETast.stmt) (gamma:gamma) : delta =
 143   let check_expr = check_expr env in
 144   match stmt with
 145   | Noop ->
 146     empty_delta_with_next_cont gamma
 147   | Expr expr ->
 148     let gamma = check_expr expr gamma in
 149     empty_delta_with_next_cont gamma
 150   | Fallthrough ->
 151     empty_delta_with_cont C.Fallthrough gamma
 152   | Break _ ->
 153     empty_delta_with_cont C.Break gamma
 154   | Continue _ ->
 155     empty_delta_with_cont C.Continue gamma
 156   | Throw (_is_terminal, expr) ->
 157     let gamma = check_expr expr gamma in
 158     empty_delta_with_cont C.Catch gamma
 159   | Return (_, expropt) ->
 160     let gamma = match expropt with
 161     | None -> gamma
 162     | Some expr ->
 163       let gamma = check_expr expr gamma in
 164       gamma in
 165     empty_delta_with_cont C.Exit gamma
 166   | If (cond, block1, block2) ->
 167     let gamma = check_expr cond gamma in
 168     let gamma1 = refine cond true gamma in
 169     let delta1 = check_block env block1 gamma1 in
 170     let gamma2 = refine cond false gamma in
 171     let delta2 = check_block env block2 gamma2 in
 172     union env delta1 delta2
 173   | Do _
 174   | While _
 175   | For _
 176   | Foreach _
 177   | Switch _
 178   | Try _
 179   | Using _
 180   | Def_inline _
 181   | Let _
 182   | Static_var _
 183   | Global_var _
 184   | Awaitall _ ->
 185     raise Not_implemented
 186   | Goto _
 187   | GotoLabel _
 188   | Unsafe_block _
 189   | Block _
 190   | Markup _
 191   | Declare _ ->
 192     raise Cant_check
 193
 194
 195 and check_block env (block:ETast.block) gamma =
 196   let rec go block gamma delta =
 197     match block with
 198     | [] -> delta
 199     | stmt :: block ->
 200       let delta_s = check_stmt env stmt gamma in
 201       let delta = drop_cont C.Next delta in
 202       (* TODO there shouldn't be any need for 'env' because there shouldn't be
 203        * any type variable to resolve any more. *)
 204       let delta = union env delta delta_s in
 205       match get_next_cont delta_s with
 206       | None -> delta
 207       | Some gamma -> go block gamma delta in
 208   go block gamma (empty_delta_with_next_cont gamma)
 209
 210 let check_func_body env (body:ETast.func_body) gamma =
 211   if body.fb_annotation = Tast.Annotations.FuncBodyAnnotation.HasUnsafeBlocks
 212   then raise Cant_check
 213   else
 214     let _ = check_block env body.fb_ast gamma in
 215     ()
 216
 217 (* TODO It's annoying to have to carry this giant 'env' everywhere. Can we
 218  * localize without it? *)
 219 let localize env hint =
 220   match hint with
 221   | None -> failwith "There should be a hint in strict mode."
 222   | Some decl_ty ->
 223     let ty = Decl_hint.hint env.Env.decl_env decl_ty in
 224     let _env, ty = Phase.localize ~ety_env:(Phase.env_with_self env) env ty in
 225     ty
 226
 227 let gamma_from_params env (params:ETast.fun_param list) =
 228   let add_param_to_gamma gamma param =
 229     if param.param_user_attributes <> [] then raise Not_implemented;
 230     let name = make_local_id param.param_name in
 231     let ty = localize env param.param_hint in
 232     (* TODO can we avoid this? *)
 233     let reas_ty_to_pos_reas_ty (r, _ as ty) = (Typing_reason.to_pos r, ty) in
 234     let ty = reas_ty_to_pos_reas_ty ty in
 235     add_to_gamma name ty gamma in
 236   List.fold ~init:empty_gamma ~f:add_param_to_gamma params
 237
 238 let check_fun env (f:ETast.fun_def) =
 239   if not (FileInfo.is_strict f.f_mode) then () else
 240   let gamma = gamma_from_params env f.f_params in
 241   if f.f_tparams <> []
 242     || f.f_where_constraints <> []
 243     || f.f_variadic <> FVnonVariadic
 244   then raise Not_implemented else
 245   check_func_body env f.f_body gamma
 246   (* TODO check return type *)
 247
 248 let check_def env (def:ETast.def) =
 249   try match def with
 250   | Fun f -> check_fun env f
 251   | _ -> ()
 252   with
 253   | Cant_check ->
 254     Printf.printf "The TAST for this definition is not checkable.\n"
 255   | Not_implemented ->
 256     Printf.printf "The TAST for this definition contains nodes which are not yet implemented.\n"
 257
 258 let check_program env (program:ETast.program) =
 259   List.iter ~f:(check_def env) program
 260
 261 let check env tast =
 262   let errors, () = Errors.do_ (fun () -> check_program env tast) in
 263   errors