Skip to content

Commit db81055

Browse files
mikeshulmanmikeshulman
committed
split on datatype terms
1 parent de0b9ea commit db81055

File tree

4 files changed

+97
-31
lines changed

4 files changed

+97
-31
lines changed

‎docs/source/interactive.rst‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -33,15 +33,19 @@ Finally, if the cursor is over a hole, then the commands ``C-c ;`` (normalize a
3333
Splitting in holes
3434
------------------
3535

36-
Narya has a limited ability to infer the shape of a term to solve a hole with from the type of that hole. In ProofGeneral mode, if you position the cursor over a hole and type ``C-c C-y``, Narya will try to guess the shape of a term to fill the hole with, leaving additional holes in appropriate places. This includes:
36+
Narya has a limited ability to infer the shape of a term to solve a hole with from the type of that hole or from the type of an argument to match against. In ProofGeneral mode, if you position the cursor over a hole and type ``C-c C-y``, you will be prompted for a term on which to split, or to leave it blank to split on the type of the goal. Narya will then try to guess the shape of a term to fill the hole with, leaving additional holes in appropriate places. This includes:
3737

38-
- If the hole has a function type, the term inserted will be an abstraction with a new hole in the body. The variable names in the abstraction are taken from the function type, e.g. for ``(x : A) → B`` the term inserted will be ``x ↦ ?``. For a function type with unnamed variable like ``A → B``, the variable inserted will be a placeholder ``_``. Iterated function-types like ``(x : A) (y : B) → C`` lead to iterated abstractions ``x y ↦ ?``, and higher-dimensional function-types like ``Id ((x : A) → B) f g`` lead to :ref:`Cubes of variables` ``x ⤇ ?``.
38+
- If you enter a term, that term must synthesize a datatype (see :ref:`Inductive datatypes and matching`). The term inserted will then be a match against that term, with appropriate branches for all of its constructors. The variable names for the arguments of each constructor are taken from the datatype declaration. This includes higher-dimensional versions of data types (see :ref:`Id of datatypes`). However, it is not currently possible to use this method to insert :ref:`Multiple matches and deep matches`.
3939

40-
- If the hole has a record type (see :ref:`Record types and tuples`), the term inserted will be a tuple with all fields labeled such as ``(fst ≔ ?, snd ≔ ?)``. This includes higher-dimensional versions of record types (see :ref:`Id of record types`).
40+
- If you don't enter a term, and the hole has a function type, the term inserted will be an abstraction with a new hole in the body. The variable names in the abstraction are taken from the function type, e.g. for ``(x : A) → B`` the term inserted will be ``x ↦ ?``. For a function type with unnamed variable like ``A → B``, the variable inserted will be a placeholder ``_``. Iterated function-types like ``(x : A) (y : B) → C`` lead to iterated abstractions ``x y ↦ ?``, and higher-dimensional function-types like ``Id ((x : A) → B) f g`` lead to :ref:`Cubes of variables` ``x ⤇ ?``.
4141

42-
- If the hole has a codata type (see :ref:`Codatatypes and comatching`), including higher-dimensional versions thereof, the term inserted will be a comatch such as ``[ .head ↦ ? | .tail ↦ ? ]``. This also works with :ref:`higher coinductive types`: the correct number of copies of each higher field are inserted depending on the dimension of the type.
42+
- If you don't enter a term, and the hole has a record type (see :ref:`Record types and tuples`), the term inserted will be a tuple with all fields labeled such as ``(fst ≔ ?, snd ≔ ?)``. This includes higher-dimensional versions of record types (see :ref:`Id of record types`).
4343

44-
You can also split on a hole directly in interactive mode, identifying a hole by its number as in ``split 0 ≔ _``. (The placeholder ``_`` is necessary, as in the future we may also implement splitting on a supplied term that belongs to some datatype.) This can be a bit confusing, though, because it doesn't inform you about the term that was inserted, only about all the new holes.
44+
- If you don't enter a term, and the hole has a codata type (see :ref:`Codatatypes and comatching`), including higher-dimensional versions thereof, the term inserted will be a comatch such as ``[ .head ↦ ? | .tail ↦ ? ]``. This also works with :ref:`higher coinductive types`: the correct number of copies of each higher field are inserted depending on the dimension of the type.
45+
46+
If none of these cases apply, an error results.
47+
48+
You can also split on a hole directly in interactive mode, identifying a hole by its number as in ``split 0 ≔ M`` to split on a term ``M``, or ``split 0 ≔ _`` to split on the goal type. This can be a bit confusing, though, because it doesn't inform you about the term that was inserted, only about all the new holes.
4549

4650

4751
Undoing solved holes

‎lib/core/reporter.ml‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,7 @@ module Code = struct
242242
| Incompatible_flags : string * string -> t
243243
| Actions_in_compiled_file : string -> t
244244
| No_such_hole : int -> t
245-
| Invalid_split : string -> t
245+
| Invalid_split : [ `Term | `Goal ] * string -> t
246246
| Forbidden_interactive_command : string -> t
247247
| Not_enough_to_undo : t
248248
| Commands_undone : int -> t
@@ -997,7 +997,12 @@ module Code = struct
997997
| Actions_in_compiled_file file ->
998998
textf "not re-executing echo/synth/show commands when loading compiled file %s" file
999999
| No_such_hole i -> textf "no open hole numbered %d" i
1000-
| Invalid_split str -> textf "invalid split: hole belongs to a %s" str
1000+
| Invalid_split (which, str) ->
1001+
textf "invalid split: %s belongs to a %s"
1002+
(match which with
1003+
| `Goal -> "goal"
1004+
| `Term -> "term")
1005+
str
10011006
| Hole_solved h ->
10021007
if h > 1 then textf "hole solved, containing %d new holes" h
10031008
else if h = 1 then text "hole solved, containing 1 new hole"

‎lib/parser/command.ml‎

Lines changed: 76 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -956,15 +956,15 @@ let rec execute :
956956
{ global = _; scope; status = _; vars } )) =
957957
Eternity.find_number data.number in
958958
match metatm with
959-
| `Undefined -> (
959+
| `Undefined ->
960960
Scope.run ~init_visible:scope @@ fun () ->
961961
let (Wrap tm) = !(data.tm) in
962-
match tm.value with
963-
| Placeholder _ ->
964-
Global.HolesAllowed.run ~env:(Ok ()) @@ fun () ->
965-
let ctx = Norm.eval_ctx termctx in
966-
let ety = Norm.eval_term (Ctx.env ctx) ty in
967-
let content =
962+
Global.HolesAllowed.run ~env:(Ok ()) @@ fun () ->
963+
let ctx = Norm.eval_ctx termctx in
964+
let content =
965+
match tm.value with
966+
| Placeholder _ -> (
967+
let ety = Norm.eval_term (Ctx.env ctx) ty in
968968
match View.view_type ety "split" with
969969
| Canonical (_, Pi (_, doms, _), _, _) ->
970970
let cube, mapsto =
@@ -993,19 +993,76 @@ let rec execute :
993993
let fields = Bwd.fold_right do_field fields [] in
994994
match eta with
995995
| Eta ->
996-
"(" ^ String.concat ", " (List.map (fun fld -> fld ^ " := ?") fields) ^ ")"
996+
Token.to_string LParen
997+
^ String.concat ", "
998+
(List.map
999+
(fun fld ->
1000+
fld ^ " " ^ Token.to_string Coloneq ^ " " ^ Token.to_string Query)
1001+
fields)
1002+
^ Token.to_string RParen
9971003
| Noeta ->
998-
"["
999-
^ String.concat " | " (List.map (fun fld -> "." ^ fld ^ " |-> ?") fields)
1000-
^ "]")
1001-
| Canonical (_, UU _, _, _) -> fatal (Invalid_split "universe")
1002-
| Canonical (_, Data _, _, _) -> fatal (Invalid_split "datatype")
1003-
| Neutral _ -> fatal (Invalid_split "neutral") in
1004-
(data.tm := TermParse.Term.(final (parse (`String { title = None; content }))));
1005-
execute ~action_taken ~get_file (Solve data)
1006-
| _ ->
1007-
let _ptm = process vars tm in
1008-
fatal (Unimplemented "splitting on terms"))
1004+
Token.to_string LBracket
1005+
^ String.concat " | "
1006+
(List.map
1007+
(fun fld ->
1008+
"."
1009+
^ fld
1010+
^ " "
1011+
^ Token.to_string Mapsto
1012+
^ " "
1013+
^ Token.to_string Query)
1014+
fields)
1015+
^ Token.to_string RBracket)
1016+
| Canonical (_, UU _, _, _) -> fatal (Invalid_split (`Goal, "universe"))
1017+
| Canonical (_, Data _, _, _) -> fatal (Invalid_split (`Goal, "datatype"))
1018+
| Neutral _ -> fatal (Invalid_split (`Goal, "neutral")))
1019+
| _ -> (
1020+
match process vars tm with
1021+
| { value = Synth rtm; loc } -> (
1022+
let _, sty = Check.synth (Kinetic `Nolet) ctx (Asai.Range.locate_opt loc rtm) in
1023+
match View.view_type sty "split" with
1024+
| Canonical (_, Data { dim; constrs; _ }, _, _) ->
1025+
let mapsto =
1026+
match D.compare_zero dim with
1027+
| Zero -> Token.to_string Mapsto
1028+
| Pos _ -> Token.to_string DblMapsto in
1029+
let rec do_args : type a p ap.
1030+
(a, p, ap) Term.Telescope.t -> string -> string =
1031+
fun args acc ->
1032+
match args with
1033+
| Emp -> acc
1034+
| Ext (x, _, args) ->
1035+
Option.value ~default:(Token.to_string Underscore) x
1036+
^ " "
1037+
^ do_args args acc in
1038+
let do_constrs : type m ij.
1039+
Constr.t * (m, ij) Value.dataconstr -> string list -> string list =
1040+
fun (c, Dataconstr { args; _ }) acc ->
1041+
(Constr.to_string c
1042+
^ ". "
1043+
^ do_args args " "
1044+
^ mapsto
1045+
^ " "
1046+
^ Token.to_string Query)
1047+
:: acc in
1048+
let constrs = Bwd.fold_right do_constrs constrs [] in
1049+
let buf = Buffer.create 10 in
1050+
PPrint.(
1051+
ToBuffer.pretty 1.0 (Display.columns ()) buf
1052+
(pp_complete_term (Wrap tm) `None));
1053+
Token.to_string Match
1054+
^ " "
1055+
^ Buffer.contents buf
1056+
^ " "
1057+
^ Token.to_string LBracket
1058+
^ " "
1059+
^ String.concat " | " constrs
1060+
^ " "
1061+
^ Token.to_string RBracket
1062+
| _ -> fatal (Invalid_split (`Term, "non-datatype")))
1063+
| _ -> fatal (Nonsynthesizing "splitting term")) in
1064+
(data.tm := TermParse.Term.(final (parse (`String { title = None; content }))));
1065+
execute ~action_taken ~get_file (Solve data)
10091066
| `Defined _ | `Axiom -> fatal (Anomaly "hole already defined"))
10101067
| Show { what; _ } -> (
10111068
action_taken ();

‎proofgeneral/narya.el‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -481,13 +481,13 @@ handling in Proof General."
481481

482482
(defun narya-solve-hole (term)
483483
"Solve the current hole with a user-provided term."
484-
(interactive "MEnter the term to solve the hole: ")
484+
(interactive "MSolve hole with: ")
485485
(narya-solve-or-split-hole nil term))
486486

487-
(defun narya-split-hole ()
488-
"Solve the current hole with a term inferred from its type."
489-
(interactive)
490-
(narya-solve-or-split-hole t "_"))
487+
(defun narya-split-hole (term)
488+
"Solve the current hole by matching a term or inferring from its type."
489+
(interactive "MSplit on term (leave blank to split on goal): ")
490+
(narya-solve-or-split-hole t (if (equal term "") "_" term)))
491491

492492
(defun narya-solve-or-split-hole (split term)
493493
"Issue either solve or split command, depending on the argument."

0 commit comments

Comments
 (0)