From 97f84ccace4e634b4e02178a702818e69292dc9f Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 8 Jul 2024 22:01:42 +0200
Subject: implement top-level definitions

---
 src/ast/Ast.ml               |  9 +++++++
 src/bin/dune                 |  8 +++---
 src/bin/main.ml              | 42 +++++++++++++++++++++--------
 src/driver/Driver.ml         | 12 +++++++++
 src/driver/dune              | 12 +++++++++
 src/driver/test.toytt        |  1 +
 src/elaborator/Elaborator.ml | 64 +++++++++++++++++++++++++++++---------------
 src/elaborator/dune          |  3 ++-
 src/error/Error.ml           | 16 +++++++----
 src/nbe/Conversion.ml        | 63 ++++++++++++++++++++++++++++++++-----------
 src/nbe/Data.ml              | 16 ++++++-----
 src/nbe/Domain.ml            | 12 +++++++--
 src/nbe/Eval.ml              | 27 ++++++++++++++++---
 src/nbe/NbE.ml               |  3 +++
 src/nbe/Quote.ml             |  8 ++++--
 src/nbe/Syntax.ml            |  1 +
 src/parser/Grammar.mly       | 11 +++++++-
 src/parser/Lexer.mll         | 11 +++++++-
 src/parser/Parser.ml         | 23 ++++++++++++----
 src/pretty/Pretty.ml         |  1 +
 src/pretty/dune              |  4 +--
 src/toplevel/TopLevel.ml     |  6 +++++
 src/toplevel/dune            |  7 +++++
 23 files changed, 279 insertions(+), 81 deletions(-)
 create mode 100644 src/driver/Driver.ml
 create mode 100644 src/driver/dune
 create mode 100644 src/driver/test.toytt
 create mode 100644 src/toplevel/TopLevel.ml
 create mode 100644 src/toplevel/dune

(limited to 'src')

diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml
index 3a6fac6..974409f 100644
--- a/src/ast/Ast.ml
+++ b/src/ast/Ast.ml
@@ -29,6 +29,15 @@ and raw_expr =
 
 and expr = raw_expr Asai.Range.located
 
+type item =
+  | Def of {
+      name : ident;
+      tp : expr;
+      tm : expr;
+    }
+
+type file = item List.t
+
 let dump_ident fmt ({ value; _ } : ident) = Ident.pp fmt value
 
 let dump_local_name fmt ({ value; _ } : local_name) = match value with
diff --git a/src/bin/dune b/src/bin/dune
index f11979a..87fe556 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -4,8 +4,8 @@
  (libraries
   asai
   linenoise
-  toytt.elaborator
-  toytt.nbe
-  toytt.parser
+  yuujinchou
   toytt.error
-  ))
+  toytt.driver
+  toytt.parser
+  toytt.toplevel))
diff --git a/src/bin/main.ml b/src/bin/main.ml
index e1be039..4cbeef7 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -1,19 +1,39 @@
 module Term = Asai.Tty.Make(Error.Message)
 
-let ep input =
+let display = Term.display ~show_backtrace:false
+
+let handle_error f =
+  Error.run ~emit:display ~fatal:display f
+
+let handle_fatal f =
+  Error.run ~emit:display ~fatal:(fun msg -> display msg; exit 1) f
+
+let ep ~toplvl input =
   let ast = Parser.parse_expr input in
-  let (tp, tm) = Elaborator.infer_toplevel ast in
-  let value = NbE.eval ~env:Emp tm in
+  let toplvl = Option.value toplvl ~default:Yuujinchou.Trie.empty in
+  let (tp, tm) = Elaborator.infer_toplevel ~toplvl ast in
+  let value = NbE.eval_toplevel tm in
   Format.printf "%a : %a\n%!"
-    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 value)
-    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 tp)
+    (Pretty.pp ~names:Emp) (NbE.quote_toplevel @@ NbE.force_all value)
+    (Pretty.pp ~names:Emp) (NbE.quote_toplevel @@ NbE.force_all tp)
 
-let rec repl () =
+let rec repl ~toplvl () =
   match LNoise.linenoise "toytt> " with
-  | Some input -> 
-    Error.run ~emit:(Term.display ~show_backtrace:false) ~fatal:(Term.display ~show_backtrace:false) (fun () -> ep input);
+  | Some input ->
+    handle_error (fun () -> ep ~toplvl input);
     let _ = LNoise.history_add input in
-    repl ()
-  | None -> repl ()
+    repl ~toplvl ()
+  | None -> repl ~toplvl ()
+
+let input_file = ref None
 
-let () = repl ();
+let () =
+  let anon_fun path = input_file := Some path in
+  let usage_msg = "usage: toytt [input file]" in
+  let () = Arg.parse [] anon_fun usage_msg in
+  match !input_file with
+  | None ->
+    repl ~toplvl:None ()
+  | Some path ->
+    let toplvl = handle_fatal (fun () -> Driver.process_file path) in
+    repl ~toplvl:(Some toplvl) ()
diff --git a/src/driver/Driver.ml b/src/driver/Driver.ml
new file mode 100644
index 0000000..a2c4364
--- /dev/null
+++ b/src/driver/Driver.ml
@@ -0,0 +1,12 @@
+let process_item (toplvl : TopLevel.t) (item : Ast.item) : TopLevel.t =
+  let (name, item) = match item with
+    | Ast.Def { name; tp; tm } ->
+      let tp = Elaborator.check_tp_toplevel ~toplvl tp in
+      let tm = Elaborator.check_toplevel ~toplvl ~tm ~tp in
+      (name, TopLevel.Def { tp; tm = lazy (NbE.eval_toplevel tm) })
+  in
+  Yuujinchou.Trie.update_singleton name.value (fun _ -> Some (item, ())) toplvl
+
+let process_file (path : string) : TopLevel.t =
+  let file = Parser.parse_file path in
+  List.fold_left process_item Yuujinchou.Trie.empty file
diff --git a/src/driver/dune b/src/driver/dune
new file mode 100644
index 0000000..db5f824
--- /dev/null
+++ b/src/driver/dune
@@ -0,0 +1,12 @@
+(library
+ (name Driver)
+ (public_name toytt.driver)
+ (libraries
+  algaeff
+  bwd
+  toytt.ast
+  toytt.elaborator
+  toytt.error
+  toytt.nbe
+  toytt.parser
+  toytt.toplevel))
diff --git a/src/driver/test.toytt b/src/driver/test.toytt
new file mode 100644
index 0000000..273b42b
--- /dev/null
+++ b/src/driver/test.toytt
@@ -0,0 +1 @@
+def t : bool := true
diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml
index f40076d..c366ff3 100644
--- a/src/elaborator/Elaborator.ml
+++ b/src/elaborator/Elaborator.ml
@@ -5,32 +5,42 @@ module A = Ast
 module S = NbE.Syntax
 module D = NbE.Domain
 
-(* invariant: `tps`, `tms` and `names` all have length `size` *)
 type env = {
+  (* local context *)
+  (* invariant: `tps`, `tms` and `names` all have length `size` *)
   tps : D.env;
   tms : D.env;
   names : Ident.local bwd;
   size : int;
+
+  (* top-level context *)
+  toplvl : TopLevel.t;
 }
 
 module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
 
-(** General helpers *)
-
-let lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with
-  | Some name -> begin
-      let env = Eff.read() in
-      match Bwd.find_index ((=) name) env.names with
-      | Some ix ->
-        let tp = Bwd.nth env.tps ix in
-        (tp, S.Var ix)
-      | None -> Error.unbound_variable id
-    end
-  | None -> Error.unbound_variable id
+(* general helpers *)
+
+let lookup (id : Ident.t) : D.t * S.t =
+  let env = Eff.read() in
+  (* search through local context *)
+  match Option.bind 
+          (Ident.to_local id) 
+          (fun name -> Bwd.find_index ((=) name) env.names) with
+  | Some ix ->
+    let tp = Bwd.nth env.tps ix in
+    (tp, S.Var ix)
+  | None ->
+    (* look up in top-level context *)
+    match Yuujinchou.Trie.find_singleton id env.toplvl with
+    | Some (Def { tp; tm }, _) ->
+      (tp, S.Def (id, tm))
+    | None -> Error.unbound_variable id
 
 let bind ~(name : Ident.local) ~(tp : D.t) f =
   let arg = D.var (Eff.read()).size in
-  let update env = {
+  let update env = { 
+    env with
     tps = env.tps <: tp;
     tms = env.tms <: arg;
     names = env.names <: name;
@@ -38,15 +48,15 @@ let bind ~(name : Ident.local) ~(tp : D.t) f =
   } in
   Eff.scope update (fun () -> f arg)
 
-(** NbE helpers *)
+(* NbE helpers *)
 
 let eval tm = NbE.eval ~env:(Eff.read()).tms tm
 
-(** Evaluate under the current environment augmented by `arg` *)
+(* evaluate under the current environment augmented by `arg` *)
 (* TODO: this is kind of inelegant, can we do better? *)
 let eval_at arg = NbE.eval ~env:((Eff.read()).tms <: arg)
 
-(** Pretty-printing helpers *)
+(* pretty-printing helpers *)
 
 let pp_tm () =
   let names = (Eff.read()).names in
@@ -57,7 +67,7 @@ let pp_val () =
   let pp_tm = pp_tm () in
   fun fmt v -> pp_tm fmt (NbE.quote ~size v)
 
-(** Main algorithm *)
+(* main algorithm *)
 
 type connective = [ `Pi | `Sigma ]
 
@@ -118,12 +128,14 @@ and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A
     end
   | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type"
 
+and check_tp (tp : A.expr) = eval @@ check ~tp:D.Type ~tm:tp
+
 and infer (tm : A.expr) : D.t * S.t =
   Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
   match tm.value with
   | A.Var name -> lookup name
   | A.Check (tm, tp) ->
-    let tp = eval @@ check ~tp:D.Type ~tm:tp in
+    let tp = check_tp tp in
     let tm = check ~tp ~tm in
     (tp, tm)
   | A.App (fn, arg) -> begin match infer fn with
@@ -158,11 +170,21 @@ and infer (tm : A.expr) : D.t * S.t =
     (motive_scrut, tm)
   | _ -> Error.not_inferable ()
 
-let empty_env : env = {
+(* interface *)
+
+let initial_env toplvl : env = {
   tps = Emp;
   tms = Emp;
   names = Emp;
   size = 0;
+  toplvl;
 }
 
-let infer_toplevel (tm : A.expr) = Eff.run ~env:empty_env @@ fun () -> infer tm
\ No newline at end of file
+let check_toplevel ~(toplvl : TopLevel.t) ~(tm : A.expr) ~(tp : D.t) =
+  Eff.run ~env:(initial_env toplvl) @@ fun () -> check ~tm ~tp
+
+let check_tp_toplevel ~(toplvl : TopLevel.t) (tp : A.expr) =
+  Eff.run ~env:(initial_env toplvl) @@ fun () -> check_tp tp
+
+let infer_toplevel ~(toplvl : TopLevel.t) (tm : A.expr) =
+  Eff.run ~env:(initial_env toplvl) @@ fun () -> infer tm
\ No newline at end of file
diff --git a/src/elaborator/dune b/src/elaborator/dune
index 941027a..e4180fa 100644
--- a/src/elaborator/dune
+++ b/src/elaborator/dune
@@ -5,7 +5,8 @@
   algaeff
   bwd
   toytt.ast
+  toytt.error
   toytt.ident
   toytt.nbe
   toytt.pretty
-  toytt.error))
+  toytt.toplevel))
diff --git a/src/error/Error.ml b/src/error/Error.ml
index 555d41c..9a5ea9e 100644
--- a/src/error/Error.ml
+++ b/src/error/Error.ml
@@ -1,6 +1,7 @@
 module Message =
 struct
   type t =
+    | FileError
     | IllegalCharacter
     | SyntaxError
     | UnboundVariable
@@ -10,6 +11,7 @@ struct
 
   let default_severity : t -> Asai.Diagnostic.severity =
     function
+    | FileError -> Error
     | IllegalCharacter -> Error
     | SyntaxError -> Error
     | UnboundVariable -> Error
@@ -19,19 +21,23 @@ struct
 
   let short_code : t -> string =
     function
+    (* operating system errors *)
+    | FileError -> "E101"
     (* parser errors *)
-    | IllegalCharacter -> "E101"
-    | SyntaxError -> "E102"
+    | IllegalCharacter -> "E201"
+    | SyntaxError -> "E202"
     (* elaboration errors *)
-    | UnboundVariable -> "E201"
-    | TypeMismatch -> "E202"
-    | NotInferable -> "E203"
+    | UnboundVariable -> "E301"
+    | TypeMismatch -> "E302"
+    | NotInferable -> "E303"
     (* misc *)
     | Bug -> "E900"
 end
 
 include Asai.Reporter.Make(Message)
 
+let file_open_error ~path ~msg = fatalf FileError
+    "unable to open file '%s': %s" path msg
 let illegal_character ~loc char = fatalf ~loc IllegalCharacter
     "illegal character '%s'" (Char.escaped char)
 let syntax_error ~loc = fatalf ~loc SyntaxError
diff --git a/src/nbe/Conversion.ml b/src/nbe/Conversion.ml
index 00bc942..8c4478e 100644
--- a/src/nbe/Conversion.ml
+++ b/src/nbe/Conversion.ml
@@ -7,31 +7,61 @@ exception Unequal
 
 module Internal =
 struct
-  (** Context size *)
-  type env = int
+  type env = {
+    mode : [`Rigid | `Flex | `Full];
+    size : int
+  }
 
   module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
 
+  let with_mode mode f = Eff.scope (fun env -> { env with mode }) f
+
   let bind f =
-    let arg = D.var (Eff.read()) in
-    Eff.scope (fun size -> size + 1) (fun () -> f arg)
+    let arg = D.var (Eff.read()).size in
+    Eff.scope (fun env -> { env with size = env.size + 1 }) @@ fun () -> f arg
+
+  let equal_unfold_head hd1 hd2 = match hd1, hd2 with
+    | D.Def (p1, _), D.Def (p2, _) -> p1 = p2
 
-  let rec equate v1 v2 = match v1, v2 with
-    | D.Neutral ne, v | v, D.Neutral ne -> equate_ne ne v
-    | D.Pi (_, base1, fam1), D.Pi (_, base2, fam2) ->
+  let rec equate v1 v2 = match v1, v2, (Eff.read()).mode with
+    | D.Neutral ne, v, _ | v, D.Neutral ne, _ -> equate_ne ne v
+    | D.Pi (_, base1, fam1), D.Pi (_, base2, fam2), _  ->
       equate base1 base2;
       equate_clo fam1 fam2
-    | D.Lam (_, clo1), D.Lam (_, clo2) -> equate_clo clo1 clo2
-    | D.Sg (_, base1, fam1), D.Sg (_, base2, fam2) ->
+    | D.Lam (_, clo1), D.Lam (_, clo2), _  -> equate_clo clo1 clo2
+    | D.Sg (_, base1, fam1), D.Sg (_, base2, fam2), _  ->
       equate base1 base2;
       equate_clo fam1 fam2
-    | D.Pair (fst1, snd1), D.Pair (fst2, snd2) ->
+    | D.Pair (fst1, snd1), D.Pair (fst2, snd2), _  ->
       equate fst1 fst2;
       equate snd1 snd2
-    | Type, Type -> ()
-    | Bool, Bool -> ()
-    | True, True -> ()
-    | False, False -> ()
+    | Type, Type, _  -> ()
+    | Bool, Bool, _  -> ()
+    | True, True, _  -> ()
+    | False, False, _  -> ()
+
+    (* approximate conversion checking in the style of smalltt, see
+       https://github.com/AndrasKovacs/smalltt?tab=readme-ov-file#approximate-conversion-checking *)
+    (* in "full" mode, we immediately unfold any defined symbol *)
+    | D.Unfold (_, _, v1), v2, `Full -> equate (Lazy.force v1) v2
+    | v1, D.Unfold (_, _, v2), `Full -> equate v1 (Lazy.force v2)
+    (* in "flex" mode, we cannot unfold any top-level definition; we can only
+       recurse into spines if head symbols are equal *)
+    | D.Unfold (hd1, sp1, _), D.Unfold (hd2, sp2, _), `Flex ->
+      if equal_unfold_head hd1 hd2 then
+        equate_spine sp1 sp2
+      else raise Unequal
+    (* in "rigid" mode, we can initiate speculation if we have the same
+       top-level head symbol on both sides *)
+    | D.Unfold (hd1, sp1, v1), D.Unfold (hd2, sp2, v2), `Rigid ->
+      if equal_unfold_head hd1 hd2 then
+        try with_mode `Flex @@ fun () -> equate_spine sp1 sp2 with
+        | Unequal -> with_mode `Full @@ fun () -> equate (Lazy.force v1) (Lazy.force v2)
+      else
+        equate (Lazy.force v1) (Lazy.force v2)
+    | D.Unfold (_, _, v1), v2, `Rigid -> equate (Lazy.force v1) v2
+    | v1, D.Unfold (_, _, v2), `Rigid -> equate v1 (Lazy.force v2)
+
     | _ -> raise Unequal
 
   and equate_clo clo1 clo2 = bind @@ fun arg ->
@@ -71,5 +101,6 @@ struct
     | _ -> raise Unequal
 end
 
-let equate ~size v1 v2 = Internal.Eff.run ~env:size @@ fun () ->
-  Internal.equate v1 v2
+let equate ~size v1 v2 =
+  let env = { Internal.mode = `Rigid; size } in
+  Internal.Eff.run ~env @@ fun () -> Internal.equate v1 v2
diff --git a/src/nbe/Data.ml b/src/nbe/Data.ml
index d2f94d3..8589ea5 100644
--- a/src/nbe/Data.ml
+++ b/src/nbe/Data.ml
@@ -1,9 +1,8 @@
 open Bwd
 
-(** Syntactic terms *)
-
 type syn =
   | Var of int
+  | Def of Ident.t * value Lazy.t
   | Pi of Ident.local * syn * (* BINDS *) syn
   | Lam of Ident.local * (* BINDS *) syn
   | App of syn * syn
@@ -23,10 +22,9 @@ type syn =
       scrut : syn;
     }
 
-(** Semantic domain *)
-
-type value =
+and value =
   | Neutral of ne
+  | Unfold of unfold
   | Pi of Ident.local * value * clo
   | Lam of Ident.local * clo
   | Sg of Ident.local * value * clo
@@ -37,7 +35,13 @@ type value =
   | False
 
 and ne = ne_head * frm bwd
-and ne_head = Var of int (* De Bruijn levels *)
+and ne_head =
+  | Var of int (* De Bruijn levels *)
+
+and unfold = unfold_head * frm bwd * value Lazy.t
+and unfold_head =
+  | Def of Ident.t * value Lazy.t
+
 and frm = 
   | App of value
   | Fst
diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml
index 6f5e11c..bf5ed90 100644
--- a/src/nbe/Domain.ml
+++ b/src/nbe/Domain.ml
@@ -2,6 +2,7 @@ open Bwd
 
 type t = Data.value =
   | Neutral of ne
+  | Unfold of unfold
   | Pi of Ident.local * t * clo
   | Lam of Ident.local * clo
   | Sg of Ident.local * t * clo
@@ -12,7 +13,13 @@ type t = Data.value =
   | False
 
 and ne = Data.ne
-and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
+and ne_head = Data.ne_head =
+  | Var of int (* De Bruijn levels *)
+
+and unfold = Data.unfold
+and unfold_head = Data.unfold_head =
+  | Def of Ident.t * t Lazy.t
+
 and frm = Data.frm =
   | App of t
   | Fst
@@ -27,4 +34,5 @@ and frm = Data.frm =
 and env = Data.env
 and clo = Data.clo = Clo of { body : Data.syn; env : env }
 
-let var i = Neutral (Var i, Bwd.Emp)
+let var i = Neutral (Var i, Emp)
+let def p v = Unfold (Def (p, v), Emp, v)
diff --git a/src/nbe/Eval.ml b/src/nbe/Eval.ml
index bd8326e..2730ac0 100644
--- a/src/nbe/Eval.ml
+++ b/src/nbe/Eval.ml
@@ -16,27 +16,41 @@ struct
 
   and app v w = match v with
     | D.Lam (_, clo) -> inst_clo clo w
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.App w)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.App w, Lazy.map (fun v -> app v w) v)
     | _ -> invalid_arg "Eval.app"
 
   and fst = function
     | D.Pair (v, _) -> v
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Fst)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.Fst)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.Fst, Lazy.map (fun v -> fst v) v)
     | _ -> invalid_arg "Eval.fst"
 
   and snd = function
     | D.Pair (_, v) -> v
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd)
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.Snd)
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.Snd, Lazy.map (fun v -> snd v) v)
     | _ -> invalid_arg "Eval.snd"
 
   and bool_elim motive_var motive true_case false_case = function
     | D.True -> true_case
     | D.False -> false_case
-    | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case })
+    | D.Neutral (hd, frms) ->
+      D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case })
+    | D.Unfold (hd, frms, v) ->
+      D.Unfold (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case }, 
+                Lazy.map (fun v -> bool_elim motive_var motive true_case false_case v) v)
     | _ -> invalid_arg "Eval.bool_elim"
 
   and eval = function
     | S.Var i -> Bwd.nth (Eff.read()) i
+    | S.Def (p, v) -> D.def p v
     | S.Pi (name, base, fam) -> D.Pi (name, eval base, make_clo fam)
     | S.Lam (name, body) -> D.Lam (name, make_clo body)
     | S.App (a, b) -> app (eval a) (eval b)
@@ -53,4 +67,9 @@ struct
 end
 
 let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm
+let eval_toplevel tm = eval ~env:Emp tm
 let inst_clo = Internal.inst_clo
+
+let rec force_all = function
+  | D.Unfold (_, _, v) -> force_all (Lazy.force v)
+  | v -> v
diff --git a/src/nbe/NbE.ml b/src/nbe/NbE.ml
index 3ec1f6d..edd71a5 100644
--- a/src/nbe/NbE.ml
+++ b/src/nbe/NbE.ml
@@ -2,9 +2,12 @@ module Syntax = Syntax
 module Domain = Domain
 
 let eval = Eval.eval
+let eval_toplevel = Eval.eval_toplevel
 let inst_clo = Eval.inst_clo
+let force_all = Eval.force_all
 
 let quote = Quote.quote
+let quote_toplevel = Quote.quote_toplevel
 
 exception Unequal = Conversion.Unequal
 let equate = Conversion.equate
diff --git a/src/nbe/Quote.ml b/src/nbe/Quote.ml
index cc5a81e..94c8395 100644
--- a/src/nbe/Quote.ml
+++ b/src/nbe/Quote.ml
@@ -12,9 +12,10 @@ struct
     let arg = D.var (Eff.read()) in
     Eff.scope (fun size -> size + 1) @@ fun () ->
     f arg
-    
+
   let rec quote = function
     | D.Neutral ne -> quote_ne ne
+    | D.Unfold uf -> quote_unfold uf
     | D.Pi (name, base, fam) -> S.Pi (name, quote base, quote_clo fam)
     | D.Lam (name, clo) -> S.Lam (name, quote_clo clo)
     | D.Sg (name, base, fam) -> S.Sg (name, quote base, quote_clo fam)
@@ -27,9 +28,11 @@ struct
   and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg)
 
   and quote_ne (hd, frms) = Bwd.fold_left quote_frm (quote_ne_head hd) frms
-
   and quote_ne_head (D.Var i) = S.Var (Eff.read() - i - 1) (* converting from levels to indices *)
 
+  and quote_unfold (hd, frms, _) = Bwd.fold_left quote_frm (quote_unfold_head hd) frms
+  and quote_unfold_head (D.Def (p, v)) = S.Def (p, v)
+
   and quote_frm hd = function
     | D.App v -> S.App (hd, quote v)
     | D.Fst -> S.Fst hd
@@ -45,3 +48,4 @@ struct
 end
 
 let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v)
+let quote_toplevel v = quote ~size:0 v
diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml
index dd690fb..5de5281 100644
--- a/src/nbe/Syntax.ml
+++ b/src/nbe/Syntax.ml
@@ -1,5 +1,6 @@
 type t = Data.syn =
   | Var of int
+  | Def of Ident.t * Data.value Lazy.t
   | Pi of Ident.local * t * (* BINDS *) t
   | Lam of Ident.local * (* BINDS *) t
   | App of t * t
diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly
index d8e9ee0..d49c050 100644
--- a/src/parser/Grammar.mly
+++ b/src/parser/Grammar.mly
@@ -5,7 +5,8 @@ open Ast
 %token <string> IDENT
 %token LPR RPR
 %token LBR RBR
-%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE
+%token ARROW ASSIGN ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE
+%token DEF
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
 %token TYPE
@@ -17,6 +18,7 @@ open Ast
 %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
 %start <Ast.expr> start_expr
+%start <Ast.file> start_file
 
 %%
 
@@ -81,4 +83,11 @@ raw_expr:
 %inline
 expr: e = locate(raw_expr) { e }
 
+item:
+  | DEF; name = ident; COLON; tp = expr; ASSIGN; tm = expr
+    { Def { name; tp; tm } }
+
+file: items = list(item) { items }
+
 start_expr: e = expr; EOF { e }
+start_file: f = file; EOF { f }
diff --git a/src/parser/Lexer.mll b/src/parser/Lexer.mll
index 708bb64..22ae387 100644
--- a/src/parser/Lexer.mll
+++ b/src/parser/Lexer.mll
@@ -11,11 +11,13 @@ let ident = letter+
 rule token =
   parse
   | whitespace { token lexbuf }
+
   | "(" { LPR }
   | ")" { RPR }
   | "[" { LBR }
   | "]" { RBR }
   | "->" { ARROW }
+  | ":=" { ASSIGN }
   | "*" { ASTERISK }
   | "\\" { BACKSLASH }
   | "::" { DOUBLE_COLON }
@@ -24,14 +26,21 @@ rule token =
   | "." { DOT }
   | "=>" { FATARROW }
   | "_" { UNDERSCORE }
-  | "at" { AT }
+
+  | "def" { DEF }
+
   | "fst" { FST }
   | "snd" { SND }
+
   | "type" { TYPE }
+
   | "bool" { BOOL }
   | "true" { TRUE }
   | "false" { FALSE }
   | "bool-elim" { BOOL_ELIM }
+  | "at" { AT }
+
   | ident { IDENT (Lexing.lexeme lexbuf) }
+
   | eof { EOF }
   | (_ as illegal_char) { raise (IllegalCharacter illegal_char) }
diff --git a/src/parser/Parser.ml b/src/parser/Parser.ml
index 88448c9..ae86885 100644
--- a/src/parser/Parser.ml
+++ b/src/parser/Parser.ml
@@ -1,3 +1,9 @@
+let handle_syntax_error ~source ~lexbuf f = try f () with
+  | Lexer.IllegalCharacter illegal_char ->
+    Error.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char
+  | Grammar.Error ->
+    Error.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf)
+
 let parse_expr (s : string) : Ast.expr =
   let lexbuf = Lexing.from_string s in
   let string_source : Asai.Range.string_source = {
@@ -6,8 +12,15 @@ let parse_expr (s : string) : Ast.expr =
   } in
   let source = `String string_source in
   Eff.run ~env:source @@ fun () ->
-  try Grammar.start_expr Lexer.token lexbuf with
-  | Lexer.IllegalCharacter illegal_char ->
-    Error.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char
-  | Grammar.Error ->
-    Error.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf)
+  handle_syntax_error ~source ~lexbuf @@ fun () ->
+  Grammar.start_expr Lexer.token lexbuf
+
+let parse_file (path : string) : Ast.file =
+  let inchan = try open_in path with
+    | Sys_error msg -> Error.file_open_error ~path ~msg
+  in
+  let lexbuf = Lexing.from_channel inchan in
+  let source = `File path in
+  Eff.run ~env:source @@ fun () ->
+  handle_syntax_error ~source ~lexbuf @@ fun () ->
+  Grammar.start_file Lexer.token lexbuf
diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml
index 8b7ad1a..fa25a40 100644
--- a/src/pretty/Pretty.ml
+++ b/src/pretty/Pretty.ml
@@ -74,6 +74,7 @@ struct
   (* TODO: improve indentation *)
   and pp fmt = function
     | S.Var ix -> pp_var fmt ix
+    | S.Def (p, _) -> Ident.pp fmt p
     | S.Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam)
     | S.Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body
     | S.Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam)
diff --git a/src/pretty/dune b/src/pretty/dune
index ee17573..708b5b1 100644
--- a/src/pretty/dune
+++ b/src/pretty/dune
@@ -4,6 +4,6 @@
  (libraries
   bwd
   fmt
+  toytt.error
   toytt.ident
-  toytt.nbe
-  toytt.error))
+  toytt.nbe))
diff --git a/src/toplevel/TopLevel.ml b/src/toplevel/TopLevel.ml
new file mode 100644
index 0000000..9ff8986
--- /dev/null
+++ b/src/toplevel/TopLevel.ml
@@ -0,0 +1,6 @@
+module D = NbE.Domain
+
+type item =
+  | Def of { tp : D.t; tm : D.t Lazy.t }
+
+type t = (item, unit) Yuujinchou.Trie.t
diff --git a/src/toplevel/dune b/src/toplevel/dune
new file mode 100644
index 0000000..720635c
--- /dev/null
+++ b/src/toplevel/dune
@@ -0,0 +1,7 @@
+(library
+ (name TopLevel)
+ (public_name toytt.toplevel)
+ (libraries
+  yuujinchou
+  toytt.ident
+  toytt.nbe))
-- 
cgit 1.4.1