Runtime improvements and changes to type syntax

examples/higher_order.kha

@@ -1,8 +1,11 @@
 let example f x
-    : ∀a b, (a -> b) -> a -> b=
+    : ∀a b, (a -> b) -> a -> b =
     f x
 
-let main x : () -> () =
+let main x : () -> ()  =
     let temp = example Stdlib.print_int in
     temp 10;
     temp 5
+
+
+let test : ()  = ()

lib/backend/native.ml

@@ -9,7 +9,7 @@ int main(void) {
   if (ret->tag != TUPLE) {
   fprintf(stderr, "RETURN VALUE NOT TUPLE - TYPE SYSTEM INVALID\n");
   }  
-  unref(ret);  
+  unref(ret);
   return 0;  
 }
 |}
@@ -20,20 +20,24 @@ let prelude () =
 #include <stdarg.h>
 #include <stdint.h>
 #include <stdlib.h>
+#include <stdbool.h>
+#include <unistd.h>
+#include <pthread.h>
+#include <time.h>
+#include <stdatomic.h>
+#include <assert.h>
 |}
 
 let flags =
   KhasmUTF.utf8_map
     (fun x -> if x = "\n" then "" else x)
-    {| -O3
+    {| -O0
         -Wall
         -Wextra
         -Wno-incompatible-pointer-types
         -Wno-sign-compare
-    -L`jemalloc-config --libdir`
-        -Wl,-rpath,`jemalloc-config --libdir`
-        -ljemalloc
-        `jemalloc-config --libs`  |}
+        -g 
+        |}
 
 let compile code (args : Args.cliargs) =
   let code = prelude () ^ Runtime_lib.runtime_c ^ code ^ gen_main () in

lib/dune

@@ -13,9 +13,9 @@
  (preprocess
   (pps ppx_deriving.show ppx_deriving.make ppx_deriving.eq ppx_inline_test))
  (flags
-  (:standard -warn-error -A -g -annot))
+  (:standard -warn-error -A))
  (ocamlopt_flags
-  (:standard -g -annot -afl-instrument)))
+  (:standard -O3)))
 
 (rule
  (targets runtime_lib.ml)

lib/frontend/ast.ml

@@ -4,7 +4,7 @@ type typeprim = Basic of string | Bound of string | Param of int * string
 type typesig =
   | TSBase of string
   | TSMeta of string
-  | TSApp of typesig * string
+  | TSApp of typesig list * string
   | TSMap of typesig * typesig
   | TSForall of string * typesig
   | TSTuple of typesig list
@@ -20,7 +20,8 @@ let rec pshow_typesig ts =
   match ts with
   | TSBase x -> x
   | TSMeta x -> x
-  | TSApp (x, y) -> brac (pshow_typesig x) ^ " " ^ y
+  | TSApp (x, y) ->
+      brac (y ^ " " ^ String.concat " " @@ List.map pshow_typesig x)
   | TSMap (x, y) -> brac (pshow_typesig x) ^ " -> " ^ brac (pshow_typesig y)
   | TSForall (x, y) -> "∀" ^ x ^ ", " ^ pshow_typesig y
   | TSTuple x -> brac (by_sep (List.map pshow_typesig x) ", ")

lib/frontend/parser.ml

@@ -201,6 +201,9 @@ let rec id_list state =
 let nonempty l exp state =
   match l with [] -> error state EMPTY [ exp ] | _ -> l
 
+let rec repeat_until f x =
+  match f x with None -> [] | Some t -> t :: repeat_until f x
+
 exception ParseExprHelper of kexpr
 
 let rec nop () = ()
@@ -275,42 +278,40 @@ and parse_type_tuple state =
   | RPAREN -> lhs :: []
   | x -> error state x [ COMMA; RPAREN ]
 
-and parse_type_mulop state =
-  let lhs = parse_type state in
-  match pop state with
-  | MUL_OP "*" -> lhs :: parse_type_tuple state
-  | RPAREN -> lhs :: []
-  | x -> error state x [ MUL_OP "*"; RPAREN ]
+and parse_type_compound state =
+  match parse_type_tuple state with
+  | [] -> impossible "empty type"
+  | [ x ] -> x
+  | x -> TSTuple x
 
-and parse_type_tuple_2 state =
-  let lhs = parse_type state in
-  match pop state with
-  | COMMA -> lhs :: parse_type_tuple state
-  | MUL_OP "*" -> lhs :: parse_type_mulop state
-  | RPAREN -> lhs :: []
-  | x -> error state x [ COMMA; RPAREN; MUL_OP "*" ]
+and parse_single state =
+  match peek state 1 with
+  | T_IDENT t ->
+      toss state;
+      Some (TSBase t)
+  | LPAREN ->
+      toss state;
+      Some (parse_type_compound state)
+  | _ -> None
 
 and parse_type_helper state =
-  let first =
-    match peek state 1 with
-    | T_IDENT s ->
-        toss state;
-        TSBase s
-    | LPAREN -> (
-        toss state;
-        let lhs = parse_type state in
-        match pop state with
-        | RPAREN -> lhs
-        | COMMA | MUL_OP "*" -> TSTuple (lhs :: parse_type_tuple_2 state)
-        | x -> error state x [ RPAREN; COMMA; MUL_OP "*" ])
-    | RPAREN -> TSTuple []
-    | x -> error state x [ T_IDENT "example1"; LPAREN ]
-  in
   match peek state 1 with
-  | T_IDENT s ->
+  | T_IDENT t -> (
       toss state;
-      TSApp (first, s)
-  | _ -> first
+      let list = repeat_until parse_single state in
+      match list with [] -> TSBase t | x -> TSApp (x, t))
+  | LPAREN -> (
+      toss state;
+      match peek state 1 with
+      | RPAREN ->
+          toss state;
+          TSTuple []
+      | _ -> (
+          match parse_type_tuple state with
+          | [] -> impossible "empty type"
+          | [ x ] -> x
+          | x -> TSTuple x))
+  | x -> error state x [ T_IDENT "example"; LPAREN ]
 
 and parse_type_pratt state =
   let lhs = parse_type_helper state in

lib/frontend/typecheck.ml

@@ -44,7 +44,7 @@ let rec occurs_ts s ts =
     match ts with
     | TSBase x -> x = s
     | TSMeta _ -> false
-    | TSApp (x, _) -> occurs_ts s x
+    | TSApp (x, _) -> List.mem true (List.map (occurs_ts s) x)
     | TSMap (x, y) -> occurs_ts s x || occurs_ts s y
     | TSForall (x, y) -> if x = s then false else occurs_ts s y
     | TSTuple x -> List.map (fun x -> occurs_ts s x) x |> List.mem true
@@ -76,19 +76,10 @@ let rec validate_typ types ty =
       | false -> raise @@ TypeErr ("Cannot find type " ^ x))
   | TSMeta _ -> ty
   | TSApp (x, y) ->
-      (let n = typeprim_len types y in
-       match x with
-       | TSTuple l ->
-           if List.length l = n then ()
-           else
-             raise
-             @@ TypeErr ("Wrong amount of args to type-level function " ^ y)
-       | _ ->
-           if n = 1 then ()
-           else
-             raise
-             @@ TypeErr ("Wrong amount of args to type-level function " ^ y));
-      TSApp (validate_typ types x, y)
+      let n = typeprim_len types y in
+      if n <> List.length x then
+        raise @@ TypeErr ("Wrong number of args to type level function " ^ y)
+      else TSApp (List.map (validate_typ types) x, y)
   | TSMap (x, y) -> TSMap (validate_typ types x, validate_typ types y)
   | TSForall (x, y) -> TSForall (x, validate_typ (Bound x :: types) y)
   | TSTuple l -> TSTuple (List.map (validate_typ types) l)
@@ -100,8 +91,8 @@ let rec lift_ts_h t =
   | TSBase _ -> (t, false)
   | TSMeta _ -> (t, false)
   | TSApp (x, y) ->
-      let did = lift_ts_h x in
-      (TSApp (fst did, y), snd did)
+      let did = List.map lift_ts_h x in
+      (TSApp (List.map fst did, y), List.mem true (List.map snd did))
   | TSMap (x, TSForall (f, y)) ->
       if occurs_ts f x then
         let left = lift_ts_h x in
@@ -139,7 +130,7 @@ let rec subs typ nm newt =
   match typ with
   | TSBase x -> if x == nm then newt else typ
   | TSMeta _ -> typ
-  | TSApp (x, y) -> TSApp (subs x nm newt, y)
+  | TSApp (x, y) -> TSApp (List.map (fun y -> subs y nm newt) x, y)
   | TSMap (l, r) -> TSMap (subs l nm newt, subs r nm newt)
   | TSForall (nm', ts) ->
       if nm' == nm then typ else TSForall (nm', subs ts nm newt)
@@ -162,7 +153,7 @@ let rec inst_meta tp orig meta =
   match tp with
   | TSBase x -> if x = orig then meta else tp
   | TSMeta _ -> tp
-  | TSApp (ts, p) -> TSApp (inst_meta ts orig meta, p)
+  | TSApp (ts, p) -> TSApp (List.map (fun y -> inst_meta y orig meta) ts, p)
   | TSMap (a, b) -> TSMap (inst_meta a orig meta, inst_meta b orig meta)
   | TSForall (f, x) ->
       if f = orig then tp else TSForall (f, inst_meta x orig meta)
@@ -187,7 +178,7 @@ let rec elim_unused ts =
     match ts with
     | TSBase _ -> ts
     | TSMeta _ -> ts
-    | TSApp (a, b) -> TSApp (elim_unused a, b)
+    | TSApp (a, b) -> TSApp (List.map elim_unused a, b)
     | TSMap (a, b) -> TSMap (elim_unused a, elim_unused b)
     | TSForall (a, b) ->
         if occurs_ts a b then TSForall (a, elim_unused b) else elim_unused b
@@ -329,8 +320,14 @@ and unify ?loop ctx l r =
     | TSApp (a, b), TSApp (x, y) ->
         if b <> y then raise (UnifyErr ("can't unify" ^ b ^ " and " ^ y))
         else
-          let t = unify ctx a x in
-          (fst t, TSApp (snd t, b))
+          let t = List.map2 (unify ctx) a x in
+          let rec get_ctx list =
+            match list with
+            | [] -> empty_unify_ctx ()
+            | [ (c, _) ] -> c
+            | (c1, _) :: xs -> combine c1 (get_ctx xs)
+          in
+          (get_ctx t, TSApp (List.map snd t, b))
     | TSForall (a, b), TSForall (x, y) ->
         (*
          TODO: show how this works
@@ -371,7 +368,7 @@ let rec apply_unify ctx tp =
   match tp with
   | TSBase _ -> tp
   | TSMeta t -> ( match lookup_meta ctx t with Some x -> x | None -> tp)
-  | TSApp (f, x) -> TSApp (apply_unify ctx f, x)
+  | TSApp (f, x) -> TSApp (List.map (apply_unify ctx) f, x)
   | TSMap (a, b) -> TSMap (apply_unify ctx a, apply_unify ctx b)
   | TSForall (f, x) -> TSForall (f, apply_unify ctx x)
   | TSTuple t -> TSTuple (List.map (apply_unify ctx) t)
@@ -571,10 +568,17 @@ let rec typecheck_toplevel_list ctx tl =
       let ctx' =
         match x with
         | TopAssign ((id, ts), (_id, _args, body)) ->
+            if id = "main" then
+              ignore
+              @@ unify (empty_unify_ctx ()) ts (TSMap (TSTuple [], TSTuple []));
+
             let fixed = body in
             check ctx fixed ts;
             assume_typ ctx id ts
         | TopAssignRec ((id, ts), (_id, _args, body)) ->
+            if id = "main" then
+              ignore
+              @@ unify (empty_unify_ctx ()) ts (TSMap (TSTuple [], TSTuple []));
             let fixed = body in
             (*
               to check a recursive,            

lib/frontend/uniq_typevars.ml

@@ -54,7 +54,7 @@ and make_uniq_ts ts env =
       let newenv = add_binds s env in
       TSForall (get_binds newenv, make_uniq_ts t (Some newenv))
   | TSTuple x -> TSTuple (List.map (fun x -> make_uniq_ts x (Some env)) x)
-  | TSApp (x, y) -> TSApp (make_uniq_ts x (Some env), y)
+  | TSApp (x, y) -> TSApp (List.map (fun x -> make_uniq_ts x (Some env)) x, y)
   | TSMeta m -> TSMeta m
 
 let rec make_uniq_toplevel t =

lib/main.ml

@@ -44,7 +44,10 @@ let parse_args () =
     nocompile = !nocomp;
   }
 
+let round2 n = Float.round (n *. 100.) /. 100.
+
 let main_proc () =
+  let t = Unix.gettimeofday () in
   Printexc.record_backtrace true;
   Random.self_init ();
   let args = parse_args () in
@@ -61,11 +64,15 @@ let main_proc () =
   in
   Debug.debug ("\nStatus: " ^ succ);
   print_endline
-    ("/* Used " ^ string_of_int !uniq ^ " typvars, " ^ string_of_int !muniq
+    ("Used " ^ string_of_int !uniq ^ " typvars, " ^ string_of_int !muniq
    ^ " metavars, "
     ^ string_of_int (getid () - 1)
     ^ " stage 1 nodes, "
     ^ string_of_int (Kir.get_random_num () - 1)
-    ^ " stage 2 nodes. */");
+    ^ " stage 2 nodes.");
+  print_endline
+    ("Took: "
+    ^ string_of_float (round2 @@ (Unix.gettimeofday () -. t))
+    ^ " seconds.");
   if args.table then Hash.print_table () else ();
   if args.debug || succ <> "Success" then Debug.log_debug_stdout true else ()

lib/runtime/builtins.c

@@ -124,6 +124,15 @@ KHASM_ENTRY(khasm_46_Stdlib_46_print_95_int, 1, kha_obj *b) {
   return make_tuple(0, NULL);
 }
 
+KHASM_ENTRY(khasm_46_Stdlib_46_print_95_str, 1, kha_obj *b) {
+  if (b->tag != STR) {
+    fprintf(stderr, "INVALID PRINT STR\n");
+  }
+  printf("%s\n", b->data.str->data);
+  unref(b);
+  return make_tuple(0, NULL);
+}
+
 KHASM_ENTRY(khasm_46__45__1, 2, kha_obj*t, kha_obj*b) {
   if (t->tag != TUPLE) {
     fprintf(stderr, "CAN'T TUPACC NONTUP\n");