commit ca5579829cd533e5a88e9859b25cb5fe20def135
parent f7d4d562278d6d9a0df134fdd77a1b2c644333bd
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Fri, 19 Jan 2024 00:08:13 -0800
Stable state (no quoting of match yet)
Diffstat:
| M | elab.ml | | | 310 | ++++++++++++++++++++++++++++++++++++++----------------------------------------- |
| M | error.ml | | | 8 | ++++++-- |
| M | eval.ml | | | 63 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | internal.ml | | | 30 | +++++++++++++++++++++++++----- |
| M | main.ml | | | 11 | +++++++++++ |
| M | parser.mly | | | 13 | +++++++------ |
| M | pretty.ml | | | 118 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-------------- |
| M | quote.ml | | | 17 | +++++++++++++++-- |
| M | value.ml | | | 7 | ++++++- |
9 files changed, 380 insertions(+), 197 deletions(-)
diff --git a/elab.ml b/elab.ml
@@ -18,6 +18,14 @@ 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.
@@ -130,15 +138,10 @@ and elaborate'
let (body, vtyp) = elaborate' ctx body mode in
(I.Let (definers, body), vtyp)
-| A.Match (scrutinee, cases), mode -> no_impl "elaborate match"
- (*
- let (scrutinee, scrutinee_vtyp) = infer' ctx scrutinee in
- let ncases = Array.length cases in
- let cases' = Array.make ncases garbage in
- for i = 0 to ncases - 1 do
- let (names, disc) = check_patt' ctx patt scrutinee_vtyp in
- done
- *)
+| 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 V.Type in
@@ -404,6 +407,144 @@ and infer_definers'
* environment + a surface name assignment. *)
({ctx with env = !env}, definers')
+and elaborate_match'
+: 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 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 patt scrutinee_vtyp in
+
+ let vars = Uniq.fresh 1 in
+ let var = Uniq.get vars 0 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 vars = Uniq.fresh 1 in
+ let var = Uniq.get vars 0 in
+
+ 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
+
and infer_multibinder'
: context -> Loc.t -> A.binder array -> context * I.multibinder
= fun ctx loc binders ->
@@ -684,154 +825,3 @@ and check_disc'
| None -> E.abort loc @@ E.ElabUnexpectedCtor tag
end
| A.DData _, vtyp -> E.abort loc @@ E.ElabExpectedDataType (quote ctx.env vtyp)
-
-
-
-
-(*
-Use during evaluation of Match (belongs in eval.ml probably):
- type var_tree =
- | Wild of Uniq.t
- | Data of Uniq.t * var_tree array
-or
- type bindee =
- | Var of Uniq.t
- | Tree of Uniq.t option * bindee array
- ^^^^^^
- because top-level of multibinder has no variable
-or, to deal with the option issue above,
- type bindee = Bindee of subbindee array
- and subbindee =
- | Var of Uniq.t
- | Tree of Uniq.t * subbindee array
-Note that Var is not the same as Tree with an empty subbindee array, because
-the former establishes no definitions, whereas the latter defines the variable
-to equal a V.Data with no fields.
-
-
-
-
-*)
-
-(*
- 1. Check each A.patt against inferred type of scrutinee, resulting in
- an array of I.discriminant.
- 2. For each case, bind the discriminant (which involves (a) "linearizing"
- the discriminant into an array of variables in a depth-first
- left-to-right fashion and (b) establishing definitions between variables
- corresponding to subpatterns and the evaluated subpatterns themselves)
- and infer/check the body of the case (according to the ambient mode) in
- this extended context. This produces an I.case corresponding to each
- A.case.
- 3. Produce the switch tree for efficient evaluation with the following
- algorithm: We're given (clause * int) array, where each clause is
-*)
-
-(* A clause is a conjunction of tests, and we view an array of clauses
- * disjunctively. The case:int is the index of the body that the match
- * expression evaluates to if the clause matches. *)
-(*
-type clause = {
- tests: I.data_discriminant Uniq.Map.t;
- case: int;
-}
-
-let rec elaborate_match loc scrutinee cases =
- let vars = Uniq.fresh 1 in
- let env = Env.bind Env.empty vars in
-
- let to_clause i case =
- let tests = match case with
- | I.Case (I.DWild, _) -> Uniq.Map.empty
- | I.Case (I.DData data_disc, _) ->
- Uniq.Map.singleton vars.(0) data_disc in
- {tests; case = i} in
- let clauses = Array.mapi to_clause cases in
-
- let used_cases = Array.make (Array.length cases) false in
- 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 -> E.abort loc ErrRedundantCase
- | None -> ()
- end;
-
- I.Match {scrutinee; cases; switch}
-
-and elaborate_switch match_loc used_cases env clauses =
- let clause_count = Array.length clauses in
-
- if clause_count > 0 then
- match Uniq.Map.min_binding_opt clauses.(0).tests with
- (* Base case: An empty clause is a vacuous conjunction and hence always
- * matches. *)
- | None ->
- let case = clauses.(0).case in
- used_cases.(case) <- true;
- I.Goto case
-
- (* 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; }; _}) ->
- (* Recursively create a switch tree for each constructor. *)
- let ctor_count = Array.length ctors in
- let subswitches = Array.make ctor_count garbage in
- for i = 0 to ctor_count - 1 do
- let arity = Array.length ctors.(i).binders in
- subswitches.(i) <- elaborate_switch_branch
- match_loc used_cases env clauses var arity i
- done;
-
- let index = match Env.quote env var with
- | Some ij -> ij
- | None -> impossible () in
- I.Switch (index, subswitches)
- else
- (* TODO: Give an example of a missing case. *)
- 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
- let subvars = Uniq.fresh arity in
-
- (* Count the number of clauses in the subproblem. *)
- let subclause_count = ref 0 in
- for j = 0 to clause_count - 1 do
- match Uniq.Map.find_opt var clauses.(j).tests with
- | Some {tag = Tag.Index.Of (i', _); _} when i' = i ->
- (* Clause j has a test of form "var = C ...", where C is ctor. *)
- incr subclause_count
- | None ->
- (* Clause j has no opinion on var. *)
- incr subclause_count
- done;
-
- (* Collect the subclauses. *)
- let subclauses = Inc_array.make !subclause_count in
- for j = 0 to clause_count - 1 do
- let {tests; case} = clauses.(j) in
- match Uniq.Map.find_opt var tests with
- | Some {tag = Tag.Index.Of (i', _); subdiscs; _} when i' = i ->
- (* Clause j has a test of form "var = C (d_1,...,d_n)", where C is
- * ctor. In the subproblem, replace this clause by clauses
- * "subvar_i = d_i" for each i such that d_i is a data
- * discriminant. *)
- let tests = Uniq.Map.remove var tests in
- let add_test tests subvar = function
- | I.DWild -> tests
- | I.DData data_disc -> Uniq.Map.add subvar data_disc tests in
- let tests = fold_left2 add_test tests subvars subdiscs in
- Inc_array.add subclauses {tests; case}
- | None ->
- (* Clause j has no opinion on var, so add this clause unchanged
- * into the subproblem. *)
- Inc_array.add subclauses {tests; case}
- done;
- let subclauses = Inc_array.to_array subclauses in
-
- let env = Env.bind env subvars in
- elaborate_switch match_loc used_cases env subclauses
-*)
diff --git a/error.ml b/error.ml
@@ -32,8 +32,9 @@ and error' =
| ElabUnboundVar of Name.Var.t * int
| ElabFnArityMismatch
| ElabFnPlicityMismatch
-(*| ElabNonExhaustiveMatch*)
-(*| ElabRedundantCase*)
+| ElabNonExhaustiveMatch
+| ElabRedundantCase
+| ElabCantInferMatch
(*| ElabExpectedFnType of I.term*)
let rec pp_print ppf {loc; data = e} =
@@ -89,6 +90,9 @@ and pp_print' ppf = function
| ElabFnPlicityMismatch -> F.pp_print_string ppf "ErrFnPlicityMismatch"
| ElabUnexpectedCtor _ -> F.pp_print_string ppf "ErrUnexpectedCtor"
| ElabDuplicateName _ -> F.pp_print_string ppf "ErrDuplicateName"
+| ElabNonExhaustiveMatch -> F.pp_print_string ppf "ElabNonExhaustiveMatch"
+| ElabRedundantCase -> F.pp_print_string ppf "ElabRedundantCase"
+| ElabCantInferMatch -> F.pp_print_string ppf "ElabCantInferMatch"
(*| ElabExpectedFnType _ -> "ErrExpectedFnType"*)
exception Exn of error
diff --git a/eval.ml b/eval.ml
@@ -1,3 +1,4 @@
+open Util
module I = Internal
module V = Value
@@ -5,6 +6,32 @@ module V = Value
* cases? *)
(* TODO: Lazily evaluate args? *)
+let rec define_data_args
+: V.environment -> V.value -> I.patt -> V.environment
+= fun env value {disc; _} -> match value, disc with
+| value, I.DWild -> env
+| V.Data {tagi = data_tagi; args; _}, I.DData {tagi = disc_tagi; subpatts; _} ->
+ begin if data_tagi <> disc_tagi then
+ impossible "Eval.define_along_patt: value and disc have different tag"
+ end;
+
+ let arity = Array.length args in
+ begin if arity <> Array.length subpatts then
+ impossible "Eval.define_along_patt: value and disc have different arity"
+ end;
+
+ let subvars = Uniq.fresh arity in
+ let env = Env.bind env subvars in
+ let env = ref env in
+ for i = 0 to arity - 1 do
+ env := Env.define !env (Uniq.get subvars i) args.(i);
+ env := define_data_args !env args.(i) subpatts.(i)
+ done;
+
+ !env
+| _, I.DData _ ->
+ impossible "Eval.define_along_patt: value is not data, but disc is"
+
let rec eval env = function
| I.Let (definers, body) ->
let ndefiners = Array.length definers in
@@ -19,6 +46,23 @@ let rec eval env = function
done;
eval !env body
+| I.Match {scrutinee; cases; switch} ->
+ let scrutinee = eval env scrutinee in
+ let vars = Uniq.fresh 1 in
+ let var = Uniq.get vars 0 in
+ let switch_env = Env.bind Env.empty vars in
+ let switch_env = Env.define switch_env var scrutinee in
+ begin match do_switch switch_env (Index.Of (0, 0)) switch with
+ | Some casei ->
+ let {I.patt; I.body} = cases.(casei) in
+ let vars = Uniq.fresh 1 in
+ let env = Env.bind env vars in
+ let env = Env.define env (Uniq.get vars 0) scrutinee in
+ let env = define_data_args env scrutinee patt in
+ eval env body
+ | None -> V.Match {scrutinee; clo = env; cases; switch}
+ end
+
| I.App (fn, args) -> apply (eval env fn) (Array.map (eval env) args)
| I.Fn fn -> V.FnClosure (env, fn)
@@ -49,6 +93,25 @@ let rec eval env = function
| I.Builtin b -> V.Builtin b
+and do_switch env ij = function
+| Switch {index = ij'; subswitches; _} ->
+ let var = Env.index env ij in
+ begin match Env.eval env var with
+ | Some (V.Data {tagi; args; _}) ->
+ let arity = Array.length args in
+ let subvars = Uniq.fresh arity in
+ let env = Env.bind env subvars in
+ let env = ref env in
+ for i = 0 to arity - 1 do
+ let subvar = Uniq.get subvars i in
+ env := Env.define !env subvar args.(i)
+ done;
+ do_switch !env ij' subswitches.(tagi)
+ | Some _ -> None (* Neutral match *)
+ | None -> impossible "Eval.switch: undefined variable"
+ end
+| Goto casei -> Some casei
+
and apply fn args = match fn, args with
| V.Rec {env; rhs}, args -> apply (eval !env rhs) args
| V.FnClosure (clo, {multibinder = {binders; _}; body; _}), args ->
diff --git a/internal.ml b/internal.ml
@@ -39,11 +39,11 @@ type builtin =
type term =
| Let of definer array * term
-(*| Match of {
+| Match of {
scrutinee: term;
cases: case array;
switch: switch;
-}*)
+}
| App of term * term array
| Fn of fn
| FnType of fntype
@@ -74,12 +74,32 @@ and case = {
* non-empty datatype, and Goto is a leaf node that jumps to the indicated
* case. *)
and switch =
-| Switch of Index.t * switch array
+| Switch of {
+ index: Index.t;
+ subswitches: switch array;
+ names: int Name.Ctor.Map.t; (* For pretty-printing. *)
+}
| Goto of int
(* TODO: Generalize binders/multibinders to include discriminants, i.e.,
* generalize from linear to tree structure. When we bind such a binder,
- * we also establish some definitions according to the tree structure. *)
+ * we also establish some definitions according to the tree structure.
+
+and binder = {
+ plicity: Plicity.t;
+ names: Name.Var.t node array;
+ disc: discriminant;
+ typ: term;
+}
+
+and discriminant =
+| DWild
+| DData of {
+ tag: Name.Ctor.t;
+ tagi: int;
+ sub: multibinder;
+}
+*)
and binder = {
plicity: Plicity.t;
@@ -105,7 +125,7 @@ and fntype = {
and datatype = {
ctors: multibinder array;
- names: int Name.Ctor.Map.t;
+ names: int Name.Ctor.Map.t; (* TODO: Rename to "tagis" for consistency *)
}
and patt = {
diff --git a/main.ml b/main.ml
@@ -13,6 +13,17 @@ let buf = Lexing.from_string "\
(*
let buf = Lexing.from_string "\
+ Bool := #{@false; @true};\n\
+ T := #(b: Bool, (if b then Nat else Type));\n\
+ ((@true, 3): T match {\n\
+ (@true, n) => n,\n\
+ (@false, _) => 2,\n\
+ }): Nat\n\
+"
+*)
+
+(*
+let buf = Lexing.from_string "\
f := fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat =>\
fn a: Nat, b: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat => 3; 3\
"
diff --git a/parser.mly b/parser.mly
@@ -232,16 +232,17 @@ expr4f: expr5 { $1 }
expr5:
| expr6 expr6 expr6_apposition_list {
- let (len, lst) = $3 in
- loc () @$ App ($1, len + 1, $2 :: lst)
- }
- | ctor_name expr6_apposition_list {
- let (len, lst) = $2 in
- loc () @$ Variant ($1, len, lst)
+ let (len, lst) = cons $2 $3 in
+ match $1.data with
+ | Variant (tag, 0, []) ->
+ loc () @$ Variant (tag, len, lst)
+ | _ ->
+ loc () @$ App ($1, len, lst)
}
| expr6 { $1 }
expr6:
+ | ctor_name { loc () @$ Variant ($1, 0, []) }
| UNDERSCORE { loc () @$ Underscore }
| indexed_var_name {
let (x, i) = $1 in
diff --git a/pretty.ml b/pretty.ml
@@ -19,7 +19,11 @@ and pp_print_term
(F.pp_print_array ~pp_sep:pp_print_comma pp_print_definer) definers
(pp_print_term 0) body
-(* TODO: Match *)
+| Match {scrutinee; cases; switch} ->
+ pp_print_with_parens m 1 ppf "@[<v 4>%a match {%a} %a@]"
+ (pp_print_term 2) scrutinee
+ pp_print_cases cases
+ pp_print_switch switch
| App (fn, args) ->
pp_print_with_parens m 5 ppf "@[<4>%a%a@]"
@@ -40,9 +44,10 @@ and pp_print_term
(pp_print_term 3) codomain
| Data {tag; args; datatype; _} ->
- pp_print_with_parens m 2 ppf "@[@[<4>%a%a@] ::@;<1 4>%a@]"
+ pp_print_with_parens m 2 ppf "@[@[<4>%a%a@]%t%a@]"
Name.Ctor.pp_print tag
pp_print_args args
+ (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) (DataType datatype)
| DataType {ctors; names} ->
@@ -72,15 +77,79 @@ and pp_print_definer
: F.formatter -> definer -> unit
= fun ppf {names; rhs; typ} ->
F.fprintf ppf "@[@[<hv 4>%a%t%a@;<1 -4>@]:=@;<1 4>%a@]"
- pp_print_names names
+ (pp_print_names 3) names
(F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 0, ""))
(pp_print_term 2) typ
(pp_print_term 1) rhs
+and pp_print_cases
+: F.formatter -> case array -> unit
+= fun ppf -> function
+| [||] -> ()
+| cases ->
+ for i = 0 to Array.length cases - 1 do
+ F.fprintf ppf "@,@[%a =>@;<1 4>%a@],"
+ (pp_print_patt 2) cases.(i).patt
+ (pp_print_term 1) cases.(i).body
+ done;
+ F.fprintf ppf "@;<0 -4>"
+
+and pp_print_patt
+: int -> F.formatter -> patt -> unit
+= fun m ppf -> function
+| {names = [||]; disc} ->
+ pp_print_disc m ppf disc
+| {names; disc = DWild} ->
+ pp_print_names m ppf names
+| {names; disc = DData _ as disc} ->
+ (* XXX: The grammar uses precdence 4 for all binops. *)
+ pp_print_with_parens m 4 ppf "%a & %a"
+ (pp_print_names 4) names
+ (pp_print_disc 4) disc
+
+and pp_print_disc
+: int -> F.formatter -> discriminant -> unit
+= fun m ppf -> function
+| DWild ->
+ pp_print_with_parens m 6 ppf "_"
+| DData {tag; subpatts = [||]; _} ->
+ pp_print_with_parens m 6 ppf "%a"
+ Name.Ctor.pp_print tag
+| DData {tag; subpatts; _} ->
+ pp_print_with_parens m 5 ppf "%a %a"
+ Name.Ctor.pp_print tag
+ (F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_patt 6)) subpatts
+
+and pp_print_switch
+: F.formatter -> switch -> unit
+= fun ppf -> function
+| Switch {index; subswitches; names} ->
+ F.fprintf ppf "%a switch {%a}"
+ Index.pp_print index
+ pp_print_subswitches (subswitches, names)
+| Goto casei ->
+ F.fprintf ppf "goto %d"
+ casei
+
+and pp_print_subswitches
+: F.formatter -> switch array * int Name.Ctor.Map.t -> unit
+= fun ppf -> function
+| ([||], _) -> ()
+| (subswitches, names) ->
+ (* TODO: Doing this conversion sucks. *)
+ let names = Array.of_list (Name.Ctor.Map.to_list names) in
+ for i = 0 to Array.length subswitches - 1 do
+ let (tag, _) = names.(i) in
+ F.fprintf ppf "@,@[%a =>@;<1 4>%a@],"
+ Name.Ctor.pp_print tag
+ pp_print_switch subswitches.(i)
+ done;
+ F.fprintf ppf "@;<0 -4>"
+
and pp_print_args
: F.formatter -> term array -> unit
= fun ppf -> function
-| [||] -> () (* This only happens for Data, not Fn. *)
+| [||] -> () (* This only happens for Data, not App. *)
| args ->
F.fprintf ppf "@ %a"
(F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6)) args
@@ -95,10 +164,16 @@ and pp_print_binder
= fun ppf {plicity; names; typ} ->
F.fprintf ppf "@[%a%a%t%a@]"
pp_print_plicity plicity
- pp_print_names names
+ (pp_print_names 3) names
(F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) typ
+and pp_print_plicity
+: F.formatter -> Plicity.t -> unit
+= fun ppf -> function
+| Plicity.Im -> F.fprintf ppf "?"
+| Plicity.Ex -> ()
+
and pp_print_ctors
: F.formatter -> multibinder array * int Name.Ctor.Map.t -> unit
= fun ppf (ctors, names) ->
@@ -116,17 +191,25 @@ and pp_print_ctors
pp_print_binders binders
) names
-and pp_print_plicity
-: F.formatter -> Plicity.t -> unit
+and pp_print_builtin
+: F.formatter -> builtin -> unit
= fun ppf -> function
-| Plicity.Im -> F.pp_print_string ppf "?"
-| Plicity.Ex -> ()
+| NatType -> F.fprintf ppf "~Nat"
+| NatOpAdd -> F.fprintf ppf "~+"
+| NatOpMul -> F.fprintf ppf "~*"
and pp_print_names
-: F.formatter -> Name.Var.t node array -> unit
-= fun ppf -> function
-| [||] -> F.fprintf ppf "_"
-| names -> F.pp_print_array ~pp_sep:pp_print_and pp_print_name ppf names
+: int -> F.formatter -> Name.Var.t node array -> unit
+= fun m ppf -> function
+| [||] ->
+ pp_print_with_parens m 6 ppf "_"
+| [|name|] ->
+ pp_print_with_parens m 6 ppf "%a"
+ pp_print_name name
+| names ->
+ (* XXX: The grammar uses precdence 4 for all binops. *)
+ pp_print_with_parens m 4 ppf "%a"
+ (F.pp_print_array ~pp_sep:pp_print_and pp_print_name) names
and pp_print_name
: F.formatter -> Name.Var.t node -> unit
@@ -138,11 +221,4 @@ and pp_print_comma
and pp_print_and
: F.formatter -> unit -> unit
-= fun ppf () -> F.pp_print_string ppf " & "
-
-and pp_print_builtin
-: F.formatter -> builtin -> unit
-= fun ppf -> function
-| NatType -> F.pp_print_string ppf "~Nat"
-| NatOpAdd -> F.pp_print_string ppf "~+"
-| NatOpMul -> F.pp_print_string ppf "~*"
+= fun ppf () -> F.fprintf ppf " & "
diff --git a/quote.ml b/quote.ml
@@ -5,6 +5,19 @@ module V = Value
let rec quote env = function
| V.Rec {env = env'; rhs} -> quote env (eval !env' rhs)
+(*
+| V.Match {scrutinee; clo; cases; switch} ->
+ let scrutinee = quote env scrutinee in
+ let ncases = Array.length cases in
+ let cases' = Array.make ncases garbage in
+ for i = 0 to ncases - 1 do
+ let {I.patt; I.body} = cases.(i) in
+ let vars = Uniq.fresh 1 in
+ let env = Env.bind env vars in
+ let env = define_data_args env scrutinee patt in
+ done;
+ I.Match {scrutinee; ; switch}
+*)
| V.App (fn, args) -> I.App (quote env fn, Array.map (quote env) args)
| V.FnClosure (clo, {multibinder; body; codomain}) ->
let (env, clo, multibinder) =
@@ -30,11 +43,11 @@ let rec quote env = function
| V.Arb var ->
begin match Env.quote env var with
| Some ij -> I.Var ij
- | None -> impossible "Eval.quote: env does not bind variable in value"
+ | None -> impossible "Eval.quote: env does not bind variable"
end
| V.Type -> I.Type
| V.Builtin b -> I.Builtin b
-| V.Future _ -> impossible "Eval.quote: "
+| V.Future _ -> impossible "Eval.quote: can not quote future"
and quote_datatype env clo {ctors; names} = {
ctors = Array.map (quote_multibinder env clo) ctors;
diff --git a/value.ml b/value.ml
@@ -5,7 +5,12 @@ type value =
env: environment ref;
rhs: I.term;
}
-(*| Switch of ...*)
+| Match of {
+ scrutinee: value;
+ clo: environment;
+ cases: I.case array;
+ switch: I.switch;
+}
| App of value * value array
| FnClosure of environment * I.fn
| FnTypeClosure of environment * I.fntype
