diff --git a/README.md b/README.md index 8cdfa818..75207b44 100644 --- a/README.md +++ b/README.md @@ -67,6 +67,10 @@ The Narya executable accepts at least the following command-line flags. - `-unicode` and `-ascii`: Display and reformat code using Unicode (default) or ASCII - `-noncompact` and `-compact`: Select reformatting mode - `-reformat`: Display reformatted code on stdout after parsing +- `-show-function-boundaries`: Display boundaries of functions, when implicit +- `-hide-function-boundaries`: Hide boundaries of functions, when implicit +- `-show-type-boundaries`: Display boundaries of functions, when implicit +- `-hide-type-boundaries`: Hide boundaries of functions, when implicit #### Controlling parametricity @@ -161,7 +165,18 @@ In interactive mode, the following additional commands are also available. (How 1. `display SETTING` - Set one of the display settings (that are also set by command-line flags), which can be either `unicode`, `ascii`, `compact`, or `noncompact`. + Set one of the display settings (that are also set by command-line flags). Possible display settings are + + ``` + display style ≔ compact + display style ≔ noncompact + display chars ≔ unicode + display chars ≔ ascii + display function boundaries ≔ on + display function boundaries ≔ off + display type boundaries ≔ on + display type boundaries ≔ off + ``` ### ProofGeneral mode @@ -1543,13 +1558,13 @@ There are many ways in which a type theory can be "higher-dimensional", by which ### Identity/bridge types of canonical types -Every type `A` has a binary identity/bridge type denoted `Id A x y`, and each term `x:A` has a reflexivity term `refl x : Id A x x`. (The argument of `refl` must synthesize.) There is no "transport" for these types (hence "bridge" is really a more appropriate name). But they are "observational" in the sense that the identity/bridge type of a canonical type is another canonical type of the same sort. +Every type `A` has a binary identity/bridge type denoted `Id A x y`, and each term `x:A` has a reflexivity term `refl x : Id A x x`. (The argument of `refl` must synthesize.) There is no built-in "transport" for these types (hence "bridge" is really a more appropriate name). But they are "observational" in the sense that the identity/bridge type of a canonical type is another canonical type of the same sort. For example, `Id (A → B) f g` is a function-type `(x₀ x₁ : A) (x₂ : Id A x₀ x₁) → Id B (f x₀) (g x₁)`. In particular, `refl f` is a function of a type `(x₀ x₁ : A) (x₂ : Id A x₀ x₁) → Id B (f x₀) (f x₁)`, witnessing that all functions preserve "equalities" or "relatedness". Thus the operation traditionally denoted `ap` in homotopy type theory is just `refl` applied to a function (although since the argument of `refl` must synthesize, if the function is an abstraction it must be ascribed). Similarly, `Id (A × B) u v` is a type of pairs of identities, so if we have `p : Id A (u .fst) (v .fst)` and `q : Id B (u .snd) (v .snd)` we can form `(p,q) : Id (A × B) u v`, and so on for other record types, datatypes, and codatatypes. However, in Narya `Id (A → B) f g` does not *reduce* to the *ordinary* function-type `(x₀ x₁ : A) (x₂ : Id A x₀ x₁) → Id B (f x₀) (g x₁)`: instead it simply *behaves* like it, in the sense that its elements can be applied like functions and we can define elements of its as abstractions. This should be compared with how `Covec A 2` doesn't reduce to `A × (A × ⊤)` but behaves like it in terms of what its elements are and what we can do with them. In particular, `Id (A → B) f g` and `(x₀ x₁ : A) (x₂ : Id A x₀ x₁) → Id B (f x₀) (g x₁)` are definitionally isomorphic, with the functions in both directions being η-expansions `f ↦ (x₀ x₁ x₂ ↦ f x₀ x₁ x₂)`. For most purposes this behavior is just as good as a reduction, and it retains more information about the type, which, as before, is useful for many purposes. (In fact, with our current understanding, it appears to be *essential* for Narya's normalization and typechecking algorithms.) -The same is true for other canonical types, e.g. `Id (A × B) u v` does not reduce to `Id A (u .fst) (v .fst) × Id B (u .snd) (v .snd)`, but it is *a* record type that is definitionally isomorphic to it. Similarly, identity types of codatatypes behave like types of bisimulations: `Id (Stream A) s t` is a codatatype that behaves as if it were defined by +The same is true for other canonical types, e.g. `Id (A × B) u v` does not reduce to `Id A (u .fst) (v .fst) × Id B (u .snd) (v .snd)`, but it is *a* record type, with fields named `fst` and `snd`, that is definitionally isomorphic to it by η-expansions. Similarly, identity types of codatatypes behave like types of bisimulations: `Id (Stream A) s t` is a codatatype that behaves as if it were defined by ``` codata [ | _ .head : Id A (s .head) (t .head) @@ -1575,6 +1590,8 @@ According to internal parametricity, we morally think of `Id Type A B` as being The first is literally true: given `R : Id Type A B` and `a:A`, `b:B` we have `R a b : Type`. We refer to this as *instantiating* the higher-dimensional type `R`. In fact, `Id A x y` itself is an instantiation, as we have `Id A : Id Type A A`, which moreover is really just a notational variant of `refl A`. +However, unlike a true function `A → B → Type`, an element of `Id Type A B` cannot be "partially applied": you cannot write `Id A a`. But of course, you can η-expand it and write `x ↦ Id A a x`. (If there is demand, we might implement an automatic η-expansion of the former to the latter.) + For the second there is another wrinkle: we can define elements of `Id Type A B` by abstracting, but the body of the abstraction must be a *newly declared canonical type* rather than a pre-existing one. This also seems to be essential to deal with symmetries (see below) in the normalization and typechecking algorithm. Moreover, the current implementation allows this body to be a *record type* or *codatatype*, but not a *datatype*, and it does not permit other case tree operations in between such as pattern-matching. For record types, there is a syntax that reflects this restriction: instead of the expected `x y ↦ sig (⋯)` we write `sig x y ↦ (⋯)`, explicitly binding all the boundary variables as part of the record type syntax. For example, here is the universal 1-dimensional record type, traditionally called "Gel": @@ -1583,12 +1600,12 @@ def Gel (A B : Type) (R : A → B → Type) : Id Type A B ≔ sig a b ↦ ( unge ``` For codatatypes, we simply use the ordinary syntax, but the "self" variable automatically becomes a cube variable of the appropriate dimension (see below). -We plan to lift this restriction in the future, but in practice it is not very onerous. For most applications, the above "Gel" record type can simply be defined once and used everywhere, rather than declaring new higher-dimensional types all the time. Note that because record-types satisfy η-conversion, `Gel A B R a b` is definitionally isomorphic to `R a b`. Thus, `Id Type A B` contains `A → B → Type` as a "retract up to definitional isomorphism". This appears to be sufficient for all applications of internal parametricity. (`Id Type` does not itself satisfy any η-conversion rule.) +We may allow more flexibility in the future, but in practice the current restrictions do not seem very onerous. For most applications, the above "Gel" record type can simply be defined once and used everywhere, rather than declaring new higher-dimensional types all the time. Note that because record-types satisfy η-conversion, `Gel A B R a b` is definitionally isomorphic to `R a b`. Thus, `Id Type A B` contains `A → B → Type` as a "retract up to definitional isomorphism". This appears to be sufficient for all applications of internal parametricity. (`Id Type` does not itself satisfy any η-conversion rule.) ### Heterogeneous identity/bridge types -If `B : A → Type`, then `refl B x₀ x₁ x₂ : Id Type (B x₀) (B x₁)`. Thus, given `y₀ : B x₀` and `y₁ : B x₁`, we can instantiate this identification at them to obtain a type `refl B x₀ x₁ x₂ y₀ y₁`. of *heterogeneous* identifications/bridges relating `y₀` and `y₁` "along" or "over" `x₂`. +If `B : A → Type`, then `refl B x₀ x₁ x₂ : Id Type (B x₀) (B x₁)`. Thus, given `y₀ : B x₀` and `y₁ : B x₁`, we can instantiate this identification at them to obtain a type `refl B x₀ x₁ x₂ y₀ y₁`. of *heterogeneous* identifications/bridges relating `y₀` and `y₁` "along" or "over" `x₂`. Since `Id` is a notational variant of `refl`, this type can also be written suggestively as `Id B x₀ x₁ x₂ y₀ y₁`. Such heterogeneous identity/bridge types are used in the computation (up to definitional isomorphism) of identity/bridge types of *dependent* function types. Specifically, `Id ((x:A) → B x) f g` acts like a function-type `(x₀ x₁ : A) (x₂ : Id A x₀ x₁) → refl B x₀ x₁ x₂ (f x₀) (g x₁)`. They also appear in identity/bridge types of other canonical types, such as when one field of a record type depends on previous ones. For instance, `Id (Σ A B) u v` behaves like a record type ``` @@ -1621,7 +1638,7 @@ B₂ : refl Π A₀ A₁ A₂ (x₀ ↦ Type) (x₁ ↦ Type) (x₀ x₁ x₂ In particular, this is what Narya uses when printing higher-dimensional function-types (although it also uses cube variables, see below). -### Higher-dimensional cubes and degeneracies +### Higher-dimensional cubes Iterating `Id` or `refl` multiple times produces higher-dimensional cube types and cubes. For instance, since `Id A` acts like a function `A → A → Type`, *its* identity type or reflexivity type `Id (Id A)` acts as a function-type ``` @@ -1629,13 +1646,40 @@ Iterating `Id` or `refl` multiple times produces higher-dimensional cube types a → (x₁₀ : A) (x₁₁ : A) (x₁₂ : Id A x₁₀ x₁₁) → (x₂₀ : Id A x₀₀ x₁₀) (x₂₁ : Id A x₀₁ x₁₁) → Type ``` -We can view this as assigning to any boundary for a 2-dimensional square a type of fillers for that square. Similarly, `Id (Id (Id A))` yields a type of 3-dumensional cubes, and so on. +We can view this as assigning to any boundary for a 2-dimensional square a type of fillers for that square. Similarly, `Id (Id (Id A))` yields a type of 3-dumensional cubes, and so on. Likewise, iterating `refl` on functions acts on these cubes: if `f : A → B`, then +``` +refl (refl f) : Id A a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁ + → Id B (f a₀₀) (f a₀₁) (refl f a₀₀ a₀₁ a₀₂) (f a₁₀) (f a₁₁) (refl f a₁₀ a₁₁ a₁₂) + (refl f a₀₀ a₁₀ a₂₀) (refl f a₀₁ a₁₁ a₂₁) +``` + +More generally, just as any "1-dimensional type" `A₂ : Id Type A₀ A₁` can be instantiated at endpoints `a₀:A₀` and `a₁:A₁` to produce an ordinary (0-dimensional) type `A₂ a₀ a₁ : Type`, any element `A₂₂ : Id (Id Type) A₀₀ A₀₁ A₀₂ A₁₀ A₁₁ A₁₂ A₂₀ A₂₁` can be instantiated at a "heterogeneous square boundary" consisting of +``` +a₀₀ : A₀₀ +a₀₁ : A₀₁ +a₀₂ : A₀₂ a₀₀ a₀₁ +a₁₀ : A₁₀ +a₁₁ : A₁₁ +a₁₂ : A₁₂ a₁₀ a₁₁ +a₂₀ : A₂₀ a₀₀ a₁₀ +a₂₁ : A₂₁ a₀₁ a₁₁ +``` +to obtain an ordinary 0-dimensional type `A₂₂ a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁` whose elements are "heterogeneous squares". + +We mentioned above that a 1-dimensional type cannot be "partially instantiated" such as `Id A a₀`. A higher-dimensional type *can* be partially instantiated, but not arbitrarily: you must give exactly enough arguments to reduce it to a type of some specific lower dimension. For a 2-dimensional type such as `A₂₂` above, this means that in addition to its full 0-dimensional instantiations such as `A₂₂ a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁`, it has partial 1-dimensional instantiations such as +``` +A₂₂ a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ : Id Type (A₂₀ a₀₀ a₁₀) (A₂₁ a₀₁ a₁₁) +``` +Note that this has exactly the right type that it can be *further* instantiated by `a₂₀ a₂₁` to produce a 0-dimensional type. In fact, the fundamental operation is actually a "partial instantiation" that reduces the dimension by one; a "full instantiation" is just a sequence of these. + + +### Symmetries and degeneracies There is a symmetry operation `sym` that acts on at-least-two dimensional cubes, swapping or transposing the last two dimensions. Like `refl`, if the argument of `sym` synthesizes, then the `sym` synthesizes a symmetrized type; but in this case the argument must synthesize a "2-dimensional" type. (The need to be able to "detect" 2-dimensionality here is roughly what imposes the requirements on our normalization/typechecking algorithm mentioned above.) In addition, unlike `refl`, an application of `sym` can also check if its argument does, since the type it is checked against can be "unsymmetrized" to obtain the necessary type for its argument to check against. Combining versions of `refl` and `sym` yields arbitrary higher-dimensional "degeneracies" (from the BCH cube category). There is also a generic syntax for such degeneracies, for example `M⁽²ᵉ¹⁾` or `M^(2e1)` where the superscript represents the degeneracy, with `e` denoting a degenerate dimension and nonzero digits denoting a permutation. (The `e` stands for "equality", since our `Id` is eventually intended to be the identity type of Higher Observational Type Theory.) In the unlikely event you are working with dimensions greater than nine, you can separate multi-digit numbers and letters with a hyphen, e.g. `M⁽¹⁻²⁻³⁻⁴⁻⁵⁻⁶⁻⁷⁻⁸⁻⁹⁻¹⁰⁾` or `M^(0-1-2-3-4-5-6-7-8-9-10)`. This notation can always synthesize if `M` does, while like `sym` it can also check if the degeneracy is a "pure permutation", consisting only of digits without any `e`s. -Degeneracies can be extended by identities on the left and remain the same operator. For instance, the two degeneracies taking a 1-dimensional object to a 2-dimensional one are denoted `1e` and `e1`, and of these `1e` can be written as simply `e` and coincides with ordinary `refl` applied to an object that happens to be 1-dimensional. +Degeneracies can be extended by identities on the left and remain the same operation. For instance, the two degeneracies taking a 1-dimensional object to a 2-dimensional one are denoted `1e` and `e1`, and of these `1e` can be written as simply `e` and coincides with ordinary `refl` applied to an object that happens to be 1-dimensional. Similarly, the basic symmetry `sym` of a 3-dimensional object actually acts on the last two dimensions, so it coincides with the superscripted operation `132`. A mnemonic for the names of permutation operators is that the permutation numbers indicate the motion of arguments. For instance, if we have a 3-dimensional cube ``` @@ -1654,14 +1698,39 @@ a222⁽³¹²⁾ : A⁽ᵉᵉᵉ⁾ Degeneracy operations are functorial. For pure symmetries, this means composing permutations. For instance, the "Yang-Baxter equation" holds, equating `M⁽²¹³⁾⁽¹³²⁾⁽²¹³⁾` with `M⁽¹³²⁾⁽²¹³⁾⁽¹³²⁾`, as both reduce to `M⁽³²¹⁾`. Reflexivities also compose with permutations in a fairly straightforward way, e.g. `M⁽¹ᵉ⁾⁽²¹⁾` reduces to `M^⁽ᵉ¹⁾`. -The principle that the identity/bridge types of a canonical type are again canonical types of the same sort applies also to higher degeneracies, with one exception. Ordinary canonical types are "intrinsically" 0-dimensional, and therefore any operations on them reduce to a "pure degeneracy" consisting entirely of `e`s, e.g. `M⁽ᵉᵉ⁾⁽²¹⁾` reduces to simply `M⁽ᵉᵉ⁾`. These pure degeneracies of canonical types are again canonical types of the same form, as discussed for `Id` and `refl` above. However, an intrinsically higher-dimensional canonical type like `Gel` admits some degeneracies that permute the intrinsic dimension with some of the additional dimensions; the simplest of these is `e1`. These degeneracies of a higher-dimensional canonical type are *not* any longer canonical; but they are isomorphic to a canonical type by the action of a pure symmetry. +The principle that the identity/bridge types of a canonical type are again canonical types of the same sort applies also to symmetries and higher degeneracies of such types, with one exception. To explain the exception, observe that ordinary canonical types are "intrinsically" 0-dimensional, and therefore any operations on them reduce to a "pure degeneracy" consisting entirely of `e`s, e.g. `M⁽ᵉᵉ⁾⁽²¹⁾` reduces to simply `M⁽ᵉᵉ⁾`. These pure degeneracies of canonical types are again canonical types of the same form, as discussed for `Id` and `refl` above. However, an intrinsically higher-dimensional canonical type like `Gel` admits some degeneracies that permute the intrinsic dimension with some of the additional dimensions; the simplest of these is `1e`. These degeneracies of a higher-dimensional canonical type are *not* any longer canonical; but they are isomorphic to a canonical type by the action of a pure symmetry. For instance, `Gel A B R` is a 1-dimensional type, belonging to `Id Type A B`. Thus, we can form the 2-dimensional type `(Gel A B R)⁽ᵉ¹⁾`, and instantiate it using `a₂ : Id A a₀ a₁` and `b₂ : Id B b₀ b₁` and `r₀ : R a₀ b₀` and `r₁ : R a₁ b₁` to get a 0-dimensional type `(Gel A B R)⁽ᵉ¹⁾ a₀ b₀ (r₀,) a₁ b₁ (r₁,) a₂ b₂`. But this type is not canonical, and in particular not a record type; in particular given `M : (Gel A B R)⁽ᵉ¹⁾ a₀ b₀ (r₀,) a₁ b₁ (r₁,) a₂ b₂` we cannot write `M .ungel`. However, we have `sym M : (Gel A B R)⁽¹ᵉ⁾ a₀ a₁ a₂ b₀ b₁ b₂ (r₀,) (r₁,)`, which doesn't permute the intrinsic dimension `1` with the degenerate dimension `e` and *is* therefore a record type, and so we can write `sym M .ungel`, which has type `Id R a₀ a₁ a₂ b₀ b₁ b₂ r₀ r₁`. In addition, since `(Gel A B R)⁽ᵉ¹⁾ a₀ b₀ (r₀,) a₁ b₁ (r₁,) a₂ b₂` is *isomorphic* to this record type, it also satisfies an eta-rule: two of its terms `M` and `N` are definitionally equal as soon as `sym M .ungel` and `sym N .ungel` are. +### Implicit boundaries + +Until now we have been writing all the arguments of higher-dimensional types and functions explicitly. There are times when this is necessary, but it is clear that in many cases it is redundant. For instance, in `refl f a₀ a₁ a₂`, since the type of `a₂` must be `Id A a₀ a₁`, if we know this type (that is, if `a₂` synthesizes) then `a₀` and `a₁` are uniquely determined. + +In general, this is the sort of issue that implicit arguments and higher-order unification are designed to deal with. Narya does not yet have either of these features in general, but it does have a specialized version that essentially uses bidirectional typechecking to synthesize the redundant parts of boundaries in higher-dimensional function applications and type instantiations. This feature is currently off by default; it can be turned on with the two commands +``` +option function boundaries ≔ implicit +option type boundaries ≔ implicit +``` +(and back off again with the similar `≔ explicit` commands). + +When *function* boundaries are implicit, a higher-dimensional function application takes only *one* argument, the top-dimensional one; thus instead of `refl f a₀ a₁ a₂` you can (and must) write `refl f a₂`, and instead of `refl (refl f) a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁ a₂₂` you can (and must) write `refl f a₂₂`. It is possible to give the implicit arguments explicitly by surrounding them with curly braces, as in `refl f {a₀} {a₁} a₂`, but if you do this you must give *all* of them explicitly; there are no half measures. The main reason you might need to do this is if `a₂` is a term that doesn't synthesize, since in that case `refl f a₂` won't be able to infer the boundaries `a₀` and `a₁`. + +When *type* boundaries are implicit, a full instantiation of a higher-dimensional type takes only the *highest-dimensional* arguments. For ordinary 1-dimensional identity types, this changes nothing, since both arguments `a₀` and `a₁` of `Id A a₀ a₁` are 0-dimensional and that is the highest dimension of any argument. But for squares, instead of `Id (Id A) a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁` you can (and must) write `Id (Id A) a₀₂ a₁₂ a₂₀ a₂₁` since these are the four 1-dimensional arguments; the 0-dimensional ones are inferred from their boundaries (which are required to match up correctly where they overlap). And you can of course give them explicitly with `Id (Id A) {a₀₀} {a₀₁} a₀₂ {a₁₀} {a₁₁} a₁₂ a₂₀ a₂₁`. In this case there are some half measures: if you give any lower-dimensional argument explicitly you must give all the arguments in that "block" explictly, but you can omit those in other blocks; for instance you can write `Id (Id A) {a₀₀} {a₀₁} a₀₂ a₁₂ a₂₀ a₂₁` or `Id (Id A) a₀₂ {a₁₀} {a₁₁} a₁₂ a₂₀ a₂₁`. + +Normally, when boundaries are implicit, Narya also *prints* higher-dimensional function applications and type instantiations with the lower-dimensional boundaries omitted. However, you can tell it to print these arguments explicitly with the commands +``` +display function boundaries ≔ on +display type boundaries ≔ on +``` +(and switch back with `≔ off`). These commands are not available in source files, since they should not be un-done; they can be given in interactive mode, or in ProofGeneral with `C-c C-v`, or you can use the corresponding command-line flags such as `-show-function-boundaries`. When these options are `on` *and* implicitness for the relevant kinds of boundaries is also on, Narya prints *all* the lower-dimensional arguments explicitly, with curly braces around them. There are no half measures here, for functions or for types. In the future, we may implement a way to switch on such display for some constants and/or variables but not others. + +In addition, even when printing implicit boundaries is off, Narya attempts to be smart and print those boundaries when it thinks that they would be necessary in order to re-parse the printed term, because the corresponding explicit argument isn't synthesizing. In this case it can do half measures, the way you can when writing type boundaries: the implicit arguments in each "block" are printed only if the primary argument of that block is nonsynthesizing. + + ### Cubes of variables -Since there is no unifier and no implicit arguments yet, all the arguments of higher-dimensional cubes and functions must be given explicitly. However, there is a shorthand syntax for higher-dimensional abstractions: instead of `x₀ x₁ x₂ ↦ M` you can write `x ⤇ M` (or `x |=> M` in ASCII). This binds `x` as a "family" or "cube" of variables whose names are suffixed with face names in ternary notation: `x.0` and `x.1` and `x.2`, or in higher dimensions `x.00` through `x.22` and so on. (The dimension is inferred from the type at which the abstraction is checked.) Note that this is a *purely syntactic* abbreviation: there is no object "`x`", but rather there are really *three different variables* that just happen to have the names `x.0` and `x.1` and `x.2`. (There is no potential for collision with user-defined names, since ordinary local variable names cannot contain internal periods. Of course, `x.0` can shadow a global definition of a constant `0` in namespace `x`.) +Implicitness of arguments to higher-dimensional *applications* has no bearing on higher-dimensional *abstractions*: the "implicit arguments" still must be named in an abstraction in the usual way, regardless of whether implicitness is on or not. (This will also be Narya's approach to implicit arguments more generally.) However, there is a different shorthand syntax for higher-dimensional abstractions: instead of `x₀ x₁ x₂ ↦ M` you can write `x ⤇ M` (or `x |=> M` in ASCII). This binds `x` as a "family" or "cube" of variables whose names are suffixed with face names in ternary notation: `x.0` and `x.1` and `x.2`, or in higher dimensions `x.00` through `x.22` and so on. (The dimension is inferred from the type at which the abstraction is checked.) Note that this is a *purely syntactic* abbreviation: there is no object "`x`", but rather there are really *three different variables* that just happen to have the names `x.0` and `x.1` and `x.2`. (There is no potential for collision with user-defined names, since ordinary local variable names cannot contain internal periods. Of course, `x.0` can shadow a global definition of a constant `0` in namespace `x`.) These "cube variables" also appear automatically when matching against a higher-dimensional version of a datatype. For instance, we can do an encode-decode proof for the natural numbers by matching directly on `Id ℕ` (using pattern-matching abstractions): ``` @@ -1681,7 +1750,7 @@ def encode (m n : ℕ) : Id ℕ m n → code m n ≔ [ zero. ↦ () | suc. p ↦ (_ ≔ encode p.0 p.1 p.2)] ``` -Here in the definition of `encode`, the pattern variable `p` of the `suc.` branch is automatically made into a 1-dimensional cube of variables since we are matching against an element of `Id ℕ`, so in the body we can refer to `p.0`, `p.1`, and `p.2`. In the future, we may implement a dual syntax for simultaneously *applying* a function to a whole cube of variables of this sort as well. +Here in the definition of `encode`, the pattern variable `p` of the `suc.` branch is automatically made into a 1-dimensional cube of variables since we are matching against an element of `Id ℕ`, so in the body we can refer to `p.0`, `p.1`, and `p.2`. In the future, we may implement a dual syntax for simultaneously *applying* a higher-dimensional function to a whole cube of variables of this sort as well, although of course if implicit application is on you can just write `refl f x.2` and so on. Similarly, when defining a codatatype lying in a higher universe, the "self" variable automatically becomes a cube variable, so that the boundary of the type is accessible through its faces. For instance, here is a codatatype version of Gel: ``` diff --git a/bin/narya.ml b/bin/narya.ml index 3c071c41..e825a481 100644 --- a/bin/narya.ml +++ b/bin/narya.ml @@ -33,6 +33,18 @@ let speclist = ("-compact", Arg.Set compact, "Reformat code compactly"); ("-unicode", Arg.Set unicode, "Display and reformat code using Unicode for built-ins (default)"); ("-ascii", Arg.Clear unicode, "Display and reformat code using ASCII for built-ins"); + ( "-hide-function-boundaries", + Arg.Clear show_function_boundaries, + "Hide implicit boundaries of higher-dimensional applications (default)" ); + ( "-show-function-boundaries", + Arg.Set show_function_boundaries, + "Display implicit boundaries of higher-dimensional applications" ); + ( "-hide-type-boundaries", + Arg.Clear show_type_boundaries, + "Hide implicit boundaries of instantiations of higher-dimensional types (default)" ); + ( "-show-type-boundaries", + Arg.Set show_type_boundaries, + "Display implicit boundaries of instantiations of higher-dimensional types" ); ("-arity", Arg.Set_int arity, "Arity of parametricity (default = 2)"); ( "-direction", Arg.String set_refls, diff --git a/lib/core/check.ml b/lib/core/check.ml index a294cf04..55c52622 100644 --- a/lib/core/check.ml +++ b/lib/core/check.ml @@ -130,11 +130,14 @@ let vars_of_names : (* Slurp up an entire application spine. Returns the function, and all the arguments, where each argument is paired with the location of its application. So spine "f x y" would return "f" (located) along with [(location of "f x", "x" (located)); (location of "f x y", "y" (located))]. *) let spine : - type a. a synth located -> a synth located * (Asai.Range.t option * a check located) list = + type a. + a synth located -> + a synth located + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list = fun tm -> let rec spine tm args = match tm.value with - | Raw.App (fn, arg) -> spine fn ((tm.loc, arg) :: args) + | Raw.App (fn, arg, impl) -> spine fn ((tm.loc, arg, impl) :: args) | _ -> (tm, args) in spine tm [] @@ -466,6 +469,7 @@ let rec check : let new_sfn = locate_opt fn.loc (Term.App (sfn, CubeOf.singleton cty)) in let new_sty = tyof_app cods tyargs (CubeOf.singleton ty) in (* And then proceed applying to the rest of the arguments. *) + let args = List.map (fun (l, x) -> (l, x, locate_opt None `Explicit)) args in let stm, sty = synth_apps (Kinetic `Nolet) ctx new_sfn new_sty fn args in (* Then we have to check that the resulting type of the whole application agrees with the one we're checking against. *) equal_val (Ctx.length ctx) sty ty @@ -1794,7 +1798,7 @@ and synth_apps : (b, kinetic) term located -> kinetic value -> a synth located -> - (Asai.Range.t option * a check located) list -> + (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list -> (b, kinetic) term * kinetic value = fun status ctx sfn sty fn args -> (* To determine what to do, we inspect the (fully instantiated) *type* of the function being applied. Failure of view_type here is really a bug, not a user error: the user can try to check something against an abstraction as if it were a type, but our synthesis functions should never synthesize (say) a lambda-abstraction as if it were a type. *) @@ -1818,22 +1822,52 @@ and synth_apps : Annotate.tm ctx asfn.value); synth_apps status ctx asfn aty afn aargs -and synth_app : - type a b n. +(* This is a common subroutine for synth_app and synth_inst that picks up a whole cube of arguments and checks their types. Since in one case we need a cube of values and the other case a cube of normals, we let the caller choose. *) +and synth_arg_cube : + type a b n c. + err:Reporter.Code.t -> + implicit:[ `Implicit | `Explicit ] -> + which:string -> (a, b) Ctx.t -> - (b, kinetic) term located -> + (kinetic value -> normal -> c) -> (n, kinetic value) CubeOf.t -> - (n, unit) BindCube.t -> - (D.zero, n, n, normal) TubeOf.t -> - a synth located -> - (Asai.Range.t option * a check located) list -> - (b, kinetic) term located - * kinetic value + Asai.Range.t option * a synth located - * (Asai.Range.t option * a check located) list = - fun ctx sfn doms cods tyargs fn args -> + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list -> + ((n, (b, kinetic) term) CubeOf.t * (n, c) CubeOf.t) + * (Asai.Range.t option + * a synth located + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list) = + fun ~err ~implicit ~which ctx choose doms (sfnloc, fn, args) -> + (* Based on the global implicit-function-boundaries setting, the dimension of the application, and whether the first argument is implicit, decide whether we are taking a whole cube of arguments or only one argument with the boundary synthesized from it. *) + let module TakenArgs = struct + type t = Take | Given : (n, 'k, 'nk) D.plus * (D.zero, 'nk, 'nk, normal) TubeOf.t -> t + end in + let taken_args : TakenArgs.t = + match (args, implicit, D.compare_zero (CubeOf.dim doms)) with + | [], _, _ -> fatal err + (* If the application if zero-dimensional, or if the global setting is explicit, or if the global setting is implicit and the first argument is implicit, take a whole cube. *) + | _, _, Zero | _, `Explicit, Pos _ | (_, _, { value = `Implicit; _ }) :: _, `Implicit, Pos _ -> + Take + (* Otherwise, the first argument must be explicit and synthesizing. *) + | (_, { value = Synth toptm; loc }, { value = `Explicit; _ }) :: _, `Implicit, Pos _ -> ( + (* We synthesize its type, extract the instantiation arguments, and store them to fill in the boundary arguments. *) + let _, argty = synth (Kinetic `Nolet) ctx (locate_opt loc toptm) in + let (Full_tube argtyargs) = get_tyargs argty "primary argument" in + (* A function of one dimension can be applied to a primary argument of a *higher* dimension, since a cube is also a square. So we require only that the dimension of argtyargs factors through the application dimension. *) + match factor (TubeOf.inst argtyargs) (CubeOf.dim doms) with + | Some (Factor nk) -> Given (nk, argtyargs) + | None -> + fatal ~severity:Asai.Diagnostic.Error ?loc + (Dimension_mismatch + ("primary " ^ which ^ " argument", TubeOf.inst argtyargs, CubeOf.dim doms))) + | (_, _, { value = `Explicit; _ }) :: _, `Implicit, Pos _ -> + fatal (Nonsynthesizing ("primary argument with implicit " ^ which ^ " boundaries")) in let module M = Monad.State (struct - type t = Asai.Range.t option * a synth located * (Asai.Range.t option * a check located) list + type t = + Asai.Range.t option + * a synth located + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list end) in (* Pick up the right number of arguments for the dimension, leaving the others for a later call to synth_app. Then check each argument against the corresponding type in "doms", instantiated at the appropriate evaluated previous arguments, and evaluate it, producing Cubes of checked terms and values. Since each argument has to be checked against a type instantiated at the *values* of the previous ones, we also store those in a hashtable as we go. *) let eargtbl = Hashtbl.create 10 in @@ -1846,12 +1880,7 @@ and synth_app : (fun fa [ dom ] -> let open Monad.Ops (M) in let* loc, f, ts = M.get in - let* tm = - match ts with - | [] -> with_loc loc @@ fun () -> fatal Not_enough_arguments_to_function - | (l, t) :: ts -> - let* () = M.put (l, locate_opt l (App (f, t)), ts) in - return t in + (* The type of this argument is obtained by instantiating the domain higher-dimensional type at the previous arguments. *) let ty = inst dom (TubeOf.build D.zero @@ -1861,12 +1890,69 @@ and synth_app : (fun fc -> Hashtbl.find eargtbl (SFace_of (comp_sface fa (sface_of_tface fc)))); }) in - let ctm = check (Kinetic `Nolet) ctx tm ty in - let tm = eval_term (Ctx.env ctx) ctm in - Hashtbl.add eargtbl (SFace_of fa) { tm; ty }; - return (ctm @: [ tm ])); + let* ctm, tm = + match (pface_of_sface fa, taken_args) with + (* If we are synthesizing the implicit boundary and this is a proper face, we look up the corresponding normal value, check that it has the correct type, and read it back to get the required checked term. *) + | `Proper fa, Given (nk, argtyargs) -> + let (Plus ml) = D.plus (D.plus_right nk) in + let { tm = etm; ty = ety } = TubeOf.find argtyargs (pface_plus fa nk ml) in + equal_val (Ctx.length ctx) ety ty + (* TODO: The location of this error is problematic, since the implicit argument isn't there to locate it on. *) + <|> Unequal_synthesized_type (PVal (ctx, ety), PVal (ctx, ty)); + let ctm = readback_at ctx etm ety in + return (ctm, etm) + (* Otherwise, we pull an argument of the appropriate implicitness, check it against the correct type. *) + | _ -> + let* tm = + match ts with + | [] -> with_loc loc @@ fun () -> fatal err + | (l, t, ({ value = i; loc } as impl)) :: ts -> + (match (is_id_sface fa, i, implicit) with + | Some _, `Implicit, _ -> + fatal ?loc + (Unexpected_implicitness + (`Implicit, "expecting primary " ^ which ^ " argument")) + | None, `Implicit, `Explicit -> + fatal ?loc + (Unexpected_implicitness + (`Implicit, which ^ " boundaries are explicit")) + | None, `Explicit, `Implicit -> + fatal ?loc + (Unexpected_implicitness + (`Explicit, which ^ " boundaries are implicit")) + | _ -> ()); + let* () = M.put (l, locate_opt l (App (f, t, impl)), ts) in + return t in + let ctm = check (Kinetic `Nolet) ctx tm ty in + let etm = eval_term (Ctx.env ctx) ctm in + return (ctm, etm) in + (* In both cases, we store the resulting value term as a normal in the hashtable of previous values, to use in instantiating later types. *) + let ntm = { tm; ty } in + Hashtbl.add eargtbl (SFace_of fa) ntm; + return (ctm @: [ choose tm ntm ])); } - [ doms ] (Cons (Cons Nil)) (sfn.loc, fn, args) in + [ doms ] (Cons (Cons Nil)) (sfnloc, fn, args) in + ((cargs, eargs), (newloc, newfn, rest)) + +and synth_app : + type a b n. + (a, b) Ctx.t -> + (b, kinetic) term located -> + (n, kinetic value) CubeOf.t -> + (n, unit) BindCube.t -> + (D.zero, n, n, normal) TubeOf.t -> + a synth located -> + (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list -> + (b, kinetic) term located + * kinetic value + * a synth located + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list = + fun ctx sfn doms cods tyargs fn args -> + let implicit = Implicitboundaries.functions () in + let (cargs, eargs), (newloc, newfn, rest) = + synth_arg_cube ~err:Not_enough_arguments_to_function ~implicit ~which:"function" ctx + (fun tm _ -> tm) + doms (sfn.loc, fn, args) in (* Evaluate cod at these evaluated arguments and instantiate it at the appropriate values of tyargs. *) let output = tyof_app cods tyargs eargs in ({ value = Term.App (sfn.value, cargs); loc = newloc }, output, newfn, rest) @@ -1877,62 +1963,41 @@ and synth_inst : (b, kinetic) term located -> (D.zero, n, n, normal) TubeOf.t -> a synth located -> - (Asai.Range.t option * a check located) list -> + (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list -> (b, kinetic) term located * kinetic value * a synth located - * (Asai.Range.t option * a check located) list = + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list = fun ctx sfn tyargs fn args -> - let module M = Monad.State (struct - type t = Asai.Range.t option * a synth located * (Asai.Range.t option * a check located) list - end) in let n = TubeOf.inst tyargs in match D.compare_zero n with | Zero -> fatal (Instantiating_zero_dimensional_type (PTerm (ctx, sfn.value))) | Pos pn -> + let implicit = Implicitboundaries.types () in (* We take enough arguments to instatiate a type of dimension n by one. *) - let (Is_suc (m, msuc)) = suc_pos pn in - let open TubeOf.Monadic (M) in - let open TubeOf.Infix in - (* We will need random access to the previously evaluated arguments, so we store them in a hashtable as we go. *) - let eargtbl = Hashtbl.create 10 in - let tyargs1 = TubeOf.pboundary (D.zero_plus m) msuc tyargs in - (* What we really want, however, are two tubes of checked arguments *and* evaluated arguments. *) - let [ cargs; eargs ], (newloc, newfn, rest) = - pmapM - { - map = - (fun fa [ tyarg ] -> - (* We iterate monadically with the list of available arguments in a state/maybe monad, taking one more argument every time we need it as long as there is one. *) - let open Monad.Ops (M) in - let* loc, f, ts = M.get in - let* tm = - match ts with - | [] -> with_loc loc @@ fun () -> fatal Not_enough_arguments_to_instantiation - | (l, t) :: ts -> - let* () = M.put (l, locate_opt l (App (f, t)), ts) in - return t in - (* We check each such argument against the corresponding type instantiation argument, itself instantiated at the values of the appropriate previous arguments. *) - let fa = sface_of_tface fa in - let k = dom_sface fa in - let kargs = - TubeOf.build D.zero (D.zero_plus k) - { - build = - (fun fb -> - Hashtbl.find eargtbl (SFace_of (comp_sface fa (sface_of_tface fb)))); - } in - let ty = inst tyarg.tm kargs in - let ctm = check (Kinetic `Nolet) ctx tm ty in - (* Then we evaluate it and assemble a normal version to store in the hashtbl, before returning the checked and evaluated versions. *) - let tm = eval_term (Ctx.env ctx) ctm in - let ntm = { tm; ty } in - Hashtbl.add eargtbl (SFace_of fa) ntm; - return (ctm @: [ ntm ])); - } - [ tyargs1 ] (Cons (Cons Nil)) (sfn.loc, fn, args) in + let (Is_suc (m, msuc, k)) = suc_pos pn in + let tyargs1 = + TubeOf.mmap + { map = (fun _ [ { tm; ty = _ } ] -> tm) } + [ TubeOf.pboundary (D.zero_plus m) msuc tyargs ] in + let (Wrap l) = Endpoints.wrapped () in + let doms = TubeOf.to_cube_bwv k msuc l tyargs1 in + let module M = Monad.State (struct + type t = + Asai.Range.t option + * a synth located + * (Asai.Range.t option * a check located * [ `Implicit | `Explicit ] located) list + end) in + let open Bwv.Monadic (M) in + let (cargs, nargs), (newloc, newfn, rest) = + mapM1_2 + (synth_arg_cube ~err:Not_enough_arguments_to_instantiation ~implicit ~which:"type" ctx + (fun _ ntm -> ntm)) + doms (sfn.loc, fn, args) in (* The synthesized type *of* the instantiation is itself a full instantiation of a universe, at the instantiations of the type arguments at the evaluated term arguments. This is computed by tyof_inst. *) - ({ value = Term.Inst (sfn.value, cargs); loc = newloc }, tyof_inst tyargs eargs, newfn, rest) + let cargs = TubeOf.of_cube_bwv m k msuc l cargs in + let nargs = TubeOf.of_cube_bwv m k msuc l nargs in + ({ value = Term.Inst (sfn.value, cargs); loc = newloc }, tyof_inst tyargs nargs, newfn, rest) (* Check a list of terms against the types specified in a telescope, evaluating the latter in a supplied environment and in the context of the previously checked terms, and instantiating them at values given in a tube. See description in context of the call to it above during typechecking of a constructor. *) and check_at_tel : diff --git a/lib/core/dump.ml b/lib/core/dump.ml index d81e2a56..24a4d8c9 100644 --- a/lib/core/dump.ml +++ b/lib/core/dump.ml @@ -183,7 +183,10 @@ and synth : type a. formatter -> a synth -> unit = | Const c -> fprintf ppf "Const(%a)" pp_printed (print (PConstant c)) | Field (tm, fld) -> fprintf ppf "Field(%a, %s)" synth tm.value (Field.to_string_ori fld) | Pi (_, _, _) -> fprintf ppf "Pi(?)" - | App (fn, arg) -> fprintf ppf "App(%a, %a)" synth fn.value check arg.value + | App (fn, arg, { value = `Explicit; _ }) -> + fprintf ppf "App(%a, %a)" synth fn.value check arg.value + | App (fn, arg, { value = `Implicit; _ }) -> + fprintf ppf "App(%a, {%a})" synth fn.value check arg.value | Asc (tm, ty) -> fprintf ppf "Asc(%a, %a)" check tm.value check ty.value | Let (_, _, _) -> fprintf ppf "Let(?)" | Letrec (_, _, _) -> fprintf ppf "LetRec(?)" diff --git a/lib/core/implicitboundaries.ml b/lib/core/implicitboundaries.ml new file mode 100644 index 00000000..bc06b87c --- /dev/null +++ b/lib/core/implicitboundaries.ml @@ -0,0 +1,10 @@ +open Reporter + +let forward_functions : (unit -> [ `Implicit | `Explicit ]) ref = + ref (fun () -> fatal (Anomaly "Implicitboundaries.functions not set")) + +let forward_types : (unit -> [ `Implicit | `Explicit ]) ref = + ref (fun () -> fatal (Anomaly "Implicitboundaries.functions not set")) + +let functions () = !forward_functions () +let types () = !forward_types () diff --git a/lib/core/norm.ml b/lib/core/norm.ml index b520b63b..5c07455d 100644 --- a/lib/core/norm.ml +++ b/lib/core/norm.ml @@ -35,7 +35,7 @@ let rec take_args : | arg :: args, Suc plus -> take_args (Ext (env, mn, Ok arg)) mn args plus | _ -> fatal (Anomaly "wrong number of arguments in argument list") -(* A "view" is the aspect of a type or term that we match against to determine its behavior. A view of a term is just another term, but in WHNF. A view of a type is either a universe, a pi-type, another canonical type (data or codata), or a neutral. The non-neutral sorts come with their instantiations that have been checked to have the correct dimension. *) +(* A "view" is the aspect of a type or term that we match against to determine its behavior. A view of a term is just another term, but in WHNF. A view of a type is either a universe, a pi-type, another canonical type (data or codata), or a neutral. All come with their instantiations that have been checked to have the correct dimension. *) type view_type = | UU : (D.zero, 'k, 'k, normal) TubeOf.t -> view_type @@ -46,7 +46,7 @@ type view_type = * (D.zero, 'k, 'k, normal) TubeOf.t -> view_type | Canonical : head * 'k canonical * (D.zero, 'k, 'k, normal) TubeOf.t -> view_type - | Neutral : head -> view_type + | Neutral : head * (D.zero, 'k, 'k, normal) TubeOf.t -> view_type let rec view_term : type s. s value -> s value = fun tm -> @@ -121,7 +121,7 @@ and view_type ?(severity = Asai.Diagnostic.Bug) (ty : kinetic value) (err : stri (* Always a bug *) fatal (Dimension_mismatch ("view canonical", dim_canonical c, TubeOf.inst tyargs))) | Realize v -> view_type ~severity (inst v tyargs) err - | _ -> Neutral head) + | _ -> Neutral (head, tyargs)) (* Evaluation of terms and evaluation of case trees are technically separate things. In particular, evaluating a kinetic (standard) term always produces just a value, whereas evaluating a potential term (a function case tree) can either @@ -1008,6 +1008,15 @@ let rec tyof_inst : } in inst (universe m) margs +(* Get the instantiation arguments of a type, of any sort. *) +let get_tyargs ?(severity = Asai.Diagnostic.Bug) (ty : kinetic value) (err : string) : + normal full_tube = + match view_type ~severity ty err with + | UU tyargs -> Full_tube tyargs + | Pi (_, _, _, tyargs) -> Full_tube tyargs + | Canonical (_, _, tyargs) -> Full_tube tyargs + | Neutral (_, tyargs) -> Full_tube tyargs + (* Check whether a given type is discrete, or has one of the the supplied constant heads (since for testing whether a newly defined datatype can be discrete, it and members of its mutual families can appear in its own parameters and arguments). *) let is_discrete : ?discrete:unit Constant.Map.t -> kinetic value -> bool = fun ?discrete ty -> @@ -1016,7 +1025,7 @@ let is_discrete : ?discrete:unit Constant.Map.t -> kinetic value -> bool = (* The currently-being-defined types may not be canonical yet: if they don't have definitions yet they are neutral. *) | Canonical (Const { name; ins }, _, _), Some consts -> Option.is_some (is_id_ins ins) && Constant.Map.mem name consts - | Neutral (Const { name; ins }), Some consts -> + | Neutral (Const { name; ins }, _), Some consts -> Option.is_some (is_id_ins ins) && Constant.Map.mem name consts (* In theory, pi-types with discrete codomain, and record types with discrete fields, could also be discrete. But that would be trickier to check as it would require evaluating their codomain and fields under binders, and eta-conversion for those types should implement direct discreteness automatically. So the only thing we're missing is that they can't appear as arguments to a constructor of some other discrete datatype. *) | _ -> false diff --git a/lib/core/raw.ml b/lib/core/raw.ml index 8bedf5d7..3e10b8c6 100644 --- a/lib/core/raw.ml +++ b/lib/core/raw.ml @@ -107,7 +107,8 @@ module Make (I : Indices) = struct | Const : Constant.t -> 'a synth | Field : 'a synth located * Field.or_index -> 'a synth | Pi : I.name * 'a check located * 'a I.suc check located -> 'a synth - | App : 'a synth located * 'a check located -> 'a synth + (* The location of the implicitness flag is, in the implicit case, the location of the braces surrounding the implicit argument. *) + | App : 'a synth located * 'a check located * [ `Implicit | `Explicit ] located -> 'a synth | Asc : 'a check located * 'a check located -> 'a synth | UU : 'a synth (* A Let can either synthesize or (sometimes) check. It synthesizes only if its body also synthesizes, but we wait until typechecking type to look for that, so that if it occurs in a checking context the body can also be checking. Thus, we make it a "synthesizing term". The term being bound must also synthesize; the shorthand notation "let x : A := M" is expanded during parsing to "let x := M : A". *) @@ -247,7 +248,7 @@ module Resolve (R : Resolver) = struct | Const c -> Const c | Field (tm, fld) -> Field (synth ctx tm, fld) | Pi (x, dom, cod) -> Pi (R.rename ctx x, check ctx dom, check (R.snoc ctx x) cod) - | App (fn, arg) -> App (synth ctx fn, check ctx arg) + | App (fn, arg, impl) -> App (synth ctx fn, check ctx arg, impl) | Asc (tm, ty) -> Asc (check ctx tm, check ctx ty) | UU -> UU | Let (x, tm, body) -> Let (R.rename ctx x, synth ctx tm, (check (R.snoc ctx x)) body) diff --git a/lib/core/reporter.ml b/lib/core/reporter.ml index 4b0e55aa..c1611459 100644 --- a/lib/core/reporter.ml +++ b/lib/core/reporter.ml @@ -91,6 +91,7 @@ module Code = struct | Low_dimensional_argument_of_degeneracy : (string * 'a D.t) -> t | Missing_argument_of_degeneracy : string -> t | Applying_nonfunction_nontype : printable * printable -> t + | Unexpected_implicitness : [ `Implicit | `Explicit ] * string -> t | Unimplemented : string -> t | Matching_datatype_has_degeneracy : printable -> t | Wrong_number_of_arguments_to_pattern : Constr.t * int -> t @@ -164,6 +165,7 @@ module Code = struct | Section_closed : string list -> t | No_such_section : t | Display_set : string * string -> t + | Option_set : string * string -> t | Break : t | Accumulated : t Asai.Diagnostic.t Bwd.t -> t | No_holes_allowed : string -> t @@ -214,6 +216,7 @@ module Code = struct | Invalid_variable_face _ -> Error | Not_enough_arguments_to_instantiation -> Error | Applying_nonfunction_nontype _ -> Error + | Unexpected_implicitness _ -> Error | Wrong_number_of_arguments_to_constructor _ -> Error | Unimplemented _ -> Error | Matching_datatype_has_degeneracy _ -> Error @@ -287,6 +290,7 @@ module Code = struct | Section_closed _ -> Info | No_such_section -> Error | Display_set _ -> Info + | Option_set _ -> Info | Break -> Error | Accumulated _ -> Error | No_holes_allowed _ -> Error @@ -341,6 +345,7 @@ module Code = struct (* Function-types *) | Checking_lambda_at_nonfunction _ -> "E0700" | Applying_nonfunction_nontype _ -> "E0701" + | Unexpected_implicitness _ -> "E0702" (* Record fields *) | No_such_field _ -> "E0800" (* Tuples *) @@ -436,7 +441,8 @@ module Code = struct | Commands_undone _ -> "I0006" | Section_opened _ -> "I0007" | Section_closed _ -> "I0008" - | Display_set _ -> "I0100" + | Option_set _ -> "I0100" + | Display_set _ -> "I0101" (* Control of execution *) | Quit _ -> "I0200" | Break -> "E0201" @@ -579,6 +585,12 @@ module Code = struct textf "@[attempt to apply/instantiate@;<1 2>%a@ of type@;<1 2>%a@ which is not a function-type or universe@]" pp_printed (print tm) pp_printed (print ty) + | Unexpected_implicitness (i, str) -> + textf "unexpected %s argument: %s" + (match i with + | `Implicit -> "implicit" + | `Explicit -> "explicit") + str | Unimplemented str -> textf "%s not yet implemented" str | Matching_datatype_has_degeneracy ty -> textf "@[can't match on element of datatype@;<1 2>%a@ that has a degeneracy applied@]" @@ -733,6 +745,7 @@ module Code = struct | Section_opened prefix -> textf "section %s opened" (String.concat "." prefix) | Section_closed prefix -> textf "section %s closed" (String.concat "." prefix) | Display_set (setting, str) -> textf "display set %s to %s" setting str + | Option_set (setting, str) -> textf "option set %s to %s" setting str | No_such_section -> text "no section here to end" | Break -> text "user interrupt" | No_holes_allowed cmd -> textf "command '%s' cannot contain holes" cmd diff --git a/lib/dim/dim.ml b/lib/dim/dim.ml index 2d9e2d8e..8a7a2143 100644 --- a/lib/dim/dim.ml +++ b/lib/dim/dim.ml @@ -9,6 +9,7 @@ let is_pos : type n. n D.t -> bool = function module Endpoints = Endpoints include Arith +include Singleton include Deg include Perm include Sface @@ -32,19 +33,12 @@ let string_of_dim : type n. n D.t -> string = fun n -> string_of_deg (deg_zero n (* ********** Special generators ********** *) -type one = D.one - -let one = D.one let refl : (one, D.zero) deg = Zero D.one type two = D.two let sym : (two, two) deg = Suc (Suc (Zero D.zero, Now), Later Now) -type _ is_suc = Is_suc : 'n D.t * ('n, one, 'm) D.plus -> 'm is_suc - -let suc_pos : type n. n D.pos -> n is_suc = fun (Pos n) -> Is_suc (n, Suc Zero) - let deg_of_name : string -> any_deg option = fun str -> if List.exists (fun s -> s = str) (Endpoints.refl_names ()) then Some (Any refl) diff --git a/lib/dim/dim.mli b/lib/dim/dim.mli index 9ea52a25..75d74375 100644 --- a/lib/dim/dim.mli +++ b/lib/dim/dim.mli @@ -16,10 +16,17 @@ module Endpoints : sig val run : arity:int -> refl_char:char -> refl_names:string list -> internal:bool -> (unit -> 'a) -> 'a + val uniq : 'l1 len -> 'l2 len -> ('l1, 'l2) Eq.t + val len : 'l len -> 'l N.t val wrapped : unit -> wrapped val internal : unit -> bool end +type _ is_singleton +type _ is_suc = Is_suc : 'n D.t * ('n, 'one, 'm) D.plus * 'one is_singleton -> 'm is_suc + +val suc_pos : 'n D.pos -> 'n is_suc + type any_dim = Any : 'n D.t -> any_dim val dim_of_string : string -> any_dim option @@ -216,6 +223,7 @@ val tface_plus : type ('m, 'n) pface = ('m, D.zero, 'n, 'n) tface val pface_of_sface : ('m, 'n) sface -> [ `Proper of ('m, 'n) pface | `Id of ('m, 'n) Eq.t ] +val pface_plus : ('k, 'm) pface -> ('m, 'n, 'mn) D.plus -> ('k, 'n, 'kn) D.plus -> ('kn, 'mn) pface val sface_plus_tface : ('k, 'm) sface -> @@ -247,6 +255,15 @@ type (_, _, _) pface_of_plus = val pface_of_plus : ('m, 'n, 'k, 'nk) tface -> ('m, 'n, 'k) pface_of_plus +val singleton_tface : + ('m, 'n, 'k, 'nk) tface -> 'k is_singleton -> 'l Endpoints.len -> ('m, 'n) sface * 'l N.index + +val is_codim1 : ('m, 'n, 'k, 'nk) tface -> unit option + +type (_, _, _) tface_of = Tface_of : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of + +val codim1_envelope : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of + module Tube (F : Fam2) : sig module C : module type of Cube (F) @@ -259,6 +276,21 @@ module Tube (F : Fam2) : sig val pboundary : ('m, 'k, 'mk) D.plus -> ('k, 'l, 'kl) D.plus -> ('m, 'kl, 'mkl, 'b) t -> ('mk, 'l, 'mkl, 'b) t + val of_cube_bwv : + 'n D.t -> + 'k is_singleton -> + ('n, 'k, 'nk) D.plus -> + 'l Endpoints.len -> + (('n, 'b) C.t, 'l) Bwv.t -> + ('n, 'k, 'nk, 'b) t + + val to_cube_bwv : + 'k is_singleton -> + ('n, 'k, 'nk) D.plus -> + 'l Endpoints.len -> + ('n, 'k, 'nk, 'b) t -> + (('n, 'b) C.t, 'l) Bwv.t + val plus : ('m, 'k, 'mk, 'b) t -> ('m, 'k, 'mk) D.plus val inst : ('m, 'k, 'mk, 'b) t -> 'k D.t val uninst : ('m, 'k, 'mk, 'b) t -> 'm D.t @@ -554,13 +586,6 @@ module Plusmap : sig end (* *) -type one - -val one : one D.t - -type _ is_suc = Is_suc : 'n D.t * ('n, one, 'm) D.plus -> 'm is_suc - -val suc_pos : 'n D.pos -> 'n is_suc val deg_of_name : string -> any_deg option val name_of_deg : ('a, 'b) deg -> string option diff --git a/lib/dim/singleton.ml b/lib/dim/singleton.ml new file mode 100644 index 00000000..dcbfb361 --- /dev/null +++ b/lib/dim/singleton.ml @@ -0,0 +1,5 @@ +type one = D.one +type _ is_singleton = One : one is_singleton +type _ is_suc = Is_suc : 'n D.t * ('n, 'one, 'm) D.plus * 'one is_singleton -> 'm is_suc + +let suc_pos : type n. n D.pos -> n is_suc = fun (Pos n) -> Is_suc (n, Suc Zero, One) diff --git a/lib/dim/tface.ml b/lib/dim/tface.ml index 1797e558..f5613855 100644 --- a/lib/dim/tface.ml +++ b/lib/dim/tface.ml @@ -1,4 +1,5 @@ open Util +open Singleton open Sface (* "Tube faces" are strict faces that are constrained to lie in a particular tube. *) @@ -70,6 +71,10 @@ let rec pface_of_sface : type m n. (m, n) sface -> [ `Proper of (m, n) pface | ` | `Proper fb -> `Proper (Mid fb) | `Id Eq -> `Id Eq) +let pface_plus : + type m n mn k kn. (k, m) pface -> (m, n, mn) D.plus -> (k, n, kn) D.plus -> (kn, mn) pface = + fun d mn kn -> tface_plus d mn mn kn + (* Any strict face can be added to a tube face on the left to get another tube face. *) let rec sface_plus_tface : @@ -124,3 +129,31 @@ let pface_of_plus : type m n k nk. (m, n, k, nk) tface -> (m, n, k) pface_of_plu let (TFace_of_plus (pq, s, d)) = tface_of_plus Zero d in let Eq = D.plus_uniq (cod_plus_of_tface d) (D.zero_plus (codr_tface d)) in PFace_of_plus (pq, s, d) + +(* A tube face with exactly one instantiated dimension can be decomposed into an endpoint and a strict face. *) + +let singleton_tface : + type m n k nk l. + (m, n, k, nk) tface -> k is_singleton -> l Endpoints.len -> (m, n) sface * l N.index = + fun d k l -> + let One = k in + match d with + | End (s, n0, (l', i)) -> + let Zero = n0 in + let Eq = Endpoints.uniq l l' in + (s, i) + +(* A tface is codimension-1 if it has exactly one endpoint. *) + +let rec is_codim1 : type m n k nk. (m, n, k, nk) tface -> unit option = function + | End (fa, _, _) -> Option.map (fun _ -> ()) (is_id_sface fa) + | Mid s -> is_codim1 s + +type (_, _, _) tface_of = Tface_of : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of + +(* Every tface belongs to a unique codimension-1 tface. *) +let rec codim1_envelope : type m n k nk. (m, n, k, nk) tface -> (n, k, nk) tface_of = function + | End (fa, nk, l) -> Tface_of (End (id_sface (cod_sface fa), nk, l)) + | Mid s -> + let (Tface_of s1) = codim1_envelope s in + Tface_of (Mid s1) diff --git a/lib/dim/tube.ml b/lib/dim/tube.ml index e272cf45..d75d39fc 100644 --- a/lib/dim/tube.ml +++ b/lib/dim/tube.ml @@ -3,6 +3,7 @@ open Util open Signatures open Tlist open Hlist +open Singleton open Cube open Sface open Bwsface @@ -125,6 +126,32 @@ module Tube (F : Fam2) = struct (m, k, mk) D.plus -> (k, l, kl) D.plus -> (m, kl, mkl, b) t -> (mk, l, mkl, b) t = fun mk kl tr -> gpboundary mk kl tr + (* A tube that instantiates exactly one dimension is equivalently a Bwv of cubes. *) + let of_cube_bwv : + type n k nk b l. + n D.t -> + k is_singleton -> + (n, k, nk) D.plus -> + l Endpoints.len -> + ((n, b) C.t, l) Bwv.t -> + (n, k, nk, b) t = + fun n k nk l cubes -> + let One, Suc Zero = (k, nk) in + Branch (l, cubes, Leaf n) + + let to_cube_bwv : + type n k nk b l. + k is_singleton -> + (n, k, nk) D.plus -> + l Endpoints.len -> + (n, k, nk, b) t -> + ((n, b) C.t, l) Bwv.t = + fun k nk l tube -> + let One, Suc Zero = (k, nk) in + let (Branch (l', cubes, Leaf _)) = tube in + let Eq = Endpoints.uniq l l' in + cubes + (* Heterogeneous lists and multimaps *) (* The structure of hlists for tubes is exactly parallel to that for cubes. *) @@ -135,44 +162,6 @@ module Tube (F : Fam2) = struct ('m, 'k, 'mk, 'nk, 'x) gt * ('m, 'k, 'mk, 'nk, 'xs) hgt -> ('m, 'k, 'mk, 'nk, ('x, 'xs) cons) hgt - (* Unused *) - (* - type (_, _, _, _, _, _) hgts = - | Nil : ('m, 'k, 'mk, 'nk, nil, nil) hgts - | Cons : - ('m, 'k, 'mk, 'nk, 'xs, 'ys) hgts - -> ('m, 'k, 'mk, 'nk, ('x, 'xs) cons, (('m, 'k, 'mk, 'nk, 'x) gt, 'ys) cons) hgts - - let rec hlist_of_hgt : - type m k mk n xs ys. (m, k, mk, n, xs, ys) hgts -> (m, k, mk, n, xs) hgt -> ys hlist = - fun hs xs -> - match (hs, xs) with - | Nil, [] -> [] - | Cons hs, x :: xs -> x :: hlist_of_hgt hs xs - - let rec hgt_of_hlist : - type m k mk n xs ys. (m, k, mk, n, xs, ys) hgts -> ys hlist -> (m, k, mk, n, xs) hgt = - fun hs xs -> - match (hs, xs) with - | Nil, [] -> [] - | Cons hs, x :: xs -> x :: hgt_of_hlist hs xs - - let rec tlist_hgts : type m k mk n xs ys. (m, k, mk, n, xs, ys) hgts -> xs tlist -> ys tlist = - fun hs xs -> - match (hs, xs) with - | Nil, Nil -> Nil - | Cons hs, Cons xs -> Cons (tlist_hgts hs xs) - - type (_, _, _, _, _) has_hgts = - | Hgts : ('m, 'k, 'mk, 'nk, 'xs, 'xss) hgts -> ('m, 'k, 'mk, 'nk, 'xs) has_hgts - - let rec hgts_of_tlist : type m k mk n xs. xs tlist -> (m, k, mk, n, xs) has_hgts = function - | Nil -> Hgts Nil - | Cons xs -> - let (Hgts xss) = hgts_of_tlist xs in - Hgts (Cons xss) - *) - type (_, _, _) ends = | Ends : 'l Endpoints.len * ('mk, 'n, 'bs, 'hs) C.Heter.hgts * ('hs, 'l) Bwv.Heter.ht diff --git a/lib/parser/builtins.ml b/lib/parser/builtins.ml index 305a575e..d27a2592 100644 --- a/lib/parser/builtins.ml +++ b/lib/parser/builtins.ml @@ -19,6 +19,31 @@ let parens = make "parens" Outfix (* Parentheses are parsed, processed, and printed along with tuples, since their notation overlaps. *) +(* ******************** + Braces + ******************** *) + +(* Braces were defined in Postprocess; here we say how to parse and print them, and how *not* to process them on their own. *) + +let () = + set_tree braces (Closed_entry (eop LBrace (term RBrace (Done_closed braces)))); + set_processor braces { process = (fun _ _ _ _ -> fatal Parse_error) }; + set_print braces (fun space ppf obs ws -> + match obs with + | [ body ] -> + let wslbrace, ws = take LBrace ws in + let wsrbrace, ws = take RBrace ws in + taken_last ws; + pp_open_hovbox ppf 1; + if true then ( + pp_tok ppf LBrace; + pp_ws `None ppf wslbrace; + pp_term `None ppf body; + pp_tok ppf RBrace); + pp_close_box ppf (); + pp_ws space ppf wsrbrace + | _ -> fatal (Anomaly "invalid notation arguments for braces")) + (* ******************** Let-binding ******************** *) @@ -1915,6 +1940,7 @@ let builtins = ref (Situation.empty |> Situation.add parens + |> Situation.add braces |> Situation.add letin |> Situation.add letrec |> Situation.add asc diff --git a/lib/parser/command.ml b/lib/parser/command.ml index 9c167f2a..9d466025 100644 --- a/lib/parser/command.ml +++ b/lib/parser/command.ml @@ -81,7 +81,20 @@ module Command = struct wscoloneq : Whitespace.t list; what : [ `Style of Whitespace.t list * Display.style * Whitespace.t list - | `Chars of Whitespace.t list * Display.chars * Whitespace.t list ]; + | `Chars of Whitespace.t list * Display.chars * Whitespace.t list + | `Function_boundaries of + Whitespace.t list * Whitespace.t list * Display.show * Whitespace.t list + | `Type_boundaries of + Whitespace.t list * Whitespace.t list * Display.show * Whitespace.t list ]; + } + | Option of { + wsoption : Whitespace.t list; + wscoloneq : Whitespace.t list; + what : + [ `Function_boundaries of + Whitespace.t list * Whitespace.t list * Options.implicitness * Whitespace.t list + | `Type_boundaries of + Whitespace.t list * Whitespace.t list * Options.implicitness * Whitespace.t list ]; } | Undo of { wsundo : Whitespace.t list; count : int; wscount : Whitespace.t list } | Section of { @@ -476,6 +489,11 @@ module Parse = struct | Ident [ "ascii" ] -> Some `ASCII | _ -> None + let show_of_token : Token.t -> Display.show option = function + | Ident [ "on" ] -> Some `Show + | Ident [ "off" ] -> Some `Hide + | _ -> None + let display = let* wsdisplay = token Display in let* what, wswhat = @@ -483,19 +501,73 @@ module Parse = struct match tok with | Ident [ "style" ] -> Some ((`Style, ws), state) | Ident [ "chars" ] -> Some ((`Chars, ws), state) + | Ident [ "function" ] -> Some ((`Function, ws), state) + | Ident [ "type" ] -> Some ((`Type, ws), state) | _ -> None) in - let* wscoloneq = token Coloneq in match what with | `Style -> + let* wscoloneq = token Coloneq in step "" (fun state _ (tok, ws) -> let open Monad.Ops (Monad.Maybe) in let* style = style_of_token tok in return (Display { wsdisplay; wscoloneq; what = `Style (wswhat, style, ws) }, state)) | `Chars -> + let* wscoloneq = token Coloneq in step "" (fun state _ (tok, ws) -> let open Monad.Ops (Monad.Maybe) in let* chars = chars_of_token tok in return (Display { wsdisplay; wscoloneq; what = `Chars (wswhat, chars, ws) }, state)) + | `Function -> + let* wsb = token (Ident [ "boundaries" ]) in + let* wscoloneq = token Coloneq in + step "" (fun state _ (tok, ws) -> + let open Monad.Ops (Monad.Maybe) in + let* show = show_of_token tok in + return + ( Display { wsdisplay; wscoloneq; what = `Function_boundaries (wswhat, wsb, show, ws) }, + state )) + | `Type -> + let* wsb = token (Ident [ "boundaries" ]) in + let* wscoloneq = token Coloneq in + step "" (fun state _ (tok, ws) -> + let open Monad.Ops (Monad.Maybe) in + let* show = show_of_token tok in + return + ( Display { wsdisplay; wscoloneq; what = `Type_boundaries (wswhat, wsb, show, ws) }, + state )) + + let implicit_of_token : Token.t -> Options.implicitness option = function + | Ident [ "implicit" ] -> Some `Implicit + | Ident [ "explicit" ] -> Some `Explicit + | _ -> None + + let option = + let* wsoption = token Option in + let* what, wswhat = + step "" (fun state _ (tok, ws) -> + match tok with + | Ident [ "function" ] -> Some ((`Function, ws), state) + | Ident [ "type" ] -> Some ((`Type, ws), state) + | _ -> None) in + match what with + | `Function -> + let* wsb = token (Ident [ "boundaries" ]) in + let* wscoloneq = token Coloneq in + step "" (fun state _ (tok, ws) -> + let open Monad.Ops (Monad.Maybe) in + let* show = implicit_of_token tok in + return + ( Option { wsoption; wscoloneq; what = `Function_boundaries (wswhat, wsb, show, ws) }, + state )) + | `Type -> + let* wsb = token (Ident [ "boundaries" ]) in + let* wscoloneq = token Coloneq in + step "" (fun state _ (tok, ws) -> + let open Monad.Ops (Monad.Maybe) in + let* show = implicit_of_token tok in + return + ( Option { wsoption; wscoloneq; what = `Type_boundaries (wswhat, wsb, show, ws) }, + state )) let undo = let* wsundo = token Undo in @@ -535,6 +607,7 @@ module Parse = struct solve show display + option undo section endcmd @@ -618,6 +691,7 @@ let to_string : Command.t -> string = function | Solve _ -> "solve" | Show _ -> "show" | Display _ -> "display" + | Option _ -> "option" | Quit _ -> "quit" | Undo _ -> "undo" | Section _ -> "section" @@ -784,11 +858,12 @@ let execute : action_taken:(unit -> unit) -> get_file:(string -> Scope.trie) -> | Solve { number; tm = Term tm; _ } -> ( (* Solve does NOT create a new history entry because it is NOT undoable. *) let (Find_number - (m, { tm = metatm; termctx; ty; energy = _ }, { global; scope; status; vars })) = + (m, { tm = metatm; termctx; ty; energy = _ }, { global; scope; status; vars; options })) + = Eternity.find_number number in match metatm with | `Undefined -> - History.run_with_scope ~init_visible:scope @@ fun () -> + History.run_with_scope ~init_visible:scope ~options @@ fun () -> let tm = process vars tm in (* We set the hole location offset to the start of the *term*, so that ProofGeneral can create hole overlays in the right places when solving a hole and creating new holes. *) Global.HolePos.modify (fun st -> @@ -812,7 +887,26 @@ let execute : action_taken:(unit -> unit) -> get_file:(string -> Scope.trie) -> emit (Display_set ("style", Display.to_string (style :> Display.values))) | `Chars (_, chars, _) -> Display.modify (fun s -> { s with chars }); - emit (Display_set ("chars", Display.to_string (chars :> Display.values)))) + emit (Display_set ("chars", Display.to_string (chars :> Display.values))) + | `Function_boundaries (_, _, function_boundaries, _) -> + Display.modify (fun s -> { s with function_boundaries }); + emit + (Display_set + ("function boundaries", Display.to_string (function_boundaries :> Display.values))) + | `Type_boundaries (_, _, type_boundaries, _) -> + Display.modify (fun s -> { s with type_boundaries }); + emit + (Display_set ("type boundaries", Display.to_string (type_boundaries :> Display.values))) + ) + | Option { what; _ } -> ( + History.do_command @@ fun () -> + match what with + | `Function_boundaries (_, _, function_boundaries, _) -> + Scope.modify_options (fun opt -> { opt with function_boundaries }); + emit (Option_set ("function boundaries", Options.to_string function_boundaries)) + | `Type_boundaries (_, _, type_boundaries, _) -> + Scope.modify_options (fun opt -> { opt with type_boundaries }); + emit (Option_set ("type boundaries", Options.to_string type_boundaries))) | Undo { count; _ } -> History.undo count; emit (Commands_undone count) @@ -1029,6 +1123,18 @@ let pp_command : formatter -> t -> Whitespace.t list = | `Chars (wswhat, how, wshow) -> pp_print_string ppf "chars"; pp_ws `Nobreak ppf wswhat; + ((how :> Display.values), wshow) + | `Function_boundaries (wsfunction, wsboundaries, how, wshow) -> + pp_print_string ppf "function"; + pp_ws `Nobreak ppf wsfunction; + pp_print_string ppf "boundaries"; + pp_ws `Nobreak ppf wsboundaries; + ((how :> Display.values), wshow) + | `Type_boundaries (wstype, wsboundaries, how, wshow) -> + pp_print_string ppf "type"; + pp_ws `Nobreak ppf wstype; + pp_print_string ppf "boundaries"; + pp_ws `Nobreak ppf wsboundaries; ((how :> Display.values), wshow) in pp_tok ppf Coloneq; pp_ws `Nobreak ppf wscoloneq; @@ -1036,6 +1142,29 @@ let pp_command : formatter -> t -> Whitespace.t list = let ws, rest = Whitespace.split wshow in pp_ws `None ppf ws; rest + | Option { wsoption; wscoloneq; what } -> + pp_tok ppf Option; + pp_ws `Nobreak ppf wsoption; + let how, wshow = + match what with + | `Function_boundaries (wsfunction, wsboundaries, how, wshow) -> + pp_print_string ppf "function"; + pp_ws `Nobreak ppf wsfunction; + pp_print_string ppf "boundaries"; + pp_ws `Nobreak ppf wsboundaries; + ((how :> Options.values), wshow) + | `Type_boundaries (wstype, wsboundaries, how, wshow) -> + pp_print_string ppf "type"; + pp_ws `Nobreak ppf wstype; + pp_print_string ppf "boundaries"; + pp_ws `Nobreak ppf wsboundaries; + ((how :> Options.values), wshow) in + pp_tok ppf Coloneq; + pp_ws `Nobreak ppf wscoloneq; + pp_print_string ppf (Options.to_string how); + let ws, rest = Whitespace.split wshow in + pp_ws `None ppf ws; + rest | Undo { wsundo; count; wscount } -> pp_tok ppf Undo; pp_ws `Nobreak ppf wsundo; diff --git a/lib/parser/display.ml b/lib/parser/display.ml index cfffcdb8..1cfaa183 100644 --- a/lib/parser/display.ml +++ b/lib/parser/display.ml @@ -5,20 +5,39 @@ type chars = [ `Unicode | `ASCII ] type metas = [ `Anonymous | `Numbered ] type argstyle = [ `Spaces | `Parens ] type spacing = [ `Wide | `Narrow ] -type values = [ `Unicode | `ASCII | `Compact | `Noncompact ] +type show = [ `Show | `Hide ] +type values = [ `Unicode | `ASCII | `Compact | `Noncompact | `Show | `Hide ] let to_string : values -> string = function | `Compact -> "compact" | `Unicode -> "unicode" | `Noncompact -> "noncompact" | `ASCII -> "ASCII" + | `Show -> "on" + | `Hide -> "off" module Config = struct - type t = { style : style; chars : chars; metas : metas; argstyle : argstyle; spacing : spacing } + type t = { + style : style; + chars : chars; + metas : metas; + argstyle : argstyle; + spacing : spacing; + function_boundaries : show; + type_boundaries : show; + } end let default : Config.t = - { style = `Compact; chars = `Unicode; metas = `Numbered; argstyle = `Spaces; spacing = `Wide } + { + style = `Compact; + chars = `Unicode; + metas = `Numbered; + argstyle = `Spaces; + spacing = `Wide; + function_boundaries = `Hide; + type_boundaries = `Hide; + } module State = Util.State.Make (Config) @@ -33,6 +52,8 @@ let chars () = (State.get ()).chars let metas () = (State.get ()).metas let argstyle () = (State.get ()).argstyle let spacing () = (State.get ()).spacing +let function_boundaries () = (State.get ()).function_boundaries +let type_boundaries () = (State.get ()).type_boundaries let alt_char uni asc = match (State.get ()).chars with diff --git a/lib/parser/eternity.ml b/lib/parser/eternity.ml index 9fa784c4..1625a76d 100644 --- a/lib/parser/eternity.ml +++ b/lib/parser/eternity.ml @@ -12,6 +12,7 @@ open Reporter type ('a, 'b, 's) homewhen = { global : Global.data; scope : Scope.trie; + options : Options.t; status : ('b, 's) status; vars : (string option, 'a) Bwv.t; } @@ -58,7 +59,13 @@ let () = { def = Metadef.make ~tm:`Undefined ~termctx ~ty ~energy:(Status.energy status); homewhen = - { global = Global.get (); scope = Scope.get_visible (); status; vars }; + { + global = Global.get (); + scope = Scope.get_visible (); + status; + vars; + options = Scope.get_options (); + }; } map; })); diff --git a/lib/parser/eternity.mli b/lib/parser/eternity.mli index 38edb4bb..fccaae5e 100644 --- a/lib/parser/eternity.mli +++ b/lib/parser/eternity.mli @@ -7,6 +7,7 @@ open Term type ('a, 'b, 's) homewhen = { global : Global.data; scope : Scope.trie; + options : Options.t; status : ('b, 's) status; vars : (string option, 'a) Bwv.t; } diff --git a/lib/parser/history.ml b/lib/parser/history.ml index ecbe0d27..9d27c21b 100644 --- a/lib/parser/history.ml +++ b/lib/parser/history.ml @@ -37,7 +37,7 @@ let run_empty : type a. (unit -> a) -> a = ~set:(fun situation -> S.modify (fun d -> { d with present = { d.present with situation } })) f -(* Every undoable command (e.g. def, axiom, notation, import, export) should be wrapped in this. *) +(* Every undoable command (e.g. def, axiom, notation, import, export, option) should be wrapped in this. *) let do_command f = (* First we save the state at the end of the previous command to the past, freeing up the present to be modified by the current command. *) S.modify (fun d -> { d with past = Snoc (d.past, d.present) }); @@ -68,6 +68,6 @@ let set_visible visible = S.modify (fun d -> { d with present = { d.present with situation } }) (* Put a given starting visible namespace into the scope, and also extract the notations from it. Since this uses Scope.run and Situation.run_on, it *overrides* (dynamically, locally) the "actual" namespace and notations in the outer state. It is used for loading files and strings, which are atomic undo units, and for "going back in time" temporarily to solve an old hole. *) -let run_with_scope ~init_visible f = - Scope.run ~init_visible @@ fun () -> +let run_with_scope ~init_visible ?options f = + Scope.run ~init_visible ?options @@ fun () -> Situation.run_on (Situation.add_users !Builtins.builtins init_visible) @@ f diff --git a/lib/parser/lexer.ml b/lib/parser/lexer.ml index 51f75ffb..340e2416 100644 --- a/lib/parser/lexer.ml +++ b/lib/parser/lexer.ml @@ -223,6 +223,7 @@ let canonicalize (rng : Position.range) : string -> Token.t t = function | "solve" -> return Solve | "show" -> return Show | "display" -> return Display + | "option" -> return Option | "undo" -> return Undo | "section" -> return Section | "end" -> return End diff --git a/lib/parser/options.ml b/lib/parser/options.ml new file mode 100644 index 00000000..37c052da --- /dev/null +++ b/lib/parser/options.ml @@ -0,0 +1,12 @@ +(* Configuration options that affect the following code, and are scoped in sections, but don't change the underlying type theory. *) + +type implicitness = [ `Implicit | `Explicit ] +type values = [ `Implicit | `Explicit ] + +let to_string : values -> string = function + | `Implicit -> "implicit" + | `Explicit -> "explicit" + +type t = { function_boundaries : implicitness; type_boundaries : implicitness } + +let default : t = { function_boundaries = `Explicit; type_boundaries = `Explicit } diff --git a/lib/parser/postprocess.ml b/lib/parser/postprocess.ml index 7a3db497..0cb3c748 100644 --- a/lib/parser/postprocess.ml +++ b/lib/parser/postprocess.ml @@ -4,11 +4,14 @@ open Dim open Core open Raw open Reporter -open Notation open Asai.Range +open Notation open Monad.Ops (Monad.Maybe) module StringMap = Map.Make (String) +(* We define this here so we can refer to it in parsing implicit applications. *) +let braces = make "braces" Outfix + (* Require the argument to be either a valid local variable name (to be bound, so faces of cubical variables are not allowed) or an underscore, and return a corresponding 'string option'. *) let get_var : type lt ls rt rs. (lt, ls, rt, rs) parse located -> string option = fun { value; loc } -> @@ -165,12 +168,22 @@ and process_apply : n synth located -> (observation * Asai.Range.t option) list -> n check located = - fun ctx fn args -> - match args with + fun ctx fn fnargs -> + match fnargs with | [] -> { value = Synth fn.value; loc = fn.loc } | (Term { value = Field (fld, _); _ }, loc) :: args -> process_apply ctx { value = Field (fn, Field.intern_ori fld); loc } args - | (Term arg, loc) :: args -> process_apply ctx { value = Raw.App (fn, process ctx arg); loc } args + | (Term { value = Notn n; loc = braceloc }, loc) :: rest when equal (notn n) braces -> ( + match args n with + | [ Term arg ] -> + process_apply ctx + { value = Raw.App (fn, process ctx arg, locate_opt braceloc `Implicit); loc } + rest + | _ -> fatal (Anomaly "invalid notation arguments for braces")) + | (Term arg, loc) :: args -> + process_apply ctx + { value = Raw.App (fn, process ctx arg, locate_opt arg.loc `Explicit); loc } + args and process_synth : type n lt ls rt rs. @@ -226,7 +239,8 @@ let process_user : | `Constant c -> let spine = List.fold_left - (fun acc k -> Raw.App ({ value = acc; loc }, StringMap.find k args)) + (fun acc k -> + Raw.App ({ value = acc; loc }, StringMap.find k args, locate_opt None `Explicit)) (Const c) val_vars in Raw.Synth spine | `Constr (c, _) -> diff --git a/lib/parser/scope.ml b/lib/parser/scope.ml index 5943fa89..36619b15 100644 --- a/lib/parser/scope.ml +++ b/lib/parser/scope.ml @@ -42,14 +42,18 @@ module M = Algaeff.Mutex.Make () exception Locked = M.Locked -(* Scope state: a visible namespace, an export namespace, and an export prefix. *) +(* Scope state: a visible namespace, an export namespace, an export prefix, and a set of configuration options. *) type trie = (Param.data, Param.tag) Trie.t -type scope = { visible : trie; export : trie; prefix : Trie.bwd_path } +type scope = { visible : trie; export : trie; prefix : Trie.bwd_path; options : Options.t } (* A Scope.t has an inner scope and also maintains a stack of outer scopes. *) type t = { outer : scope Bwd.t; inner : scope } -let empty : t = { outer = Emp; inner = { visible = Trie.empty; export = Trie.empty; prefix = Emp } } +let empty : t = + { + outer = Emp; + inner = { visible = Trie.empty; export = Trie.empty; prefix = Emp; options = Options.default }; + } module S = State.Make (struct type nonrec t = t @@ -75,6 +79,10 @@ let modify_visible ?context_visible m = { s.inner with visible = Mod.modify ?context:context_visible ~prefix:Emp m s.inner.visible }; } +let modify_options f = + M.exclusively @@ fun () -> + S.modify @@ fun s -> { s with inner = { s.inner with options = f s.inner.options } } + let modify_export ?context_export m = M.exclusively @@ fun () -> S.modify @@ fun s -> @@ -164,6 +172,11 @@ let import_subtree ?context_modifier ?context_visible ?(modifier = Yuujinchou.La let get_visible () = M.exclusively @@ fun () -> (S.get ()).inner.visible let get_export () = M.exclusively @@ fun () -> (S.get ()).inner.export +let get_options () = M.exclusively @@ fun () -> (S.get ()).inner.options + +let () = + (Implicitboundaries.forward_functions := fun () -> (get_options ()).function_boundaries); + Implicitboundaries.forward_types := fun () -> (get_options ()).type_boundaries (* Set the visible namespace, e.g. before going into interactive mode. *) let set_visible visible = @@ -174,7 +187,12 @@ let start_section prefix = M.exclusively @@ fun () -> S.modify (fun s -> let new_scope : scope = - { visible = s.inner.visible; export = Trie.empty; prefix = Bwd.of_list prefix } in + { + visible = s.inner.visible; + export = Trie.empty; + prefix = Bwd.of_list prefix; + options = s.inner.options; + } in { outer = Snoc (s.outer, s.inner); inner = new_scope }) (* Wrap up a section, integrating its exported names into the previous section's namespace with the prefix attached. Returns the prefix that was used. *) @@ -191,10 +209,12 @@ let end_section () = with Failure _ -> None (* We remove the Mod.run from Scope.run and let the caller control it separately. *) -let run ?(export_prefix = Emp) ?(init_visible = Trie.empty) f = +let run ?(export_prefix = Emp) ?(init_visible = Trie.empty) ?(options = Options.default) f = let init = - { outer = Emp; inner = { visible = init_visible; export = Trie.empty; prefix = export_prefix } } - in + { + outer = Emp; + inner = { visible = init_visible; export = Trie.empty; prefix = export_prefix; options }; + } in M.run @@ fun () -> S.run ~init f (* Like 'run', but override the handlers for the scope state effects instead of running a state module; hence no init_visible is given. Unlike most RedPRL try_with functions, this one isn't designed for calling *inside* of an outer "run" to override some things locally, instead it is for *replacing* "run" by passing out the state effects to our History module. Hence why it starts a new Mutex as well, and why we call it "run_with" instead of "try_with". *) diff --git a/lib/parser/scope.mli b/lib/parser/scope.mli index bb9bc9c8..f9a2208f 100644 --- a/lib/parser/scope.mli +++ b/lib/parser/scope.mli @@ -53,6 +53,7 @@ val empty : t val resolve : Trie.path -> (Param.data * Param.tag) option val modify_visible : ?context_visible:Param.context -> Param.hook Yuujinchou.Language.t -> unit val modify_export : ?context_export:Param.context -> Param.hook Yuujinchou.Language.t -> unit +val modify_options : (Options.t -> Options.t) -> unit val export_visible : ?context_modifier:Param.context -> @@ -94,12 +95,17 @@ val import_subtree : val get_visible : unit -> trie val get_export : unit -> trie +val get_options : unit -> Options.t val set_visible : trie -> unit val start_section : string list -> unit val end_section : unit -> string list option val run : - ?export_prefix:string Bwd.t -> ?init_visible:(Param.data, Param.tag) Trie.t -> (unit -> 'a) -> 'a + ?export_prefix:string Bwd.t -> + ?init_visible:(Param.data, Param.tag) Trie.t -> + ?options:Options.t -> + (unit -> 'a) -> + 'a val run_with : ?get:(unit -> t) -> ?set:(t -> unit) -> (unit -> 'a) -> 'a val lookup : Trie.path -> Constant.t option diff --git a/lib/parser/token.ml b/lib/parser/token.ml index 93d1baf4..ed3f512a 100644 --- a/lib/parser/token.ml +++ b/lib/parser/token.ml @@ -41,6 +41,7 @@ type t = | Solve | Show | Display + | Option | Undo | Section | End @@ -183,6 +184,7 @@ let to_string = function | Solve -> "solve" | Show -> "show" | Display -> "display" + | Option -> "option" | Undo -> "undo" | Section -> "section" | End -> "end" diff --git a/lib/parser/unparse.ml b/lib/parser/unparse.ml index 2646f4bc..78009cb5 100644 --- a/lib/parser/unparse.ml +++ b/lib/parser/unparse.ml @@ -165,21 +165,51 @@ let rec get_bwd : get_bwd (CubeOf.find_top rdc) (CubeOf.find_top rac :: elts) | _ -> None +let synths : type n. (n, kinetic) term -> bool = function + | Var _ | Const _ + | Meta (_, _) + | MetaEnv (_, _) + | Field (_, _) + | UU _ + | Inst (_, _) + | Pi (_, _, _) + | App (_, _) + | Act (_, _) + | Let (_, _, _) -> true + | Constr (_, _, _) | Lam (_, _) | Struct (_, _, _, _) -> false + (* Given a term, extract its head and arguments as an application spine. If the spine contains a field projection, stop there and return only the arguments after it, noting the field name and what it is applied to (which itself be another spine). *) let rec get_spine : type b n. (n, kinetic) term -> - [ `App of (n, kinetic) term * (n, kinetic) term Bwd.t - | `Field of (n, kinetic) term * Field.t * (n, kinetic) term Bwd.t ] = + [ `App of (n, kinetic) term * ((n, kinetic) term * [ `Implicit | `Explicit ]) Bwd.t + | `Field of (n, kinetic) term * Field.t * ((n, kinetic) term * [ `Implicit | `Explicit ]) Bwd.t + ] = fun tm -> match tm with | App (fn, arg) -> ( let module M = CubeOf.Monadic (Monad.State (struct - type t = (n, kinetic) term Bwd.t + type t = ((n, kinetic) term * [ `Implicit | `Explicit ]) Bwd.t end)) in (* To append the entries in a cube to a Bwd, we iterate through it with a Bwd state. *) let append_bwd args = - snd (M.miterM { it = (fun _ [ x ] s -> ((), Snoc (s, x))) } [ arg ] args) in + let all_args = not (synths (CubeOf.find_top arg)) in + snd + (M.miterM + { + it = + (fun fa [ x ] s -> + match + ( Implicitboundaries.functions (), + Display.function_boundaries (), + is_id_sface fa, + all_args ) + with + | `Implicit, `Hide, None, false -> ((), s) + | `Implicit, _, None, _ -> ((), Snoc (s, (x, `Implicit))) + | _ -> ((), Snoc (s, (x, `Explicit)))); + } + [ arg ] args) in match get_spine fn with | `App (head, args) -> `App (head, append_bwd args) | `Field (head, fld, args) -> `Field (head, fld, append_bwd args)) @@ -217,15 +247,34 @@ let rec unparse : | Inst (ty, tyargs) -> (* We unparse instantiations like application spines, since that is how they are represented in user syntax. TODO: How can we allow special notations for some instantiations, like x=y for Id A x y? *) - unparse_spine vars (`Term ty) - (Bwd.map (make_unparser vars) (TubeOf.append_bwd Emp tyargs)) - li ri + let module M = TubeOf.Monadic (Monad.State (struct + type t = unparser Bwd.t + end)) in + (* To append the entries in a cube to a Bwd, we iterate through it with a Bwd state. *) + let (), args = + M.miterM + { + it = + (fun fa [ x ] s -> + let (Tface_of fa1) = codim1_envelope fa in + let all_args = not (synths (TubeOf.find tyargs fa1)) in + match + (Implicitboundaries.types (), Display.type_boundaries (), is_codim1 fa, all_args) + with + | `Implicit, `Hide, None, false -> ((), s) + | `Implicit, _, None, _ -> ((), Snoc (s, make_unparser_implicit vars (x, `Implicit))) + | _ -> ((), Snoc (s, make_unparser_implicit vars (x, `Explicit)))); + } + [ tyargs ] Emp in + unparse_spine vars (`Term ty) args li ri | Pi _ -> unparse_pis vars Emp tm li ri | App _ -> ( match get_spine tm with - | `App (fn, args) -> unparse_spine vars (`Term fn) (Bwd.map (make_unparser vars) args) li ri + | `App (fn, args) -> + unparse_spine vars (`Term fn) (Bwd.map (make_unparser_implicit vars) args) li ri | `Field (head, fld, args) -> - unparse_spine vars (`Field (head, fld)) (Bwd.map (make_unparser vars) args) li ri) + unparse_spine vars (`Field (head, fld)) (Bwd.map (make_unparser_implicit vars) args) li ri + ) | Act (tm, s) -> unparse_act vars { unparse = (fun li ri -> unparse vars tm li ri) } s li ri | Let (x, tm, body) -> ( let tm = unparse vars tm Interval.entire Interval.entire in @@ -269,7 +318,7 @@ let rec unparse : ~first:(unlocated (Ident ([ Field.to_string fld ], []))) ~inner:Emp ~last:tm ~left_ok:(No.le_refl No.minus_omega) ~right_ok:(No.le_refl No.minus_omega)) - (* An unlabeled 1-tuple must be written (_ := M). *) + (* An unlabeled 1-tuple is currently unparsed as (_ := M), not (M,). *) | `Unlabeled when Bwd.length fields = 1 -> unlocated (infix ~notn:coloneq ~ws:[] ~first:(unlocated (Placeholder [])) @@ -309,6 +358,20 @@ let rec unparse : and make_unparser : type n. n Names.t -> (n, kinetic) term -> unparser = fun vars tm -> { unparse = (fun li ri -> unparse vars tm li ri) } +(* A version that wraps implicit arguments in braces. *) +and make_unparser_implicit : + type n. n Names.t -> (n, kinetic) term * [ `Implicit | `Explicit ] -> unparser = + fun vars (tm, i) -> + match i with + | `Explicit -> { unparse = (fun li ri -> unparse vars tm li ri) } + | `Implicit -> + { + unparse = + (fun _ _ -> + let tm = unparse vars tm Interval.entire Interval.entire in + unlocated (outfix ~notn:Postprocess.braces ~ws:[] ~inner:(Snoc (Emp, Term tm)))); + } + (* Unparse a spine with its arguments whose head could be many things: an as-yet-not-unparsed term, a constructor, a field projection, a degeneracy, or a general delayed unparsing. *) and unparse_spine : type n lt ls rt rs. @@ -529,9 +592,24 @@ and unparse_pis : type t = unparser Bwd.t end) in let module MOf = CubeOf.Monadic (S) in + let all_args = not (synths (CubeOf.find_top doms)) in let (), args = MOf.miterM - { it = (fun _ [ dom ] args -> ((), Snoc (args, make_unparser vars dom))) } + { + it = + (fun fa [ dom ] args -> + let newdoms = + match + ( Implicitboundaries.functions (), + Display.function_boundaries (), + is_id_sface fa, + all_args ) + with + | `Implicit, `Hide, None, false -> [] + | `Implicit, _, None, _ -> [ (dom, `Implicit) ] + | _ -> [ (dom, `Explicit) ] in + ((), Bwd.append args (List.map (make_unparser_implicit vars) newdoms))); + } [ doms ] Emp in let module MCod = CodCube.Monadic (S) in let (), args = @@ -539,10 +617,15 @@ and unparse_pis : { it = (fun fa [ cod ] args -> + let impl = + match (Implicitboundaries.functions (), is_id_sface fa) with + | `Implicit, None -> `Implicit + | _ -> `Explicit in ( (), Snoc - (args, make_unparser vars (Lam (singleton_variables (dom_sface fa) x, cod))) - )); + ( args, + make_unparser_implicit vars + (Lam (singleton_variables (dom_sface fa) x, cod), impl) ) )); } [ cods ] args in unparse_pis_final vars accum diff --git a/lib/top/top.ml b/lib/top/top.ml index 1e1dfdc9..6579360c 100644 --- a/lib/top/top.ml +++ b/lib/top/top.ml @@ -25,6 +25,8 @@ let source_only = ref false let number_metas = ref true let parenthesize_arguments = ref false let extra_spaces = ref true +let show_function_boundaries = ref false +let show_type_boundaries = ref false (* Marshal the current flags to a file. *) let marshal_flags chan = @@ -95,6 +97,8 @@ let run_top ?use_ansi ?onechar_ops ?ascii_symbols f = metas = (if !number_metas then `Numbered else `Anonymous); argstyle = (if !parenthesize_arguments then `Parens else `Spaces); spacing = (if !extra_spaces then `Wide else `Narrow); + function_boundaries = (if !show_function_boundaries then `Show else `Hide); + type_boundaries = (if !show_type_boundaries then `Show else `Hide); } @@ fun () -> Annotate.run @@ fun () -> diff --git a/lib/util/bwv.ml b/lib/util/bwv.ml index c3d9c89c..68a98ae3 100644 --- a/lib/util/bwv.ml +++ b/lib/util/bwv.ml @@ -196,6 +196,29 @@ module Applicatic (M : Applicative.Plain) = struct let mapM2 : type x y z n. (x -> y -> z M.t) -> (x, n) t -> (y, n) t -> (z, n) t M.t = fun f xs ys -> mmapM (fun [ x; y ] -> f x y) [ xs; ys ] + let mapM1_2 : type x y z n. (x -> (y * z) M.t) -> (x, n) t -> ((y, n) t * (z, n) t) M.t = + fun f xs -> + let open Applicative.Ops (M) in + let+ [ ys; zs ] = + pmapM + (fun [ x ] -> + let+ y, z = f x in + [ y; z ]) + [ xs ] (Cons (Cons Nil)) in + (ys, zs) + + let mapM1_3 : + type x y z w n. (x -> (y * z * w) M.t) -> (x, n) t -> ((y, n) t * (z, n) t * (w, n) t) M.t = + fun f xs -> + let open Applicative.Ops (M) in + let+ [ ys; zs; ws ] = + pmapM + (fun [ x ] -> + let+ y, z, w = f x in + [ y; z; w ]) + [ xs ] (Cons (Cons (Cons Nil))) in + (ys, zs, ws) + let iterM : type x n. (x -> unit M.t) -> (x, n) t -> unit M.t = fun f xs -> miterM (fun [ x ] -> f x) [ xs ] diff --git a/lib/util/fwn.ml b/lib/util/fwn.ml index ea8aadea..13da30e5 100644 --- a/lib/util/fwn.ml +++ b/lib/util/fwn.ml @@ -2,6 +2,12 @@ type zero = private Dummy_zero type 'n suc = private Dummy_suc +type one = zero suc +type two = one suc +type three = two suc +type four = three suc +type five = four suc +type six = five suc (* We can add a backwards nat to a forwards nat and get a backwards one. This is the length-level analogue of appending a forward list on the end of a backwards one. *) @@ -16,8 +22,6 @@ let zero : zero t = Zero let suc : type n. n t -> n suc t = function | n -> Suc n -type one = zero suc - let one : one t = suc zero let rec bplus_right : type a b ab. (a, b, ab) bplus -> b t = function diff --git a/proofgeneral/narya-syntax.el b/proofgeneral/narya-syntax.el index a48857f5..9429618b 100644 --- a/proofgeneral/narya-syntax.el +++ b/proofgeneral/narya-syntax.el @@ -2,7 +2,7 @@ ;; We omit "display", "solve", "show", and "undo" because these should NOT appear in source files. (defconst narya-commands - "\\<\\(axiom\\|def\\|echo\\|synth\\|notation\\|import\\|export\\|quit\\|section\\|end\\)\\>") + "\\<\\(axiom\\|def\\|echo\\|synth\\|notation\\|import\\|export\\|quit\\|section\\|option\\|end\\)\\>") ;; As noted in the PG source, the default function proof-generic-state-preserving-p is not really correct; it thinks that things like "def" are state-preserving. These are the commands that it makes sense for PG to issue directly to the prover without their being in the file. (defun narya-state-preserving-p (cmd) diff --git a/proofgeneral/narya.el b/proofgeneral/narya.el index ca8e5c0f..467c967f 100644 --- a/proofgeneral/narya.el +++ b/proofgeneral/narya.el @@ -389,7 +389,11 @@ pending hole data stored by `narya-handle-output`." "display style ≔ compact" "display style ≔ noncompact" "display chars ≔ unicode" - "display chars ≔ ascii")) + "display chars ≔ ascii" + "display function boundaries ≔ on" + "display function boundaries ≔ off" + "display type boundaries ≔ on" + "display type boundaries ≔ off")) (defun narya-minibuffer-cmd (cmd) "Wrapper around `proof-minibuffer-cmd' with completion for Narya commands." diff --git a/test/black/display.t b/test/black/display.t index e6d72a36..788eefdc 100644 --- a/test/black/display.t +++ b/test/black/display.t @@ -10,13 +10,13 @@ Type → Type : Type - ￫ info[I0100] + ￫ info[I0101] ￮ display set chars to ASCII Type -> Type : Type - ￫ info[I0100] + ￫ info[I0101] ￮ display set chars to unicode Type → Type diff --git a/test/black/implicit-boundaries.t/implicit-boundaries.ny b/test/black/implicit-boundaries.t/implicit-boundaries.ny new file mode 100644 index 00000000..94409fb1 --- /dev/null +++ b/test/black/implicit-boundaries.t/implicit-boundaries.ny @@ -0,0 +1,112 @@ +axiom A:Type +axiom B:Type +axiom f:A→B + +axiom a0:A +axiom a1:A +axiom a2:Id A a0 a1 + +echo refl f a0 a1 a2 + +{` When function boundaries are implicit, we don't give a0 and a1. `} + +option function boundaries ≔ implicit + +echo refl f a2 + +{` Similarly for cubes `} + +axiom a00 : A +axiom a01 : A +axiom a02 : Id A a00 a01 +axiom a10 : A +axiom a11 : A +axiom a12 : Id A a10 a11 +axiom a20 : Id A a00 a10 +axiom a21 : Id A a01 a11 +axiom a22 : Id (Id A) a00 a01 a02 a10 a11 a12 a20 a21 + +echo refl (refl f) a22 + +{` Similarly for types *of* cubes `} + +option type boundaries ≔ implicit + +echo Id (Id A) a02 a12 a20 a21 + +echo Id (Id A) {a00} {a01} a02 a12 a20 a21 + +echo Id (Id A) {a00} {a01} a02 {a10} {a11} a12 a20 a21 + +echo Id (Id A) a02 {a10} {a11} a12 a20 a21 + +{` Mixing and matching function and type options `} + +option function boundaries ≔ explicit + +echo refl (refl f) a00 a01 a02 a10 a11 a12 a20 a21 a22 + +option type boundaries ≔ explicit + +echo refl (refl f) a00 a01 a02 a10 a11 a12 a20 a21 a22 + +{` These options don't survive the ends of sections `} + +section test ≔ + + option function boundaries ≔ implicit + + echo refl (refl f) a22 + +end + +echo refl (refl f) a00 a01 a02 a10 a11 a12 a20 a21 a22 + +{` The dimension of the argument can be greater than the dimension of the application (this is a 1-dimensional application). `} + +axiom g : (x0:A) (x1:A) (x2:Id A x0 x1) → B + +echo refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + +option function boundaries ≔ implicit + +echo refl g a02 a12 a22 + +{` Even when printing implicit arguments is off, they are included if the corresponding primary argument doesn't synthesize. `} + +axiom C : Type +def A×B : Type ≔ sig (fst : A, snd : B) +axiom h : A×B → C + +axiom b0:B +axiom b1:B +axiom b2:Id B b0 b1 + +echo refl h {(a0,b0)} {(a1,b1)} (a2,b2) + +axiom b00 : B +axiom b01 : B +axiom b02 : Id B b00 b01 +axiom b10 : B +axiom b11 : B +axiom b12 : Id B b10 b11 +axiom b20 : Id B b00 b10 +axiom b21 : Id B b01 b11 +axiom b22 : Id (Id B) b00 b01 b02 b10 b11 b12 b20 b21 + +echo refl (refl h) {(a00,b00)} {(a01,b01)} {(a02,b02)} {(a10,b10)} {(a11,b11)} {(a12,b12)} {(a20,b20)} {(a21,b21)} (a22,b22) + +option type boundaries ≔ implicit + +echo refl (refl h) {(a00,b00)} {(a01,b01)} {(a02,b02)} {(a10,b10)} {(a11,b11)} {(a12,b12)} {(a20,b20)} {(a21,b21)} (a22,b22) + +axiom ab10 : A×B +axiom ab11 : A×B +axiom ab12 : Id A×B ab10 ab11 +axiom ab20 : Id A×B (a00,b00) ab10 +axiom ab21 : Id A×B (a01,b01) ab11 +axiom ab22 : Id (Id A×B) {(a00,b00)} {(a01,b01)} (a02,b02) {ab10} {ab11} ab12 ab20 ab21 + +echo ab22 + +echo refl (refl h) {(a00,b00)} {(a01,b01)} {(a02,b02)} {ab10} {ab11} {ab12} {ab20} {ab21} ab22 diff --git a/test/black/implicit-boundaries.t/run.t b/test/black/implicit-boundaries.t/run.t new file mode 100644 index 00000000..48934896 --- /dev/null +++ b/test/black/implicit-boundaries.t/run.t @@ -0,0 +1,1055 @@ + $ narya -v -fake-interact=implicit-boundaries.ny + ￫ info[I0001] + ￮ axiom A assumed + + ￫ info[I0001] + ￮ axiom B assumed + + ￫ info[I0001] + ￮ axiom f assumed + + ￫ info[I0001] + ￮ axiom a0 assumed + + ￫ info[I0001] + ￮ axiom a1 assumed + + ￫ info[I0001] + ￮ axiom a2 assumed + + refl f a0 a1 a2 + : refl B (f a0) (f a1) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl f a2 + : refl B (f a0) (f a1) + + ￫ info[I0001] + ￮ axiom a00 assumed + + ￫ info[I0001] + ￮ axiom a01 assumed + + ￫ info[I0001] + ￮ axiom a02 assumed + + ￫ info[I0001] + ￮ axiom a10 assumed + + ￫ info[I0001] + ￮ axiom a11 assumed + + ￫ info[I0001] + ￮ axiom a12 assumed + + ￫ info[I0001] + ￮ axiom a20 assumed + + ￫ info[I0001] + ￮ axiom a21 assumed + + ￫ info[I0001] + ￮ axiom a22 assumed + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + ￫ info[I0100] + ￮ option set function boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (refl f a00 a01 a02) (refl f a10 a11 a12) (refl f a00 a10 a20) + (refl f a01 a11 a21) + + ￫ info[I0100] + ￮ option set type boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0007] + ￮ section test opened + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0008] + ￮ section test closed + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0001] + ￮ axiom g assumed + + refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl g a02 a12 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0001] + ￮ axiom C assumed + + ￫ info[I0000] + ￮ constant A×B defined + + ￫ info[I0001] + ￮ axiom h assumed + + ￫ info[I0001] + ￮ axiom b0 assumed + + ￫ info[I0001] + ￮ axiom b1 assumed + + ￫ info[I0001] + ￮ axiom b2 assumed + + refl h {( a0, b0 )} {( a1, b1 )} ( a2, b2 ) + : refl C (h ( a0, b0 )) (h ( a1, b1 )) + + ￫ info[I0001] + ￮ axiom b00 assumed + + ￫ info[I0001] + ￮ axiom b01 assumed + + ￫ info[I0001] + ￮ axiom b02 assumed + + ￫ info[I0001] + ￮ axiom b10 assumed + + ￫ info[I0001] + ￮ axiom b11 assumed + + ￫ info[I0001] + ￮ axiom b12 assumed + + ￫ info[I0001] + ￮ axiom b20 assumed + + ￫ info[I0001] + ￮ axiom b21 assumed + + ￫ info[I0001] + ￮ axiom b22 assumed + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (h ( a00, b00 )) (h ( a01, b01 )) + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (h ( a10, b10 )) + (h ( a11, b11 )) (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0001] + ￮ axiom ab10 assumed + + ￫ info[I0001] + ￮ axiom ab11 assumed + + ￫ info[I0001] + ￮ axiom ab12 assumed + + ￫ info[I0001] + ￮ axiom ab20 assumed + + ￫ info[I0001] + ￮ axiom ab21 assumed + + ￫ info[I0001] + ￮ axiom ab22 assumed + + ab22 + : A×B⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} ( a02, b02 ) ab12 ab20 ab21 + + h⁽ᵉᵉ⁾ ab22 + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (refl h ab12) + (refl h ab20) (refl h ab21) + + + $ narya -v -show-function-boundaries -fake-interact=implicit-boundaries.ny + ￫ info[I0001] + ￮ axiom A assumed + + ￫ info[I0001] + ￮ axiom B assumed + + ￫ info[I0001] + ￮ axiom f assumed + + ￫ info[I0001] + ￮ axiom a0 assumed + + ￫ info[I0001] + ￮ axiom a1 assumed + + ￫ info[I0001] + ￮ axiom a2 assumed + + refl f a0 a1 a2 + : refl B (f a0) (f a1) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl f {a0} {a1} a2 + : refl B (f a0) (f a1) + + ￫ info[I0001] + ￮ axiom a00 assumed + + ￫ info[I0001] + ￮ axiom a01 assumed + + ￫ info[I0001] + ￮ axiom a02 assumed + + ￫ info[I0001] + ￮ axiom a10 assumed + + ￫ info[I0001] + ￮ axiom a11 assumed + + ￫ info[I0001] + ￮ axiom a12 assumed + + ￫ info[I0001] + ￮ axiom a20 assumed + + ￫ info[I0001] + ￮ axiom a21 assumed + + ￫ info[I0001] + ￮ axiom a22 assumed + + f⁽ᵉᵉ⁾ {a00} {a01} {a02} {a10} {a11} {a12} {a20} {a21} a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f {a00} {a01} a02) (f a10) (f a11) + (refl f {a10} {a11} a12) (refl f {a00} {a10} a20) + (refl f {a01} {a11} a21) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + ￫ info[I0100] + ￮ option set function boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (refl f a00 a01 a02) (refl f a10 a11 a12) (refl f a00 a10 a20) + (refl f a01 a11 a21) + + ￫ info[I0100] + ￮ option set type boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0007] + ￮ section test opened + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + f⁽ᵉᵉ⁾ {a00} {a01} {a02} {a10} {a11} {a12} {a20} {a21} a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f {a00} {a01} a02) (f a10) (f a11) + (refl f {a10} {a11} a12) (refl f {a00} {a10} a20) + (refl f {a01} {a11} a21) + + ￫ info[I0008] + ￮ section test closed + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0001] + ￮ axiom g assumed + + refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl g {a00} {a01} a02 {a10} {a11} a12 {a20} {a21} a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0001] + ￮ axiom C assumed + + ￫ info[I0000] + ￮ constant A×B defined + + ￫ info[I0001] + ￮ axiom h assumed + + ￫ info[I0001] + ￮ axiom b0 assumed + + ￫ info[I0001] + ￮ axiom b1 assumed + + ￫ info[I0001] + ￮ axiom b2 assumed + + refl h {( a0, b0 )} {( a1, b1 )} ( a2, b2 ) + : refl C (h ( a0, b0 )) (h ( a1, b1 )) + + ￫ info[I0001] + ￮ axiom b00 assumed + + ￫ info[I0001] + ￮ axiom b01 assumed + + ￫ info[I0001] + ￮ axiom b02 assumed + + ￫ info[I0001] + ￮ axiom b10 assumed + + ￫ info[I0001] + ￮ axiom b11 assumed + + ￫ info[I0001] + ￮ axiom b12 assumed + + ￫ info[I0001] + ￮ axiom b20 assumed + + ￫ info[I0001] + ￮ axiom b21 assumed + + ￫ info[I0001] + ￮ axiom b22 assumed + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (h ( a00, b00 )) (h ( a01, b01 )) + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (h ( a10, b10 )) + (h ( a11, b11 )) (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0001] + ￮ axiom ab10 assumed + + ￫ info[I0001] + ￮ axiom ab11 assumed + + ￫ info[I0001] + ￮ axiom ab12 assumed + + ￫ info[I0001] + ￮ axiom ab20 assumed + + ￫ info[I0001] + ￮ axiom ab21 assumed + + ￫ info[I0001] + ￮ axiom ab22 assumed + + ab22 + : A×B⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} ( a02, b02 ) ab12 ab20 ab21 + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {ab10} {ab11} {ab12} + {ab20} {ab21} ab22 + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {ab10} {ab11} ab12) (refl h {( a00, b00 )} {ab10} ab20) + (refl h {( a01, b01 )} {ab11} ab21) + + + $ narya -v implicit-boundaries.ny + ￫ info[I0001] + ￮ axiom A assumed + + ￫ info[I0001] + ￮ axiom B assumed + + ￫ info[I0001] + ￮ axiom f assumed + + ￫ info[I0001] + ￮ axiom a0 assumed + + ￫ info[I0001] + ￮ axiom a1 assumed + + ￫ info[I0001] + ￮ axiom a2 assumed + + refl f a0 a1 a2 + : refl B (f a0) (f a1) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl f a2 + : refl B (f a0) (f a1) + + ￫ info[I0001] + ￮ axiom a00 assumed + + ￫ info[I0001] + ￮ axiom a01 assumed + + ￫ info[I0001] + ￮ axiom a02 assumed + + ￫ info[I0001] + ￮ axiom a10 assumed + + ￫ info[I0001] + ￮ axiom a11 assumed + + ￫ info[I0001] + ￮ axiom a12 assumed + + ￫ info[I0001] + ￮ axiom a20 assumed + + ￫ info[I0001] + ￮ axiom a21 assumed + + ￫ info[I0001] + ￮ axiom a22 assumed + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + ￫ info[I0100] + ￮ option set function boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (refl f a00 a01 a02) (refl f a10 a11 a12) (refl f a00 a10 a20) + (refl f a01 a11 a21) + + ￫ info[I0100] + ￮ option set type boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0007] + ￮ section test opened + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0008] + ￮ section test closed + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0001] + ￮ axiom g assumed + + refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl g a02 a12 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0001] + ￮ axiom C assumed + + ￫ info[I0000] + ￮ constant A×B defined + + ￫ info[I0001] + ￮ axiom h assumed + + ￫ info[I0001] + ￮ axiom b0 assumed + + ￫ info[I0001] + ￮ axiom b1 assumed + + ￫ info[I0001] + ￮ axiom b2 assumed + + refl h {( a0, b0 )} {( a1, b1 )} ( a2, b2 ) + : refl C (h ( a0, b0 )) (h ( a1, b1 )) + + ￫ info[I0001] + ￮ axiom b00 assumed + + ￫ info[I0001] + ￮ axiom b01 assumed + + ￫ info[I0001] + ￮ axiom b02 assumed + + ￫ info[I0001] + ￮ axiom b10 assumed + + ￫ info[I0001] + ￮ axiom b11 assumed + + ￫ info[I0001] + ￮ axiom b12 assumed + + ￫ info[I0001] + ￮ axiom b20 assumed + + ￫ info[I0001] + ￮ axiom b21 assumed + + ￫ info[I0001] + ￮ axiom b22 assumed + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (h ( a00, b00 )) (h ( a01, b01 )) + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (h ( a10, b10 )) + (h ( a11, b11 )) (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0001] + ￮ axiom ab10 assumed + + ￫ info[I0001] + ￮ axiom ab11 assumed + + ￫ info[I0001] + ￮ axiom ab12 assumed + + ￫ info[I0001] + ￮ axiom ab20 assumed + + ￫ info[I0001] + ￮ axiom ab21 assumed + + ￫ info[I0001] + ￮ axiom ab22 assumed + + ab22 + : A×B⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} ( a02, b02 ) ab12 ab20 ab21 + + h⁽ᵉᵉ⁾ ab22 + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (refl h ab12) + (refl h ab20) (refl h ab21) + + + $ narya -v -show-function-boundaries implicit-boundaries.ny + ￫ info[I0001] + ￮ axiom A assumed + + ￫ info[I0001] + ￮ axiom B assumed + + ￫ info[I0001] + ￮ axiom f assumed + + ￫ info[I0001] + ￮ axiom a0 assumed + + ￫ info[I0001] + ￮ axiom a1 assumed + + ￫ info[I0001] + ￮ axiom a2 assumed + + refl f a0 a1 a2 + : refl B (f a0) (f a1) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl f {a0} {a1} a2 + : refl B (f a0) (f a1) + + ￫ info[I0001] + ￮ axiom a00 assumed + + ￫ info[I0001] + ￮ axiom a01 assumed + + ￫ info[I0001] + ￮ axiom a02 assumed + + ￫ info[I0001] + ￮ axiom a10 assumed + + ￫ info[I0001] + ￮ axiom a11 assumed + + ￫ info[I0001] + ￮ axiom a12 assumed + + ￫ info[I0001] + ￮ axiom a20 assumed + + ￫ info[I0001] + ￮ axiom a21 assumed + + ￫ info[I0001] + ￮ axiom a22 assumed + + f⁽ᵉᵉ⁾ {a00} {a01} {a02} {a10} {a11} {a12} {a20} {a21} a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f {a00} {a01} a02) (f a10) (f a11) + (refl f {a10} {a11} a12) (refl f {a00} {a10} a20) + (refl f {a01} {a11} a21) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ a02 a12 a20 a21 + : Type + + ￫ info[I0100] + ￮ option set function boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (refl f a00 a01 a02) (refl f a10 a11 a12) (refl f a00 a10 a20) + (refl f a01 a11 a21) + + ￫ info[I0100] + ￮ option set type boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0007] + ￮ section test opened + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + f⁽ᵉᵉ⁾ {a00} {a01} {a02} {a10} {a11} {a12} {a20} {a21} a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f {a00} {a01} a02) (f a10) (f a11) + (refl f {a10} {a11} a12) (refl f {a00} {a10} a20) + (refl f {a01} {a11} a21) + + ￫ info[I0008] + ￮ section test closed + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0001] + ￮ axiom g assumed + + refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl g {a00} {a01} a02 {a10} {a11} a12 {a20} {a21} a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0001] + ￮ axiom C assumed + + ￫ info[I0000] + ￮ constant A×B defined + + ￫ info[I0001] + ￮ axiom h assumed + + ￫ info[I0001] + ￮ axiom b0 assumed + + ￫ info[I0001] + ￮ axiom b1 assumed + + ￫ info[I0001] + ￮ axiom b2 assumed + + refl h {( a0, b0 )} {( a1, b1 )} ( a2, b2 ) + : refl C (h ( a0, b0 )) (h ( a1, b1 )) + + ￫ info[I0001] + ￮ axiom b00 assumed + + ￫ info[I0001] + ￮ axiom b01 assumed + + ￫ info[I0001] + ￮ axiom b02 assumed + + ￫ info[I0001] + ￮ axiom b10 assumed + + ￫ info[I0001] + ￮ axiom b11 assumed + + ￫ info[I0001] + ￮ axiom b12 assumed + + ￫ info[I0001] + ￮ axiom b20 assumed + + ￫ info[I0001] + ￮ axiom b21 assumed + + ￫ info[I0001] + ￮ axiom b22 assumed + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (h ( a00, b00 )) (h ( a01, b01 )) + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (h ( a10, b10 )) + (h ( a11, b11 )) (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0001] + ￮ axiom ab10 assumed + + ￫ info[I0001] + ￮ axiom ab11 assumed + + ￫ info[I0001] + ￮ axiom ab12 assumed + + ￫ info[I0001] + ￮ axiom ab20 assumed + + ￫ info[I0001] + ￮ axiom ab21 assumed + + ￫ info[I0001] + ￮ axiom ab22 assumed + + ab22 + : A×B⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} ( a02, b02 ) ab12 ab20 ab21 + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {ab10} {ab11} {ab12} + {ab20} {ab21} ab22 + : C⁽ᵉᵉ⁾ (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) + (refl h {ab10} {ab11} ab12) (refl h {( a00, b00 )} {ab10} ab20) + (refl h {( a01, b01 )} {ab11} ab21) + + + $ narya -v -show-type-boundaries -fake-interact=implicit-boundaries.ny + ￫ info[I0001] + ￮ axiom A assumed + + ￫ info[I0001] + ￮ axiom B assumed + + ￫ info[I0001] + ￮ axiom f assumed + + ￫ info[I0001] + ￮ axiom a0 assumed + + ￫ info[I0001] + ￮ axiom a1 assumed + + ￫ info[I0001] + ￮ axiom a2 assumed + + refl f a0 a1 a2 + : refl B (f a0) (f a1) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl f a2 + : refl B (f a0) (f a1) + + ￫ info[I0001] + ￮ axiom a00 assumed + + ￫ info[I0001] + ￮ axiom a01 assumed + + ￫ info[I0001] + ￮ axiom a02 assumed + + ￫ info[I0001] + ￮ axiom a10 assumed + + ￫ info[I0001] + ￮ axiom a11 assumed + + ￫ info[I0001] + ￮ axiom a12 assumed + + ￫ info[I0001] + ￮ axiom a20 assumed + + ￫ info[I0001] + ￮ axiom a21 assumed + + ￫ info[I0001] + ￮ axiom a22 assumed + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + A⁽ᵉᵉ⁾ {a00} {a01} a02 {a10} {a11} a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ {a00} {a01} a02 {a10} {a11} a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ {a00} {a01} a02 {a10} {a11} a12 a20 a21 + : Type + + A⁽ᵉᵉ⁾ {a00} {a01} a02 {a10} {a11} a12 a20 a21 + : Type + + ￫ info[I0100] + ￮ option set function boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ {f a00} {f a01} (refl f a00 a01 a02) {f a10} {f a11} + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0100] + ￮ option set type boundaries to explicit + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0007] + ￮ section test opened + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + f⁽ᵉᵉ⁾ a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a02) (f a10) (f a11) (refl f a12) + (refl f a20) (refl f a21) + + ￫ info[I0008] + ￮ section test closed + + f⁽ᵉᵉ⁾ a00 a01 a02 a10 a11 a12 a20 a21 a22 + : B⁽ᵉᵉ⁾ (f a00) (f a01) (refl f a00 a01 a02) (f a10) (f a11) + (refl f a10 a11 a12) (refl f a00 a10 a20) (refl f a01 a11 a21) + + ￫ info[I0001] + ￮ axiom g assumed + + refl g a00 a01 a02 a10 a11 a12 a20 a21 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0100] + ￮ option set function boundaries to implicit + + refl g a02 a12 a22 + : refl B (g a00 a10 a20) (g a01 a11 a21) + + ￫ info[I0001] + ￮ axiom C assumed + + ￫ info[I0000] + ￮ constant A×B defined + + ￫ info[I0001] + ￮ axiom h assumed + + ￫ info[I0001] + ￮ axiom b0 assumed + + ￫ info[I0001] + ￮ axiom b1 assumed + + ￫ info[I0001] + ￮ axiom b2 assumed + + refl h {( a0, b0 )} {( a1, b1 )} ( a2, b2 ) + : refl C (h ( a0, b0 )) (h ( a1, b1 )) + + ￫ info[I0001] + ￮ axiom b00 assumed + + ￫ info[I0001] + ￮ axiom b01 assumed + + ￫ info[I0001] + ￮ axiom b02 assumed + + ￫ info[I0001] + ￮ axiom b10 assumed + + ￫ info[I0001] + ￮ axiom b11 assumed + + ￫ info[I0001] + ￮ axiom b12 assumed + + ￫ info[I0001] + ￮ axiom b20 assumed + + ￫ info[I0001] + ￮ axiom b21 assumed + + ￫ info[I0001] + ￮ axiom b22 assumed + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ (h ( a00, b00 )) (h ( a01, b01 )) + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) (h ( a10, b10 )) + (h ( a11, b11 )) (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0100] + ￮ option set type boundaries to implicit + + h⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} {( a02, b02 )} {( a10, b10 )} + {( a11, b11 )} {( a12, b12 )} {( a20, b20 )} {( a21, b21 )} ( a22, b22 ) + : C⁽ᵉᵉ⁾ {h ( a00, b00 )} {h ( a01, b01 )} + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) {h ( a10, b10 )} + {h ( a11, b11 )} (refl h {( a10, b10 )} {( a11, b11 )} ( a12, b12 )) + (refl h {( a00, b00 )} {( a10, b10 )} ( a20, b20 )) + (refl h {( a01, b01 )} {( a11, b11 )} ( a21, b21 )) + + ￫ info[I0001] + ￮ axiom ab10 assumed + + ￫ info[I0001] + ￮ axiom ab11 assumed + + ￫ info[I0001] + ￮ axiom ab12 assumed + + ￫ info[I0001] + ￮ axiom ab20 assumed + + ￫ info[I0001] + ￮ axiom ab21 assumed + + ￫ info[I0001] + ￮ axiom ab22 assumed + + ab22 + : A×B⁽ᵉᵉ⁾ {( a00, b00 )} {( a01, b01 )} ( a02, b02 ) {ab10} {ab11} ab12 + ab20 ab21 + + h⁽ᵉᵉ⁾ ab22 + : C⁽ᵉᵉ⁾ {h ( a00, b00 )} {h ( a01, b01 )} + (refl h {( a00, b00 )} {( a01, b01 )} ( a02, b02 )) {h ab10} {h ab11} + (refl h ab12) (refl h ab20) (refl h ab21) + diff --git a/test/testutil/pmp.ml b/test/testutil/pmp.ml index e15e888a..1fe88638 100644 --- a/test/testutil/pmp.ml +++ b/test/testutil/pmp.ml @@ -59,7 +59,8 @@ and parse_syn : type n. (string, n) Bwv.t -> pmt -> n Raw.synth located = | Field (x, fld) -> unlocated (Raw.Field (parse_syn ctx x, Field.intern_ori fld)) | Pi (x, dom, cod) -> unlocated (Raw.Pi (Some x, parse_chk ctx dom, parse_chk (Snoc (ctx, x)) cod)) - | App (fn, arg) -> unlocated (Raw.App (parse_syn ctx fn, parse_chk ctx arg)) + | App (fn, arg) -> + unlocated (Raw.App (parse_syn ctx fn, parse_chk ctx arg, locate_opt None `Explicit)) | Deg (x, str) -> ( let x = (parse_chk ctx x).value in match Dim.deg_of_name str with diff --git a/test/testutil/repl.ml b/test/testutil/repl.ml index 4cc17c70..34ce7ee4 100644 --- a/test/testutil/repl.ml +++ b/test/testutil/repl.ml @@ -109,6 +109,7 @@ let print (tm : string) : unit = let run f = Lexer.Specials.run @@ fun () -> Parser.Unparse.install (); + History.run_empty @@ fun () -> Eternity.run ~init:Eternity.empty @@ fun () -> Global.run ~init:Global.empty @@ fun () -> Builtins.run @@ fun () -> @@ -126,7 +127,7 @@ let run f = raise (Failure "Fatal error")) @@ fun () -> let init_visible = Parser.Pi.install Scope.Trie.empty in - Scope.run ~init_visible @@ fun () -> f () + Scope.run ~init_visible ~options:Options.default @@ fun () -> f () let gel_install () = def "Gel" "(A B : Type) (R : A → B → Type) → Id Type A B" "A B R ↦ sig a b ↦ ( ungel : R a b )"