From 19c11ad9c80c30063906508ed6507092d7a6e200 Mon Sep 17 00:00:00 2001 From: elvis Date: Wed, 6 Nov 2024 17:21:14 +0100 Subject: [PATCH] Started work for type inference --- lib/miniFun/TypeChecker.ml | 223 +++++++++---------------------------- lib/miniFun/Types.ml | 11 +- lib/miniFun/Types.mli | 37 +++++- lib/utility.ml | 12 ++ lib/utility.mli | 2 + 5 files changed, 112 insertions(+), 173 deletions(-) diff --git a/lib/miniFun/TypeChecker.ml b/lib/miniFun/TypeChecker.ml index 2bfcdec..2498200 100644 --- a/lib/miniFun/TypeChecker.ml +++ b/lib/miniFun/TypeChecker.ml @@ -5,175 +5,56 @@ Random.self_init () let (let*) = Result.bind -let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, error) result = - match program with - Integer _ -> Ok IntegerType - | Boolean _ -> Ok BooleanType - | Variable x -> ( (* check for the type in the context *) - match VariableMap.find_opt x context with - None -> Error (`AbsentAssignment - ("The variable " ^ x ^ " is not defined.")) - | Some t -> Ok t - ) - | Function (xs, typef, fbody) -> ( - (* first check that the function has the right specified type then check - that the number of inputs are the right number, finally eval the type - of the body using the bindings for the inputs *) - match typef with - FunctionType (tin, tout) -> ( - if List.length xs <> List.length tin then - Error (`WrongTypeSpecification - ("Type specification for function has wrong arity.")) - else - let context1 = List.fold_left2 - (fun acc x t -> VariableMap.add x t acc) - context - xs - tin - in - let* typefbody = evaluate_type fbody context1 in - if (typefbody = tout) then - Ok typef - else - Error (`WrongTypeSpecification - ("Function does not return specified type.")) - ) - | _ -> Error (`WrongTypeSpecification - ("Specification of function is not a function type.")) - ) - | Application (f, xs) -> ( - (* check that the type is actually a function, then checks that the - supplied inputs are of the right type, returns the return type if all - inputs are supplied, otherwise a function from the remaining inputs to - the output types *) - let* evalf = evaluate_type f context in - match evalf with - FunctionType (tin, tout) -> ( - let rec helper (params: t_exp list) (typeparams: ftype list) = - (* consumes until params are exausted *) - match (params, typeparams) with - ([], _) -> Ok typeparams - | (_, []) -> Error (`WrongArity ("Function application has arity " ^ - (List.length tin |> string_of_int) ^ - ", but was applied to " ^ - (List.length xs |> string_of_int) ^ - " parameters")) - | (p::tlparams, v::tltypeparams) -> - if evaluate_type p context = Ok v then - helper tlparams tltypeparams - else - Error (`WrongType "Argument with wrong type.") - in - let* typesremaining = helper xs tin in - match typesremaining with - [] -> Ok tout - | t -> Ok (FunctionType (t, tout)) - ) - | _ -> Error (`WrongType "Applying to a non function type") - ) - | Plus (x, y) - | Minus (x, y) - | Times (x, y) - | Division (x, y) - | Modulo (x, y) - | Power (x, y) -> ( - let* typex = evaluate_type x context in - let* typey = evaluate_type y context in - match typex, typey with - | (IntegerType, IntegerType) -> Ok IntegerType - | (IntegerType, _) -> Error (`WrongType "Second term is not an integer.") - | (_, _) -> Error (`WrongType "First term is not an integer.") - ) - | PowerMod (x, y, z) -> ( - let* typex = evaluate_type x context in - let* typey = evaluate_type y context in - let* typez = evaluate_type z context in - match typex, typey, typez with - | (IntegerType, IntegerType, IntegerType) -> Ok IntegerType - | (IntegerType, IntegerType, _) -> Error (`WrongType ("Third term is " ^ - "not an integer.")) - | (IntegerType, _, _) -> Error (`WrongType - ("Second term is not an integer.")) - | (_, _, _) -> Error (`WrongType "First term is not an integer.") - ) - | Rand (x) -> ( - let* typex = evaluate_type x context in - match typex with - | (IntegerType) -> Ok IntegerType - | (_) -> Error (`WrongType "Term is not an integer.") - ) - | BAnd (x, y) - | BOr (x, y) -> ( - let* typex = evaluate_type x context in - let* typey = evaluate_type y context in - match typex, typey with - | (BooleanType, BooleanType) -> Ok BooleanType - | (BooleanType, _) -> Error (`WrongType "Second term is not a boolean.") - | (_, _) -> Error (`WrongType "First term is not a boolean.") - ) - | BNot (x) -> ( - let* typex = evaluate_type x context in - match typex with - | (BooleanType) -> Ok BooleanType - | (_) -> Error (`WrongType "Term is not a boolean.") - ) - | Cmp (x, y) - | CmpLess (x, y) - | CmpLessEq (x, y) - | CmpGreater (x, y) - | CmpGreaterEq (x, y) -> ( - let* typex = evaluate_type x context in - let* typey = evaluate_type y context in - match typex, typey with - | (IntegerType, IntegerType) -> Ok BooleanType - | (IntegerType, _) -> Error (`WrongType "Second term is not an integer.") - | (_, _) -> Error (`WrongType "First term is not an integer.") - ) - | IfThenElse (guard, if_exp, else_exp) -> ( - let* typeguard = evaluate_type guard context in - let* typeif_exp = evaluate_type if_exp context in - let* typeelse_exp = evaluate_type else_exp context in - match typeguard, typeif_exp, typeelse_exp with - (BooleanType, t1, t2) -> ( - if t1 = t2 then - Ok t1 - else - Error (`WrongType "If branches do not have the same type.") - ) - | (_, _, _) -> Error (`WrongType "If guard is not a boolean.") - ) - | LetIn (x, xval, rest) -> - (* bind the type to the variable name in the context *) - let* typex = evaluate_type xval context in - evaluate_type rest (VariableMap.add x typex context) - | LetFun (f, xs, typef, fbody, rest) -> - (* like with the function type, but also add f itself to the bindings *) - match typef with - FunctionType (tin, tout) -> ( - if List.length xs <> List.length tin then - Error (`WrongArity "Type specification for function has wrong arity.") - else - let context1 = VariableMap.add f typef context in - let context2 = List.fold_left2 - (fun acc x t -> VariableMap.add x t acc) - context1 - xs - tin - in - let* typefbody = evaluate_type fbody context2 in - let* typerest = evaluate_type rest context1 in - match (typefbody = tout, typerest) with - (false, _) -> Error (`WrongTypeSpecification - "Function does not return specified type.") - | (true, t) -> Ok t - ) - | _ -> Error (`WrongTypeSpecification - "Specification of function is not a function type.") -let typecheck (program: t_exp) : (ftype, error) result = - let* typeprogram = evaluate_type program VariableMap.empty in - match typeprogram with - FunctionType ([IntegerType], IntegerType) -> ( - Ok (FunctionType ([IntegerType], IntegerType)) - ) - | _ -> Error (`WrongType "Program is not a function from int to int.") +let rec principalTypings (D: ) (e: t_exp) : () result + +let evaluate_type (_program: t_exp) (_context: typingshape) : (typingshape, error) result = + failwith "asd" + (* match program with *) + (* Integer _ -> Ok (VariableMap.empty, IntegerType) *) + (* | Boolean _ -> Ok (VariableMap.empty, BooleanType) *) + (* | Variable x -> ( *) + (* match (VariableMap.find_opt x (fst context)) with *) + (* (None) -> ( *) + (* let u = PolimorphicType (Utility.fromIntToString !globalIdentifier) in *) + (* globalIdentifier := !globalIdentifier + 1; *) + (* Ok (VariableMap.singleton x u, u) *) + (* ) *) + (* | (Some u) -> Ok (VariableMap.singleton x u, u) *) + (* ) *) + (* | Function (xs, typef, fbody) -> failwith "Not Implemented" *) + (* | Application (f, xs) -> failwith "Not Implemented" *) + (* | Plus (x, y) *) + (* | Minus (x, y) *) + (* | Times (x, y) *) + (* | Division (x, y) *) + (* | Modulo (x, y) *) + (* | Power (x, y) -> ( *) + (* let* partialResx = evaluate_type x context in *) + (* let* partialResy = evaluate_type y context in *) + (* match (partialResx, partialResy) with *) + (* ((conx, IntegerType), (cony, IntegerType)) -> *) + (* Ok (VariableMap.union (fun _ x _ -> Some x) conx cony, *) + (* FunctionType ([IntegerType; IntegerType], IntegerType)) *) + (* | ((conx, PolimorphicType xv), (cony, IntegerType)) -> *) + (* Ok (unify ) *) + (* | ((_conx, IntegerType), (_cony, PolimorphicType _yv)) *) + (* | ((_conx, PolimorphicType _xv), (_cony, PolimorphicType _yv)) -> failwith "ads" *) + (* | (_, _) -> Error (`WrongType "The arguments are of the wrong type") *) + (* ) *) + (* | PowerMod (x, y, z) -> failwith "Not Implemented" *) + (* | Rand (x) -> failwith "Not Implemented" *) + (* | BAnd (x, y) *) + (* | BOr (x, y) -> failwith "Not Implemented" *) + (* | BNot (x) -> failwith "Not Implemented" *) + (* | Cmp (x, y) *) + (* | CmpLess (x, y) *) + (* | CmpLessEq (x, y) *) + (* | CmpGreater (x, y) *) + (* | CmpGreaterEq (x, y) -> failwith "Not Implemented" *) + (* | IfThenElse (guard, if_exp, else_exp) -> failwith "Not Implemented" *) + (* | LetIn (x, xval, rest) -> failwith "Not Implemented" *) + (* | LetFun (f, xs, typef, fbody, rest) -> failwith "Not Implemented" *) + +let typecheck (_program: t_exp) : (ftype, error) result = + failwith "Not Implemented" diff --git a/lib/miniFun/Types.ml b/lib/miniFun/Types.ml index 2a0865c..bf685a5 100644 --- a/lib/miniFun/Types.ml +++ b/lib/miniFun/Types.ml @@ -1,12 +1,21 @@ type variable = string +let globalIdentifier = ref 1 + module VariableMap = Map.Make(String) module VariableSet = Set.Make(String) type ftype = IntegerType | BooleanType + | PolimorphicType of string | FunctionType of ftype list * ftype +type fsubstitution = (* goes from polimorphic types to types *) + ftype VariableMap.t +type fenvironment = (* goes from variables to types *) + ftype VariableMap.t +type typingshape = (* tuple of a simple type environment and a simple type *) + fenvironment * ftype type t_exp = Integer of int (* x := a *) @@ -32,7 +41,7 @@ type t_exp = | CmpGreaterEq of t_exp * t_exp (* x >= x *) | IfThenElse of t_exp * t_exp * t_exp (* if b then c else c *) | LetIn of variable * t_exp * t_exp (* let x = x in x *) - | LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x*) + | LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x *) type permittedValues = IntegerPermitted of int diff --git a/lib/miniFun/Types.mli b/lib/miniFun/Types.mli index b622858..59262cd 100644 --- a/lib/miniFun/Types.mli +++ b/lib/miniFun/Types.mli @@ -1,12 +1,47 @@ type variable = string +val globalIdentifier : int ref + module VariableMap : Map.S with type key = variable module VariableSet : Set.S with type elt = string type ftype = IntegerType | BooleanType + | PolimorphicType of variable | FunctionType of ftype list * ftype +type fsubstitution = (* goes from polimorphic types to types *) + ftype VariableMap.t +type fenvironment = (* goes from variables to types *) + ftype VariableMap.t +type typingshape = (* tuple of a simple type environment and a simple type *) + fenvironment * ftype + +type intermediaryType = + IInteger + | IBoolean + | IVariable of variable + | IFunction of variable list * ftype list * intermediaryType + | IApplication of intermediaryType * intermediaryType list + | IPlus of intermediaryType * intermediaryType + | IMinus of intermediaryType * intermediaryType + | ITimes of intermediaryType * intermediaryType + | IDivision of intermediaryType * intermediaryType + | IModulo of intermediaryType * intermediaryType + | IPower of intermediaryType * intermediaryType + | IPowerMod of intermediaryType * intermediaryType * intermediaryType + | IRand of intermediaryType + | IBAnd of intermediaryType * intermediaryType + | IBOr of intermediaryType * intermediaryType + | IBNot of intermediaryType + | ICmp of intermediaryType * intermediaryType + | ICmpLess of intermediaryType * intermediaryType + | ICmpLessEq of intermediaryType * intermediaryType + | ICmpGreater of intermediaryType * intermediaryType + | ICmpGreaterEq of intermediaryType * intermediaryType + | IIfThenElse of intermediaryType * intermediaryType * intermediaryType + | ILetIn of variable * ftype * intermediaryType * intermediaryType + | ILetFun of variable * ftype * variable list * ftype list * intermediaryType * intermediaryType type t_exp = Integer of int (* x := a *) @@ -32,7 +67,7 @@ type t_exp = | CmpGreaterEq of t_exp * t_exp (* x >= x *) | IfThenElse of t_exp * t_exp * t_exp (* if b then c else c *) | LetIn of variable * t_exp * t_exp (* let x = x in x *) - | LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x*) + | LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x *) type permittedValues = IntegerPermitted of int diff --git a/lib/utility.ml b/lib/utility.ml index d16e044..ee5fbde 100644 --- a/lib/utility.ml +++ b/lib/utility.ml @@ -11,3 +11,15 @@ let rec powmod a d = function | n -> let b = (powmod a d (n / 2)) mod d in (((b * b) mod d) * (if n mod 2 = 0 then 1 else a)) mod d + + +let alphabet = "abcdefghijklmnopqrstuvwxyz" +let base = 26 + +let rec fromIntToString (x: int) : string = + if x < 0 then + "" + else if x < base then + String.get alphabet x |> String.make 1 + else + (fromIntToString (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1) diff --git a/lib/utility.mli b/lib/utility.mli index c5f2cfb..95ba827 100644 --- a/lib/utility.mli +++ b/lib/utility.mli @@ -1,3 +1,5 @@ val pow : int -> int -> int val powmod : int -> int -> int -> int + +val fromIntToString : int -> string