<commit_before>(* Copyright (c) 2013-2017 The Cervoise developers. *)
(* See the LICENSE file at the top-level directory. *)

open UntypedTree

let type_fail ~loc ~has ~expected =
  Err.fail_doc ~loc
    Utils.PPrint.(str "This value has type" ^^^
                  squotes (NType.dump has) ^^^
                  str "but was expected of type" ^^^
                  squotes (NType.dump expected) ^^^
                  dot)

let eff_fail ~loc ~has ~expected =
  Err.fail_doc ~loc
    Utils.PPrint.(str "This effect has type" ^^^
                  squotes (NType.dump_eff has) ^^^
                  str "but was expected of type" ^^^
                  squotes (NType.dump_eff expected) ^^^
                  dot)

let check_type ~loc env ty' ty =
  let ty = NType.check ~pure_arrow:`Allow env ty in
  if not (NType.is_subset_of ty' ty) then
    type_fail ~loc ~has:ty' ~expected:ty;
  ty

let check_eff ~loc env eff' eff =
  let eff = NType.check_eff ~pure_arrow:`Allow env eff in
  if not (NType.eff_is_subset_of eff' eff) then
    eff_fail ~loc ~has:eff' ~expected:eff;
  eff

let check_eff_opt ~loc env eff' =
  Option.map_or ~default:[] (check_eff ~loc env eff')

let unit options = TypedEnv.NTy (Builtins.unit options)
let is_main ~current_module = Ident.Name.equal (Builtins.main ~current_module)
let io options = TypedEnv.NTy (Builtins.io options)
let has_io options = List.exists (NType.is_subset_of (io options))

let get_const options = function
  | PretypedTree.Int n -> (`Int n, Builtins.int options)
  | PretypedTree.Float n -> (`Float n, Builtins.float options)
  | PretypedTree.Char c -> (`Char c, Builtins.char options)
  | PretypedTree.String s -> (`String s, Builtins.string options)

let get_rep name = function
  | TypedEnv.Index idx -> Index idx
  | TypedEnv.Exn -> Exn (Ident.Constr.to_name name)

let eff_of_ty ~loc options = function
  | TypedEnv.NSum [] ->
      assert false (* TODO: Check this. This shouldn't happen *)
  | TypedEnv.NSum sum ->
      let exn = TypedEnv.NTy (Builtins.exn options) in
      List.map (fun t -> TypedEnv.NApp (exn, NType.to_type t)) sum
  | TypedEnv.NTy _ | TypedEnv.NFun _
  | TypedEnv.NForall _ | TypedEnv.NApp _ as t ->
      Err.fail_doc
        ~loc
        Utils.PPrint.(str "Cannot throw exception of type" ^^^
                      squotes (NType.dump t) ^^^
                      dot)

let rec get_supertype ty eff = function
  | [] ->
      (ty, eff)
  | (loc, ty', eff')::tys ->
      if NType.is_subset_of ty ty' then
        get_supertype ty' (eff @ eff') tys
      else if NType.is_subset_of ty' ty then
        get_supertype ty (eff @ eff') tys
      else
        type_fail ~loc ~has:ty' ~expected:ty

let rec filter_effects options eff = function
  | [] ->
      eff
  | ((name, _), _)::branches ->
      (* TODO: Check duplication *)
      let exn = TypedEnv.NTy (Builtins.exn options) in
      let ty' = TypedEnv.NApp (exn, TypedEnv.Ty (Ident.Constr.to_type name)) in
      let eff = List.filter (fun ty -> not (NType.is_subset_of ty ty')) eff in
      filter_effects options eff branches

let p_as name (ps, a) =
  (List.map (fun p -> PretypedTree.As (p, name)) ps, a)

let specialize ~eq ~ty_size =
  let rec aux (p, a) = match p with
    | [] -> assert false (* NOTE: This is forbidden by the syntax *)
    | PretypedTree.TyConstr (_, c, qs)::ps when eq c -> [(qs @ ps, a)]
    | PretypedTree.TyConstr _::_ -> []
    | PretypedTree.Wildcard as p::ps -> [(List.replicate ty_size p @ ps, a)]
    | PretypedTree.Or (q1, q2)::ps -> aux (q1::ps, a) @ aux (q2::ps, a)
    | PretypedTree.As (p, name)::ps -> List.map (p_as name) (aux (p::ps, a))
  in
  fun m -> List.flatten (List.map aux m)

let decompose =
  let rec aux (p, a) = match p with
    | [] -> assert false (* NOTE: This is forbidden by the syntax *)
    | PretypedTree.TyConstr _::_ -> []
    | PretypedTree.Wildcard::ps -> [(ps, a)]
    | PretypedTree.Or (q1, q2)::ps -> aux (q1::ps, a) @ aux (q2::ps, a)
    | PretypedTree.As (p, name)::ps -> List.map (p_as name) (aux (p::ps, a))
  in
  fun m -> List.flatten (List.map aux m)

let jump a =
  let exception Failed in
  let rec aux i = function
    | [] -> Jump a
    | PretypedTree.TyConstr _::_ -> raise Failed
    | PretypedTree.Wildcard::xs -> Swap (i, aux (succ i) xs)
    | PretypedTree.Or _::_ -> raise Failed
    | PretypedTree.As (p, name)::xs -> Alias (name, aux i (p::xs))
  in
  fun row -> try Some (aux 1 row) with Failed -> None

let compile env = function
  | [] -> assert false (* NOTE: This is forbidden by the syntax *)
  | (row, a)::m -> begin match jump a row with
    | Some t -> t
    | None ->
        let heads = assert false (* TODO *) in
        assert false (* TODO *)
  end

let unify_list _ _ =
  assert false (* TODO *)

let pattern_to_matrix env ty (pattern, a) =
  let rec aux ty = function
    | PretypedTree.TyConstr _ ->
        assert false (* TODO *)
    | PretypedTree.Wildcard ->
        (PretypedTree.Wildcard, [])
    | PretypedTree.Or (p1, p2) ->
        let (p1, tys1) = aux ty p1 in
        let (p2, tys2) = aux ty p2 in
        let tys = unify_list tys1 tys2 in
        (PretypedTree.Or (p1, p2), tys)
    | PretypedTree.As (p, name) ->
        let (p, tys) = aux ty p in
        (PretypedTree.As (p, name), (name, ty)::tys)
  in
  let (p, tys) = aux ty pattern in
  (([p], a), tys)

let patterns_to_matrix env ty patterns =
  let m = List.map (pattern_to_matrix env ty) patterns in
  List.split m

let split_patterns patterns =
  let (patterns, results) = List.split patterns in
  let aux a pattern = (pattern, a) in
  (List.mapi aux patterns, results)

(* TODO: Check unused cases by checking the produced decision tree for
   every action indexes *)

let rec check_try_branch options env ((name, args), t) =
  match EnvMap.Constr.find name env.TypedEnv.constrs with
  | TypedEnv.Exn, ty' ->
      let (args', _) = NType.funs ty' in
      let aux env name (ty, _) = Env.add_value name ty env in
      let env = try List.fold_left2 aux env args args' with
        | Invalid_argument _ ->
            Err.fail
              ~loc:(Ident.Constr.loc name)
              "Wrong number of parameters. Has %d but expected %d."
              (List.length args)
              (List.length args')
      in
      let loct = fst t in
      let (t, tyt, eff) = check_term options env t in
      (((Ident.Constr.to_name name, args), t), (loct, tyt, eff))
  | TypedEnv.Index _, _ ->
      Err.fail
        ~loc:(Ident.Constr.loc name)
        "This data constructor is not an exception"

and check_try_branches options ty eff env = function
  | [] ->
      assert false (* NOTE: This is forbidden by the syntax *)
  | branches ->
      let eff = filter_effects options eff branches in
      let branches = List.map (check_try_branch options env) branches in
      let (branches, tys) = List.split branches in
      let (ty, eff) = get_supertype ty eff tys in
      (branches, ty, eff)

and check_results _ _ _ =
  assert false (* TODO *)

and check_term options env = function
  | (_, PretypedTree.Abs ((name, ty), t)) ->
      let ty = NType.check ~pure_arrow:`Forbid env ty in
      let env = Env.add_value name ty env in
      let (t, ty', eff) = check_term options env t in
      (Abs (name, t), TypedEnv.NFun (ty, eff, ty'), [])
  | (loc, PretypedTree.TAbs ((name, k), t)) ->
      let env = Env.add_abstract_type name k env in
      let (t, ty, eff) = check_term options env t in
      if not (List.is_empty eff) then
        Err.fail ~loc "Effects are forbidden under type abstractions.";
      (t, TypedEnv.NForall (name, k, ty), [])
  | (_, PretypedTree.CAbs _) ->
      assert false (* TODO *)
  | (loc, PretypedTree.App (t1, t2)) ->
      let (t1, ty1, eff1) = check_term options env t1 in
      let (t2, ty2, eff2) = check_term options env t2 in
      let (ty, eff3) = app ~loc ty2 ty1 in
      (App (t1, t2), ty, eff1 @ eff2 @ eff3)
  | (loc, PretypedTree.TApp (t, ty)) ->
      let (t, ty', eff) = check_term options env t in<commit_msg>Rename get_supertype to unify<commit_after>(* Copyright (c) 2013-2017 The Cervoise developers. *)
(* See the LICENSE file at the top-level directory. *)

open UntypedTree

let type_fail ~loc ~has ~expected =
  Err.fail_doc ~loc
    Utils.PPrint.(str "This value has type" ^^^
                  squotes (NType.dump has) ^^^
                  str "but was expected of type" ^^^
                  squotes (NType.dump expected) ^^^
                  dot)

let eff_fail ~loc ~has ~expected =
  Err.fail_doc ~loc
    Utils.PPrint.(str "This effect has type" ^^^
                  squotes (NType.dump_eff has) ^^^
                  str "but was expected of type" ^^^
                  squotes (NType.dump_eff expected) ^^^
                  dot)

let check_type ~loc env ty' ty =
  let ty = NType.check ~pure_arrow:`Allow env ty in
  if not (NType.is_subset_of ty' ty) then
    type_fail ~loc ~has:ty' ~expected:ty;
  ty

let check_eff ~loc env eff' eff =
  let eff = NType.check_eff ~pure_arrow:`Allow env eff in
  if not (NType.eff_is_subset_of eff' eff) then
    eff_fail ~loc ~has:eff' ~expected:eff;
  eff

let check_eff_opt ~loc env eff' =
  Option.map_or ~default:[] (check_eff ~loc env eff')

let unit options = TypedEnv.NTy (Builtins.unit options)
let is_main ~current_module = Ident.Name.equal (Builtins.main ~current_module)
let io options = TypedEnv.NTy (Builtins.io options)
let has_io options = List.exists (NType.is_subset_of (io options))

let get_const options = function
  | PretypedTree.Int n -> (`Int n, Builtins.int options)
  | PretypedTree.Float n -> (`Float n, Builtins.float options)
  | PretypedTree.Char c -> (`Char c, Builtins.char options)
  | PretypedTree.String s -> (`String s, Builtins.string options)

let get_rep name = function
  | TypedEnv.Index idx -> Index idx
  | TypedEnv.Exn -> Exn (Ident.Constr.to_name name)

let eff_of_ty ~loc options = function
  | TypedEnv.NSum [] ->
      assert false (* TODO: Check this. This shouldn't happen *)
  | TypedEnv.NSum sum ->
      let exn = TypedEnv.NTy (Builtins.exn options) in
      List.map (fun t -> TypedEnv.NApp (exn, NType.to_type t)) sum
  | TypedEnv.NTy _ | TypedEnv.NFun _
  | TypedEnv.NForall _ | TypedEnv.NApp _ as t ->
      Err.fail_doc
        ~loc
        Utils.PPrint.(str "Cannot throw exception of type" ^^^
                      squotes (NType.dump t) ^^^
                      dot)

let rec unify ty eff = function
  | [] ->
      (ty, eff)
  | (loc, ty', eff')::tys ->
      if NType.is_subset_of ty ty' then
        unify ty' (eff @ eff') tys
      else if NType.is_subset_of ty' ty then
        unify ty (eff @ eff') tys
      else
        type_fail ~loc ~has:ty' ~expected:ty

let unify_list _ _ =
  assert false (* TODO *)

let rec filter_effects options eff = function
  | [] ->
      eff
  | ((name, _), _)::branches ->
      (* TODO: Check duplication *)
      let exn = TypedEnv.NTy (Builtins.exn options) in
      let ty' = TypedEnv.NApp (exn, TypedEnv.Ty (Ident.Constr.to_type name)) in
      let eff = List.filter (fun ty -> not (NType.is_subset_of ty ty')) eff in
      filter_effects options eff branches

let p_as name (ps, a) =
  (List.map (fun p -> PretypedTree.As (p, name)) ps, a)

let specialize ~eq ~ty_size =
  let rec aux (p, a) = match p with
    | [] -> assert false (* NOTE: This is forbidden by the syntax *)
    | PretypedTree.TyConstr (_, c, qs)::ps when eq c -> [(qs @ ps, a)]
    | PretypedTree.TyConstr _::_ -> []
    | PretypedTree.Wildcard as p::ps -> [(List.replicate ty_size p @ ps, a)]
    | PretypedTree.Or (q1, q2)::ps -> aux (q1::ps, a) @ aux (q2::ps, a)
    | PretypedTree.As (p, name)::ps -> List.map (p_as name) (aux (p::ps, a))
  in
  fun m -> List.flatten (List.map aux m)

let decompose =
  let rec aux (p, a) = match p with
    | [] -> assert false (* NOTE: This is forbidden by the syntax *)
    | PretypedTree.TyConstr _::_ -> []
    | PretypedTree.Wildcard::ps -> [(ps, a)]
    | PretypedTree.Or (q1, q2)::ps -> aux (q1::ps, a) @ aux (q2::ps, a)
    | PretypedTree.As (p, name)::ps -> List.map (p_as name) (aux (p::ps, a))
  in
  fun m -> List.flatten (List.map aux m)

let jump a =
  let exception Failed in
  let rec aux i = function
    | [] -> Jump a
    | PretypedTree.TyConstr _::_ -> raise Failed
    | PretypedTree.Wildcard::xs -> Swap (i, aux (succ i) xs)
    | PretypedTree.Or _::_ -> raise Failed
    | PretypedTree.As (p, name)::xs -> Alias (name, aux i (p::xs))
  in
  fun row -> try Some (aux 1 row) with Failed -> None

let compile env = function
  | [] -> assert false (* NOTE: This is forbidden by the syntax *)
  | (row, a)::m -> begin match jump a row with
    | Some t -> t
    | None ->
        let heads = assert false (* TODO *) in
        assert false (* TODO *)
  end

let pattern_to_matrix env ty (pattern, a) =
  let rec aux ty = function
    | PretypedTree.TyConstr _ ->
        assert false (* TODO *)
    | PretypedTree.Wildcard ->
        (PretypedTree.Wildcard, [])
    | PretypedTree.Or (p1, p2) ->
        let (p1, tys1) = aux ty p1 in
        let (p2, tys2) = aux ty p2 in
        let tys = unify_list tys1 tys2 in
        (PretypedTree.Or (p1, p2), tys)
    | PretypedTree.As (p, name) ->
        let (p, tys) = aux ty p in
        (PretypedTree.As (p, name), (name, ty)::tys)
  in
  let (p, tys) = aux ty pattern in
  (([p], a), tys)

let patterns_to_matrix env ty patterns =
  let m = List.map (pattern_to_matrix env ty) patterns in
  List.split m

let split_patterns patterns =
  let (patterns, results) = List.split patterns in
  let aux a pattern = (pattern, a) in
  (List.mapi aux patterns, results)

(* TODO: Check unused cases by checking the produced decision tree for
   every action indexes *)

let rec check_try_branch options env ((name, args), t) =
  match EnvMap.Constr.find name env.TypedEnv.constrs with
  | TypedEnv.Exn, ty' ->
      let (args', _) = NType.funs ty' in
      let aux env name (ty, _) = Env.add_value name ty env in
      let env = try List.fold_left2 aux env args args' with
        | Invalid_argument _ ->
            Err.fail
              ~loc:(Ident.Constr.loc name)
              "Wrong number of parameters. Has %d but expected %d."
              (List.length args)
              (List.length args')
      in
      let loct = fst t in
      let (t, tyt, eff) = check_term options env t in
      (((Ident.Constr.to_name name, args), t), (loct, tyt, eff))
  | TypedEnv.Index _, _ ->
      Err.fail
        ~loc:(Ident.Constr.loc name)
        "This data constructor is not an exception"

and check_try_branches options ty eff env = function
  | [] ->
      assert false (* NOTE: This is forbidden by the syntax *)
  | branches ->
      let eff = filter_effects options eff branches in
      let branches = List.map (check_try_branch options env) branches in
      let (branches, tys) = List.split branches in
      let (ty, eff) = unify ty eff tys in
      (branches, ty, eff)

and check_results _ _ _ =
  assert false (* TODO *)

and check_term options env = function
  | (_, PretypedTree.Abs ((name, ty), t)) ->
      let ty = NType.check ~pure_arrow:`Forbid env ty in
      let env = Env.add_value name ty env in
      let (t, ty', eff) = check_term options env t in
      (Abs (name, t), TypedEnv.NFun (ty, eff, ty'), [])
  | (loc, PretypedTree.TAbs ((name, k), t)) ->
      let env = Env.add_abstract_type name k env in
      let (t, ty, eff) = check_term options env t in
      if not (List.is_empty eff) then
        Err.fail ~loc "Effects are forbidden under type abstractions.";
      (t, TypedEnv.NForall (name, k, ty), [])
  | (_, PretypedTree.CAbs _) ->
      assert false (* TODO *)
  | (loc, PretypedTree.App (t1, t2)) ->
      let (t1, ty1, eff1) = check_term options env t1 in
      let (t2, ty2, eff2) = check_term options env t2 in
      let (ty, eff3) = app ~loc ty2 ty1 in
      (App (t1, t2), ty, eff1 @ eff2 @ eff3)
  | (loc, PretypedTree.TApp (t, ty)) ->
      let (t, ty', eff) = check_term options env t in
{'fraction_non_alphanumeric': 0.12754460919829103, 'fraction_numerical': 0.006031666247800955, 'mean_word_length': 2.5013198416190057, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 111, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5664047', 'n_tokens_mistral': 5675, 'n_tokens_neox': 5574, 'n_words': 1848}