diff --git a/lib/backend/add_new.ml b/lib/backend/add_new.ml index 3a8f8ae..5dd6f7c 100644 --- a/lib/backend/add_new.ml +++ b/lib/backend/add_new.ml @@ -1,6 +1,5 @@ open Khagm -open Middleend -(* Gives the lambda lifted things names *) +(** Gives the lambda lifted things names *) let rec add_new top nms = match top with diff --git a/lib/backend/emit_c.ml b/lib/backend/emit_c.ml index add0a6e..4eb18df 100644 --- a/lib/backend/emit_c.ml +++ b/lib/backend/emit_c.ml @@ -1,6 +1,5 @@ open Khagm open Add_new -open Helpers open Exp open KhasmUTF @@ -16,7 +15,7 @@ let mangler id = "_" ^ string_of_int asint ^ "_" let mangle_top nms id = - let (Some nm) = Middleend.Kir.get_bind_id nms id in + let (Some nm) = Kir.get_bind_id nms id in let nm = snd nm in match nm with "main" -> "main_____Khasm" | _ -> utf8_map mangler nm @@ -46,7 +45,7 @@ let function_name name argnum = ^ ", " ^ string_of_int argnum ^ ", " ^ args ^ ") {\n" let is_toplevel id tbl = - match Middleend.Kir.get_bind_id tbl id with Some _ -> true | None -> false + match Kir.get_bind_id tbl id with Some _ -> true | None -> false let lookup x (tbl : (khagmid * string) list) = match List.assoc_opt x tbl with @@ -65,8 +64,8 @@ let adds_default () = [ "IFELSETEMP" ] let adds = ref [ "IFELSETEMP" ] let emit_ptr tbl name = - let (Some (_, nm')) = Middleend.Kir.get_bind_id tbl name in - match Middleend.Kir.get_constr tbl nm' with + let (Some (_, nm')) = Kir.get_bind_id tbl name in + match Kir.get_constr tbl nm' with | Some (_, arity, _) -> if arity = 0 then mangle_top tbl name ^ "()" diff --git a/lib/backend/khagm.ml b/lib/backend/khagm.ml index 11607f3..9673b1d 100644 --- a/lib/backend/khagm.ml +++ b/lib/backend/khagm.ml @@ -1,4 +1,4 @@ -open Helpers.Exp +open Exp type khagmid = int [@@deriving show { with_path = false }] @@ -28,5 +28,5 @@ type khagmtop = | Noop [@@deriving show { with_path = false }] -type khagm = khagmtop list * Middleend.Kir.kir_table +type khagm = khagmtop list * Kir.kir_table [@@deriving show { with_path = false }] diff --git a/lib/backend/native.ml b/lib/backend/native.ml index b854139..b26206f 100644 --- a/lib/backend/native.ml +++ b/lib/backend/native.ml @@ -1,4 +1,4 @@ -open Helpers.Exp +open Exp open Args let gen_main () = @@ -29,7 +29,7 @@ let prelude () = |} let flags = - Helpers.KhasmUTF.utf8_map + KhasmUTF.utf8_map (fun x -> if x = "\n" then "" diff --git a/lib/dune b/lib/dune index f31445b..5771e3b 100644 --- a/lib/dune +++ b/lib/dune @@ -1,4 +1,4 @@ -(include_subdirs qualified) +(include_subdirs unqualified) (ocamllex lexer) diff --git a/lib/front_to_middle/translateftm.ml b/lib/front_to_middle/translateftm.ml index 832cd23..a6e05ae 100644 --- a/lib/front_to_middle/translateftm.ml +++ b/lib/front_to_middle/translateftm.ml @@ -1,9 +1,7 @@ -open Helpers.Exp -open Frontend -open Middleend -open Helpers - +open Exp open Either + +open ListHelpers (** Converts between the frontend IR and the middleend IR. *) let rec fold_tup_flat f s l = @@ -123,12 +121,12 @@ and push_bind_into_expr tbl ident kirexpr kexpr = and split_on head body outputs = let open Ast in - let open ListHelpers in + let open List in let comp i (pat, expr) = match List.hd pat with | MPApp (q, _) -> if i = q then - True + ListHelpers.True else False | _ -> Both diff --git a/lib/frontend/ast.ml b/lib/frontend/ast.ml index bcc4e94..2bd5714 100644 --- a/lib/frontend/ast.ml +++ b/lib/frontend/ast.ml @@ -39,7 +39,7 @@ type info = { } [@@deriving show { with_path = false }] -let dummy_info () = { id = -1; complex = -2 } +let dummyinfo = { id = 0; complex = 0 } let idgen = ref 0 let getid () = diff --git a/lib/frontend/complexity.ml b/lib/frontend/complexity.ml index 77f1520..a5d25c4 100644 --- a/lib/frontend/complexity.ml +++ b/lib/frontend/complexity.ml @@ -1,5 +1,5 @@ open Ast -open Helpers.Exp +open Exp (* Computes a complexity for each node. Not currently used. *) diff --git a/lib/frontend/elim_modules.ml b/lib/frontend/elim_modules.ml index 0b934dd..06d65df 100644 --- a/lib/frontend/elim_modules.ml +++ b/lib/frontend/elim_modules.ml @@ -1,7 +1,7 @@ open Ast -open Helpers.Exp +open Exp -open Helpers.ListHelpers +open ListHelpers (** Elimintates modules from a list of programs, reducing them to a flat file structure with fully resolved names *) @@ -403,13 +403,13 @@ let%test "Elim modules all" = [ TopAssign ( ("d", TSBase "int"), - ("d", [], Base (mkinfo (), Int "1")) ); + ("d", [], Base (dummyinfo, Int "1")) ); ] ); ] ); ] ); TopAssign ( ("one", TSBase "int"), - ("one", [], ModAccess (mkinfo (), [ "a"; "b"; "c" ], "d")) ); + ("one", [], ModAccess (dummyinfo, [ "a"; "b"; "c" ], "d")) ); ] in match elim [ prog ] with @@ -419,16 +419,24 @@ let%test "Elim modules all" = [ TopAssign ( ("khasm.a.b.c.d", TSBase "int"), - ("khasm.a.b.c.d", [], Base ({ id = 1; complex = -1 }, Int "1")) + ("khasm.a.b.c.d", [], Base (dummyinfo, Int "1")) ); TopAssign ( ("khasm.one", TSBase "int"), ( "khasm.one", [], Base - ( { id = 0; complex = -1 }, - Ident ({ id = 0; complex = -1 }, "khasm.a.b.c.d") ) ) ); + (dummyinfo, + Ident (dummyinfo, "khasm.a.b.c.d") ) ) ); ] in - after = should - | _ -> false + if after = should then + true + else + begin + print_endline (show_program after); + print_endline (show_program should); + false + end + | _ -> + false diff --git a/lib/frontend/parser.ml b/lib/frontend/parser.ml index 5b9c8a6..ebe022e 100644 --- a/lib/frontend/parser.ml +++ b/lib/frontend/parser.ml @@ -88,12 +88,13 @@ type token = | RPAREN | EMPTY | ANY + | UNDERSCORE [@@deriving show { with_path = false }] exception ParseError open Ast -open Helpers.ListHelpers +open ListHelpers module Lexing = struct include Lexing @@ -122,7 +123,7 @@ let parse_error lines (offsets : Lexing.position) actual follow_set = print_endline @@ "Expected [" ^ delim ", " (List.map show_token follow_set) ^ "]" - with Invalid_argument _ -> + with Invalid_argument _ | Failure _ -> print_endline @@ "Error in file " ^ offsets.pos_fname ^ " line " ^ string_of_int offsets.pos_lnum; print_endline @@ "Got " ^ show_token actual; @@ -197,7 +198,7 @@ module ParserState = struct end open ParserState -open Helpers.Exp +open Exp let rec id_list state = match peek state 1 with @@ -415,6 +416,9 @@ and parse_match_list state = | T_IDENT t -> toss state; MPId t :: parse_match_list state + | UNDERSCORE -> + toss state; + MPWild :: parse_match_list state | LPAREN -> ( toss state; match peek state 1 with @@ -434,6 +438,7 @@ and parse_match_pattern state = MPApp (t, []) | T_IDENT t -> ( match parse_match_list state with [] -> MPId t | xs -> MPApp (t, xs)) + | UNDERSCORE -> MPWild | LPAREN -> ( match peek state 1 with | RPAREN -> @@ -726,9 +731,7 @@ and parse_module state = SimplModule (name, top) and parse_bind state = - expect state LPAREN; let op = get_binop state in - expect state RPAREN; (match pop state with EQ_OP "=" -> () | x -> error state x [ EQ_OP "=" ]); let name = get_ident state in Bind (op, [], name) diff --git a/lib/frontend/typecheck.ml b/lib/frontend/typecheck.ml index b84c038..d94bc04 100644 --- a/lib/frontend/typecheck.ml +++ b/lib/frontend/typecheck.ml @@ -1,22 +1,34 @@ -open Helpers.Exp +open Exp open Ast open Uniq_typevars open Hash open Debug -open Helpers - (** - This file serves as *the* typechecker for khasm programs. + This file serves as the typechecker for khasm programs. It handles everything related to ensuring a program is well typed. TODO: Split this into multiple files. + In a long story short, this is a: + - Bidirectional typechecking algorithm, based around: + - Unification, using subs contexts instead of refs (TODO) + - There's some special care needed to properly handle typechecking GADTs, + but it's mostly self-contained - ie, the GADT code doesn't + make anything else more complicated for any reason. + + At some point we need to think about how this can be properly split + into multiple files without encountering ocaml's lack of multi-file + mutual recursion as a major issue. + + The main problem I see is the plans in the future for linear types / a borrow checker, + as that'll majorly complicate the typechecker even more then it already is, + which is less then ideal seeing as it's almost 1,000 lines already :P + Notes about this code: - Foralls are order dependent due to typelam elaboration - GADT typechecking is like, 70% confidence, not right *) -(* See below for more details *) (** The global context for typechecking *) type ctx = { @@ -349,7 +361,7 @@ let rec unify_list ctx l1 l2 = if you're doing this in ocaml (or any language with ref cells) there's actually a really neat trick to optimize (and simplify 😄) metavars. - ``` + {[ type meta_state = | Solved of typ | Unsolved of name (* used for pretty printing *) @@ -357,24 +369,21 @@ let rec unify_list ctx l1 l2 = | Arrow of typ * typ | ... | Meta of meta_state ref - ``` + ]} so now the metavar is mutable, and when you solve it it gets "propagated up" automatically. actually implementing it introduces a couple of other subtleties but I think it's worth it. -*) -(** - MetaVar strategy: -``` +{[ given f x instantiate f with metavariables until reaching a non-forall type check that f's type matches 'a -> 'b unify x's type and 'a apply that unification to 'b return that type -``` -so, for example: -``` + + so, for example: + f : ∀'a, 'a -> 'a x : float @@ -390,48 +399,14 @@ f : float -> float (in this application) → return RHS(f) : float -``` - + ]} -*) - -(* - returns a tuple of env, typ - *) + returns a tuple of env, typ -(** Unifies two types, solving all needed metavars. *) + Unifies two types, solving all needed metavars. *) and unify ?loop ctx l r = - (* - unification takes something with metavariables, eg - $m1 -> $m1 - - and figures out what the metavariables should be: - - unify - $m1 -> $m1 - int -> int - ∴ - $m1 = int - - it does this by returning a tuple of (ctx, tm) - - where the ctx contains metavariable info. - on a map, it can then check that the metavar info is the same on - both sides, and go forth as such. - - - note that metavars can appear on both sides - - this is why there's a default case at the bottom to switch - the arguments around, using an optional param to make sure - that it doesn't loop forever (way easier then rewriting the - logic for both sides lol) - - *) let l = elim_unused @@ lift_ts l in let r = elim_unused @@ lift_ts r in - (*print_endline "unify:"; - print_endline (pshow_typesig l); - print_endline (pshow_typesig r);*) let res = match (l, r) with | TSBase x, TSBase y -> @@ -556,9 +531,8 @@ let rec infer_base ctx tm = in typ -(** Infers the type of a match expression. *) -and infer_match ctx main pats = - (** A few things happen here. +(** Infers the type of a match expression. + A few things happen here. - 1. We need to figure out the types of all the bound variables in `main`, and ensure there are no duplicates. - 2. We need to figure out the type of `main`, @@ -568,7 +542,8 @@ and infer_match ctx main pats = - 4. We need to make sure all of the `pats` have the same type * this should be a fairly trivial fold over unification. - *) +*) +and infer_match ctx main pats = let main_typ = infer ctx main in let throw_t _ctx _id typ = match typ with None -> raise @@ TypeErr "MPId no type" | Some x -> x @@ -604,12 +579,10 @@ and infer_match ctx main pats = t | MPTup t -> TSTuple (List.map (pat_to_type mctx) t) in - print_endline @@ "main_type: " ^ pshow_typesig main_typ; let typs = List.map (fun (p, e) -> let ty = pat_to_type ctx p in - print_endline @@ "got_type: " ^ pshow_typesig ty; let frees = frees_type p (Some main_typ) in let ctx' = List.fold_left (fun c (x, y) -> assume_typ c x y) ctx frees @@ -625,31 +598,34 @@ and infer_match ctx main pats = in typs -(** Infers the type of a term *) -and infer ctx tm = - (* - infer the type of a term - *) - let res = - match tm with - | Base (inf, x) -> (inf, infer_base ctx x) - | FCall (inf, f, x) -> ( - (** +(** Infers the type of a term + w.r.t function inference: + alright, so this mess. Basically what this does is infer instation of a function - ie, it takes + {[ f x and turns it into - f \[typeof x\] x - + f [typeof x] x + ]} but it's not always that simple + does this by inserting metavariables into all the foralls, then unifying the LHS of the function with the argument, then applying that to the RHS. this is basically just normal sysF with unification? kinda? - - *) + +*) +and infer ctx tm = + (* + infer the type of a term + *) + let res = + match tm with + | Base (inf, x) -> (inf, infer_base ctx x) + | FCall (inf, f, x) -> ( let typ_r = infer ctx f in let inst_r = inst_all typ_r in let typ_l = infer ctx x in @@ -792,7 +768,7 @@ let rec forall_to_typelam ts body = match ts with | TSForall (fv, bd) -> let tmp = forall_to_typelam bd body in - (fst tmp, TypeLam (dummy_info (), fv, snd tmp)) + (fst tmp, TypeLam (dummyinfo, fv, snd tmp)) | _ -> (lift_ts ts, body) (** See conv_args_body_to_typelams *) @@ -811,6 +787,7 @@ let rec add_args ts args body = (** The purpose of this is to transform arguments into typelams and annotlams so that you can do + {[ sig ∀a b, a -> (a -> b) -> b in let apply x f = f x @@ -823,7 +800,7 @@ let rec add_args ts args body = λx : A => λf : A -> B => f x - + ]} this is currently *really hacky* and also depends on the order of the typevars if there aren't enough arguments to the function, so uh @@ -903,11 +880,6 @@ let rec typecheck_toplevel_list ctx tl = | [ x ] -> TSMap (x, p) | x :: xs -> TSMap (x, go xs p) in - let rec wrap_foralls fs e = - match fs with - | [] -> e - | y :: ys -> TSForall (y, wrap_foralls ys e) - in let ctx' = List.fold_left (fun ctx pat -> @@ -939,8 +911,6 @@ let rec typecheck_toplevel_list ctx tl = ts args |> inst_all in - print_endline "NEWER, BETTER:"; - print_endline (pshow_typesig @@ ts'); assume_typ ctx pat.head ts') ctx pats in @@ -983,3 +953,19 @@ let rec typecheck_program_list_h pl ctx = (** Helper *) let typecheck_program_list pl = typecheck_program_list_h pl None + +let%test "Typechecking general" = + let tm = + Program( + [ + TopAssign(("test",TSBase("int")),("test",[], + Base(dummyinfo, Int("5")) + )) + ] + ) + in + try + typecheck_program_list [tm]; + true + with + | _ -> false diff --git a/lib/helpers/ListHelpers.ml b/lib/helpers/ListHelpers.ml index 5008b53..3f7f0ef 100644 --- a/lib/helpers/ListHelpers.ml +++ b/lib/helpers/ListHelpers.ml @@ -21,7 +21,7 @@ let filter_extract fn list = filter_extract_h fn list [] [] let rec last xs = match xs with - | [] -> raise @@ Impossible "ListHelpers.last : empty list" + | [] -> raise @@ Impossible "Listlast : empty list" | [ x ] -> x | _ :: xs -> last xs diff --git a/lib/helpers/khasmUTF.ml b/lib/helpers/khasmUTF.ml index be0f70c..b29be4d 100644 --- a/lib/helpers/khasmUTF.ml +++ b/lib/helpers/khasmUTF.ml @@ -1,6 +1,6 @@ open Exp -(** Helpers for unicode *) +(** for unicode *) exception Malformed_Unicode diff --git a/lib/lexer.mll b/lib/lexer.mll index c2bf79c..c16504a 100644 --- a/lib/lexer.mll +++ b/lib/lexer.mll @@ -1,7 +1,7 @@ { open Lexing - open Frontend.Parser + open Parser exception SyntaxError of string exception NotImpl of string exception EOF of string @@ -46,11 +46,11 @@ let digit = ['0'-'9'] let alpha = ['a'-'z' 'A'-'Z'] let INT = (digit)+ -let start = ['a'-'z' 'A'-'Z' '_'] +let start = ['a'-'z' 'A'-'Z'] let all = ['a'-'z' 'A'-'Z' '_' '\'' '0'-'9' ] -let IDENT = start all* +let IDENT = (start all*) | ('_' all+) let INTIDENT = '`' start all+ @@ -100,6 +100,7 @@ rule token = parse | "#" {incr_by lexbuf; HASH} | "," {incr_by lexbuf; COMMA} | ";" {incr_by lexbuf; SEMICOLON} + | "_" {incr_by lexbuf; UNDERSCORE} | "->" {incr_by lexbuf; TS_TO} | "=>" {incr_by lexbuf; LAM_TO} | bang_op {incr_by lexbuf; BANG_OP (Lexing.lexeme lexbuf)} diff --git a/lib/main.ml b/lib/main.ml index dbb8bd3..d2cfd12 100644 --- a/lib/main.ml +++ b/lib/main.ml @@ -1,11 +1,8 @@ open Batteries open Lexing open Lexer -open Frontend open Typecheck open Uniq_typevars -open Middleend -open Helpers open Exp open Ast open Hash diff --git a/lib/middle_to_back/translatemtb.ml b/lib/middle_to_back/translatemtb.ml index 6b643e3..9348d26 100644 --- a/lib/middle_to_back/translatemtb.ml +++ b/lib/middle_to_back/translatemtb.ml @@ -1,9 +1,5 @@ -open Helpers.Exp -open Middleend -open Backend - -(* Converts the middleend format to the backend format *) -open Helpers +open Exp +(** Converts the middleend format to the backend format *) let kirval_to_khagmid x = x let kv_to_kg = kirval_to_khagmid diff --git a/lib/middleend/kir.ml b/lib/middleend/kir.ml index 5e2efd3..1d5486c 100644 --- a/lib/middleend/kir.ml +++ b/lib/middleend/kir.ml @@ -1,6 +1,5 @@ -open Helpers.Exp +open Exp -open Frontend (** The middleend IR *) type kirtype = Ast.typesig [@@deriving show { with_path = false }] diff --git a/lib/middleend/lamlift.ml b/lib/middleend/lamlift.ml index 7a9e9aa..4d6b490 100644 --- a/lib/middleend/lamlift.ml +++ b/lib/middleend/lamlift.ml @@ -1,7 +1,7 @@ -open Helpers.Exp +open Exp + open Kir -open Frontend -(* Performs lambda lifting, putting all lambdas on the toplevel *) +(** Performs lambda lifting, putting all lambdas on the toplevel *) type lamctx = { frees : (kirval * kirtype) list } [@@deriving show { with_path = false }] diff --git a/lib/process.ml b/lib/process.ml index 7e44ad4..907a366 100644 --- a/lib/process.ml +++ b/lib/process.ml @@ -1,11 +1,6 @@ (** The main process of compilation *) open Args -open Frontend -open Front_to_middle -open Middleend -open Middle_to_back -open Backend let rec normalise files = match files with diff --git a/stdlib/stdlib.kha b/stdlib/stdlib.kha index 75023c8..09e4918 100644 --- a/stdlib/stdlib.kha +++ b/stdlib/stdlib.kha @@ -12,42 +12,40 @@ internal_extern 1 `print_int: int -> () = print_int internal_extern 1 `print_str : string -> () = print_str internal_extern 1 `print_float : float -> () = print_float - - internal_extern 2 `s_eq : ∀a, a -> a -> bool = s_eq -bind (=) = s_eq +bind = = s_eq -bind (+) = iadd -bind (-) = isub -bind (/) = idiv -bind ( * ) = imul +bind + = iadd +bind - = isub +bind / = idiv +bind * = imul -bind (+.) = fadd -bind (-.) = fsub -bind ( *. ) = fmul -bind (/.) = fdiv +bind +. = fadd +bind -. = fsub +bind *. = fmul +bind /. = fdiv let pipe x0 f1 : ∀a b, a -> (a -> b) -> b = f1 x0 -bind (|>) = pipe +bind |> = pipe let apply f2 x3 : ∀a b, (a -> b) -> a -> b = f2 x3 -bind ($) = apply +bind $ = apply let compose f4 g5 x6 : ∀a b c, (b -> c) -> (a -> b) -> a -> c = f4 (g5 x6) -bind (%) = compose +bind % = compose let rcompose f7 g8 x9 : ∀a b c, (a -> b) -> (b -> c) -> a -> c = g8 (f7 x9) -bind (%>) = rcompose +bind %> = rcompose diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..8ce37b0 --- /dev/null +++ b/test/dune @@ -0,0 +1,9 @@ +(include_subdirs unqualified) + +(library + (name khasmc_test) + (libraries khasmc fmt batteries ppx_deriving fileutils) + (inline_tests + (flags (-verbose))) + (preprocess + (pps ppx_deriving.show ppx_deriving.make ppx_deriving.eq ppx_inline_test))) diff --git a/test/frontend/test_parser.ml b/test/frontend/test_parser.ml new file mode 100644 index 0000000..f6393d0 --- /dev/null +++ b/test/frontend/test_parser.ml @@ -0,0 +1,30 @@ +let%test_unit "Parser" = + let open Khasmc.Parser in + let open Khasmc.Lexer in + let source = + {| + internal_extern 1 `whatever : forall a, a -> a = sub + bind / = foo + bind @++++++++ = gobbo + let foo a b c d : int = a b c d + let rec bar : int = bar + let a : int = 1 + 2 + let b : int = 1 +++++++ 5 + let c : int = 1 + 2 + 3 + 4 + 5 + 6 + let d : function = fun x : int => x + let e : int = tfun T => fun x : T => x + let f : tup = tuple.0 + let g : woop = + match k with + | 'Three => 1 + | Two a => g + | (a, b) => f + | (((((a),b),c),d),e) => f + | _ => k + end +|} + in + let lex = Lexing.from_string source in + Lexing.set_filename lex "test"; + let _res = program token lex "test" in + () diff --git a/test/frontend/test_typecheck.ml b/test/frontend/test_typecheck.ml new file mode 100644 index 0000000..d4537e2 --- /dev/null +++ b/test/frontend/test_typecheck.ml @@ -0,0 +1,363 @@ +let%test_unit "Typechecker" = + let open Khasmc.Typecheck in + let open Khasmc.Ast in + let tm = + [ + Program + [ + IntExtern + ( "`int_add", + "khasm.Stdlib.iadd", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`int_sub", + "khasm.Stdlib.isub", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`int_mul", + "khasm.Stdlib.imul", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`int_div", + "khasm.Stdlib.idiv", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`float_add", + "khasm.Stdlib.fadd", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`float_sub", + "khasm.Stdlib.fsub", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`float_div", + "khasm.Stdlib.fdiv", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`float_mul", + "khasm.Stdlib.fmul", + 2, + TSForall ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "a"))) + ); + IntExtern + ( "`print_int", + "khasm.Stdlib.print_int", + 1, + TSMap (TSBase "int", TSTuple []) ); + IntExtern + ( "`print_str", + "khasm.Stdlib.print_str", + 1, + TSMap (TSBase "string", TSTuple []) ); + IntExtern + ( "`print_float", + "khasm.Stdlib.print_float", + 1, + TSMap (TSBase "float", TSTuple []) ); + IntExtern + ( "`s_eq", + "khasm.Stdlib.s_eq", + 2, + TSForall + ("a", TSMap (TSBase "a", TSMap (TSBase "a", TSBase "bool"))) ); + Bind ("khasm.Stdlib.=", [], "khasm.Stdlib.s_eq"); + Bind ("khasm.Stdlib.+", [], "khasm.Stdlib.iadd"); + Bind ("khasm.Stdlib.-", [], "khasm.Stdlib.isub"); + Bind ("khasm.Stdlib./", [], "khasm.Stdlib.idiv"); + Bind ("khasm.Stdlib.*", [], "khasm.Stdlib.imul"); + Bind ("khasm.Stdlib.+.", [], "khasm.Stdlib.fadd"); + Bind ("khasm.Stdlib.-.", [], "khasm.Stdlib.fsub"); + Bind ("khasm.Stdlib.*.", [], "khasm.Stdlib.fmul"); + Bind ("khasm.Stdlib./.", [], "khasm.Stdlib.fdiv"); + TopAssign + ( ( "khasm.Stdlib.pipe", + TSForall + ( "a", + TSForall + ( "b", + TSMap + ( TSBase "a", + TSMap (TSMap (TSBase "a", TSBase "b"), TSBase "b") + ) ) ) ), + ( "khasm.Stdlib.pipe", + [ "x0"; "f1" ], + FCall + ( { id = 67; complex = 5 }, + Base + ( { id = 64; complex = 2 }, + Ident ({ id = 63; complex = 1 }, "f1") ), + Base + ( { id = 66; complex = 2 }, + Ident ({ id = 65; complex = 1 }, "x0") ) ) ) ); + Bind ("khasm.Stdlib.|>", [], "khasm.Stdlib.pipe"); + TopAssign + ( ( "khasm.Stdlib.apply", + TSForall + ( "a", + TSForall + ( "b", + TSMap + ( TSMap (TSBase "a", TSBase "b"), + TSMap (TSBase "a", TSBase "b") ) ) ) ), + ( "khasm.Stdlib.apply", + [ "f2"; "x3" ], + FCall + ( { id = 72; complex = 5 }, + Base + ( { id = 69; complex = 2 }, + Ident ({ id = 68; complex = 1 }, "f2") ), + Base + ( { id = 71; complex = 2 }, + Ident ({ id = 70; complex = 1 }, "x3") ) ) ) ); + Bind ("khasm.Stdlib.$", [], "khasm.Stdlib.apply"); + TopAssign + ( ( "khasm.Stdlib.compose", + TSForall + ( "a", + TSForall + ( "b", + TSForall + ( "c", + TSMap + ( TSMap (TSBase "b", TSBase "c"), + TSMap + ( TSMap (TSBase "a", TSBase "b"), + TSMap (TSBase "a", TSBase "c") ) ) ) ) ) ), + ( "khasm.Stdlib.compose", + [ "f4"; "g5"; "x6" ], + FCall + ( { id = 80; complex = 8 }, + Base + ( { id = 74; complex = 2 }, + Ident ({ id = 73; complex = 1 }, "f4") ), + FCall + ( { id = 79; complex = 5 }, + Base + ( { id = 76; complex = 2 }, + Ident ({ id = 75; complex = 1 }, "g5") ), + Base + ( { id = 78; complex = 2 }, + Ident ({ id = 77; complex = 1 }, "x6") ) ) ) ) ); + Bind ("khasm.Stdlib.%", [], "khasm.Stdlib.compose"); + TopAssign + ( ( "khasm.Stdlib.rcompose", + TSForall + ( "a", + TSForall + ( "b", + TSForall + ( "c", + TSMap + ( TSMap (TSBase "a", TSBase "b"), + TSMap + ( TSMap (TSBase "b", TSBase "c"), + TSMap (TSBase "a", TSBase "c") ) ) ) ) ) ), + ( "khasm.Stdlib.rcompose", + [ "f7"; "g8"; "x9" ], + FCall + ( { id = 88; complex = 8 }, + Base + ( { id = 82; complex = 2 }, + Ident ({ id = 81; complex = 1 }, "g8") ), + FCall + ( { id = 87; complex = 5 }, + Base + ( { id = 84; complex = 2 }, + Ident ({ id = 83; complex = 1 }, "f7") ), + Base + ( { id = 86; complex = 2 }, + Ident ({ id = 85; complex = 1 }, "x9") ) ) ) ) ); + Bind ("khasm.Stdlib.%>", [], "khasm.Stdlib.rcompose"); + ]; + Program + [ + Typedecl + ( "khasm.Match.List", + [ "a" ], + [ + { + head = "khasm.Match.Nil"; + args = []; + typ = Ok (TSApp ([ TSBase "a" ], "khasm.Match.List")); + }; + { + head = "khasm.Match.Cons"; + args = + [ TSBase "a"; TSApp ([ TSBase "a" ], "khasm.Match.List") ]; + typ = Ok (TSApp ([ TSBase "a" ], "khasm.Match.List")); + }; + ] ); + TopAssignRec + ( ( "khasm.Match.map", + TSForall + ( "q", + TSForall + ( "w", + TSMap + ( TSMap (TSBase "q", TSBase "w"), + TSMap + ( TSApp ([ TSBase "q" ], "khasm.Match.List"), + TSApp ([ TSBase "w" ], "khasm.Match.List") ) ) + ) ) ), + ( "khasm.Match.map", + [ "f"; "x" ], + Match + ( { id = 21; complex = -1 }, + Base + ( { id = 1; complex = -1 }, + Ident ({ id = 0; complex = -1 }, "x") ), + [ + ( MPApp ("khasm.Match.Nil", []), + Base + ( { id = 3; complex = -1 }, + Ident ({ id = 2; complex = -1 }, "khasm.Match.Nil") + ) ); + ( MPApp ("khasm.Match.Cons", [ MPId "q"; MPId "w" ]), + FCall + ( { id = 20; complex = -1 }, + FCall + ( { id = 11; complex = -1 }, + Base + ( { id = 5; complex = -1 }, + Ident + ( { id = 4; complex = -1 }, + "khasm.Match.Cons" ) ), + FCall + ( { id = 10; complex = -1 }, + Base + ( { id = 7; complex = -1 }, + Ident ({ id = 6; complex = -1 }, "f") ), + Base + ( { id = 9; complex = -1 }, + Ident ({ id = 8; complex = -1 }, "q") ) + ) ), + FCall + ( { id = 19; complex = -1 }, + FCall + ( { id = 16; complex = -1 }, + Base + ( { id = 13; complex = -1 }, + Ident + ( { id = 12; complex = -1 }, + "khasm.Match.map" ) ), + Base + ( { id = 15; complex = -1 }, + Ident ({ id = 14; complex = -1 }, "f") + ) ), + Base + ( { id = 18; complex = -1 }, + Ident ({ id = 17; complex = -1 }, "w") ) ) + ) ); + ] ) ) ); + TopAssignRec + ( ( "khasm.Match.make", + TSMap + (TSBase "int", TSApp ([ TSBase "int" ], "khasm.Match.List")) + ), + ( "khasm.Match.make", + [ "i" ], + IfElse + ( { id = 47; complex = 28 }, + FCall + ( { id = 28; complex = 8 }, + FCall + ( { id = 27; complex = 5 }, + Base + ( { id = 26; complex = 2 }, + Ident + ({ id = 25; complex = 1 }, "khasm.Stdlib.=") + ), + Base + ( { id = 23; complex = 2 }, + Ident ({ id = 22; complex = 1 }, "i") ) ), + Base ({ id = 24; complex = 2 }, Int "0") ), + Base + ( { id = 30; complex = 2 }, + Ident ({ id = 29; complex = 1 }, "khasm.Match.Nil") ), + FCall + ( { id = 46; complex = 17 }, + FCall + ( { id = 35; complex = 5 }, + Base + ( { id = 32; complex = 2 }, + Ident + ({ id = 31; complex = 1 }, "khasm.Match.Cons") + ), + Base + ( { id = 34; complex = 2 }, + Ident ({ id = 33; complex = 1 }, "i") ) ), + FCall + ( { id = 45; complex = 11 }, + Base + ( { id = 37; complex = 2 }, + Ident + ({ id = 36; complex = 1 }, "khasm.Match.make") + ), + FCall + ( { id = 44; complex = 8 }, + FCall + ( { id = 43; complex = 5 }, + Base + ( { id = 42; complex = 2 }, + Ident + ( { id = 41; complex = 1 }, + "khasm.Stdlib.-" ) ), + Base + ( { id = 39; complex = 2 }, + Ident ({ id = 38; complex = 1 }, "i") ) + ), + Base ({ id = 40; complex = 2 }, Int "1") ) ) ) + ) ) ); + TopAssign + ( ("main", TSMap (TSTuple [], TSTuple [])), + ( "main", + [ "q" ], + LetIn + ( { id = 62; complex = 17 }, + "l", + FCall + ( { id = 51; complex = 5 }, + Base + ( { id = 49; complex = 2 }, + Ident ({ id = 48; complex = 1 }, "khasm.Match.make") + ), + Base ({ id = 50; complex = 2 }, Int "1000") ), + LetIn + ( { id = 61; complex = 11 }, + "p", + FCall + ( { id = 59; complex = 8 }, + FCall + ( { id = 56; complex = 5 }, + Base + ( { id = 53; complex = 2 }, + Ident + ( { id = 52; complex = 1 }, + "khasm.Match.map" ) ), + Base + ( { id = 55; complex = 2 }, + Ident + ( { id = 54; complex = 1 }, + "khasm.Stdlib.print_int" ) ) ), + Base + ( { id = 58; complex = 2 }, + Ident ({ id = 57; complex = 1 }, "l") ) ), + Base ({ id = 60; complex = 2 }, Tuple []) ) ) ) ); + ]; + ] + in + typecheck_program_list tm diff --git a/test/parser.kha b/test/parser.kha deleted file mode 100644 index 2e4f958..0000000 --- a/test/parser.kha +++ /dev/null @@ -1,19 +0,0 @@ -(* This file is meant to test as much of the parser as possible. It's not meant to typecheck or anything. *) - - -module test = struct - let goofy : string = "hi" -end - -open test - -bind (+) = goofy - - -internal_extern 2 `wacky : int -> int = foo - -let rec foo x : int -> int = x - -let l1 : int = - let x : int -> int = fun x : int => x in - x 5 \ No newline at end of file