diff --git a/FSharpActivePatterns/bin/REPL.ml b/FSharpActivePatterns/bin/REPL.ml index 89e6e8c23..f8ebe5386 100644 --- a/FSharpActivePatterns/bin/REPL.ml +++ b/FSharpActivePatterns/bin/REPL.ml @@ -61,31 +61,35 @@ let run_repl dump_parsetree input_file = | None -> stdin | Some n -> open_in n in - let rec run_repl_helper run = + let rec run_repl_helper run env state = let open Format in match run ic with | Fail -> fprintf err_formatter "Error occured\n" | Empty -> fprintf std_formatter "\n"; print_flush (); - run_repl_helper run + run_repl_helper run env state | End -> () | Result ast -> - let result = infer ast in + let result = infer ast env state in (match result with - | Error err -> + | new_state, Error err -> fprintf err_formatter "Type checking failed: %a\n" pp_error err; - print_flush () - | Ok t -> + print_flush (); + run_repl_helper run env new_state + | new_state, Ok (env, types) -> (match dump_parsetree with | true -> print_construction std_formatter ast | false -> - fprintf std_formatter "- : "; - pp_typ std_formatter t); - print_flush ()); - run_repl_helper run + List.iter + (fun t -> + fprintf std_formatter "- : "; + pp_typ std_formatter t) + types; + print_flush ()); + run_repl_helper run env new_state) in - run_repl_helper run_single + run_repl_helper run_single TypeEnvironment.empty 0 ;; type opts = diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml index 3cfe55884..80f89e2b3 100644 --- a/FSharpActivePatterns/lib/inferencer.ml +++ b/FSharpActivePatterns/lib/inferencer.ml @@ -44,7 +44,7 @@ module R : sig end val fresh : int t - val run : 'a t -> ('a, error) Result.t + val run : 'a t -> int -> int * ('a, error) Result.t module RMap : sig val fold : ('a, 'b, 'c) Map.t -> init:'d t -> f:('a -> 'b -> 'd -> 'd t) -> 'd t @@ -112,7 +112,7 @@ end = struct (* takes current state, returns state + 1 *) let fresh : int t = fun last -> last + 1, Result.Ok last - let run m = snd (m 0) + let run m state = m state end type fresh = int @@ -122,7 +122,7 @@ module Type : sig type t = typ val occurs_in : fresh -> t -> bool - (* val free_vars : t -> binder_set *) + val free_vars : t -> binder_set end = struct type t = typ @@ -139,17 +139,17 @@ end = struct ;; (* collects all type variables *) - (* let free_vars = - let rec helper acc = function - | Primitive _ -> acc - | Type_var b -> VarSet.add b acc - | Arrow (fst, snd) -> helper (helper acc fst) snd - | Type_list typ -> helper acc typ - | Type_tuple (fst, snd, rest) -> List.fold (fst :: snd :: rest) ~init:acc ~f:helper - | TOption t -> helper acc t - in - helper VarSet.empty - ;; *) + let free_vars = + let rec helper acc = function + | Primitive _ -> acc + | Type_var b -> VarSet.add b acc + | Arrow (fst, snd) -> helper (helper acc fst) snd + | Type_list typ -> helper acc typ + | Type_tuple (fst, snd, rest) -> List.fold (fst :: snd :: rest) ~init:acc ~f:helper + | TOption t -> helper acc t + in + helper VarSet.empty + ;; end (* module of substitution *) @@ -190,8 +190,8 @@ end = struct ;; (* aliases for Map actions *) - let find map key = Map.find map key - let remove map key = Map.remove map key + let find = Map.find + let remove = Map.remove (* search for input in given map, if there is no match, output input type, else output found typ value associated w this key. @@ -217,7 +217,6 @@ end = struct let rec unify fst snd = match fst, snd with | Primitive fst, Primitive snd when String.equal fst snd -> return empty - | Primitive _, Primitive _ -> fail (`Unification_failed (fst, snd)) | Type_var f, Type_var s when Int.equal f s -> return empty | Type_var b, t | t, Type_var b -> singleton b t | Arrow (f1, s1), Arrow (f2, s2) -> @@ -267,7 +266,7 @@ module Scheme : sig (* val occurs_in : fresh -> t -> bool *) val apply : Substitution.t -> t -> t - (* val free_vars : t -> binder_set *) + val free_vars : t -> binder_set end = struct type t = scheme @@ -277,47 +276,58 @@ end = struct ;; *) (* take all vars that are not bound in typ *) - (* let free_vars = function - | S (vars, t) -> VarSet.diff (Type.free_vars t) vars - ;; *) + let free_vars = function + | Scheme (vars, t) -> VarSet.diff (Type.free_vars t) vars + ;; (* take substitution and scheme, remove its free vars from substitution, form new scheme according to substitution (apply it to typ) *) - let apply subst (S (vars, t)) = + let apply subst (Scheme (vars, t)) = let subst2 = VarSet.fold (fun key s -> Substitution.remove s key) vars subst in - S (vars, Substitution.apply subst2 t) + Scheme (vars, Substitution.apply subst2 t) ;; (* let pp = pp_scheme *) end module TypeEnvironment : sig - val extend : ('a, 'b, 'c) Base.Map.t -> 'a -> 'b -> ('a, 'b, 'c) Base.Map.t - val apply : Substitution.t -> ('a, scheme, 'b) Base.Map.t -> ('a, scheme, 'b) Base.Map.t - val empty : (string, 'a, Base.String.comparator_witness) Base.Map.t - val find : 'a -> ('a, 'b, 'c) Base.Map.t -> 'b option + type t + + val free_vars : t -> VarSet.t + val extend : t -> string -> scheme -> t + val apply : Substitution.t -> t -> t + val empty : t + val find : t -> string -> scheme option + val find_exn : t -> string -> scheme + val find_typ_exn : t -> string -> typ + val remove : t -> string -> t end = struct open Base (* environment (context?) -- pairs of names and their types list *) - (* type t = (ident, scheme, String.comparator_witness) Map.t *) + type t = (string, scheme, String.comparator_witness) Map.t (* if pair (key, some old value) exists in map env, then replace old value with new, else add pair (key, value) into map *) let extend env key value = Map.update env key ~f:(fun _ -> value) - - (* let remove env key = Map.remove env key *) + let remove env key = Map.remove env key let empty = Map.empty (module String) (* apply given substitution to all elements of environment *) let apply subst env = Map.map env ~f:(Scheme.apply subst) - let find key env = Map.find env key + let find = Map.find + let find_exn = Map.find_exn + + let find_typ_exn env key = + match find_exn env key with + | Scheme (_, typ) -> typ + ;; (* collect all free vars from environment *) - (* let free_vars : t -> VarSet.t = - Map.fold ~init:VarSet.empty ~f:(fun ~key:_ ~data:s acc -> - VarSet.union acc (Scheme.free_vars s)) - ;; *) + let free_vars : t -> VarSet.t = + Map.fold ~init:VarSet.empty ~f:(fun ~key:_ ~data:s acc -> + VarSet.union acc (Scheme.free_vars s)) + ;; (* TODO: custom pp_scheme? not from deriving *) (* let pp fmt map = @@ -336,24 +346,29 @@ let make_fresh_var = fresh >>| fun n -> Type_var n (* replace all type vars with fresh ones *) let instantiate : scheme -> typ R.t = - fun (S (vars, t)) -> + fun (Scheme (vars, t)) -> VarSet.fold - (fun name ty -> - let* ty = ty in + (fun name typ -> + let* typ = typ in let* fr_var = make_fresh_var in let* subst = Substitution.singleton name fr_var in - return (Substitution.apply subst ty)) + return (Substitution.apply subst typ)) vars (return t) ;; (* take free vars of type t and environment, put difference between them in S constructor so all vars are context independent *) -(* let generalize : TypeEnvironment.t -> Type.t -> Scheme.t = - fun env t -> - let free = VarSet.diff (Type.free_vars t) (TypeEnvironment.free_vars env) in - S (free, t) - ;; *) +let generalize env typ = + let free = VarSet.diff (Type.free_vars typ) (TypeEnvironment.free_vars env) in + Scheme (free, typ) +;; + +let generalize_rec env typ rec_name = + let env = TypeEnvironment.remove env rec_name in + let free = VarSet.diff (Type.free_vars typ) (TypeEnvironment.free_vars env) in + Scheme (free, typ) +;; let infer_lt = function | Int_lt _ -> return (Substitution.empty, int_typ) @@ -364,24 +379,24 @@ let infer_lt = function let rec infer_pattern env = function | Wild -> - let* fresh_type = make_fresh_var in - return (fresh_type, env) + let* fresh_var = make_fresh_var in + return (fresh_var, env) | PConst lt -> let* _, t = infer_lt lt in return (t, env) | PVar (Ident (name, _)) -> (* подумать что делать с типом в Ident*) let* fresh = make_fresh_var in - let scheme = S (VarSet.empty, fresh) in + let scheme = Scheme (VarSet.empty, fresh) in let env = TypeEnvironment.extend env name scheme in return (fresh, env) | POption None -> - let* fresh_type = make_fresh_var in - return (fresh_type, env) + let* fresh_var = make_fresh_var in + return (fresh_var, env) | POption (Some p) -> infer_pattern env p | PList [] -> - let* fresh_type = make_fresh_var in - return (Type_list fresh_type, env) + let* fresh_var = make_fresh_var in + return (Type_list fresh_var, env) | PList (hd :: tl) -> let* typ1, env = infer_pattern env hd in let* subst_unify, typ_unified = @@ -418,11 +433,28 @@ let rec infer_pattern env = function return (Type_tuple (typ1, typ2, typs_rest), env) ;; +let extract_names_from_let_binds let_binds = + List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name) +;; + +let extend_env_with_bind_names env let_binds = + let bind_names = extract_names_from_let_binds let_binds in + let fresh_vars = List.init (List.length let_binds) ~f:(fun _ -> make_fresh_var) in + List.fold2_exn + ~init:(return env) + ~f:(fun acc bind_name fresh_var -> + let* fresh_var = fresh_var in + let* acc = acc in + return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var)))) + bind_names + fresh_vars +;; + let rec infer_expr env = function | Const lt -> infer_lt lt | Variable (Ident (varname, _)) -> (* подумать что делать с типом Ident*) - (match TypeEnvironment.find varname env with + (match TypeEnvironment.find env varname with | Some s -> let* t = instantiate s in return (Substitution.empty, t) @@ -453,15 +485,13 @@ let rec infer_expr env = function | Binary_greater | Binary_greater_or_equal | Binary_less | Binary_less_or_equal -> return (int_typ, int_typ, bool_typ) | Binary_equal | Binary_unequal -> - let* fresh_type = make_fresh_var in - return (fresh_type, fresh_type, bool_typ) + let* fresh_var = make_fresh_var in + return (fresh_var, fresh_var, bool_typ) | Binary_cons -> - let* fresh_type = make_fresh_var in - return (fresh_type, Type_list fresh_type, Type_list fresh_type) + let* fresh_var = make_fresh_var in + return (fresh_var, Type_list fresh_var, Type_list fresh_var) in let* subst3 = Substitution.unify (Substitution.apply subst2 typ1) e1typ in - (*Format.printf "Checking types: res_typ1 = %a\n" pp_typ (Substitution.apply subst2 typ1); - Format.printf "Checking types: res_typ2 = %a\n" pp_typ (Substitution.apply subst3 typ2);*) let* subst4 = Substitution.unify (Substitution.apply subst3 typ2) e2typ in let* subst_res = Substitution.compose_all [ subst1; subst2; subst3; subst4 ] in return (subst_res, Substitution.apply subst_res etyp) @@ -485,15 +515,10 @@ let rec infer_expr env = function ~init:(return (Substitution.empty, [])) in let* subst_result = Substitution.compose_all [ subst1; subst2; subst_rest ] in - let typ1 = Substitution.apply subst_result typ1 in - let typ2 = Substitution.apply subst_result typ2 in - let typs_rest = - List.map typs_rest ~f:(fun typ -> Substitution.apply subst_result typ) - in return (subst_result, Type_tuple (typ1, typ2, typs_rest)) | List [] -> - let* fresh_type = make_fresh_var in - return (Substitution.empty, Type_list fresh_type) + let* fresh_var = make_fresh_var in + return (Substitution.empty, Type_list fresh_var) | List (hd :: tl) -> let* subst1, typ1 = infer_expr env hd in let typ1 = Substitution.apply subst1 typ1 in @@ -529,10 +554,11 @@ let rec infer_expr env = function | Apply (f, arg) -> let* subst1, typ1 = infer_expr env f in let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) arg in - let* fresh_type = make_fresh_var in - let* subst3 = unify (Substitution.apply subst2 typ1) (Arrow (typ2, fresh_type)) in + let* fresh_var = make_fresh_var in + let typ1 = Substitution.apply subst2 typ1 in + let* subst3 = unify typ1 (Arrow (typ2, fresh_var)) in let* subst_result = Substitution.compose_all [ subst1; subst2; subst3 ] in - return (subst_result, Substitution.apply subst_result fresh_type) + return (subst_result, Substitution.apply subst3 fresh_var) | Lambda (arg, args, e) -> let* env, arg_types = RList.fold_right @@ -544,54 +570,125 @@ let rec infer_expr env = function in let* subst, e_type = infer_expr env e in return (subst, Substitution.apply subst (arrow_of_types arg_types e_type)) - (* | LetIn (Rec, let_bind, let_binds, e) -> - let bind_names = - List.map (let_bind :: let_binds) ~f:(fun let_bind -> - match let_bind with - | Let_bind (Ident (name, _), _, _) -> name) - in - let* env = - List.fold - ~init:(return env) - ~f:(fun acc name -> - let* fresh_type = make_fresh_var in - let* acc = acc in - return (TypeEnvironment.extend acc name (S (VarSet.empty, fresh_type)))) - bind_names - in - x *) - | _ -> fail (`WIP "Expr inference WIP") + | LetIn (Rec, let_bind, let_binds, e) -> + let let_binds = let_bind :: let_binds in + let* env = extend_env_with_bind_names env let_binds in + let* env, subst1 = extend_env_with_let_binds env Rec let_binds in + let* subst2, typ = infer_expr env e in + let* subst_final = Substitution.compose subst1 subst2 in + return (subst_final, typ) + | LetIn (Nonrec, let_bind, let_binds, e) -> + let* env, subst1 = extend_env_with_let_binds env Nonrec (let_bind :: let_binds) in + let* subst2, typ = infer_expr env e in + let* subst_final = Substitution.compose subst1 subst2 in + return (subst_final, typ) + | Match (e, p1, e1, rest) -> + let* subst_init, match_type = infer_expr env e in + let env = TypeEnvironment.apply subst_init env in + let* fresh_typevar = make_fresh_var in + let* subst, typ = + List.fold + ((p1, e1) :: rest) + ~init:(return (subst_init, fresh_typevar)) + ~f:(fun acc (pat, expr) -> + let* subst1, return_type = acc in + let* pat, env = infer_pattern env pat in + let* subst2 = unify match_type pat in + let env = TypeEnvironment.apply subst2 env in + let* subst3, expr_typ = infer_expr env expr in + let* subst4 = unify return_type expr_typ in + let* subst = Substitution.compose_all [ subst1; subst2; subst3; subst4 ] in + return (subst, Substitution.apply subst return_type)) + in + return (subst, typ) + +and extend_env_with_let_binds env is_rec let_binds = + List.fold + let_binds + ~init:(return (env, Substitution.empty)) + ~f:(fun acc let_bind -> + let* env, subst_acc = acc in + let* subst, bind_varname, scheme = infer_let_bind env is_rec let_bind in + let env = TypeEnvironment.extend env bind_varname scheme in + let env = TypeEnvironment.apply subst env in + let* subst_acc = Substitution.compose subst_acc subst in + return (env, subst_acc)) + +and infer_let_bind env is_rec = function + | Let_bind (Ident (bind_varname, _), args, e) -> + let* fresh_vars = + (* Hack for get typ list, not typ t list*) + List.fold args ~init:(return []) ~f:(fun acc _ -> + let* fresh_var = make_fresh_var in + let* acc = acc in + return (fresh_var :: acc)) + in + let arg_names = List.map args ~f:(function Ident (name, _) -> name) in + let* env_with_args = + List.fold2_exn + ~init:(return env) + ~f:(fun acc arg fresh_var -> + let* acc = acc in + return (TypeEnvironment.extend acc arg (Scheme (VarSet.empty, fresh_var)))) + arg_names + fresh_vars + in + let* subst1, typ1 = infer_expr env_with_args e in + let bind_type = Substitution.apply subst1 (arrow_of_types fresh_vars typ1) in + (* If let_bind is recursive, then bind_varname was already in environment *) + let* bind_typevar = + match is_rec with + | Rec -> return (TypeEnvironment.find_typ_exn env bind_varname) + | Nonrec -> make_fresh_var + in + let env = + match is_rec with + | Rec -> TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_type)) + | Nonrec -> env + in + let* subst2 = unify (Substitution.apply subst1 bind_typevar) bind_type in + let* subst = Substitution.compose subst1 subst2 in + let env = TypeEnvironment.apply subst env in + let bind_type = Substitution.apply subst bind_type in + let bind_var_scheme = + match is_rec with + | Rec -> generalize_rec env bind_type bind_varname + | Nonrec -> generalize env bind_type + in + return (subst, bind_varname, bind_var_scheme) ;; -(* and infer_let_bind env fresh_type = function - | Let_bind (_, args, e) -> - let arg_names = - List.map args ~f:(fun arg -> - match arg with - | Ident (name, _) -> name) - in - let* env = - List.fold - ~init:(return env) - ~f:(fun acc arg -> - let* fresh_type = make_fresh_var in - let* acc = acc in - return (TypeEnvironment.extend acc arg (S (VarSet.empty, fresh_type)))) - arg_names - in - let* subst1, typ1 = infer_expr env e in - let* subst2 = unify (Substitution.apply subst1 fresh_type) typ1 in - let* subst = Substitution.compose subst1 subst2 in - let env = TypeEnvironment.apply subst env in - let typ2 = generalize env (Substitution.apply subst fresh_type) in - return (subst, typ2) - ;; *) +let infer_statement env = function + | Let (Rec, let_bind, let_binds) -> + let let_binds = let_bind :: let_binds in + let* env = extend_env_with_bind_names env let_binds in + let* env, _ = extend_env_with_let_binds env Rec let_binds in + let bind_names = extract_names_from_let_binds let_binds in + let bind_types = + List.map bind_names ~f:(fun name -> + match TypeEnvironment.find_exn env name with + | Scheme (_, typ) -> typ) + in + return (env, bind_types) + | Let (Nonrec, let_bind, let_binds) -> + let let_binds = let_bind :: let_binds in + let* env, _ = extend_env_with_let_binds env Nonrec let_binds in + let bind_names = extract_names_from_let_binds let_binds in + let bind_types = + List.map bind_names ~f:(fun name -> + match TypeEnvironment.find_exn env name with + | Scheme (_, typ) -> typ) + in + return (env, bind_types) +;; let infer_construction env = function | Expr exp -> let* _, typ = infer_expr env exp in - return typ - | _ -> fail (`WIP "Statement inference WIP") + return (env, [ typ ]) + | Statement s -> + let* env, types = infer_statement env s in + return (env, types) ;; -let infer c = run (infer_construction TypeEnvironment.empty c) +let infer c env state = run (infer_construction env c) state diff --git a/FSharpActivePatterns/lib/inferencer.mli b/FSharpActivePatterns/lib/inferencer.mli index 04854645b..3ac24e5bf 100644 --- a/FSharpActivePatterns/lib/inferencer.mli +++ b/FSharpActivePatterns/lib/inferencer.mli @@ -6,6 +6,12 @@ open Ast open TypedTree open Format +module TypeEnvironment : sig + type t + + val empty : t +end + type error = [ `Occurs_check | `Undef_var of string @@ -14,4 +20,9 @@ type error = ] val pp_error : formatter -> error -> unit -val infer : construction -> (typ, error) result + +val infer + : construction + -> TypeEnvironment.t + -> int + -> int * (TypeEnvironment.t * typ list, error) result diff --git a/FSharpActivePatterns/lib/parser.ml b/FSharpActivePatterns/lib/parser.ml index a85b8706a..6b7a84491 100644 --- a/FSharpActivePatterns/lib/parser.ml +++ b/FSharpActivePatterns/lib/parser.ml @@ -242,7 +242,9 @@ let p_let p_expr = return (Let (rec_flag, Let_bind (name, args, body), let_bind_list)) ;; -let p_apply p_expr = chainl1 p_expr (return (fun expr1 expr2 -> Apply (expr1, expr2))) +let p_apply p_expr = + chainl1 (p_expr <* peek_sep1) (return (fun expr1 expr2 -> Apply (expr1, expr2))) +;; let p_option p make_option = skip_ws *> string "None" *> peek_sep1 *> return (make_option None) diff --git a/FSharpActivePatterns/lib/typedTree.ml b/FSharpActivePatterns/lib/typedTree.ml index 54ff2528f..26ab398a2 100644 --- a/FSharpActivePatterns/lib/typedTree.ml +++ b/FSharpActivePatterns/lib/typedTree.ml @@ -13,9 +13,9 @@ type typ = | TOption of typ [@@deriving show { with_path = false }] -let arrow_of_types first_types last = +let arrow_of_types first_types last_type = let open Base in - List.fold_right first_types ~init:last ~f:(fun left right -> Arrow (left, right)) + List.fold_right first_types ~init:last_type ~f:(fun left right -> Arrow (left, right)) ;; module VarSet = struct @@ -31,7 +31,7 @@ end type binder_set = VarSet.t [@@deriving show { with_path = false }] (* binder_set here -- list of all type vars in context (?) *) -type scheme = S of binder_set * typ [@@deriving show { with_path = false }] +type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }] let int_typ = Primitive "int" let bool_typ = Primitive "bool" diff --git a/FSharpActivePatterns/lib/typedTree.mli b/FSharpActivePatterns/lib/typedTree.mli index 09c2ff54a..d8f8667a1 100644 --- a/FSharpActivePatterns/lib/typedTree.mli +++ b/FSharpActivePatterns/lib/typedTree.mli @@ -21,7 +21,7 @@ module VarSet : sig end type binder_set = VarSet.t -type scheme = S of binder_set * typ [@@deriving show { with_path = false }] +type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }] val int_typ : typ val bool_typ : typ diff --git a/FSharpActivePatterns/lib/typesPp.ml b/FSharpActivePatterns/lib/typesPp.ml index 8e18b1ef4..59207a761 100644 --- a/FSharpActivePatterns/lib/typesPp.ml +++ b/FSharpActivePatterns/lib/typesPp.ml @@ -9,7 +9,10 @@ let pp_typ fmt typ = let rec helper fmt = function | Primitive s -> fprintf fmt "%S" s | Type_var var -> fprintf fmt "'_%d" var - | Arrow (fst, snd) -> fprintf fmt "(%a) -> %a" helper fst helper snd + | Arrow (fst, snd) -> + (match fst with + | Arrow _ -> fprintf fmt "(%a) -> %a" helper fst helper snd + | _ -> fprintf fmt "%a -> %a" helper fst helper snd) | Type_list typ -> fprintf fmt "%a list" helper typ | Type_tuple (first, second, rest) -> fprintf fmt "(";