trait resolution and bugfixing

lib/common/error.ml

@@ -40,13 +40,3 @@ let option_app (f : 'a -> ('b, 'c) result) (x : 'a option) :
   | None -> ok None
   | Some n -> (
       match f n with Ok s -> ok @@ Some s | Error e -> Error e)
-
-type error_location = Frontend'
-[@@deriving show { with_path = false }]
-
-let compiler_error loc str =
-  print_string
-    ("Compiler error in " ^ show_error_location loc ^ " :\n");
-  print_string str;
-  print_string "\n\n Aborting compilation.\n";
-  exit 1

lib/common/fresh.ml

@@ -0,0 +1,5 @@
+let fresh =
+  let i = ref (-1) in
+  fun () ->
+    incr i;
+    !i

lib/common/info.ml

@@ -1,10 +1,13 @@
 type info = ..
 type data = ..
+type info += Dummy
+type data += Dummy'
 
 (* unique ids *)
 type id = Id of int [@@deriving show { with_path = false }]
 
 let noid = Id (-1)
+let id' () = Id (Fresh.fresh ())
 
 let p_INFO_TABLE : (id, (info * data) list) Hashtbl.t =
   Hashtbl.create 100
@@ -22,3 +25,13 @@ let set_property (id : id) (prop : info) (data : data) : unit =
   | Some l ->
       (* update *)
       Hashtbl.replace p_INFO_TABLE id ((prop, data) :: l)
+
+let print_related_entries i printer =
+  Hashtbl.iter
+    (fun id v ->
+      List.iter
+        (fun (info, data) ->
+          if info = i then
+            printer id data)
+        v)
+    p_INFO_TABLE

lib/common/log.ml

@@ -0,0 +1,62 @@
+type level =
+  | TRACE
+  | DEBUG
+  | INFO
+  | WARN
+  | ERROR
+  | FATAL
+
+let lvl_to_ident (lvl : level) =
+  match lvl with
+  | TRACE -> "\x1B[0;32mTrace:"
+  | DEBUG -> "\x1B[0;36mDebug:"
+  | INFO -> "\x1B[0;34mInfo:"
+  | WARN -> "\x1B[0;33mWarn:"
+  | ERROR -> "\x1B[0;31mError:"
+  | FATAL -> "\x1B[1;31m!!! FATAL !!!"
+
+let reset = "\x1B[0m"
+
+type message = Msg of level * string
+
+let log_ : message list ref = ref []
+let init_log () = ()
+let append_ msg = log_ := msg :: !log_
+let get_ () = List.rev !log_
+
+let msg_to_str (Msg (lvl, msg)) =
+  let intro = lvl_to_ident lvl in
+  intro ^ "\n" ^ reset ^ msg ^ "\n\n"
+
+let print_log () =
+  let l = get_ () in
+  match l with
+  | [] -> print_endline "\n\x1B[1;35mlog was empty :)\x1B[0m\n"
+  | _ ->
+      print_string "\n\x1B[1;35m~~~   LOG   ~~~ \x1B[0m\n\n";
+      List.iter (fun x -> print_string (msg_to_str x)) l;
+      print_string "\x1B[1;35m~~~ END LOG ~~~ \x1B[0m\n"
+
+let log level str rest =
+  let m = Msg (level, Printf.sprintf str rest) in
+  append_ m;
+  match level with
+  | FATAL -> raise (Invalid_argument "fatal")
+  | _ -> ()
+
+let log_fatal level str rest =
+  let m = Msg (level, Printf.sprintf str rest) in
+  append_ m;
+  match level with
+  | FATAL ->
+      print_log ();
+      print_endline "Khasmc terminated from fatal error!";
+      exit 1
+  | _ -> raise (Invalid_argument "non-fatal")
+
+let trace x = log TRACE "%s" x
+let debug x = log DEBUG "%s" x
+let info x = log INFO "%s" x
+let warn x = log WARN "%s" x
+let error x = log ERROR "%s" x
+let fatal x = log_fatal FATAL "%s" x

lib/front/ast.ml

@@ -87,7 +87,7 @@ and pp_ty (fmt : Format.formatter) (ty : ty) : unit =
   | Free s -> Format.fprintf fmt "'%s" s
   | Custom t -> Format.fprintf fmt "%a" pp_path t
   | Tuple t -> Format.fprintf fmt "(%a)" (pp_list fmt) t
-  | Arrow (a, b) -> Format.fprintf fmt "%a -> %a" pp_ty a pp_ty b
+  | Arrow (a, b) -> Format.fprintf fmt "(%a) -> %a" pp_ty a pp_ty b
   | TApp (p, l) ->
       Format.fprintf fmt "%a (%a)" pp_path p (pp_list fmt) l
   | TForall (s, t) ->
@@ -102,6 +102,11 @@ and pp_list fmt fmt x =
       Format.fprintf fmt ", ")
     x
 
+let print_ty ty =
+  pp_ty Format.std_formatter ty;
+  Format.print_newline ();
+  Format.print_flush ()
+
 (* also carries free vars *)
 type ty' = freevar list * ty [@@deriving show { with_path = false }]
 
@@ -150,8 +155,6 @@ type tm =
   | Record of id * path * (string * tm) list
   (* foo.bar *)
   | Project of id * tm * string
-  (* error *)
-  | Poison of id * exn
 [@@deriving show { with_path = false }]
 
 type definition_no_body = {
@@ -160,6 +163,7 @@ type definition_no_body = {
   constraints : constraint' list;
   args : (string * ty) list;
   ret : ty;
+  id : Common.Info.id;
 }
 [@@deriving show { with_path = false }]
 
@@ -170,18 +174,19 @@ type definition = {
   args : (string * ty) list;
   ret : ty;
   body : tm;
+  id : Common.Info.id;
 }
 [@@deriving show { with_path = false }]
 
 let to_definition_no_body (d : definition) : definition_no_body =
   match d with
-  | { name; free_vars; constraints; args; ret; body = _body } ->
-      { name; free_vars; constraints; args; ret }
+  | { name; free_vars; constraints; id; args; ret; body = _body } ->
+      { name; free_vars; constraints; id; args; ret }
 
 let to_definition (b : tm) (d : definition_no_body) : definition =
   match d with
-  | { name; free_vars; constraints; args; ret } ->
-      { body = b; name; free_vars; constraints; args; ret }
+  | { name; free_vars; constraints; id; args; ret } ->
+      { body = b; name; free_vars; id; constraints; args; ret }
 
 type trait = {
   name : string;
@@ -192,31 +197,34 @@ type trait = {
   constraints : constraint' list;
   (* member functions *)
   functions : definition_no_body list;
+  id : Common.Info.id;
 }
 [@@deriving show { with_path = false }]
 
 type impl = {
   name : string;
-  args : ty list;
+  args : (string * ty) list;
   assoc_types : (string * ty) list;
   impls : definition list;
+  id : Common.Info.id;
 }
 [@@deriving show { with_path = false }]
 
 type typ = {
   name : string;
   args : freevar list;
   expr : tyexpr;
+  id : Common.Info.id;
 }
 [@@deriving show { with_path = false }]
 
 type statement =
   (* name, freevars, constraints, args, return type, term *)
-  | Definition of id * definition
+  | Definition of definition
   (* name, args, body *)
-  | Type of id * typ
-  | Trait of id * trait
-  | Impl of id * impl
+  | Type of typ
+  | Trait of trait
+  | Impl of impl
 [@@deriving show { with_path = false }]
 
 type file = {
@@ -259,6 +267,5 @@ let get_tm_id (t : tm) : id =
   | ITE (i, _, _, _)
   | Annot (i, _, _)
   | Record (i, _, _)
-  | Project (i, _, _)
-  | Poison (i, _) ->
+  | Project (i, _, _) ->
       i

lib/front/convert_idents_to_strings.ml

@@ -56,7 +56,6 @@ let rec collapse_tm (tm : tm) : tm =
           collapse pth,
           List.map (fun (a, b) -> (a, collapse_tm b)) flds )
   | Project (i, p, s) -> Project (i, collapse_tm p, s)
-  | Poison (_, _) -> tm
 
 let rec collapse_tyexpr (tyexpr : tyexpr) : tyexpr =
   match (tyexpr : tyexpr) with
@@ -69,64 +68,74 @@ let rec collapse_tyexpr (tyexpr : tyexpr) : tyexpr =
 
 let convert' (s : statement) : statement =
   match (s : statement) with
-  | Definition (id, { name; free_vars; constraints; args; ret; body })
+  | Definition { id; name; free_vars; constraints; args; ret; body }
     ->
       Definition
-        ( id,
-          {
-            name;
-            free_vars;
-            constraints = collapse_cons constraints;
-            args = List.map (fun (a, b) -> (a, collapse_ty b)) args;
-            ret = collapse_ty ret;
-            body = collapse_tm body;
-          } )
-  | Type (id, { name; args; expr }) ->
-      Type (id, { name; args; expr = collapse_tyexpr expr })
-  | Trait (i, { name; args; assoc_types; constraints; functions }) ->
+        {
+          id;
+          name;
+          free_vars;
+          constraints = collapse_cons constraints;
+          args = List.map (fun (a, b) -> (a, collapse_ty b)) args;
+          ret = collapse_ty ret;
+          body = collapse_tm body;
+        }
+  | Type { id; name; args; expr } ->
+      Type { id; name; args; expr = collapse_tyexpr expr }
+  | Trait { id; name; args; assoc_types; constraints; functions } ->
       Trait
-        ( i,
-          {
-            name;
-            args;
-            assoc_types;
-            constraints = collapse_cons constraints;
-            functions =
-              List.map
-                (fun ({ name; free_vars; constraints; args; ret } :
-                       definition_no_body) ->
-                  {
-                    name;
-                    free_vars;
-                    constraints = collapse_cons constraints;
-                    args =
-                      List.map (fun (a, b) -> (a, collapse_ty b)) args;
-                    ret = collapse_ty ret;
-                  })
-                functions;
-          } )
-  | Impl (i, { name; args; assoc_types; impls }) ->
+        {
+          id;
+          name;
+          args;
+          assoc_types;
+          constraints = collapse_cons constraints;
+          functions =
+            List.map
+              (fun ({ name; id; free_vars; constraints; args; ret } :
+                     definition_no_body) ->
+                {
+                  id;
+                  name;
+                  free_vars;
+                  constraints = collapse_cons constraints;
+                  args =
+                    List.map (fun (a, b) -> (a, collapse_ty b)) args;
+                  ret = collapse_ty ret;
+                })
+              functions;
+        }
+  | Impl { id; name; args; assoc_types; impls } ->
       Impl
-        ( i,
-          {
-            name;
-            args = List.map collapse_ty args;
-            assoc_types =
-              List.map (fun (a, b) -> (a, collapse_ty b)) assoc_types;
-            impls =
-              List.map
-                (fun { name; free_vars; constraints; args; ret; body } ->
-                  {
-                    name;
-                    free_vars;
-                    constraints = collapse_cons constraints;
-                    args =
-                      List.map (fun (a, b) -> (a, collapse_ty b)) args;
-                    ret = collapse_ty ret;
-                    body = collapse_tm body;
-                  })
-                impls;
-          } )
+        {
+          id;
+          name;
+          args = List.map (fun (a, b) -> (a, collapse_ty b)) args;
+          assoc_types =
+            List.map (fun (a, b) -> (a, collapse_ty b)) assoc_types;
+          impls =
+            List.map
+              (fun {
+                     id;
+                     name;
+                     free_vars;
+                     constraints;
+                     args;
+                     ret;
+                     body;
+                   } ->
+                {
+                  id;
+                  name;
+                  free_vars;
+                  constraints = collapse_cons constraints;
+                  args =
+                    List.map (fun (a, b) -> (a, collapse_ty b)) args;
+                  ret = collapse_ty ret;
+                  body = collapse_tm body;
+                })
+              impls;
+        }
 
 let convert (s : statement list) : statement list =
   List.map convert' s

lib/front/driver.ml

@@ -10,4 +10,5 @@ let do_frontend (files : file list) : (statement list, 'a) result =
     Convert_idents_to_strings.convert statements
   in
   let+ tycheckd = Tycheck.typecheck compressed_paths in
+  Instance_resolve.test ();
   []