dtlc

elab.ml (29470B)

---

 open Util
 open Node
 module E = Error
 open Eval
 open Quote
 open Unify
 module A = Abstract
 module I = Internal
 module V = Value
 
 (*module R = Porig.NoneOneTons*)
 
 exception BlockedOnFuture of Uniq.uniq * int * Name.Var.t
 
 type mode =
 | Infer
 | Check of V.value
 
 (* A clause is a conjunction of tests, and we view an array of clauses
  * disjunctively. The casei:int is the index of the body that the match
  * expression evaluates to if the clause matches. *)
 type clause = {
 	tests: I.data_discriminant Uniq.UniqMap.t;
 	casei: int;
 }
 
 (* Convention: An elaboration-related function can have two versions, one whose
  * 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? *)
 
 let add_name'
 : Name.Var.Set.t -> Name.Var.t node -> Name.Var.Set.t * Name.Var.t
 = fun name_set {loc; data = name} ->
 	if Name.Var.Set.mem name name_set then
 		E.abort loc @@ E.ElabDuplicateName name
 	else
 		(Name.Var.Set.add name name_set, name)
 
 let rec assign_patt
 : V.context -> I.patt -> V.value -> Uniq.uniq -> V.context
 = fun ctx {names; disc} vtyp var ->
 	let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb var) in
 
 	match disc with
 	| I.DWild _ -> ctx
 	| I.DData {tag; tagi; subpatts; datatype} ->
 		let {I.binders; I.order} = datatype.ctors.(tagi) in
 		let arity = Array.length subpatts in
 		let subvars = Uniq.fresh arity in
 		let data = V.Data {
 			tag;
 			tagi;
 			args = Array.init arity (fun i -> V.Arb (Uniq.get subvars i));
 			(* datatype is formed in a context without subvars bound. *)
 			datatype_clo = (ctx.env, datatype);
 		} in
 		let ctx = Ctx.bind ctx subvars in
 		let ctx = Ctx.define ctx var data in
 
 		(* Assign each subpattern in type-dependency order, because that's the
 		 * order that check_disc' elaborates subpatterns in. The order matters
 		 * here, because assign_patt binds variables. *)
 		let ctx' = ref ctx in
 		for i = 0 to arity - 1 do
 			let j = order.(i) in
 			let subtyp = I.disc_type binders.(j).patt.disc in
 			let vsubtyp = eval ctx.env subtyp in
 			ctx' := assign_patt !ctx' subpatts.(j) vsubtyp (Uniq.get subvars j)
 		done;
 
 		!ctx'
 
 (* Elaborate explicits to Some and implicits to None. *)
 let elaborate_args'
 : 'a. Loc.t -> 'a array -> I.binder array -> 'a option array
 = fun loc explicit_args binders ->
 	let arity = Array.length binders in
 	let explicit_count = Array.length explicit_args in
 	let implicit_count = ref 0 in
 
 	let args = Array.make arity garbage in
 	for i = 0 to arity - 1 do
 		(* TODO: Once we allow passing an implicit argument explicitly,
 		 * this logic will need to change a bit. *)
 		args.(i) <- match binders.(i).plicity with
 		| Plicity.Ex ->
 			let j = i - !implicit_count in
 			begin if explicit_count <= j then
 				E.abort loc E.ElabArityMismatch
 			end;
 			Some (explicit_args.(j))
 		| Plicity.Im ->
 			incr implicit_count;
 			None
 	done;
 
 	(* We had enough explicit args, but now ensure we don't have too many. *)
 	begin if explicit_count > arity - !implicit_count then
 		E.abort loc E.ElabArityMismatch
 	end;
 
 	args
 
 let rec infer
 : V.context -> A.term -> (I.term * V.value, E.error) result
 = fun ctx t ->
 	try Ok (infer' ctx t) with
 	| E.Exn e -> Error e
 
 and infer'
 : V.context -> A.term -> I.term * V.value
 = fun ctx t -> elaborate' ctx t Infer
 
 and check
 : V.context -> A.term -> V.value -> (I.term, E.error) result
 = fun ctx t vtyp ->
 	try Ok (check' ctx t vtyp) with
 	| E.Exn e -> Error e
 
 and check'
 : V.context -> A.term -> V.value -> I.term
 = fun ctx t vtyp ->
 	let (t, _) = elaborate' ctx t (Check (force ctx.env vtyp)) in
 	t
 
 and elaborate
 : V.context -> A.term -> mode -> (I.term * V.value, E.error) result
 = fun ctx t mode ->
 	try Ok (elaborate' ctx t mode) with
 	| E.Exn e -> Error e
 
 and elaborate'
 : V.context -> A.term -> mode -> I.term * V.value
 = fun ctx {loc; data = t} mode -> match t, mode with
 | A.Let (definers, body), mode ->
 	let (ctx, definers) = infer_definers' ctx definers in
 	let (body, vtyp) = elaborate' ctx body mode in
 	(I.Let (definers, body), vtyp)
 
 | A.Match _, Infer -> E.abort loc E.ElabCantInferMatch
 
 | A.Match (scrutinee, cases), Check vtyp ->
 	(elaborate_match' ctx loc scrutinee cases vtyp, vtyp)
 
 | A.Annot (tm, typ), Infer ->
 	let typ = check' ctx typ Std.v_Type in
 	let vtyp = eval ctx.env typ in
 	let tm = check' ctx tm vtyp in
 	(tm, vtyp)
 
 | A.App (fn, explicit_args), Infer ->
 	let (fn, vtyp) = infer' ctx fn in
 	begin match force ctx.env vtyp with
 	| V.FnTypeClosure (clo, {multibinder; term = codomain}) ->
 		let (args, clo) = check_args' ctx loc explicit_args clo multibinder in
 		let vcodomain = eval clo codomain in
 		(I.App (fn, args), vcodomain)
 	| vtyp -> E.abort loc @@ E.ElabApplyNonFunction (quote ctx.env vtyp)
 	end
 
 | A.Fn {data = {multibinder = params; term = body}; _}, Infer ->
 	let (ctx', multibinder) = infer_multibinder' ctx loc params in
 	let (body, vcodomain) = infer' ctx' body in
 	let codomain = quote ctx'.env vcodomain in
 	let fn = I.Fn {multibinder; term = body} in
 	let vfntype = V.FnTypeClosure (ctx.env, {multibinder; term = codomain}) in
 	(fn, vfntype)
 
 | A.Fn {data = {multibinder = {data = params; _}; term = body}; _},
 		Check (V.FnTypeClosure (clo, fntype) as vfntype) ->
 	let {I.multibinder = {binders = domains; order}; I.term = codomain} = fntype in
 
 	begin if Array.length params <> Array.length domains then
 		E.abort loc E.ElabFnArityMismatch
 	end;
 	let arity = Array.length params in
 
 	let vars = Uniq.fresh arity in
 	let ctx = Ctx.bind ctx vars in
 	let clo = Env.bind clo vars in
 
 	let ctx = ref ctx in
 	let name_set = ref Name.Var.Set.empty in
 	let params' = Array.make arity garbage in
 	for i = 0 to arity - 1 do
 		let j = order.(i) in
 		let param = params.(j).data in
 		let domain = domains.(j) in
 
 		begin if param.plicity <> domain.plicity then
 			E.abort loc E.ElabFnPlicityMismatch
 		end;
 		let plicity = param.plicity in
 
 		let vtyp = eval clo (I.disc_type domain.patt.disc) in
 		let typ = quote !ctx.env vtyp in
 		let (name_set', names) = check_irrefutable_patt'
 			!ctx !name_set param.patt vtyp in
 		name_set := name_set';
 
 		let (ctx', _) = Ctx.assign !ctx names vtyp (V.Arb (Uniq.get vars j)) in
 		ctx := ctx';
 		params'.(j) <- {I.plicity; I.patt = {names; disc = I.DWild typ}}
 	done;
 
 	let vcodomain = eval clo codomain in
 	let body = check' !ctx body vcodomain in
 
 	(I.Fn {multibinder = {binders = params'; order}; term = body}, vfntype)
 
 | A.Fn _, Check vtyp ->
 	let typ = quote ctx.env vtyp in
 	E.abort loc @@ E.ElabExpectedFnType typ
 
 | A.FnType {data = {multibinder = domains; term = codomain}; _}, Infer ->
 	let (ctx, multibinder) = infer_multibinder' ctx loc domains in
 	let codomain = check' ctx codomain Std.v_Type in
 	(I.FnType {multibinder; term = codomain}, Std.v_Type)
 
 | A.Data _, Infer -> E.abort loc E.ElabCantInferData
 
 | A.Data ({data = tag; _}, explicit_args),
 		Check (V.DataTypeClosure (clo, datatype) as vdatatype) ->
 	begin match Name.Tag.Map.find_opt tag datatype.names with
 	| Some tagi ->
 		let (args, _) = check_args' ctx loc explicit_args clo
 			datatype.ctors.(tagi) in
 		let datatype = shift_datatype ctx.env clo datatype in
 		(I.Data {tag; tagi; args; datatype}, vdatatype)
 	| None -> E.abort loc @@ E.ElabUnexpectedTag tag
 	end
 
 | A.Data _, Check vtyp ->
 	let typ = quote ctx.env vtyp in
 	E.abort loc @@ E.ElabExpectedDataType typ
 
 | A.TupleData args, Infer ->
 	let arity = Array.length args in
 
 	(* Only needed so that the indices in the type are correct. *)
 	let vars = Uniq.fresh arity in
 	let clo = Env.bind ctx.env vars in
 
 	let args' = Array.make arity garbage in
 	let binders = Array.make arity garbage in
 	for i = 0 to arity - 1 do
 		let (arg', vtyp) = infer' ctx args.(i) in
 		args'.(i) <- arg';
 		let typ = quote clo vtyp in
 		binders.(i) <- {
 			I.plicity = Plicity.Ex;
 			I.patt = {
 				names = [||];
 				disc = DWild typ;
 			};
 		}
 	done;
 
 	let tag = Name.Tag.Of (string_of_int arity) in
 	let datatype = {
 		I.ctors = [|{binders; order = Array.init arity Fun.id}|];
 		I.names = Name.Tag.Map.singleton tag 0;
 	} in
 	(I.Data {tag; tagi = 0; args = args'; datatype},
 		V.DataTypeClosure (clo, datatype))
 
 | A.TupleData args, Check vtyp ->
 	(* XXX: Kinda hacky. *)
 	let tag = Name.Tag.Of (string_of_int (Array.length args)) in
 	elaborate' ctx (loc @$ A.Data (Loc.Nowhere @$ tag, args)) (Check vtyp)
 
 | A.DataType ctors, Infer ->
 	let next = ref 0 in
 	let ctors' = Array.make (Name.Tag.Map.cardinal ctors) garbage in
 	let go binders =
 		let i = !next in
 		incr next;
 		let (_, multibinder) = infer_multibinder' ctx loc binders in
 		ctors'.(i) <- multibinder;
 		i in
 	let names = Name.Tag.Map.map go ctors in
 	(I.DataType {ctors = ctors'; names}, Std.v_Type)
 
 | A.Nat n, Infer -> (I.Nat n, Std.v_Nat)
 
 | A.Var ({data = name; _}, i), Infer ->
 	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 -> E.abort loc @@ E.ElabUnboundVar (name, i)
 	end
 
 | A.Builtin b, Infer -> (I.Builtin b, Std.infer b)
 
 | (A.Annot _ | A.App _ | A.FnType _ | A.DataType _ | A.Nat _
 		| A.Var _ | A.Builtin _) as t, Check vexpected ->
 	let (t, vinferred) = infer' ctx {loc; data = t} in
 	begin try unify ctx.env vexpected vinferred with
 	| UnifyFail -> 
 		let expected = quote ctx.env vexpected in
 		let inferred = quote ctx.env vinferred in
 		E.abort loc @@ E.ElabUnifyFail (expected, inferred)
 	end;
 	(t, vexpected)
 
 (* Check the given explicit arguments against the given multibinder.
  * Return the elaborated terms and the multibinder's closure extended with
  * fresh variables defined to the arguments' values. *)
 and check_args'
 : V.context -> Loc.t -> A.term array -> V.environment -> I.multibinder
 	-> I.term array * V.environment
 = fun ctx loc explicit_args clo {binders; order} ->
 	let arity = Array.length binders in
 	let args = elaborate_args' loc explicit_args binders in
 
 	let vars = Uniq.fresh arity in
 	let clo = Env.bind clo vars in
 
 	let args' = Array.make arity garbage in
 	let clo = ref clo in
 	for i = 0 to arity - 1 do
 		let j = order.(i) in
 		let vtyp = eval !clo (I.disc_type binders.(j).patt.disc) in
 		let arg = match args.(j) with
 		| Some arg -> check' ctx arg vtyp
 		| None -> no_impl "implicit args" in
 		args'.(j) <- arg;
 		let varg = eval ctx.env arg in
 		clo := Env.define !clo (Uniq.get vars j) varg
 	done;
 
 	(args', !clo)
 
 (* Infer the given definers. Return the elaborated definers and the context
  * extended with fresh variables for the definers defined to each rhs. *)
 (* TODO: We need to check for circularity. Idea for algorithm: Have elaboration
  * routines track not only variable usage, but also the least "delay"
  * asssociated with each variable usage. E.g., a variable x uses x with delay 0
  * (it's used immediately), a function uses the variables used in its body with
  * their delay + 1, and a β-redex uses the variables in the lambda with their
  * delay - 1. *)
 and infer_definers'
 : V.context -> A.definer array -> V.context * I.definer array
 = fun ctx definers ->
 	let ndefiners = Array.length definers in
 
 	(* To simplify context handling, we work in a weakened contexted from the
 	 * very beginning, even though the lhs of each definer is not allowed to
 	 * refer to these variables. *)
 	let vars = Uniq.fresh ndefiners in
 	let ctx = Ctx.bind ctx vars in
 
 	match definers with
 	| [||] -> impossible "Elab.infer_definers': no definers"
 
 	(* Single non-recursive definer. These are handled specially, because
 	 * the type annotation on the lhs is optional. *)
 	(* TODO: Maybe we should make this distinction in internal syntax (maybe
 	 * abstract syntax as well). I.e., Let vs LetRec. *)
 	| [|{loc; data = {recursive = false; lhs; rhs}}|] ->
 		let (names, rhs, vtyp) =
 			(* First try to infer from lhs (and check rhs). *)
 			match infer_irrefutable_patt ctx Name.Var.Set.empty lhs with
 			| Ok (_, names, vtyp) ->
 				let rhs = check' ctx rhs vtyp in
 				(names, rhs, vtyp)
 			| 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 Name.Var.Set.empty lhs vtyp in
 				(names, rhs, vtyp)
 			| Error e -> E.abort e.loc e.data in
 		let typ = quote ctx.env vtyp in
 		(* XXX: vrhs doesn't need to be a RefClo. We could eagerly evaluate it,
 		 * or add some other mechanism for laziness (like glued eval). *)
 		let vrhs = V.RefClo (ref ctx.env, rhs) in
 		let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb (Uniq.get vars 0)) in
 		let ctx = Ctx.define ctx (Uniq.get vars 0) vrhs in
 		(ctx, [|{names; rhs; typ}|])
 
 	(* Single recursive definer or many mutually-recursive definers. In either
 	 * case, a type annotation on the lhs is mandatory. Probably, we could use
 	 * meta-variables/unification to permit omitting annotations in some cases
 	 * (e.g., like OCaml does with let rec ... and ...), but we generally try
 	 * to avoid meta-variables/unification, because they're unpredictable;
 	 * inference should only rely on local information. *)
 	| definers ->
 		(* Infer each lhs (in the original context, because definitions are
 		 * not allowed to have mutually dependent types), and make all
 		 * assignments. We later set the active flag to false on assignments
 		 * for non-recusive definers, so that the rhs of non-recursive definers
 		 * can not access their own assignment. *)
 		(* TODO: Actually, we should allow definer types to depend on each
 		 * other in a well-ordered fashion, because this allows
 		 * induction-recursion. *)
 		let ctx_with_asns = ref ctx in
 		let name_set = ref Name.Var.Set.empty in
 		let namess = Array.make ndefiners garbage in
 		let asns = Array.make ndefiners garbage in
 		for i = 0 to ndefiners - 1 do
 			let {loc; data = {A.lhs; _}} = definers.(i) in
 			match infer_irrefutable_patt ctx !name_set lhs with
 			| Ok (name_set', names, vtyp) ->
 				name_set := name_set';
 				namess.(i) <- names;
 				let (ctx_with_asns', asn) = Ctx.assign !ctx_with_asns
 					names vtyp (V.Arb (Uniq.get vars i)) in
 				ctx_with_asns := ctx_with_asns';
 				asns.(i) <- asn
 			| 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
 
 		(* Check each rhs with the appropriate assignments active, but not any
 		 * definitions. This means that each definition is "opaque" during the
 		 * elaboration of each rhs, i.e., the let-bound variables behave like
 		 * fn-bound variables. It's hard to get around this. It might be useful
 		 * to elaborate each rhs with every other rhs defined in context, but
 		 * that would require every rhs to already be elaborated! Of course,
 		 * after elaboration each rhs can see every other rhs, and we achieve
 		 * by lazily evaluating each rhs using V.Rec. *)
 		let env = ref ctx.env in
 		let definers' = Array.make ndefiners garbage in
 		for i = 0 to ndefiners - 1 do
 			let vtyp = asns.(i).typ in
 			let typ = quote ctx.env vtyp in
 
 			let rhs = definers.(i).data.rhs in
 			let rhs =
 				if definers.(i).data.recursive then
 					check' ctx rhs vtyp
 				else begin
 					(* The lhs of non-recursive definers is not in scope when
 					 * checking the rhs, so mark the lhs as inactive. *)
 					asns.(i).active <- false;
 					let rhs = check' ctx rhs vtyp in
 					asns.(i).active <- true;
 					rhs
 				end in
 			let vrhs = V.RefClo (env, rhs) in
 
 			env := Env.define !env (Uniq.get vars i) vrhs;
 			definers'.(i) <- {I.names = namess.(i); I.rhs; I.typ}
 		done;
 
 		(* TODO: For this situation, it might be nice to abstract the surface
 		 * name assignment map from contexts. Then we can say a context is an
 		 * environment + a surface name assignment. *)
 		({ctx with env = !env}, definers')
 
 and elaborate_match'
 : V.context -> Loc.t -> A.term -> A.case array -> V.value -> I.term
 = fun ctx loc scrutinee cases body_vtyp ->
 	let (scrutinee, scrutinee_vtyp) = infer' ctx scrutinee in
 	let vars = Uniq.fresh 1 in
 	let var = Uniq.get vars 0 in
 
 	let ncases = Array.length cases in
 	let cases' = Array.make ncases garbage in
 	for i = 0 to ncases - 1 do
 		let {data = {A.patt; A.body}; _} = cases.(i) in
 
 		let (_, patt) = check_patt'
 			ctx Name.Var.Set.empty patt scrutinee_vtyp in
 
 		let ctx = Ctx.bind ctx vars in
 		let ctx = assign_patt ctx patt scrutinee_vtyp var in
 		let body = check' ctx body body_vtyp in
 
 		cases'.(i) <- {I.patt; I.body}
 	done;
 
 	let to_clause
 	: int -> I.case -> clause
 	= fun casei case ->
 		let tests = match case.patt.disc with
 		| I.DWild _ -> Uniq.UniqMap.empty
 		| I.DData data_disc -> Uniq.UniqMap.singleton var data_disc in
 		{tests; casei} in
 	let clauses = Array.mapi to_clause cases' in
 
 	let used_cases = Array.make ncases false in
 	let env = Env.bind Env.empty vars in
 	let switch = elaborate_switch' loc used_cases env clauses in
 
 	begin match Array.find_index not used_cases with
 	| Some i -> E.abort cases.(i).loc E.ElabRedundantCase
 	| None -> ()
 	end;
 
 	I.Match {scrutinee; cases = cases'; switch}
 
 and elaborate_switch'
 : Loc.t -> bool array -> V.environment -> clause array -> I.switch
 = fun match_loc used_cases env clauses ->
 	let clause_count = Array.length clauses in
 
 	if clause_count > 0 then
 		match Uniq.UniqMap.min_binding_opt clauses.(0).tests with
 		(* Base case: An empty clause is a vacuous conjunction and hence always
 		 * matches. *)
 		| None ->
 			let casei = clauses.(0).casei in
 			used_cases.(casei) <- true;
 			I.Goto casei
 
 		(* Inductive case: Switch on an arbitrary variable in the first clause.
 		 * (Actually, here we switch on the least variable (i.e., such that
 		 * discriminants are analyzed breadth-first), but that's just so
 		 * that the output is predicatable when debugging.)
 		 * TODO: We may want to use some heuristic to pick the variable. *)
 		| Some (var, {datatype = {ctors; names}; _}) ->
 			(* Recursively create a switch tree for each constructor. *)
 			let ctor_count = Array.length ctors in
 			let subswitches = Array.make ctor_count garbage in
 			for tagi = 0 to ctor_count - 1 do
 				let arity = Array.length ctors.(tagi).binders in
 				subswitches.(tagi) <- elaborate_subswitch'
 					match_loc used_cases env clauses var arity tagi
 			done;
 
 			let index = match Env.quote env var with
 			| Some ij -> ij
 			| None -> impossible "Elab.elaborate_switch: switch on unknown var" in
 			I.Switch {index; subswitches; names}
 	else
 		(* TODO: Give an example of a missing case. *)
 		E.abort match_loc E.ElabNonExhaustiveMatch
 
 and elaborate_subswitch'
 : Loc.t -> bool array -> V.environment -> clause array -> Uniq.uniq -> int
 	-> int -> I.switch
 = fun match_loc used_cases env clauses var arity tagi ->
 	let clause_count = Array.length clauses in
 	let subvars = Uniq.fresh arity in
 
 	(* Count the number of clauses in the subproblem. *)
 	let subclause_count = ref 0 in
 	for i = 0 to clause_count - 1 do
 		match Uniq.UniqMap.find_opt var clauses.(i).tests with
 		| Some {tagi = tagi'; _} when tagi' = tagi ->
 			(* Clause i has a test of form "var = C ...", where C is 
 			 * constructor tagi. *)
 			incr subclause_count
 		| Some _ ->
 			(* Clause i has a test of form "var = D ...", where D <> C. *)
 			()
 		| None ->
 			(* Clause i has no opinion on var. *)
 			incr subclause_count
 	done;
 
 	(* Collect the subclauses. *)
 	let subclauses = Inc_array.make !subclause_count in
 	for i = 0 to clause_count - 1 do
 		let {tests; casei} = clauses.(i) in
 		match Uniq.UniqMap.find_opt var tests with
 		| Some {tagi = tagi'; subpatts; _} when tagi' = tagi ->
 			(* Clause i has a test of form "var = C (d_1,...,d_n)", where C is
 			 * constructor tagi. In the subproblem, replace this clause by
 			 * clauses "subvar_j = d_j" for each j such that d_j is a data
 			 * discriminant. *)
 			let tests = Uniq.UniqMap.remove var tests in
 			let tests = ref tests in
 			for j = 0 to Array.length subpatts - 1 do
 				match subpatts.(j).disc with
 				| I.DWild _ -> ()
 				| I.DData data_disc ->
 					let subvar = Uniq.get subvars j in
 					tests := Uniq.UniqMap.add subvar data_disc !tests
 			done;
 			Inc_array.add subclauses {tests = !tests; casei}
 		| Some _ ->
 			(* Clause i has a test of form "var = D ...", where D <> C, so
 			 * do ignore this clause. *)
 			()
 		| None ->
 			(* Clause i has no opinion on var, so add this clause unchanged
 			 * into the subproblem. *)
 			Inc_array.add subclauses {tests; casei}
 	done;
 	let subclauses = Inc_array.to_array subclauses in
 
 	let env = Env.bind env subvars in
 	elaborate_switch' match_loc used_cases env subclauses
 
 (* TODO: This has evolved into a complete disaster. Rewrite it. *)
 and infer_multibinder'
 : V.context -> Loc.t -> A.multibinder -> V.context * I.multibinder
 = fun ctx loc {data = binders; _} ->
 	(* We generate a globally unique id for this multibinder so that we can
 	 * determine which BlockedOnFuture exceptions belong to us (see below).
 	 * This uniq is not a variable. *)
 	let id = Uniq.get (Uniq.fresh 1) 0 in
 
 	let arity = Array.length binders in
 	let vars = Uniq.fresh arity in
 	let ctx = Ctx.bind ctx vars in
 
 	(* Add future assignments to ctx. *)
 	let ctx = ref ctx in
 	let name_set = ref Name.Var.Set.empty in
 	let asns = Array.make arity garbage in
 	for i = 0 to arity - 1 do
 		(* TODO: We should probably check that the pattern is irrefutable
 		 * here. *)
 		let names = binders.(i).data.patt.data.names in
 		let (name_set, names) = Array.fold_left_map add_name' !name_set names in
 		let typ = V.Future (id, i) in
 		let value = V.Arb (Uniq.get vars i) in
 		let (ctx', asn) = Ctx.assign !ctx names typ value in
 		ctx := ctx';
 		asns.(i) <- asn
 	done;
 	let ctx = !ctx in
 
 	(* The data structure used to track binder states. *)
 	let open struct
 		module IntSet = Set.Make(Int)
 
 		type state =
 		| Pending of {
 			dependency: (int * Name.Var.t) option;
 			dependents: IntSet.t;
 		}
 		| Elaborated of int
 
 		let start_state = Pending {
 			dependency = None;
 			dependents = IntSet.empty;
 		}
 
 		let find_cycle states start =
 			let rec search cycle i = match states.(i) with
 			| Pending {dependency = Some (j, name); _} ->
 				if i = j then
 					name :: cycle
 				else
 					search (name :: cycle) j
 			| Pending {dependency = None; _} ->
 				impossible "Elab.infer_multibinder': find_cycle called with \
 					pending binder with no dependency"
 			| Elaborated _ ->
 				impossible "Elab.infer_multibinder': find_cycle called with \
 					elaborated binder" in
 			search [] start
 	end in
 
 	let states = Array.make arity start_state in
 	let namess = Array.make arity garbage in
 
 	(* Next index in the topological sorting of <T. *)
 	let next = ref 0 in
 
 	let rec try_binder i =
 		let dependents = match states.(i) with
 		| Pending {dependency = None; dependents} -> dependents
 		| Pending {dependency = Some _; _} ->
 			impossible "Elab.infer_multibinder': try_binder called with \
 				pending binder with a dependency"
 		| Elaborated _ ->
 			impossible "Elab.infer_multibinder': try_binder called with \
 				elaborated binder" in
 		match infer_binder' ctx binders.(i) with
 		| (names, vtyp) ->
 			namess.(i) <- names;
 			asns.(i).typ <- vtyp;
 			states.(i) <- Elaborated !next;
 			incr next;
 			IntSet.iter remove_dependency dependents
 		| exception BlockedOnFuture (id', j, name) when id' = id ->
 			states.(i) <- Pending {dependency = Some (j, name); dependents};
 			states.(j) <- match states.(j) with
 			| Pending r ->
 				Pending {r with dependents = IntSet.add i r.dependents}
 			| Elaborated _ ->
 				impossible "Elab.infer_multibinder': BlockedOnFuture raised \
 					for elaborated binder"
 
 	and remove_dependency j =
 		let dependents = match states.(j) with
 		| Pending {dependency = Some _; dependents} -> dependents
 		| Pending {dependency = None; _} ->
 			impossible "Elab.infer_multibinder': remove_dependency called \
 				with pending binder with no dependency"
 		| Elaborated _ ->
 			impossible "Elab.infer_multibinder': remove_dependency called \
 				with elaborated binder" in
 		states.(j) <- Pending {dependency = None; dependents};
 		try_binder j in
 
 	for i = 0 to arity - 1 do
 		try_binder i
 	done;
 
 	let binders' = Array.make arity garbage in
 	let order = Array.make arity 0 in
 	for i = 0 to arity - 1 do
 		match states.(i) with
 		| Elaborated j ->
 			let typ = quote ctx.env asns.(i).typ in
 			binders'.(i) <- {
 				I.plicity = binders.(i).data.plicity;
 				I.patt = {
 					names = namess.(i);
 					disc = I.DWild typ;
 				};
 			};
 			order.(j) <- i
 		| Pending _ ->
 			E.abort loc @@ E.ElabBinderCycle (find_cycle states i)
 	done;
 
 	(ctx, {binders = binders'; order})
 
 and infer_binder'
 : V.context -> A.binder -> Name.Var.t array * V.value
 = fun ctx {loc; data = {plicity; patt}} ->
 	match infer_irrefutable_patt ctx Name.Var.Set.empty patt, plicity with
 	| Ok (_, names, vtyp), _ -> (names, vtyp)
 	| Error {data = E.ElabNonInferablePatt; _}, Plicity.Im ->
 		begin match check_irrefutable_patt ctx Name.Var.Set.empty patt
 			Std.v_Type with
 		| Ok (_, names) -> (names, Std.v_Type)
 		| Error root -> E.abort loc @@ E.ElabUnannotImplicitIsType root
 		end
 	| 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. *)
 and check_types'
 : V.context -> A.term array -> int -> V.value -> unit
 = fun ctx typs start vtyp ->
 	for i = start to Array.length typs - 1 do
 		let typ' = check' ctx typs.(i) Std.v_Type in
 		let vtyp' = eval ctx.env typ' in
 		try unify ctx.env vtyp vtyp' with
 		| UnifyFail -> 
 			let typ = quote ctx.env vtyp in
 			E.abort typs.(i).loc @@ E.ElabUnifyFail (typ, typ')
 	done
 
 and infer_irrefutable_patt
 : V.context -> Name.Var.Set.t -> A.patt
 	-> (Name.Var.Set.t * Name.Var.t array * V.value, E.error) result
 = fun ctx name_set patt ->
 	try Ok (infer_irrefutable_patt' ctx name_set patt) with
 	| E.Exn e -> Error e
 
 and infer_irrefutable_patt'
 : V.context -> Name.Var.Set.t -> A.patt
 	-> Name.Var.Set.t * Name.Var.t array * V.value
 = fun ctx name_set ({loc; _} as patt) ->
 	let (name_set, patt, vtyp) = infer_patt' ctx name_set patt in
 	match patt with
 	| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
 	| {names; disc = I.DWild _} -> (name_set, names, vtyp)
 
 and check_irrefutable_patt
 : V.context -> Name.Var.Set.t -> A.patt -> V.value
 	-> (Name.Var.Set.t * Name.Var.t array, E.error) result
 = fun ctx name_set patt vtyp ->
 	try Ok (check_irrefutable_patt' ctx name_set patt vtyp) with
 	| E.Exn e -> Error e
 
 and check_irrefutable_patt'
 : V.context -> Name.Var.Set.t -> A.patt -> V.value
 	-> Name.Var.Set.t * Name.Var.t array
 = fun ctx name_set ({loc; _} as patt) vtyp ->
 	let (name_set, patt) = check_patt' ctx name_set patt vtyp in
 	match patt with
 	| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
 	| {names; disc = I.DWild _} -> (name_set, names)
 
 and infer_patt'
 : V.context -> Name.Var.Set.t -> A.patt -> Name.Var.Set.t * I.patt * V.value
 = fun ctx name_set {loc; data = patt} -> match patt with
 | {typs = [||]; _} -> E.abort loc E.ElabNonInferablePatt
 | {names; typs; disc} ->
 	let (name_set, names) = Array.fold_left_map add_name' name_set names in
 	let typ = check' ctx typs.(0) Std.v_Type in
 	let vtyp = eval ctx.env typ in
 	check_types' ctx typs 1 vtyp;
 	let (names_set, disc) = check_disc' ctx name_set disc vtyp in
 	(name_set, {names; disc}, vtyp)
 
 and check_patt'
 : V.context -> Name.Var.Set.t -> A.patt -> V.value -> Name.Var.Set.t * I.patt
 = fun ctx name_set {loc; data = {names; typs; disc}} vtyp ->
 	let (name_set, names) = Array.fold_left_map add_name' name_set names in
 	check_types' ctx typs 0 vtyp;
 	let (name_set, disc) = check_disc' ctx name_set disc vtyp in
 	(name_set, {names; disc})
 
 and check_disc'
 : V.context -> Name.Var.Set.t -> A.discriminant -> V.value
 	-> Name.Var.Set.t * I.discriminant
 = fun ctx name_set {loc; data = disc} vtyp -> match disc, force ctx.env vtyp with
 | A.DWild, vtyp -> (name_set, I.DWild (quote ctx.env vtyp))
 | A.DData {tag = {data = tag; _}; subpatts = explicit_subpatts},
 		V.DataTypeClosure (clo, datatype) ->
 	begin match Name.Tag.Map.find_opt tag datatype.names with
 	| Some tagi -> (* XXX: This is very similar to check_args'. *)
 		let datatype' = shift_datatype ctx.env clo datatype in
 		let {I.binders; I.order} = datatype.ctors.(tagi) in
 		let arity = Array.length binders in
 		let vars = Uniq.fresh arity in
 		let ctx = Ctx.bind ctx vars in
 		let clo = Env.bind clo vars in
 
 		let name_set = ref name_set in
 		let subpatts = elaborate_args' loc explicit_subpatts binders in
 		let subpatts' = Array.make arity garbage in
 		let ctx = ref ctx in
 		for i = 0 to arity - 1 do
 			let j = order.(i) in
 			let typ = I.disc_type binders.(j).patt.disc in
 			let vtyp = eval clo typ in
 			let (name_set', subpatt') = match subpatts.(j) with
 			| Some patt -> check_patt' !ctx !name_set patt vtyp
 			| None -> no_impl "implicit args" in
 			name_set := name_set';
 			subpatts'.(j) <- subpatt';
 			(* XXX: I think this is a quadratic time algorithm. We should
 			 * thread a context through the check_disc calls instead of
 			 * repeatedly reassigning/rebinding/redefining stuff. *)
 			ctx := assign_patt !ctx subpatt' vtyp (Uniq.get vars j)
 		done;
 
 		let disc = I.DData {
 			tag;
 			tagi;
 			subpatts = subpatts';
 			datatype = datatype';
 		} in
 		(!name_set, disc)
 
 	| None -> E.abort loc @@ E.ElabUnexpectedTag tag
 	end
 | A.DData _, vtyp -> E.abort loc @@ E.ElabExpectedDataType (quote ctx.env vtyp)