From 9991efafbfc16e6761b3fb9330fbec24cd4b1b63 Mon Sep 17 00:00:00 2001 From: elvis Date: Fri, 31 Jan 2025 03:15:58 +0100 Subject: [PATCH] Adding simple Algorithm W implementation (no recursive functions) --- bin/dune | 52 +++-- bin/miniFunPolyInterpreter.ml | 104 ++++++++++ bin/testing.minifun | 5 + lib/miniFun/TypeChecker.ml | 313 ++++++++++++++++++++++++----- lib/miniFun/TypeChecker.mli | 2 + lib/miniFun/Types.ml | 77 ++++++- lib/miniFun/Types.mli | 130 ++++++------ lib/miniFun/dune | 2 +- lib/miniImp/dune | 2 +- test/dune | 4 + test/testingPolyFunParser.expected | 11 + test/testingPolyFunParser.ml | 138 +++++++++++++ 12 files changed, 697 insertions(+), 143 deletions(-) create mode 100644 bin/miniFunPolyInterpreter.ml create mode 100644 bin/testing.minifun create mode 100644 test/testingPolyFunParser.expected create mode 100644 test/testingPolyFunParser.ml diff --git a/bin/dune b/bin/dune index e630ca1..514bc64 100644 --- a/bin/dune +++ b/bin/dune @@ -1,26 +1,36 @@ (executable - (name miniFunInterpreter) - (public_name miniFunInterpreter) - (libraries miniFun - clap) - (package miniFun) - (modes byte exe) - ) + (name miniFunInterpreter) + (public_name miniFunInterpreter) + (libraries miniFun + clap) + (package miniFun) + (modes byte exe) +) (executable - (name miniImpInterpreter) - (public_name miniImpInterpreter) - (libraries miniImp - clap) - (package miniImp) - (modes byte exe) - ) + (name miniFunPolyInterpreter) + (public_name miniFunPolyInterpreter) + (libraries miniFun + clap) + (package miniFun) + (modes byte exe) +) + (executable - (name miniImpInterpreterReg) - (public_name miniImpInterpreterReg) - (libraries miniImp - clap) - (package miniImp) - (modes byte exe) - ) + (name miniImpInterpreter) + (public_name miniImpInterpreter) + (libraries miniImp + clap) + (package miniImp) + (modes byte exe) +) + +(executable + (name miniImpInterpreterReg) + (public_name miniImpInterpreterReg) + (libraries miniImp + clap) + (package miniImp) + (modes byte exe) +) diff --git a/bin/miniFunPolyInterpreter.ml b/bin/miniFunPolyInterpreter.ml new file mode 100644 index 0000000..df42297 --- /dev/null +++ b/bin/miniFunPolyInterpreter.ml @@ -0,0 +1,104 @@ +open MiniFun +open Lexing + +(* -------------------------------------------------------------------------- *) +(* Command Arguments *) + +let () = + Clap.description "Interpreter for MiniFun language."; + + let files = Clap.section ~description: "Files to consider." "FILES" in + let values = Clap.section ~description: "Input values." "VALUES" in + + let input = Clap.mandatory_string + ~description: "Input file." + ~placeholder: "FILENAME" + ~section: files + ~long: "input" + ~short: 'i' + () + in + + let inputval = Clap.optional_int + ~description: "Optional input value to feed to the program. \ + If not specified it is read from stdin." + ~placeholder: "INT" + ~section: values + ~long: "value" + ~short: 'v' + () + in + + let output = Clap.optional_string + ~description: "Output file. If not specified output is printed on stdout." + ~placeholder: "FILENAME" + ~section: files + ~long: "output" + ~long_synonyms: ["out"; "result"] + ~short: 'o' + () + in + + Clap.close (); + +(* -------------------------------------------------------------------------- *) +(* Interpreter *) + + let print_position outx lexbuf = + let pos = lexbuf.lex_curr_p in + Printf.fprintf outx "Encountered \"%s\" at %s:%d:%d" + (Lexing.lexeme lexbuf) pos.pos_fname + pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1) + in + + let interpret_file inch (inval: int) outch = + let lexbuf = Lexing.from_channel inch in + let program = + try Parser.prg Lexer.read lexbuf with + | Lexer.LexingError msg -> + Printf.fprintf stderr "%a: %s\n" print_position lexbuf msg; + exit (-1) + | Parser.Error -> + Printf.fprintf stderr "%a: syntax error\n" print_position lexbuf; + exit (-1) + in + let ty_program = + match TypeChecker.typecheck_polymorphic program with + | Ok ty -> ty + | Error (`AbsentAssignment msg) + | Error (`WrongTypeSpecification msg) + | Error (`WrongType msg) -> + Printf.fprintf stderr "%s\n" msg; + exit (-1) + in + let return_value = + match Semantics.reduce program inval with + Ok o -> o + | Error (`AbsentAssignment msg) + | Error (`DivisionByZero msg) + | Error (`WrongType msg) -> + Printf.fprintf stderr "%s\n" msg; + exit (-1) + in + + Printf.fprintf outch "Type of the program: %s\n" (Types.pp_type_f ty_program); + Printf.fprintf outch "%d\n" return_value + in + + + let inx = In_channel.open_text input in + let outx = match output with + None -> stdout + | Some f -> Out_channel.open_text f + in + + let inputval = match inputval with + None -> ( + Printf.fprintf stdout "Provide the input: "; + read_int () + ) + | Some o -> o + in + interpret_file inx inputval outx; + + Out_channel.close outx diff --git a/bin/testing.minifun b/bin/testing.minifun new file mode 100644 index 0000000..93973b2 --- /dev/null +++ b/bin/testing.minifun @@ -0,0 +1,5 @@ +\n: int => +let fn = + \x: int => x + n +in +fn n diff --git a/lib/miniFun/TypeChecker.ml b/lib/miniFun/TypeChecker.ml index 7220519..aec5bf7 100644 --- a/lib/miniFun/TypeChecker.ml +++ b/lib/miniFun/TypeChecker.ml @@ -5,54 +5,256 @@ Random.self_init () let (let*) = Result.bind -let evaluate_type_polimorphic (_program: t_exp) (_context: typingshape) - : (typingshape, error) result = - failwith "Not implemented" - (* 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.from_int_to_string !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" *) +(* -------------------------------------------------------------------------- *) +(* polimporphic type checking *) +(* -------------------------------------------------------------------------- *) + +let global_type_id = ref 0 + +let new_global_id () = + let id = !global_type_id in + incr global_type_id; + id + + +let rec unify type_a type_b = + if type_a == type_b then Ok () else + match (type_a, type_b) with + | IntegerTypeP, IntegerTypeP + | BooleanTypeP, BooleanTypeP -> + Ok () + + | TupleTypeP (a1, a2), TupleTypeP (b1, b2) + | ApplicationP (a1, a2), ApplicationP (b1, b2) + | FunctionTypeP (a1, a2), FunctionTypeP (b1, b2) -> + let* _ = unify a1 b1 in + unify a2 b2 + + | VariableTypeP ({contents = Link a1}), + VariableTypeP ({contents = Link b1}) -> + unify a1 b1 + + | VariableTypeP ({contents = Link ty_link}), ty_rest + | ty_rest, VariableTypeP ({contents = Link ty_link}) + when ty_link = ty_rest -> + Ok () + + | VariableTypeP ({contents = Unbound (a1, _)}), + VariableTypeP ({contents = Unbound (b1, _)}) + when a1 = b1 -> + Error (`WrongType "Only a single instance of a type should be available.") + + | type_ab, VariableTypeP ({contents = Unbound (_id, _level)} as tvar) + | VariableTypeP ({contents = Unbound (_id, _level)} as tvar), type_ab -> + tvar := Link type_ab; + Ok () + + | _, _ -> + Error (`WrongType "Cannot unify types.") + +let rec unifyable type_a type_b = + if type_a == type_b then Ok () else + match (type_a, type_b) with + | IntegerTypeP, IntegerTypeP + | BooleanTypeP, BooleanTypeP -> + Ok () + + | TupleTypeP (a1, a2), TupleTypeP (b1, b2) + | ApplicationP (a1, a2), ApplicationP (b1, b2) + | FunctionTypeP (a1, a2), FunctionTypeP (b1, b2) -> + let* _ = unifyable a1 b1 in + unifyable a2 b2 + + | VariableTypeP ({contents = Link a1}), + VariableTypeP ({contents = Link b1}) -> + unifyable a1 b1 + + | VariableTypeP ({contents = Link ty_link}), ty_rest + | ty_rest, VariableTypeP ({contents = Link ty_link}) + when ty_link = ty_rest -> + Ok () + + | VariableTypeP ({contents = Unbound (a1, _)}), + VariableTypeP ({contents = Unbound (b1, _)}) + when a1 = b1 -> + Error (`WrongType "Only a single instance of a type should be available.") + + | _type_ab, VariableTypeP ({contents = Unbound (_id, _level)}) + | VariableTypeP ({contents = Unbound (_id, _level)}), _type_ab -> + Ok () + + | _, _ -> + Error (`WrongType "Cannot unify types.") + +let rec generalize level ty = + match ty with + | VariableTypeP {contents = Unbound (id, o_level)} when o_level > level -> + VariableTypeP (ref (Generic id)) + | ApplicationP (ty, ty_arg) -> + ApplicationP (generalize level ty, generalize level ty_arg) + | FunctionTypeP (ty_arg, ty) -> + FunctionTypeP (generalize level ty_arg, generalize level ty) + | TupleTypeP (ty1, ty2) -> + TupleTypeP (generalize level ty1, generalize level ty2) + | VariableTypeP {contents = Link ty} -> + generalize level ty + | VariableTypeP {contents = Generic _} + | VariableTypeP {contents = Unbound _} + | IntegerTypeP + | BooleanTypeP -> + ty + + +let instantiate level ty = + let var_map = ref IntegerMap.empty in + let rec aux ty = + match ty with + | IntegerTypeP + | BooleanTypeP -> + ty + | TupleTypeP (ty1, ty2) -> + TupleTypeP (aux ty1, aux ty2) + | VariableTypeP {contents = Link ty} -> + aux ty + | VariableTypeP {contents = Generic id} -> ( + match IntegerMap.find_opt id !var_map with + | Some ty -> ty + | None -> + let var = VariableTypeP (ref (Unbound (new_global_id (), level))) in + var_map := IntegerMap.add id var !var_map; + var + ) + | VariableTypeP {contents = Unbound _} -> + ty + | ApplicationP (ty, ty_arg) -> + ApplicationP (aux ty, aux ty_arg) + | FunctionTypeP (ty_arg, ty) -> + FunctionTypeP (aux ty_arg, aux ty) + in + aux ty + + +let rec evaluate_type_polimorphic program (env: env) level = + match program with + | Integer _ -> Ok (IntegerTypeP) + | Boolean _ -> Ok (BooleanTypeP) + | Tuple (a, b) -> + let* type_a = evaluate_type_polimorphic a env level in + let* type_b = evaluate_type_polimorphic b env level in + Ok (TupleTypeP (type_a, type_b)) + | Variable (x) -> ( + match VariableMap.find_opt x env with + | Some (ty) -> + Ok (instantiate level ty) + | None -> + Error (`AbsentAssignment ("Variable " ^ x ^ " is not assigned.")) + ) + | Function (x, _typef, fbody) -> + let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in + let fn_env = VariableMap.add x param_type env in + let* body_type = evaluate_type_polimorphic fbody fn_env level in + Ok (FunctionTypeP (param_type, body_type)) + | Application (f, xs) -> + let* type_f = evaluate_type_polimorphic f env level in + let rec aux = + function + | FunctionTypeP (type_f_arg, type_f) -> + Ok (type_f_arg, type_f) + | VariableTypeP {contents = Link ty} -> + aux ty + | VariableTypeP ({contents = Unbound(_id, level)} as tvar) -> + let param_ty = VariableTypeP (ref (Unbound (new_global_id (), level))) + in + let f_ty = VariableTypeP (ref (Unbound (new_global_id (), level))) in + tvar := Link ( FunctionTypeP (param_ty, f_ty) ); + Ok (param_ty, f_ty) + | _ -> Error (`WrongType "Expecting a function to apply.") + in + let* param_ty, f_ty = aux type_f in + let* type_xs = evaluate_type_polimorphic xs env level in + let* _ = unify param_ty type_xs in + Ok f_ty + | Plus (a, b) + | Minus (a, b) + | Times (a, b) + | Division (a, b) + | Modulo (a, b) + | Power (a, b) -> + let* type_a = evaluate_type_polimorphic a env level in + let* type_b = evaluate_type_polimorphic b env level in + let* _ = unify type_a IntegerTypeP in + let* _ = unify type_b IntegerTypeP in + Ok (IntegerTypeP) + | First a -> ( + let* type_a = evaluate_type_polimorphic a env level in + let* _ = unify type_a + (TupleTypeP(VariableTypeP (ref (Unbound (new_global_id (), level))), + VariableTypeP (ref (Unbound (new_global_id (), level))))) + in + match type_a with + | TupleTypeP (ty_a, _) + | VariableTypeP {contents = Link TupleTypeP (ty_a, _)} -> Ok ty_a + | _ -> Error (`WrongType "Applying First to non tuple type.") + ) + | Second a -> ( + let* type_a = evaluate_type_polimorphic a env level in + let* _ = unify type_a + (TupleTypeP(VariableTypeP (ref (Unbound (new_global_id (), level))), + VariableTypeP (ref (Unbound (new_global_id (), level))))) + in + match type_a with + | TupleTypeP (_, ty_a) + | VariableTypeP {contents = Link TupleTypeP (_, ty_a)} -> Ok ty_a + | _ -> Error (`WrongType "Applying Second to non tuple type.") + ) + | PowerMod (x, y, z) -> + let* type_x = evaluate_type_polimorphic x env level in + let* type_y = evaluate_type_polimorphic y env level in + let* type_z = evaluate_type_polimorphic z env level in + let* _ = unify type_x IntegerTypeP in + let* _ = unify type_y IntegerTypeP in + let* _ = unify type_z IntegerTypeP in + Ok (IntegerTypeP) + | Rand (x) -> + let* type_x = evaluate_type_polimorphic x env level in + let* _ = unify type_x IntegerTypeP in + Ok (IntegerTypeP) + | BAnd (a, b) + | BOr (a, b) -> + let* type_a = evaluate_type_polimorphic a env level in + let* type_b = evaluate_type_polimorphic b env level in + let* _ = unify type_a BooleanTypeP in + let* _ = unify type_b BooleanTypeP in + Ok (BooleanTypeP) + | BNot (x) -> + let* type_x = evaluate_type_polimorphic x env level in + let* _ = unify type_x BooleanTypeP in + Ok (BooleanTypeP) + | Cmp (a, b) + | CmpLess (a, b) + | CmpLessEq (a, b) + | CmpGreater (a, b) + | CmpGreaterEq (a, b) -> + let* type_a = evaluate_type_polimorphic a env level in + let* type_b = evaluate_type_polimorphic b env level in + let* _ = unify type_a IntegerTypeP in + let* _ = unify type_b IntegerTypeP in + Ok (BooleanTypeP) + | IfThenElse (guard, if_exp, else_exp) -> + let* type_guard = evaluate_type_polimorphic guard env level in + let* type_if_exp = evaluate_type_polimorphic if_exp env level in + let* type_else_exp = evaluate_type_polimorphic else_exp env level in + let* _ = unify type_guard BooleanTypeP in + let* _ = unify type_if_exp type_else_exp in + Ok (type_if_exp) + | LetIn (x, xval, rest) -> + let* var_ty = evaluate_type_polimorphic xval env (level + 1) in + let generalized_ty = generalize level var_ty in + evaluate_type_polimorphic rest (VariableMap.add x generalized_ty env) level + | LetFun (_f, _xs, _typef, _fbody, _rest) -> failwith "Not Implemented" + +(* -------------------------------------------------------------------------- *) + let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, [> typechecking_error]) result = @@ -201,10 +403,19 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : | _ -> Error (`WrongTypeSpecification "Specification of function is not a function type.") + let typecheck (program: t_exp) : (ftype, [> typechecking_error]) result = let* typeprogram = evaluate_type program VariableMap.empty in match typeprogram with - FunctionType (IntegerType, IntegerType) -> ( - Ok (typeprogram) - ) + FunctionType (IntegerType, IntegerType) -> Ok (typeprogram) | _ -> Error (`WrongType "Program is not a function from int to int.") + + +let typecheck_polymorphic (program: t_exp) + : (type_f, [> typechecking_error]) result = + global_type_id := 0; + let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in + let* _ = unifyable type_program (FunctionTypeP (IntegerTypeP, IntegerTypeP)) + in + let generalized_ty = generalize (-1) type_program in + Ok (generalized_ty) diff --git a/lib/miniFun/TypeChecker.mli b/lib/miniFun/TypeChecker.mli index bb296d2..3158bc9 100644 --- a/lib/miniFun/TypeChecker.mli +++ b/lib/miniFun/TypeChecker.mli @@ -1 +1,3 @@ val typecheck : Types.t_exp -> (Types.ftype, [> Types.typechecking_error]) result + +val typecheck_polymorphic : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result diff --git a/lib/miniFun/Types.ml b/lib/miniFun/Types.ml index 734326b..883ea2e 100644 --- a/lib/miniFun/Types.ml +++ b/lib/miniFun/Types.ml @@ -5,18 +5,79 @@ let globalIdentifier = ref 1 module VariableMap = Map.Make(String) module VariableSet = Set.Make(String) -type ftype = +(* -------------------------------------------------------------------------- *) +(* polimporphic type checking types *) +(* -------------------------------------------------------------------------- *) + +type id = int +type level = int + +type type_f = + IntegerTypeP + | BooleanTypeP + | TupleTypeP of type_f * type_f + | VariableTypeP of variable_type ref + | FunctionTypeP of type_f * type_f + | ApplicationP of type_f * type_f +and variable_type = + Unbound of id * level + | Link of type_f + | Generic of id + +type env = type_f VariableMap.t +module IntegerMap = Map.Make(Int) + +let pp_type_f (ty: type_f) : string = + let id_name_map = ref IntegerMap.empty in + let count = ref 0 in + let next_name () = + let i = !count in + incr count; + Utility.from_int_to_string i + in + let rec aux is_simple ty = + match ty with + | IntegerTypeP -> "Int" + | BooleanTypeP -> "Bool" + | TupleTypeP (ty1, ty2) -> + "(" ^ aux is_simple ty1 ^ ", " ^ aux is_simple ty2 ^ ")" + | ApplicationP (ty, ty_arg) -> + aux true ty ^ "(" ^ aux false ty_arg ^ ")" + | FunctionTypeP (ty_arg, ty) -> + let ty_arg_str = aux true ty_arg in + let ty_str = aux false ty in + let str = ty_arg_str ^ " -> " ^ ty_str in + if is_simple then "(" ^ str ^ ")" else str + | VariableTypeP {contents = Generic id} -> ( + match IntegerMap.find_opt id !id_name_map with + | Some a -> a + | None -> + let name = next_name () in + id_name_map := IntegerMap.add id name !id_name_map; + name + ) + | VariableTypeP {contents = Unbound (id, _)} -> + "_" ^ string_of_int id + | VariableTypeP {contents = Link ty} -> + aux is_simple ty + in + let ty_str = aux false ty in + if !count > 0 then + let var_names = + IntegerMap.fold (fun _ value acc -> value :: acc) !id_name_map [] + in + "∀ " ^ (String.concat " " (List.sort String.compare var_names)) + ^ ", " ^ ty_str + else + ty_str + +(* -------------------------------------------------------------------------- *) + +type ftype = (* type used for specification *) IntegerType | BooleanType | TupleType of ftype * ftype - | PolimorphicType of string | FunctionType of ftype * 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 *) diff --git a/lib/miniFun/Types.mli b/lib/miniFun/Types.mli index 8045d3a..c3af3a6 100644 --- a/lib/miniFun/Types.mli +++ b/lib/miniFun/Types.mli @@ -5,73 +5,81 @@ val globalIdentifier : int ref module VariableMap : Map.S with type key = variable module VariableSet : Set.S with type elt = string -type ftype = +(* -------------------------------------------------------------------------- *) +(* polimporphic type checking types *) +(* -------------------------------------------------------------------------- *) + +type id = int +type level = int + +type type_f = + IntegerTypeP + | BooleanTypeP + | TupleTypeP of type_f * type_f + | VariableTypeP of variable_type ref + | FunctionTypeP of type_f * type_f + | ApplicationP of type_f * type_f +and variable_type = + Unbound of id * level + | Link of type_f + | Generic of id + +type env = type_f VariableMap.t +module IntegerMap : Map.S with type key = int + +val pp_type_f : type_f -> string + +(* module VariableTypeMap : Map.S with type key = variable_type *) + +(* type substitution = (\* from variable types to politypes *\) *) +(* politype VariableTypeMap.t *) + +(* type prefix = *) +(* | Lambda *) +(* | Let *) +(* | LetRec *) + +(* type typed_prefix = *) +(* (\* list of free variables in the context and the associated type *\) *) +(* (prefix * politype) VariableMap.t *) + +(* -------------------------------------------------------------------------- *) + +type ftype = (* type used for specification *) IntegerType | BooleanType | TupleType of ftype * ftype - | PolimorphicType of variable | FunctionType of ftype * 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 *) - | Boolean of bool (* v *) - | Variable of variable (* x *) - | Tuple of t_exp * t_exp (* (a, b) *) - | Function of variable * ftype * t_exp (* lambda x: t. x *) - | Application of t_exp * t_exp (* x x *) - | Plus of t_exp * t_exp (* x + x *) - | Minus of t_exp * t_exp (* x - x *) - | Times of t_exp * t_exp (* x * x *) - | Division of t_exp * t_exp (* x / x *) - | Modulo of t_exp * t_exp (* x % x *) - | Power of t_exp * t_exp (* x ^ x *) - | PowerMod of t_exp * t_exp * t_exp (* (x ^ x) % x *) - | Rand of t_exp (* rand(0, x) *) - | BAnd of t_exp * t_exp (* x && x *) - | BOr of t_exp * t_exp (* x || x *) - | BNot of t_exp (* not x *) - | First of t_exp (* fst x *) - | Second of t_exp (* scn x *) - | Cmp of t_exp * t_exp (* x == x *) - | CmpLess of t_exp * t_exp (* x < x *) - | CmpLessEq of t_exp * t_exp (* x <= x *) - | CmpGreater of t_exp * t_exp (* x > x *) - | 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 * ftype * t_exp * t_exp (* let rec x. y: t. x in x*) + Integer of int (* x := a *) + | Boolean of bool (* v *) + | Variable of variable (* x *) + | Tuple of t_exp * t_exp (* (a, b) *) + | Function of variable * ftype * t_exp (* lambda x: t. x *) + | Application of t_exp * t_exp (* x x *) + | Plus of t_exp * t_exp (* x + x *) + | Minus of t_exp * t_exp (* x - x *) + | Times of t_exp * t_exp (* x * x *) + | Division of t_exp * t_exp (* x / x *) + | Modulo of t_exp * t_exp (* x % x *) + | Power of t_exp * t_exp (* x ^ x *) + | PowerMod of t_exp * t_exp * t_exp (* (x ^ x) % x *) + | Rand of t_exp (* rand(0, x) *) + | BAnd of t_exp * t_exp (* x && x *) + | BOr of t_exp * t_exp (* x || x *) + | BNot of t_exp (* not x *) + | First of t_exp (* fst x *) + | Second of t_exp (* scn x *) + | Cmp of t_exp * t_exp (* x == x *) + | CmpLess of t_exp * t_exp (* x < x *) + | CmpLessEq of t_exp * t_exp (* x <= x *) + | CmpGreater of t_exp * t_exp (* x > x *) + | 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 * ftype * t_exp * t_exp + (* let rec x. y: t. x in x*) type permitted_values = IntegerPermitted of int diff --git a/lib/miniFun/dune b/lib/miniFun/dune index 3547f71..e9113a6 100644 --- a/lib/miniFun/dune +++ b/lib/miniFun/dune @@ -5,7 +5,7 @@ (explain true) (infer true) (flags --dump --table) - ) +) (library (name miniFun) diff --git a/lib/miniImp/dune b/lib/miniImp/dune index f3e43a6..6de9617 100644 --- a/lib/miniImp/dune +++ b/lib/miniImp/dune @@ -5,7 +5,7 @@ (explain true) (infer true) (flags --dump --table) - ) +) (library (name miniImp) diff --git a/test/dune b/test/dune index 1b83215..ebc89aa 100644 --- a/test/dune +++ b/test/dune @@ -25,3 +25,7 @@ (test (name testingTypeFunParser) (libraries miniFun)) + +(test + (name testingPolyFunParser) + (libraries miniFun)) diff --git a/test/testingPolyFunParser.expected b/test/testingPolyFunParser.expected new file mode 100644 index 0000000..2595a97 --- /dev/null +++ b/test/testingPolyFunParser.expected @@ -0,0 +1,11 @@ +Error absent assignment program: error (success) +Error wrong input type program: error (success) +Error not a function program: error (success) +Error if branches with different types program: error (success) +Error if guard is not a boolean program: error (success) +Identity program: success +Constant program: success +Partial application of function program: success +Passing functions to functions program: success +Scope program: success +Rand program: success diff --git a/test/testingPolyFunParser.ml b/test/testingPolyFunParser.ml new file mode 100644 index 0000000..d671220 --- /dev/null +++ b/test/testingPolyFunParser.ml @@ -0,0 +1,138 @@ +open MiniFun + +let get_result x = + Lexing.from_string x + |> Parser.prg Lexer.lex + |> TypeChecker.typecheck_polymorphic + +(* -------------------------------------------------------------------------- *) +(* Error absent assignment program *) + +let program = + "lambda a: int -> int => x" +;; + +Printf.printf "Error absent assignment program: "; +match get_result program with + Error (`AbsentAssignment _) -> Printf.printf "error (success)\n" +| _ -> Printf.printf "failed\n" + +(* -------------------------------------------------------------------------- *) +(* Error wrong input type program *) + +let program = + "(lambda a: int -> int => a) false" +;; + +Printf.printf "Error wrong input type program: "; +match get_result program with + Error (`WrongType _) -> Printf.printf "error (success)\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Error not a function program *) + +let program = + "0 false" +;; + +Printf.printf "Error not a function program: "; +match get_result program with + Error (`WrongType _) -> Printf.printf "error (success)\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Error if branches with different types program *) + +let program = + "lambda x: int -> int => if 1 == 2 then true else 1" +;; + +Printf.printf "Error if branches with different types program: "; +match get_result program with + Error (`WrongType _) -> Printf.printf "error (success)\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Error if guard is not a boolean program *) + +let program = + "lambda x: int -> int => (if 1 then 2 else 1)" +;; + +Printf.printf "Error if guard is not a boolean program: "; +match get_result program with + Error (`WrongType _) -> Printf.printf "error (success)\n" +| _ -> Printf.printf " failed\n" + + +(* -------------------------------------------------------------------------- *) +(* Identity program *) +let program = + "lambda a: int -> int => a" +;; + +Printf.printf "Identity program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Constant program *) +let program = + "lambda a: int -> int => 1" +;; + +Printf.printf "Constant program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Partial application of function program *) +let program = + "let f = lambda x: int -> int -> int => lambda y: int -> int => x + y in f 3" +;; + +Printf.printf "Partial application of function program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Passing functions to functions program *) +let program = + "let f = + \\z: (int -> int) -> (int -> int) -> int -> int => + \\y: (int -> int) -> int -> int => + \\x: int -> int => + if x < 0 then y x else z x + in (f (\\x: int -> int => x + 1)) (\\x: int -> int => x - 1)" +;; + +Printf.printf "Passing functions to functions program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Scope program *) +let program = + "let f = let a = 1 in fun y: int -> int => y + a in let a = 2 in f" +;; + +Printf.printf "Scope program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n" + +(* -------------------------------------------------------------------------- *) +(* Rand program *) +let program = + "fun x: int -> int => rand x" +;; + +Printf.printf "Rand program: "; +match get_result program with + Ok _ -> Printf.printf "success\n" +| _ -> Printf.printf " failed\n"