dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE
commit f7d4d562278d6d9a0df134fdd77a1b2c644333bd
parent b54df0410d20da05e9dc5d064fe16ba62f9beff7
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Wed, 17 Jan 2024 19:58:39 -0800

Test a fix issue relating to quoted names

Diffstat:

Mdesugar.ml | 8++++----


Melab.ml | 109++++++++++++++++++++++++++++++++++++++-----------------------------------------


Merror.ml | 114++++++++++++++++++++++++++++++++++++++++----------------------------------------


Mlexer.mll | 13+++++++------


Mmain.ml | 9++++++---


Mname.ml | 35+++++++++++++++++++++++++++++++----


Mparser.mly | 106++++++++++++++++++++++++++++++++++++++++----------------------------------------


Mpretty.ml | 4++--


8 files changed, 212 insertions(+), 186 deletions(-)

diff --git a/desugar.ml b/desugar.ml
@@ -1,13 +1,13 @@
 open Util
 open Node
-open Error
+module E = Error
 module C = Concrete
 module A = Abstract
 
 let ensure_distinct names =
 	let declare name_set {loc; data = name} =
 		if Name.Var.Set.mem name name_set then
-			abort loc (EDesugarDuplicateBinderName name)
+			E.abort loc (E.DesugarDuplicateBinderName name)
 		else
 			Name.Var.Set.add name name_set in
 	ignore @@ Array.fold_left declare Name.Var.Set.empty names
@@ -112,7 +112,7 @@ let rec term {loc; data = t} = match t with
 | C.VariantType ctors ->
 	let insert m {loc = ctor_loc; data = C.Ctor (tag, doms)} =
 		if Name.Ctor.Map.mem tag.data m then
-			abort tag.loc (EDesugarDuplicateCtor tag.data)
+			E.abort tag.loc (E.DesugarDuplicateCtor tag.data)
 		else
 			let ctor = ctor_loc @$ A.Ctor (Array.map domain doms) in
 			Name.Ctor.Map.add tag.data ctor m in
@@ -188,7 +188,7 @@ and discriminant names typs {loc; data = p} = match p with
 	| A.DWild, A.DWild -> loc @$ A.DWild
 	| A.DWild, A.DData _ -> qdisc
 	| A.DData _, A.DWild -> pdisc
-	| A.DData _, A.DData _ -> abort loc EDesugarDataAndData
+	| A.DData _, A.DData _ -> E.abort loc E.DesugarDataAndData
 	end
 | C.POr _ -> no_impl "or patterns"
 | C.PParen p -> discriminant names typs p
diff --git a/elab.ml b/elab.ml
@@ -1,6 +1,6 @@
 open Util
 open Node
-open Error
+module E = Error
 open Eval
 open Quote
 open Unify
@@ -19,8 +19,8 @@ type mode =
 | Check of V.value
 
 (* Convention: An elaboration-related function can have two versions, one whose
- * name ends with a prime, which can throw an Exn, and one whose name does not
- * end with a prime, which returns in the result monad.
+ * name ends with a prime, which can throw an E.Exn, and one whose name does
+ * not end with a prime, which returns in the result monad.
  * TODO: Make sure every function has both versions, even if unused? *)
 
 (* TODO: We check for name distinctness in two places; unify them. *)
@@ -28,7 +28,7 @@ let declare_name'
 : Name.Var.Set.t -> Name.Var.t node -> Name.Var.Set.t
 = fun name_set {loc; data = name} ->
 	if Name.Var.Set.mem name name_set then
-		abort loc @@ EElabDuplicateName name
+		E.abort loc @@ E.ElabDuplicateName name
 	else
 		Name.Var.Set.add name name_set
 
@@ -79,7 +79,7 @@ let elaborate_args'
 		| Plicity.Ex ->
 			let j = i - !implicit_count in
 			begin if explicit_count <= j then
-				abort loc EElabArityMismatch
+				E.abort loc E.ElabArityMismatch
 			end;
 			Some (explicit_args.(j))
 		| Plicity.Im ->
@@ -89,26 +89,26 @@ let elaborate_args'
 
 	(* We had enough explicit args, but now ensure we don't have too many. *)
 	begin if explicit_count > arity - !implicit_count then
-		abort loc EElabArityMismatch
+		E.abort loc E.ElabArityMismatch
 	end;
 
 	args
 
 let rec infer
-: context -> A.term -> (I.term * V.value, error) result
+: context -> A.term -> (I.term * V.value, E.error) result
 = fun ctx t ->
 	try Ok (infer' ctx t) with
-	| Exn e -> Error e
+	| E.Exn e -> Error e
 
 and infer'
 : context -> A.term -> I.term * V.value
 = fun ctx t -> elaborate' ctx t Infer
 
 and check
-: context -> A.term -> V.value -> (I.term, error) result
+: context -> A.term -> V.value -> (I.term, E.error) result
 = fun ctx t vtyp ->
 	try Ok (check' ctx t vtyp) with
-	| Exn e -> Error e
+	| E.Exn e -> Error e
 
 and check'
 : context -> A.term -> V.value -> I.term
@@ -117,10 +117,10 @@ and check'
 	t
 
 and elaborate
-: context -> A.term -> mode -> (I.term * V.value, error) result
+: context -> A.term -> mode -> (I.term * V.value, E.error) result
 = fun ctx t mode ->
 	try Ok (elaborate' ctx t mode) with
-	| Exn e -> Error e
+	| E.Exn e -> Error e
 
 and elaborate'
 : context -> A.term -> mode -> I.term * V.value
@@ -153,7 +153,7 @@ and elaborate'
 		let (args, clo) = check_args' ctx loc explicit_args clo multibinder in
 		let vcodomain = eval clo codomain in
 		(I.App (fn, args), vcodomain)
-	| vtyp -> abort loc @@ EElabApplyNonFunction (quote ctx.env vtyp)
+	| vtyp -> E.abort loc @@ E.ElabApplyNonFunction (quote ctx.env vtyp)
 	end
 
 | A.Fn (params, body), Infer ->
@@ -168,7 +168,7 @@ and elaborate'
 	let {I.multibinder = {binders = domains; order}; I.codomain} = fntype in
 
 	begin if Array.length params <> Array.length domains then
-		abort loc EElabFnArityMismatch
+		E.abort loc E.ElabFnArityMismatch
 	end;
 	let arity = Array.length params in
 
@@ -189,7 +189,7 @@ and elaborate'
 		end;
 
 		begin if param.plicity <> domain.plicity then
-			abort loc EElabFnPlicityMismatch
+			E.abort loc E.ElabFnPlicityMismatch
 		end;
 		let plicity = param.plicity in
 
@@ -208,14 +208,14 @@ and elaborate'
 
 	(I.Fn {multibinder = {binders = params'; order}; body; codomain}, vfntype)
 
-(*| A.Fn _, Check vtyp -> abort loc @@ ErrExpectedFnType vtyp*)
+(*| A.Fn _, Check vtyp -> E.abort loc @@ ErrExpectedFnType vtyp*)
 
 | A.FnType (domains, codomain), Infer ->
 	let (ctx, multibinder) = infer_multibinder' ctx loc domains in
 	let codomain = check' ctx codomain V.Type in
 	(I.FnType {multibinder; codomain}, V.Type)
 
-| A.Data _, Infer -> abort loc EElabCantInferData
+| A.Data _, Infer -> E.abort loc E.ElabCantInferData
 
 | A.Data ({data = tag; _}, explicit_args),
 		Check (V.DataTypeClosure (clo, datatype) as vdatatype) ->
@@ -225,10 +225,10 @@ and elaborate'
 			datatype.ctors.(tagi) in
 		let datatype = quote_datatype ctx.env clo datatype in
 		(I.Data {tag; tagi; args; datatype}, vdatatype)
-	| None -> abort loc @@ EElabUnexpectedCtor tag
+	| None -> E.abort loc @@ E.ElabUnexpectedCtor tag
 	end
 
-(*| A.Data _, Check vtyp -> abort loc @@ ErrExpectedDataType vtyp*)
+(*| A.Data _, Check vtyp -> E.abort loc @@ ErrExpectedDataType vtyp*)
 
 | A.DataType ctors, Infer ->
 	let next = ref 0 in
@@ -248,7 +248,7 @@ and elaborate'
 	begin match Ctx.lookup ctx name i with
 	| Some {typ = V.Future (id, j); _} -> raise (BlockedOnFuture (id, j, name))
 	| Some {typ; value; _} -> (quote ctx.env value, typ)
-	| None -> abort loc @@ EElabUnboundVar (name, i)
+	| None -> E.abort loc @@ E.ElabUnboundVar (name, i)
 	end
 
 | A.Type, Infer -> (I.Type, V.Type)
@@ -261,7 +261,7 @@ and elaborate'
 	else
 		let expected = quote ctx.env vexpected in
 		let inferred = quote ctx.env vinferred in
-		abort loc @@ EElabUnifyFail (expected, inferred)
+		E.abort loc @@ E.ElabUnifyFail (expected, inferred)
 
 (* Check the given explicit arguments against the given multibinder.
  * Return the elaborated terms and the multibinder's closure extended with
@@ -322,12 +322,12 @@ and infer_definers'
 			| Ok (names, vtyp) ->
 				let rhs = check' ctx rhs vtyp in
 				(names, rhs, vtyp)
-			| Error {data = EElabNonInferablePatt; _} ->
+			| Error {data = E.ElabNonInferablePatt; _} ->
 				(* Next try to infer from rhs (and check lhs). *)
 				let (rhs, vtyp) = infer' ctx rhs in
 				let names = check_irrefutable_patt' ctx lhs vtyp in
 				(names, rhs, vtyp)
-			| Error e -> abort e.loc e.data in
+			| Error e -> E.abort e.loc e.data in
 		let typ = quote ctx.env vtyp in
 		(* XXX: vrhs doesn't need to be a Rec. We could eagerly evaluate it, or
 		 * add some other mechanism for laziness (like glued eval). *)
@@ -360,9 +360,9 @@ and infer_definers'
 					names vtyp (V.Arb (Uniq.get vars i)) in
 				ctx_with_asns := ctx';
 				asns.(i) <- asn
-			| Error ({data = EElabNonInferablePatt; _} as root) -> 
-				abort loc @@ EElabNoLetAnnot root
-			| Error e -> abort e.loc e.data
+			| Error ({data = E.ElabNonInferablePatt; _} as root) -> 
+				E.abort loc @@ E.ElabNoLetAnnot root
+			| Error e -> E.abort e.loc e.data
 		done;
 		let ctx = !ctx_with_asns in
 
@@ -561,7 +561,7 @@ and infer_multibinder'
 			};
 			order.(j) <- i
 		| Pending _ ->
-			abort loc @@ EElabBinderCycle (find_cycle states i)
+			E.abort loc @@ E.ElabBinderCycle (find_cycle states i)
 	done;
 
 	(ctx, {binders = binders'; order})
@@ -577,14 +577,14 @@ and infer_binder'
 | None ->
 	match infer_irrefutable_patt ctx patt, plicity with
 	| Ok (_, vtyp), _ -> vtyp
-	| Error {data = EElabNonInferablePatt; _}, Plicity.Im ->
+	| Error {data = E.ElabNonInferablePatt; _}, Plicity.Im ->
 		begin match check_irrefutable_patt ctx patt V.Type with
 		| Ok _ -> V.Type
-		| Error root -> abort loc @@ EElabUnannotImplicitIsType root
+		| Error root -> E.abort loc @@ E.ElabUnannotImplicitIsType root
 		end
-	| Error ({data = EElabNonInferablePatt; _} as root), Plicity.Ex ->
-		abort loc @@ EElabNoBinderAnnot root
-	| Error e, _ -> abort e.loc e.data
+	| Error ({data = E.ElabNonInferablePatt; _} as root), Plicity.Ex ->
+		E.abort loc @@ E.ElabNoBinderAnnot root
+	| Error e, _ -> E.abort e.loc e.data
 
 (* Check that each term in the array starting at the given index is a type
  * convertible to the given value. *)
@@ -597,47 +597,42 @@ and check_types'
 		begin if not (conv ctx.env vtyp vtyp') then
 			let typ = quote ctx.env vtyp in
 			let typ' = quote ctx.env vtyp' in
-			abort typs.(i).loc @@ EElabUnifyFail (typ, typ')
+			E.abort typs.(i).loc @@ E.ElabUnifyFail (typ, typ')
 		end
 	done
 
 and infer_irrefutable_patt
-: context -> A.patt -> (Name.Var.t node array * V.value, error) result
+: context -> A.patt -> (Name.Var.t node array * V.value, E.error) result
 = fun ctx patt ->
 	try Ok (infer_irrefutable_patt' ctx patt) with
-	| Exn e -> Error e
+	| E.Exn e -> Error e
 
-(* TODO: Reimplement with infer_patt'? *)
 and infer_irrefutable_patt'
 : context -> A.patt -> Name.Var.t node array * V.value
-= fun ctx {loc; data = patt} -> match patt with
-| {typs = [||]; _} -> abort loc EElabNonInferablePatt
-| {disc = {loc; data = A.DData _}; _} -> abort loc EElabDataPattRefutable
-| {names; typs; disc = {data = A.DWild; _}} ->
-	let typ = check' ctx typs.(0) V.Type in
-	let vtyp = eval ctx.env typ in
-	check_types' ctx typs 1 vtyp;
-	(names, vtyp)
+= fun ctx ({loc; _} as patt) ->
+	let (patt, vtyp) = infer_patt' ctx patt in
+	match patt with
+	| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
+	| {names; disc = I.DWild} -> (names, vtyp)
 
 and check_irrefutable_patt
-: context -> A.patt -> V.value -> (Name.Var.t node array, error) result
+: context -> A.patt -> V.value -> (Name.Var.t node array, E.error) result
 = fun ctx patt vtyp ->
 	try Ok (check_irrefutable_patt' ctx patt vtyp) with
-	| Exn e -> Error e
+	| E.Exn e -> Error e
 
-(* TODO: Reimplement with check_patt'? *)
 and check_irrefutable_patt'
 : context -> A.patt -> V.value -> Name.Var.t node array
-= fun ctx {loc; data = patt} vtyp -> match patt with
-| {disc = {loc; data = A.DData _}; _} -> abort loc EElabDataPattRefutable
-| {names; typs; disc = {data = A.DWild; _}} ->
-	check_types' ctx typs 0 vtyp;
-	names
+= fun ctx ({loc; _} as patt) vtyp ->
+	let patt = check_patt' ctx patt vtyp in
+	match patt with
+	| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
+	| {names; disc = I.DWild} -> names
 
 and infer_patt'
 : context -> A.patt -> I.patt * V.value
 = fun ctx {loc; data = patt} -> match patt with
-| {typs = [||]; _} -> abort loc EElabNonInferablePatt
+| {typs = [||]; _} -> E.abort loc E.ElabNonInferablePatt
 | {names; typs; disc} ->
 	let typ = check' ctx typs.(0) V.Type in
 	let vtyp = eval ctx.env typ in
@@ -686,9 +681,9 @@ and check_disc'
 
 		I.DData {tag; tagi; subpatts = subpatts'; datatype}
 
-	| None -> abort loc @@ EElabUnexpectedCtor tag
+	| None -> E.abort loc @@ E.ElabUnexpectedCtor tag
 	end
-| A.DData _, vtyp -> abort loc @@ EElabExpectedDataType (quote ctx.env vtyp)
+| A.DData _, vtyp -> E.abort loc @@ E.ElabExpectedDataType (quote ctx.env vtyp)
 
 
 
@@ -757,7 +752,7 @@ let rec elaborate_match loc scrutinee cases =
 	let switch = elaborate_switch loc used_cases env clauses in
 	begin match Array.find_index not used_cases with
 	(* TODO: Use loc of the redundant case, not the entire match. *)
-	| Some i -> abort loc ErrRedundantCase
+	| Some i -> E.abort loc ErrRedundantCase
 	| None -> ()
 	end;
 
@@ -796,7 +791,7 @@ and elaborate_switch match_loc used_cases env clauses =
 			I.Switch (index, subswitches)
 	else
 		(* TODO: Give an example of a missing case. *)
-		abort match_loc ErrNonExhaustiveMatch
+		E.abort match_loc ErrNonExhaustiveMatch
 
 and elaborate_switch_branch match_loc used_cases env clauses var arity i =
 	let clause_count = Array.length clauses in
diff --git a/error.ml b/error.ml
@@ -4,92 +4,92 @@ module I = Internal
 
 type error = error' node
 and error' =
-| ELexerNameIndexTooBig
-| ELexerInvalidNumberTerminator
-| ELexerNoRule
+| LexerNameIndexTooBig
+| LexerInvalidNumberTerminator
+| LexerNoRule
 
-| EParserInvalidTerm
-| EParserInvalidPatt
-| EParserEmptyDomain
+| ParserInvalidTerm
+| ParserInvalidPatt
+| ParserEmptyDomain
 
-| EDesugarDuplicateCtor of Name.Ctor.t
-| EDesugarDuplicateBinderName of Name.Var.t
-| EDesugarDataAndData
+| DesugarDuplicateCtor of Name.Ctor.t
+| DesugarDuplicateBinderName of Name.Var.t
+| DesugarDataAndData
 
-| EElabApplyNonFunction of I.term
-| EElabNonInferablePatt
-| EElabUnifyFail of I.term * I.term (* TODO: Rename to ConvFail? *)
-| EElabUnexpectedCtor of Name.Ctor.t
-| EElabExpectedDataType of I.term
-| EElabNoLetAnnot of error
-| EElabBinderCycle of Name.Var.t list
-| EElabUnannotImplicitIsType of error
-| EElabNoBinderAnnot of error
-| EElabDuplicateName of Name.Var.t
-| EElabArityMismatch
-| EElabCantInferData
-| EElabDataPattRefutable
-| EElabUnboundVar of Name.Var.t * int
-| EElabFnArityMismatch
-| EElabFnPlicityMismatch
-(*| EElabNonExhaustiveMatch*)
-(*| EElabRedundantCase*)
-(*| EElabExpectedFnType of I.term*)
+| ElabApplyNonFunction of I.term
+| ElabNonInferablePatt
+| ElabUnifyFail of I.term * I.term
+| ElabUnexpectedCtor of Name.Ctor.t
+| ElabExpectedDataType of I.term
+| ElabNoLetAnnot of error
+| ElabBinderCycle of Name.Var.t list
+| ElabUnannotImplicitIsType of error
+| ElabNoBinderAnnot of error
+| ElabDuplicateName of Name.Var.t
+| ElabArityMismatch
+| ElabCantInferData
+| ElabDataPattRefutable
+| ElabUnboundVar of Name.Var.t * int
+| ElabFnArityMismatch
+| ElabFnPlicityMismatch
+(*| ElabNonExhaustiveMatch*)
+(*| ElabRedundantCase*)
+(*| ElabExpectedFnType of I.term*)
 
-let rec pp_print_error ppf {loc; data = e} =
+let rec pp_print ppf {loc; data = e} =
 	F.fprintf ppf "[%a] %a"
 		Loc.pp_print loc
-		pp_print_error' e
+		pp_print' e
 
-and pp_print_error' ppf = function
-| ELexerNameIndexTooBig ->
+and pp_print' ppf = function
+| LexerNameIndexTooBig ->
 	F.pp_print_string ppf "name index too big"
-| ELexerInvalidNumberTerminator ->
+| LexerInvalidNumberTerminator ->
 	F.pp_print_string ppf "invalid character after number literal"
-| ELexerNoRule ->
+| LexerNoRule ->
 	F.pp_print_string ppf "lexical error"
 
-| EParserInvalidTerm ->
+| ParserInvalidTerm ->
 	F.pp_print_string ppf "invalid term"
-| EParserInvalidPatt ->
+| ParserInvalidPatt ->
 	F.pp_print_string ppf "invalid pattern"
-| EParserEmptyDomain ->
+| ParserEmptyDomain ->
 	F.pp_print_string ppf "empty domain"
 
-| EDesugarDuplicateCtor tag ->
+| DesugarDuplicateCtor tag ->
 	F.fprintf ppf "%s: %a"
 		"duplicate constructor: "
 		Name.Ctor.pp_print tag
-| EDesugarDuplicateBinderName name ->
+| DesugarDuplicateBinderName name ->
 	F.fprintf ppf "%s: %a"
 		"duplicate binder name: "
 		Name.Var.pp_print name
-| EDesugarDataAndData ->
+| DesugarDataAndData ->
 	F.pp_print_string ppf "conjunction of two data patterns"
 
-| EElabApplyNonFunction typ ->
+| ElabApplyNonFunction typ ->
 	F.fprintf ppf "@[<4>%s@ %a@]"
 		"attempt to apply non-function of inferred type"
 		(Pretty.pp_print_term 0) typ
-| EElabNonInferablePatt ->
+| ElabNonInferablePatt ->
 	F.pp_print_string ppf "non-inferable pattern"
 
 (* TODO *)
-| EElabUnifyFail _             -> F.pp_print_string ppf "ErrUnifyFail"
-| EElabCantInferData           -> F.pp_print_string ppf "ErrCantInferData"
-| EElabNoLetAnnot _            -> F.pp_print_string ppf "ErrNoLetAnnot"
-| EElabNoBinderAnnot _         -> F.pp_print_string ppf "ErrNoBinderAnnot"
-| EElabUnannotImplicitIsType _ -> F.pp_print_string ppf "ErrUnannotImplicitIsType"
-| EElabDataPattRefutable       -> F.pp_print_string ppf "ErrDataPattRefutable"
-| EElabBinderCycle _           -> F.pp_print_string ppf "ErrBinderCycle"
-| EElabArityMismatch           -> F.pp_print_string ppf "ErrArityMismatch"
-| EElabUnboundVar _            -> F.pp_print_string ppf "ErrUnboundVar"
-| EElabExpectedDataType _      -> F.pp_print_string ppf "ErrExpectedDataType"
-| EElabFnArityMismatch         -> F.pp_print_string ppf "ErrFnArityMismatch"
-| EElabFnPlicityMismatch       -> F.pp_print_string ppf "ErrFnPlicityMismatch"
-| EElabUnexpectedCtor _        -> F.pp_print_string ppf "ErrUnexpectedCtor"
-| EElabDuplicateName _         -> F.pp_print_string ppf "ErrDuplicateName"
-(*| EElabExpectedFnType _        -> "ErrExpectedFnType"*)
+| ElabUnifyFail _             -> F.pp_print_string ppf "ErrUnifyFail"
+| ElabCantInferData           -> F.pp_print_string ppf "ErrCantInferData"
+| ElabNoLetAnnot _            -> F.pp_print_string ppf "ErrNoLetAnnot"
+| ElabNoBinderAnnot _         -> F.pp_print_string ppf "ErrNoBinderAnnot"
+| ElabUnannotImplicitIsType _ -> F.pp_print_string ppf "ErrUnannotImplicitIsType"
+| ElabDataPattRefutable       -> F.pp_print_string ppf "ErrDataPattRefutable"
+| ElabBinderCycle _           -> F.pp_print_string ppf "ErrBinderCycle"
+| ElabArityMismatch           -> F.pp_print_string ppf "ErrArityMismatch"
+| ElabUnboundVar _            -> F.pp_print_string ppf "ErrUnboundVar"
+| ElabExpectedDataType _      -> F.pp_print_string ppf "ErrExpectedDataType"
+| ElabFnArityMismatch         -> F.pp_print_string ppf "ErrFnArityMismatch"
+| ElabFnPlicityMismatch       -> F.pp_print_string ppf "ErrFnPlicityMismatch"
+| ElabUnexpectedCtor _        -> F.pp_print_string ppf "ErrUnexpectedCtor"
+| ElabDuplicateName _         -> F.pp_print_string ppf "ErrDuplicateName"
+(*| ElabExpectedFnType _        -> "ErrExpectedFnType"*)
 
 exception Exn of error
 
diff --git a/lexer.mll b/lexer.mll
@@ -1,13 +1,13 @@
 {
 open Node
-open Error
+module E = Error
 open Parser
 
 let abort lexbuf e =
 	let beg_pos = Lexing.lexeme_start_p lexbuf in
 	let end_pos = Lexing.lexeme_end_p lexbuf in
 	let loc = Loc.of_positions beg_pos end_pos in
-	Error.abort loc e
+	E.abort loc e
 }
 
 let ascii_horizontal = ['\t' ' '-'~']
@@ -31,9 +31,10 @@ let greek = ugreek | lgreek | lgreekalt
 
 let comment = '\\' '\\' (ascii_horizontal | greek)*
 
+(* Keep in sync with non_start and non_cont in name.ml. *)
 let ident_start = latin | greek | '_'
 let ident_cont  = latin | greek | '_' | dnumeral | '\'' | '"'
-let ident_quote = ascii_horizontal | greek
+let ident_quote = (ascii_horizontal # '`') | greek
 let name = (ident_start ident_cont* as x) | '`' (ident_quote* as x) '`'
 let tag = (ident_cont+ as x) | '`' (ident_quote* as x) '`'
 
@@ -110,15 +111,15 @@ rule token = parse
 	if Z.fits_int z then
 		INDEXED_NAME (x, Z.to_int z)
 	else
-		abort lexbuf ELexerNameIndexTooBig
+		abort lexbuf E.LexerNameIndexTooBig
 }
 | name { NAME x }
 
 | number as n { NAT (Z.of_string n) }
 | number invalid_number_terminator
-	{ abort lexbuf ELexerInvalidNumberTerminator }
+	{ abort lexbuf E.LexerInvalidNumberTerminator }
 
-| _ { abort lexbuf ELexerNoRule }
+| _ { abort lexbuf E.LexerNoRule }
 
 {
 }
diff --git a/main.ml b/main.ml
@@ -11,7 +11,6 @@ let buf = Lexing.from_string "\
 	five Nat 0 (fn n => n + 1)\n\
 "
 
-
 (*
 let buf = Lexing.from_string "\
 	f := fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat =>\
@@ -43,7 +42,8 @@ let buf = Lexing.from_string "\
 
 (*
 let buf = Lexing.from_string "\
-	(fn => Nat) ()\
+	`` := () : #();\
+	(fn => Nat) ``\
 "
 *)
 
@@ -89,11 +89,14 @@ let (internal, ty) = try
 	let abstract = Desugar.term concrete in
 	Elab.infer' ctx abstract
 with Error.Exn e ->
-	print Error.pp_print_error e;
+	print Error.pp_print e;
 	exit 1
 
 let internal' = Quote.quote ctx.env (Eval.eval ctx.env internal)
 
 let () =
 	print (Pretty.pp_print_term 0) internal;
+	print Format.pp_print_string "\
+	----------------------------------------\
+	----------------------------------------";
 	print (Pretty.pp_print_term 0) internal'
diff --git a/name.ml b/name.ml
@@ -1,3 +1,15 @@
+let non_start c = false 
+	|| ('0' <= c && c <= '9')
+	|| c = '\''
+	|| c = '"'
+
+let non_cont c = false
+	|| c < '\''
+	|| ('\'' < c && c < '0')
+	|| ('9' < c && c < 'A')
+	|| ('Z' < c && c < '_')
+	|| ('z' < c && c < '\x7F')
+
 module Var = struct
 	type var = Of of string
 	type t = var
@@ -11,8 +23,16 @@ module Var = struct
 
 	module Set = Set.Make(Ord)
 
-	(* TODO: Doesn't handled backticked names. *)
-	let pp_print ppf (Of s) = Format.fprintf ppf "%s" s
+	let requires_quotes (Of s) = false
+		|| String.length s = 0
+		|| non_start s.[0]
+		|| String.exists non_cont s
+
+	let pp_print ppf (Of s as name) =
+		if requires_quotes name then
+			Format.fprintf ppf "`%s`" s
+		else
+			Format.fprintf ppf "%s" s
 end
 
 module Ctor = struct
@@ -28,7 +48,14 @@ module Ctor = struct
 
 	let equal (Of x) (Of y) = String.equal x y
 
-	(* TODO: Doesn't handled backticked names. *)
-	let pp_print ppf (Of s) = Format.fprintf ppf "%@%s" s
+	let requires_quotes (Of s) = false
+		|| String.length s = 0
+		|| String.exists non_cont s
+
+	let pp_print ppf (Of s as name) =
+		if requires_quotes name then
+			Format.fprintf ppf "%@`%s`" s
+		else
+			Format.fprintf ppf "%@%s" s
 end
 
diff --git a/parser.mly b/parser.mly
@@ -1,7 +1,7 @@
 %{
 open Util
 open Node
-open Error
+module E = Error
 module C = Concrete
 
 (* To avoid reduce-reduce conflicts, we need to distinguish between raw
@@ -56,8 +56,8 @@ let rec term {loc; data = e} = loc @$ match e with
 | Iff (c, t) -> C.Iff (c, term t)
 | Annot (a, b) -> C.Annot (term a, term b)
 | BinOp (a, o, b) -> C.BinOp (term a, o, term b)
-| Or _ -> abort loc EParserInvalidTerm
-| And _ -> abort loc EParserInvalidTerm
+| Or _ -> E.abort loc E.ParserInvalidTerm
+| And _ -> E.abort loc E.ParserInvalidTerm
 | App (f, len, args) -> C.App (term f, Array.map term (to_array len args))
 | Fn (len, params, body) -> C.Fn (to_array len params, term body)
 | FnType (len, doms, cod) -> C.FnType (to_array len doms, term cod)
@@ -67,7 +67,7 @@ let rec term {loc; data = e} = loc @$ match e with
 | TupleType (len, doms) -> C.TupleType (to_array len doms)
 | Unit -> C.Unit
 | Nat n -> C.Nat n
-| Underscore -> abort loc EParserInvalidTerm
+| Underscore -> E.abort loc E.ParserInvalidTerm
 | IndexedVar (x, i) -> C.IndexedVar (x, i)
 | Var x -> C.Var x
 | Paren e -> C.Paren (term e)
@@ -88,14 +88,14 @@ and patt {loc; data = e} = loc @$ match e with
 | Paren p -> C.PParen (patt p)
 | Let _ | Seq _ | Match _ | If _ | Iff _ | BinOp _ | App _
 | Fn _ | FnType _ | VariantType _ | TupleType _ | IndexedVar _ ->
-	abort loc EParserInvalidPatt
+	E.abort loc E.ParserInvalidPatt
 
 let loc_of i =
 	let beg_pos = Parsing.rhs_start_pos i in
 	let end_pos = Parsing.rhs_end_pos i in
 	Loc.of_positions beg_pos end_pos
 
-let loc =
+let loc () =
 	let beg_pos = Parsing.symbol_start_pos () in
 	let end_pos = Parsing.symbol_end_pos () in
 	Loc.of_positions beg_pos end_pos
@@ -137,9 +137,9 @@ start: expr0 EOF { term $1 }
 expr0: (* Definitions and sequencing *)
 	| definer_list SEMICOLON expr0 {
 		let (len, lst) = $1 in
-		loc @$ Let (len, lst, $3)
+		loc () @$ Let (len, lst, $3)
 	}
-	| expr1 SEMICOLON expr0 { loc @$ Seq ($1, $3) }
+	| expr1 SEMICOLON expr0 { loc () @$ Seq ($1, $3) }
 	| expr1 { $1 }
 
 expr1: (* Control flow and functions *)
@@ -148,48 +148,48 @@ expr1: (* Control flow and functions *)
 	 * `$(x match ...)` for conditional compilation. *)
 	| expr2 MATCH LBRACE case_list RBRACE {
 		let (len, lst) = $4 in
-		loc @$ Match($1, len, lst)
+		loc () @$ Match($1, len, lst)
 	}
-	| IF cond THEN expr1 ELSE expr1 { loc @$ If ($2, $4, $6) }
-	| IFF cond DO expr1 { loc @$ Iff ($2, $4) }
+	| IF cond THEN expr1 ELSE expr1 { loc () @$ If ($2, $4, $6) }
+	| IFF cond DO expr1 { loc () @$ Iff ($2, $4) }
 	| FN param_list DOUBLE_ARROW expr1 {
 		let (len, lst) = $2 in
-		loc @$ Fn (len, lst, $4)
+		loc () @$ Fn (len, lst, $4)
 	}
 	| expr2 { $1 }
 
 expr2: (* Type annotations (right-associative) *)
-	| expr3 COLON expr2 { loc @$ Annot ($1, $3) }
+	| expr3 COLON expr2 { loc () @$ Annot ($1, $3) }
 	| expr3 { $1 }
 
 expr3: (* Function arrow (right-associative) *)
 	| expr6 SINGLE_ARROW expr3 {
 		let dom = loc_of 1 @$ C.ExplicitDomain (term $1) in
-		loc @$ FnType (1, [dom], $3)
+		loc () @$ FnType (1, [dom], $3)
 	}
 	| LBRACK domain_list RBRACK SINGLE_ARROW expr3 {
 		let (len, lst) = $2 in
 		if len = 0 then
-			abort (loc_of 2) EParserEmptyDomain
+			E.abort (loc_of 2) E.ParserEmptyDomain
 		else
-			loc @$ FnType (len, lst, $5)
+			loc () @$ FnType (len, lst, $5)
 	}
 	| expr4 { $1 }
 
 expr4: expr4a { $1 } (* Binary operators and relations *)
 
 expr4a: (* Logical OR (left-associative) *)
-	| expr4a PIPE2 expr4b { loc @$ BinOp ($1, C.LAnd, $3) }
+	| expr4a PIPE2 expr4b { loc () @$ BinOp ($1, C.LAnd, $3) }
 	| expr4b { $1 }
 
 expr4b: (* Logical AND (left-associative) *)
-	| expr4b AMPERSAND2 expr4c { loc @$ BinOp ($1, C.LOr, $3) }
+	| expr4b AMPERSAND2 expr4c { loc () @$ BinOp ($1, C.LOr, $3) }
 	| expr4c { $1 }
 
 expr4c: (* Relations (non-associative) *)
 	(* TODO: Chaining relations? I.e., ability to write x < y < z instead of
 	 * x < y && y < z. *)
-	| expr4d rel expr4d { loc @$ BinOp ($1, $2, $3) }
+	| expr4d rel expr4d { loc () @$ BinOp ($1, $2, $3) }
 	| expr4d { $1 }
 rel:
 	| LT { C.Lt }
@@ -200,32 +200,32 @@ rel:
 	| NE { C.Ne }
 
 expr4d: (* Additive operators (left-associative) *)
-	| expr4d0 addop expr4e { loc @$ BinOp ($1, $2, $3) }
-	| expr4d1 PIPE expr4e { loc @$ Or ($1, $3) }
+	| expr4d0 addop expr4e { loc () @$ BinOp ($1, $2, $3) }
+	| expr4d1 PIPE expr4e { loc () @$ Or ($1, $3) }
 	| expr4e { $1 }
 addop:
 	| PLUS  { C.Add }
 	| MINUS { C.Sub }
 expr4d0:
-	| expr4d0 addop expr4e { loc @$ BinOp ($1, $2, $3) }
+	| expr4d0 addop expr4e { loc () @$ BinOp ($1, $2, $3) }
 	| expr4e { $1 }
 expr4d1:
-	| expr4d1 PIPE expr4e { loc @$ Or ($1, $3) } 
+	| expr4d1 PIPE expr4e { loc () @$ Or ($1, $3) } 
 	| expr4e { $1 }
 
 expr4e: (* Multiplicative operators (left-associative) *)
-	| expr4e0 mulop expr4f { loc @$ BinOp ($1, $2, $3) }
-	| expr4e1 AMPERSAND expr4f { loc @$ And ($1, $3) }
+	| expr4e0 mulop expr4f { loc () @$ BinOp ($1, $2, $3) }
+	| expr4e1 AMPERSAND expr4f { loc () @$ And ($1, $3) }
 	| expr4f { $1 }
 mulop:
 	| ASTERISK { C.Mul }
 	| SLASH    { C.Div }
 	| PERCENT  { C.Mod }
 expr4e0:
-	| expr4e0 mulop expr4f { loc @$ BinOp ($1, $2, $3) }
+	| expr4e0 mulop expr4f { loc () @$ BinOp ($1, $2, $3) }
 	| expr4f { $1 }
 expr4e1:
-	| expr4e1 AMPERSAND expr4f { loc @$ And ($1, $3) }
+	| expr4e1 AMPERSAND expr4f { loc () @$ And ($1, $3) }
 	| expr4f { $1 }
 
 expr4f: expr5 { $1 }
@@ -233,36 +233,36 @@ expr4f: expr5 { $1 }
 expr5:
 	| expr6 expr6 expr6_apposition_list {
 		let (len, lst) = $3 in
-		loc @$ App ($1, len + 1, $2 :: lst)
+		loc () @$ App ($1, len + 1, $2 :: lst)
 	}
 	| ctor_name expr6_apposition_list {
 		let (len, lst) = $2 in
-		loc @$ Variant ($1, len, lst)
+		loc () @$ Variant ($1, len, lst)
 	}
 	| expr6 { $1 }
 
 expr6:
-	| UNDERSCORE { loc @$ Underscore }
+	| UNDERSCORE { loc () @$ Underscore }
 	| indexed_var_name {
 		let (x, i) = $1 in
-		loc @$ IndexedVar (x, i)
+		loc () @$ IndexedVar (x, i)
 	}
-	| var_name { loc @$ Var $1 }
-	| NAT { loc @$ Nat $1 }
+	| var_name { loc () @$ Var $1 }
+	| NAT { loc () @$ Nat $1 }
 	| HASH_LBRACE ctor_list RBRACE {
 		let (len, lst) = $2 in
-		loc @$ VariantType (len, lst)
+		loc () @$ VariantType (len, lst)
 	}
 	| HASH_LPAREN domain_list RPAREN {
 		let (len, lst) = $2 in
-		loc @$ TupleType (len, lst)
+		loc () @$ TupleType (len, lst)
 	}
 	| LPAREN expr1 COMMA expr1_comma_list RPAREN {
 		let (len, lst) = $4 in
-		loc @$ Tuple (len + 1, $2 :: lst)
+		loc () @$ Tuple (len + 1, $2 :: lst)
 	}
-	| LPAREN RPAREN { loc @$ Unit }
-	| LPAREN expr0 RPAREN { loc @$ Paren $2 }
+	| LPAREN RPAREN { loc () @$ Unit }
+	| LPAREN expr0 RPAREN { loc () @$ Paren $2 }
 
 expr1_comma_list:
 	| expr1 COMMA expr1_comma_list { cons $1 $3 }
@@ -274,57 +274,57 @@ expr6_apposition_list:
 	| { (0, []) }
 
 definer:
-	| expr2 COLON_EQ expr1 { loc @$ C.Definer (patt $1, term $3) }
-	| expr2 COLON_EQ REC expr1 { loc @$ C.RecDefiner (patt $1, term $4) }
+	| expr2 COLON_EQ expr1 { loc () @$ C.Definer (patt $1, term $3) }
+	| expr2 COLON_EQ REC expr1 { loc () @$ C.RecDefiner (patt $1, term $4) }
 definer_list:
 	| definer COMMA definer_list { cons $1 $3 }
 	| definer { (1, [$1]) }
 
 case:
-	| expr2 DOUBLE_ARROW expr1 { loc @$ C.Case (patt $1, term $3) }
+	| expr2 DOUBLE_ARROW expr1 { loc () @$ C.Case (patt $1, term $3) }
 case_list:
 	| case COMMA case_list { cons $1 $3 }
 	| case { (1, [$1]) }
 	| { (0, []) }
 
 cond:
-	| expr1 { loc @$ C.TrueCond (term $1) }
-	| expr2 COLON_EQ expr1 { loc @$ C.PattCond (patt $1, term $3) }
+	| expr1 { loc () @$ C.TrueCond (term $1) }
+	| expr2 COLON_EQ expr1 { loc () @$ C.PattCond (patt $1, term $3) }
 
 param:
-	| expr2 { loc @$ C.Param (Plicity.Ex, patt $1) }
-	| QUESTION expr2 { loc @$ C.Param (Plicity.Im, patt $2) }
+	| expr2 { loc () @$ C.Param (Plicity.Ex, patt $1) }
+	| QUESTION expr2 { loc () @$ C.Param (Plicity.Im, patt $2) }
 param_list:
 	| param COMMA param_list { cons $1 $3 }
 	| param { (1, [$1]) }
 	| { (0, []) }
 
 domain:
-	| expr3 { loc @$ C.ExplicitDomain (term $1) }
-	| QUESTION expr3 { loc @$ C.ImplicitTypeDomain (patt $2) }
-	| expr3 COLON expr2 { loc @$ C.AnnotDomain (Plicity.Ex, patt $1, term $3) }
-	| QUESTION expr3 COLON expr2 { loc @$ C.AnnotDomain (Plicity.Im, patt $2, term $4) }
+	| expr3 { loc () @$ C.ExplicitDomain (term $1) }
+	| QUESTION expr3 { loc () @$ C.ImplicitTypeDomain (patt $2) }
+	| expr3 COLON expr2 { loc () @$ C.AnnotDomain (Plicity.Ex, patt $1, term $3) }
+	| QUESTION expr3 COLON expr2 { loc () @$ C.AnnotDomain (Plicity.Im, patt $2, term $4) }
 domain_list:
 	| domain COMMA domain_list { cons $1 $3 }
 	| domain { (1, [$1]) }
 	| { (0, []) }
 
 ctor_name:
-	| TAG { loc @$ Name.Ctor.Of $1 }
+	| TAG { loc () @$ Name.Ctor.Of $1 }
 
 indexed_var_name:
 	| INDEXED_NAME {
 		let (x, i) = $1 in
-		(loc @$ Name.Var.Of x, i)
+		(loc () @$ Name.Var.Of x, i)
 	}
 
 var_name:
-	| NAME { loc @$ Name.Var.Of $1 }
+	| NAME { loc () @$ Name.Var.Of $1 }
 
 ctor:
 	| ctor_name domain_list {
 		let (len, lst) = $2 in
-		loc @$ Ctor ($1, len, lst)
+		loc () @$ Ctor ($1, len, lst)
 	}
 ctor_list:
 	| ctor SEMICOLON ctor_list { cons $1 $3 }
diff --git a/pretty.ml b/pretty.ml
@@ -6,8 +6,8 @@ let rec pp_print_with_parens
 : 'a. int -> int -> F.formatter -> ('a, F.formatter, unit) format -> 'a
 = fun m c ppf ->
 	if c < m then begin
-		F.fprintf ppf "(@[<h>";
-		F.kfprintf (fun ppf -> F.fprintf ppf "@])") ppf
+		F.fprintf ppf "(";
+		F.kfprintf (fun ppf -> F.fprintf ppf ")") ppf
 	end else
 		F.fprintf ppf