aya-prover / aya-dev Goto Github PK

View Code? Open in Web Editor NEW

268.0 9.0 16.0 16.07 MB

A proof assistant and a dependently-typed language

Home Page: https://www.aya-prover.org

License: MIT License

Java 97.59% Groovy 0.25% Shell 0.54% Batchfile 0.03% Lex 0.68% Nix 0.04% JavaScript 0.58% CSS 0.24% HTML 0.05%

aya proof-assistant dependent-types

aya-dev's Introduction

Website contains:

Development blogs which are written for general audience
Installation instructions (basically telling you what to download in GitHub Releases)
Tutorial for functional programming features
Tutorial for theorem proving features

Warning

Aya is under active development, so don't be surprised about bugs, usability or performance issues (please file issues or create threads in discussions!), but we have the goal to make it as user-friendly as we can feasibly do.

What to expect?

Dependent types, including Π-types, Σ-types, indexed families, etc. You could write a sized-vector type.
Set-level cubical type theory (XTT).
- Demonstration of quotient-inductive-inductive types, no forward declaration or mutual block needed! We infer the type checking order by how definitions use each other.
- Proof of funExt in paths.aya.
Pattern matching with first-match semantics. Checkout the red-black tree (without deletion yet).
A JIT-compiler that translates Aya code to higher-order abstract syntax in Java. This makes the interpreter to run tree-sort 10x faster! See benchmark code.
Overlapping and order-independent patterns. Very useful in theorem proving.
A literate programming mode with inline code fragment support, inspired from Agda and 1lab. You may preview the features (in Chinese) here.
Binary operators, with precedence specified by a partial ordering (instead of a number like in Haskell or Agda).
A fairly good termination checker. We adapted some code from Agda's implementation to accept more definitions such as the testSwapAdd example in this file (which are rejected by, e.g. Arend).

Contributing to Aya

Important

Since you need Java 21 to set this project up, in case your choice of IDE is IntelliJ IDEA, version 2023.3 or higher is required.

Questions or concerns are welcomed in the discussion area. We will try our best to answer your questions, but please be nice.
We welcome nitpicks on error reporting! Please let us know anything not perfect. We have already implemented several user-suggested error messages.
Before contributing in any form, please read the contribution guideline thoroughly and make sure you understand your responsibilities.
Please follow the Code of Conduct to ensure an inclusive and welcoming community atmosphere.
Ask @ice1000 or simply create a ticket in the discussion to become an organization member.
- If you want to contribute, ask before doing anything. We are reluctant to accept PRs that contradict our design goals. We value your time and enthusiasm, so we don't want to close your PRs :)

Use as a library

It's indexed in mvnrepository, and here are some example build configurations:

<!-- Maven -->
<dependency>
    <groupId>org.aya-prover</groupId>
    <artifactId>[project name]</artifactId>
    <version>[latest version]</version>
</dependency>

// Gradle
implementation group: 'org.aya-prover', name: '[project name]', version: '[latest version]'

[project name] specifies the subproject of Aya you want to use, and the options are pretty, base, cli-impl, parser, etc.
- The syntax definitions live in syntax.
- The parser lives in parser (the generated parsing code) and producer (transformer from parse tree to concrete syntax tree).
- The type checker lives in base.
- The JIT compiler lives in jit-compiler.
- The generalized pretty printing framework is in pretty.
- The library system, literate mode, single-file type checker, and basic REPL are in cli-impl.
- The generalized tree builder, generalized termination checker, and a bunch of other utilities (files, etc.) are in tools.
- The generalized binary operator parser, generalized mutable graph are in tools-kala because they depend on a larger subset of the kala library.
- The command and argument parsing framework is in tools-repl. It offers an implementation of jline3 parser based on Grammar-Kit and relevant facilities.
- The literate-markdown related infrastructure is in tools-md. It offers commonmark extensions for literate mode of any language with a highlighter.
[latest version] is what you see on this badge .

aya-dev's People

Stargazers

Watchers

Forkers

archive-tsao-chi-forks refparo photonquantum forked-by-mio hoshinotented cjdxhjj vitalyankh fossabot alicecooper214 hartl3y94 schrodingerzhu greathaop rohankumardubey drruisseau tisonkun lllgoyour

aya-dev's Issues

Pattern synonyms

We could start from 'pattern definitions':

\def addN (a, b : Nat) : Nat
 | zero, a => a
 | a, zero => a
 | suc a, b => suc (addN a b)
 | a, suc b => suc (addN a b)

\pat one : Nat => suc zero
\pat suc-suc-a (a : Nat) => addN (suc (suc zero)) a

\def a-2 (a : Nat) : Nat
 | suc-suc-a a => a
 | one => one
 | zero => zero

Note that I want to use \pat definitions as both patterns and functions.

Originally posted by @ice1000 in https://github.com/ice1000/aya-prover/issues/190#issuecomment-809092666

Where are we, from literature mode?

Let me start: a syntax design for a suitable markup language. Obviously we need our own markup language 🤔 and we need to compile it in our Doc backends.

'Success' test cases deduplication

Currently, we have lots of code duplicated in the 'success' test folder. How much of them are actually duplicated, and how much can we delete them? I think a lot of files can be removed.

I recently added an extremely heavy sanity check to the tycker, and it's causing some OOM on my laptop when running tests. These checks are removed in release builds, but we still want the tests to run faster.

Recover "tyck options"

E.g. "type in type"

Equal Sigma type is not equal

Commit: c7d7714

open data Unit : Type | unit

def foo : Sig Unit ** Unit => (unit, unit)

def bar : Sig Unit ** Unit => foo

Wrong parsing of lmax expression

Commit: 708d533

universe u v
def test (A : Type u) (B : Type v) : Type (lmax u v) => A

Error message:

In file code/test.aya:48:48 ->

  46 | 
  47 | universe u v
  48 | def test (A : Type u) (B : Type v) : Type (lmax u v) => A
                                                       ^-^

Error: Expected level expression, got: u v

Seemingly unsolvable level equation

Aya version: latest build (e4948a9) from GitHub Actions

Code:

struct TypeStruct : Set
  | type : Set

def setType (type' : Set) (ts : TypeStruct) : TypeStruct
  => new TypeStruct { | type => type' }

Got error:

In file code/test.aya:5:9 ->

  3 | 
  4 | def setType (type' : Set) (ts : TypeStruct) : TypeStruct
  5 |   => new TypeStruct { | type => type' }
           ^--------------------------------^ TypeStruct.u <= TypeStruct.u

Error: Cannot solve some level equation(s)

There seems no way to solve this error.

PS. Will there be a syntax for struct updating like in Idris?
PS2. Will there be partial implementation like in Arend?
PS3. Do my issues feel spamming?

Coercion

As title

First-class patterns, or, patterns-as-objects

As title. I think this is an interesting idea, and I will discuss this with y'all in the next Walpurgis night.

Optimize telescope type checking

Currently, if you write (A B : Type), it is translated into (A : Type) (B : Type) right in the parser. This convenients the rest of the passes, but it makes the type term checked multiple times. If we can make it checked only once, that will save some heat produced by tycking, saving the world from global warming.

To do so, we need to change at least the concrete syntax, but not necessarily the core syntax.

This also applies to lambda terms.

Pragma design

How do we design pragmas? This is needed for the design of prelude.

Meta solver fails to solve unused type arguments of struct type

Commit: 77e6676

This causes an "unsolved meta" error:

struct Unit : Type

open data Foo (x : Unit) : Type | foo

def foo' : Foo (new Unit {}) => foo

This works, however:

open data Unit : Type | unit

open data Foo (x : Unit) : Type | foo

def foo' : Foo unit => foo

Bin op parser

BinOp syntax could be improved. Right now we have two names for one function, which seems not good.
BinOp section, i.e. (a +)
BinOp all have lower priority than application, so one less keyword and less bind looser

NullPointerException when type checking

Aya version: latest build (0443f16) from GitHub Actions
Code:

data Entity : Set
  | john

struct EventT : Set
  | agentT : Set

struct Event (t : EventT) : Set
  | agent : t.agentT

data Run (e : Event (new EventT { | agentT => Entity })) : Set
  | (john) => run1

def mkVerb {t : EventT} (p : Event t -> Set) : (Event t -> Set) -> Set
  => \f => Sig (e : Event t) ** (Sig (p e) ** (f e))

Record inheritance

How to do this? In Lean, if structure a extends b, then we can build a by either { to_b := some_b_instance, <fields of a> } or { <fields of b>, <fields of a> }. When accessing some b field in an a instance, we can either use a.field or a.to_b.field.

How to implement completion?

As title. I'm quite unsure how to do this..

Typeclass Inheritance

Basically,

Use the same underlying structure as record inheritance
Auto search for the inherited typeclass's instance, hint user to give manually when >1 instances exist
Also introducing the parent typeclass instance into scope when child typeclass instance is in scope (e.g. Functor available when Applicative in scope)

Arend's iso

https://github.com/JetBrains/Arend/blob/124bc2ba691836b126ab1385deec0e01a6f11e5e/lib/Prelude.ard#L79-L81

How to typecheck `let`-expressions?

I've been thinking about the details of this. Firstly, if we don't have let-expressions, we only have to detect all definitions at the top-level and submodules and form a dependency graph out of it. However if we have let-expressions, I think the solution is like this:

Detect all top-level definitions and submodule definitions (but not definitions in let-expressions);
Form a dependency graph out of them (note that if some def C in some A uses B then A depends on B too);
When typechecking a definition and we meet a let-expression, we form a dependency graph of the module of the let-expression, typecheck them, and go on.

Why not directly form a dependency graph out of all definitions, including those in the let-expressions?

We need to ensure that when we typecheck let-expressions, the localCtx has the variables of the outer definition.
Hence, we should not lift the definitions of let-expressions outside like we did to modules; because this way we could not ensure the localCtx. We should typecheck them only when we meet them, at that time the localCtx will be complete.

Why won't this cause a problem in dependency?

If the def in let-expression depends on another definition outside, then that definition is also depended on by the outer definition of the let-expression. So when we check the let-expression, its dependencies are all checked too.
Another definition outside cannot depend on a definition inside let-expression at all.

Flex-flex meta resolution needs FV subsetting

As title.

Mistaking explicit argument as implicit causes TyckerException

Commit: c7d7714

open data Unit : Type | unit

def foo (x : Unit) : Unit => x

def bar : Unit => foo {unit}

Expected behavior: type error

Inline hints at the same line

Currently they're impled badly

Add `Val` and `Neutral` for NbE

Neutralization by Elimination

Does that sound like a plan? @re-xyr

Match expression in concrete and core

This should be very simple

Too many error messages

Code:

prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
  | at (i : I) : A i {
    | left => a
    | right => b
  }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
bind = looser application

def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))

Error:

In file test.aya:14:90 ->

  12 | bind = looser application
  13 | 
  14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
                                                                                                 ^^

Error: Expected type: Type
       Normalized: Type
       Want: struct type
       Because we want to type a term such as: I
In file test.aya:14:90 ->

  12 | bind = looser application
  13 | 
  14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
                                                                                                 ^---------^

Error: Expected type: Type
       Normalized: Type
       Want: pi type
       Because we want to type a term such as: I.squeeze i
In file test.aya:14:90 ->

  12 | bind = looser application
  13 | 
  14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
                                                                                                 ^-----------^

Error: Expected type: Type
       Normalized: Type
       Want: pi type
       Because we want to type a term such as: I.squeeze i j
In file test.aya:14:72 ->

  12 | bind = looser application
  13 | 
  14 | def psqueeze {A : Type} {a a' : A} (p : a = a') (i : I) : a = p.at i => path (\j => p.at (I.squeeze i j))
                                                                               ^------------------------------^

Error: Expected type: Eq {A} a (p.at i)
       Normalized: Path (λ i ⇒ A) a (p.at i)
       Actual type: Path (λ _9 ⇒ A _9) (p.at <I.squeeze i j>) (p.at <I.squeeze i
       j>)
       Normalized: Path (λ _9 ⇒ A) (p.at <I.squeeze i j>) (p.at <I.squeeze i j>)
       They don't match, sorry
🔨

Probably we only want the first error to appear.

l ≰ (lsuc (lmax l m))

Commit: 8d1e09d

universe l m

def Foo (A : Type l) : Type (lsuc (lmax l m)) => (A -> Type m) -> Type m

Unification in Typeclass Resolution

Say in type class resolution, we meet the following instance

instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C

and we have the resolution problem F X Y. In the description of the tabled typeclass resolution paper, it will generate two subgoals on this instance: F X ?M and F ?M Y.

However the ?M does not behave exactly like a metavariable. Namely, it can have multiple ~~temporary~~ [worse, may be not temporary because both solutions may be applicable to the remaining subgoal] solutions: if we have instances F X Z1 and F X Z2, then ?M equates to both in the resolution process.

Should we change how our metavariable works? Or should we use another kind of syntactic construct for this purpose?

How do we load default PP config?

From CLI args? From a file? Wdyt?

Definition cannot type check

The following file, when including the last line, cannot type check.
I suspect the normalized form is wrong.

prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
  | at (i : I) : A i {
    | left => a
    | right => b
  }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)

bind = looser application

prim arcoe
def hfill2d {A : Type}
  {a b c d : A}
  (p : a = b)
  (q : b = d)
  (r : a = c)
  (i j : I) : A
  => (arcoe (\ k => (r.at k) = (q.at k)) p i).at j
def hcomp2d {A : Type}
  {a b c d : A}
  (p : a = b)
  (q : b = d)
  (r : a = c) : c = d
  => path (hfill2d p q r right)

def sym {A : Type} {a b : A} (p : a = b) : b = a => hcomp2d (idp a) (idp a) p
def `~` trans {A : Type} {a b c : A} (p : a = b) (q : b = c) : a = c => hcomp2d p q (idp a)
def pmap {A B : Type} (f : A -> B) {a b : A} (p : a = b)
  : f a = f b => path (\ i => f (p.at i))

-- def funext {A B : Type} (f g : A -> B) (p : Pi (a : A) -> f a = g a) : f = g
--   => path (\ i => \ x => (p x).at i)

def sq {A B C : Type} {a c : A} {b d : B} (f : A -> B -> C) (p : a = c) (q : b = d) : f a b = f c d
=> trans (pmap (f a) q) (pmap (\ x => f x d) p)

def isProp (A : Type) : Type => Pi (x : A) (y : A) -> x = y

def isSet (A : Type) : Type => Pi (x : A) (y : A) -> isProp (x = y)

data Bot : Type

open data Top : Type
  | T

open data Nat : Type
  | zero
  | suc Nat

def `+` add (m n : Nat) : Nat
  | zero, n => n
  | n, zero => n
  | suc m, n => suc (add m n)
  | m, suc n => suc (add m n)

def `*` mul (m n : Nat) : Nat
  | zero, n => zero
  | m, zero => zero
  | suc m, suc n => suc (m + n + m * n)

def `*'` mul' (m n : Nat) : Nat
  | zero, n => zero
  | m, zero => zero
  | suc m, n => n + m *' n

def `*''` mul'' (m n : Nat) : Nat
  | zero, n => zero
  | m, zero => zero
  | m, suc n => m + m *'' n

bind + tighter =

bind * tighter +
bind *' tighter +
bind *'' tighter +

def BiOp (A : Type) => A -> A -> A

def Associative {A : Type} (· : BiOp A) => Pi (x y z : A) -> (· x (· y z)) = (· (· x y) z)

def Commutative {A : Type} (· : BiOp A) => Pi (x y : A) -> (· x y) = (· y x)

def Identity {A : Type} (e : A) (· : BiOp A) => Pi (x : A) -> Sig ((· e x) = x) ** ((· x e) = x)

def +-comm (x y : Nat) : x + y = y + x
  | zero, n => idp n
  | suc n, m => pmap suc (+-comm n m)

def +-assoc (x y z : Nat) : x + (y + z) = (x + y) + z
  | zero, y, z => idp _
  | suc x, y, z => pmap suc (+-assoc x y z)

def +-identity (x : Nat) : Sig (x + zero = x) ** (zero + x = x)
  | x => (idp x, idp x)

def *'-suc (m n : Nat) : m *' (suc n) = m + m *' n
  | zero, n => idp _
  | suc m, n => (pmap (\ x => suc (add n x)) (*'-suc m n))
    ~ (pmap suc (+-assoc n m (m *' n)))
    ~ (pmap (\ x => suc (x + m *' n)) (+-comm n m))
    ~ (pmap suc (sym (+-assoc m n (m *' n))))

def *'-suc-suc (m n : Nat) : (suc m) *' (suc n) = suc (m + n + m *' n)
  => (pmap (add (suc n)) (*'-suc m n))
    ~ (pmap suc (+-assoc n m (m *' n)))
    ~ (pmap (\ x => suc (x + m *' n)) (+-comm n m))

def *'-*''-iso (m n : Nat) : m *' n = m *'' n
  | m, zero => idp _
  | m, suc n => (*'-suc m n) ~ (pmap (add m) (*'-*''-iso m n))

def *-*'-iso (m n : Nat) : m *' n = m * n
  | zero, n => idp _
  | m, zero => idp _
  | suc m, suc n => (*'-suc-suc m n) ~ (pmap (\ x => suc ((m + n) + x)) (*-*'-iso m n))

def sym-*'-suc-suc (m n : Nat) : suc (m + n + m *' n) = (suc m) *' (suc n) => sym (*'-suc-suc m n)

  120 |   | suc m, suc n => (*'-suc-suc m n) ~ (pmap (\ x => suc ((m + n) + x)) (*-*'-iso m n))
  121 |
  122 | def sym-*'-suc-suc (m n : Nat) : suc (m + n + m *' n) = (suc m) *' (suc n) => sym (*'-suc-suc m n)
                                                                                      ^-----------------^

Error: Cannot check the expression of type
         Path (λ _9 ⇒ Nat) (hfill2d {Nat} {suc (add n (mul' m (suc n)))} {suc (add
        n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))} {suc (add n (mul' m (suc
        n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp {Nat} suc (add n (mul'
        m (suc n)))) (*'-suc-suc m n) right left) (hfill2d {Nat} {suc (add n (mul'
        m (suc n)))} {suc (add n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))}
        {suc (add n (mul' m (suc n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp
        {Nat} suc (add n (mul' m (suc n)))) (*'-suc-suc m n) right right)
         (Normalized: Path (λ _9 ⇒ Nat) (suc (add n (add m (mul' m n)))) (suc (add
        n (mul' m (suc n)))))
       against the type
         Eq {Nat} (suc (add (add m n) (mul' m n))) (mul' (suc m) (suc n))
         (Normalized: Path (λ i ⇒ Nat) (suc (add (add m n) (mul' m n))) (suc (add n
        (mul' m (suc n)))))

Confusing warning of nonexistent name shadowing

Aya version: latest build (e4948a9) from GitHub Actions

Code:

def f {t : Set} : t -> (((t -> Set) -> Set) -> Set) -> Set
  => \x => \f => f (\g => g x)

Got warning:

In file code/test.aya:1:24 ->

  1 | def f {t : Set} : t -> (((t -> Set) -> Set) -> Set) -> Set
                              ^-----------------^
  2 |   => \x => \f => f (\g => g x)

Warning: The newly bound name `x5` shadows a previous local definition from outer scope

Should we also allow arbitrary dependency order in structs and datas?

This means allowing fields/ctors defined later refer to those defined earlier in their types, as what we did to Stmts, as long as the dependency graph forms a DAG.

For structs,

struct A : \Type
  | v : T
  | T : \Type

For datas,

data B (n : N) : \Type \with
  | zero => { | conA (P conC) | conB }
  | suc m => { | conC | conD (P conA) }

The case for datas looks more complicated because constructors are intertwined with match clauses.

`new` expressions are pretty printed in a very ugly way

So we should improve it

The latest build broke my code

This code tycks in beca413 but not in the latest build 5b7bfe3:

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)

bind application tighter =

open data Unit : Set | unit

struct Struct : Set
  | value : Unit

def getValue (t : Struct) : Unit => t.value
def setValue (x : Unit) (t : Struct) : Struct
  => new Struct { | value => x }

def value-inv : Pi {t : Struct} {u : Unit} -> u = getValue (setValue u t)
  => \{t} {u} => idp u

def foo {A : Set}
  (get : Struct -> A)
  (set : A -> Struct -> Struct)
  (inv : Pi {t : Struct} {u : A} -> u = get (set u t))
  => unit

def bar : Unit => foo getValue setValue value-inv

(Want a better title for this issue)

Pattern matching on structs causes TyckerException

Commit: beca413

open data Bool : Set | true | false

struct BoolPair : Set
  | fst : Bool
  | snd : Bool

open data U2 (x : BoolPair) : Set
  | (false, false) => zero
  | (false, true) => one
  | (true, false) => two
  | (true, true) => three

def not2 (x : BoolPair) : BoolPair
  | (false, false) => (true, true)
  | (false, true) => (true, false)
  | (true, false) => (false, true)
  | (true, true) => (false, false)

Both the data and the function definition cause the exception.

I don't really know the syntax for pattern matching on structs, so I could only guess it's the same as tuples as in Arend. Replace the parentheses with braces and the issue still occurs.

Judging from the source code, tycking for tuple patterns is not yet completed?

Tycker tries to solve implicit argument in Pi types even when not needed

Commit: 1707136

open data Unit : Set | unit

def foo : Pi {x : Unit} -> Unit => \{x} => x

def foo' : Pi {x : Unit} -> Unit => foo

Update:

@re-xyr The real use case is much more complex and the return type does depend on the implicit argument:

-- *** Prelude

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : ooType
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : ooType => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
  => arcoe eq.at x i

bind = looser application

open data Unit : Set 0 | unit


-- *** Types

struct EventT : Set 1
  | agentT : Set 0

def getAgentT (t : EventT) : Set 0 => t.agentT
def setAgentT (x : Set 0) (t : EventT) : EventT
  => new EventT { | agentT => x }
def agentT-inv (t : EventT) (u : Set 0) : u = getAgentT (setAgentT u t)
  => idp u


struct Event (t : EventT) : Set 2
  | agent : t.agentT

def getAgent (t : EventT) (e : Event t) : t.agentT => e.agent


def Theta (setT : Set 0 -> EventT -> EventT) : ooType 4
  => Pi {u : Set 0} {t : EventT}
  -> ((u -> ooType 3) -> ooType 3)
  -> ((Event (setT u t) -> ooType 3) -> ooType 3)
  -> (Event (setT u t) -> ooType 3) -> ooType 3

def mkTheta
  (getT : EventT -> Set 0)
  (get : Pi (t : EventT) -> Event t -> getT t)
  (setT : Set 0 -> EventT -> EventT)
  (invariant : Pi (t : EventT) (u : Set 0) -> u = getT (setT u t))
  : Theta setT
  => \{u} {t} => \q p => \f =>
    q (\x => p (\e =>
      Sig (get (setT u t) e = coe (invariant t u) x right) ** (f e)))

def agent : Theta setAgentT
  => mkTheta getAgentT getAgent setAgentT agentT-inv

I had to change agent into \{u} {t} => mkTheta getAgentT getAgent setAgentT agentT-inv {u} {t} to make it type check.

I simplified it too much, sorry.

Library leftover

TODOs:

refactor resolver by taking submodules into consideration
reuse compiled core to speed up compilation
make recompile decision with a file dependency graph
#216

/cc aya-prover/aya-prover-proto#652

`forall` syntax for pi types

Similar to Agda's forall. Also, we may add exists for Sig.

More universe level related issues #3

Commit: 9984090

I'm trying to define mkVerb T p : Verb T:

universe u v

open data EventT : Type (lsuc u)
  | CarrierT (A : Type u)

def GetAgentT (T : EventT {universe u}) : Type u
  | CarrierT A => A

struct Event (T : EventT {universe u}) : Type u
  | agent : GetAgentT T

def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v

def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v))
  => Quantifier {universe u, v} (Event T)

def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type v)
  : Verb {universe u, v} T
  => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)

And Aya required that Event.u <= Verb.v:

  17 | def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type v)
  18 |   : Verb {universe u, v} T
                ^-------------^ Verb.u == u, Verb.v == v
  19 |   => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)
                           ^------------------^ Event.u <= Verb.v

So I changed the definition of mkVerb:

def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type (lmax u v))
  : Verb {universe u, lmax u v} T
  => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)

It's obvious that u <= lmax u v, but it still doesn't work.

Name one of the tools Megumu

Since we have the blue Aya (i.e. Iizunamaru Megumu) now, who is the leader of Tengu's (incl. Aya), we can consider naming one of our tools Megumu too (such as the package manager, or the installation manager). We may also use mgm as a mysterious abbreviation.

Getting rid of shitty upstream depedencies

We are currently suffering from the following projects:

Eclipse lsp4j, which is itself a shit mountain (doesn't work with jpms, caused a lot of installation/jlink problems, written in Java 8) and also has shit mountain dependencies (guava, xtext, xtend, etc.)
- I found an alternative, see georgewfraser/java-language-server#197
- Published!
The badass jlink plugin of Gradle -- it is not itself a shit mountain (it's a great project), but it's designed for shit mountains. It aims at repackaging your fatJar into a jpms module and let jlink process it. Aya is built entirely with jpms, so if we have all upstream deps jpms-ed, we can get rid of this plugin entirely.
- ~~The plugin does not work with Java 19.~~
  - There are new maintainers now, works with latest Java
Gradle -- it is fine at the moment because we still want it to offer us the ability to publish to maven central, but Gradle is also designed for maven style projects. Ughh.
ANTLR4-runtime -- doesn't support jpms is the only problem (yet). Seems not very hard to repackage with jpms support.
- We've decided #466
Commonmark -- doesn't support jpms, written in Java 8 with a return-void visitor (commonmark/commonmark-java#125). I think we can take some code from it, repackage, and add jpms support.
- ~~There is an outdated attempt to add jpms: https://github.com/xzel23/commonmark-java/tree/0.14.0-jigsaw~~
- Already repackaged and redistrubuted, see https://github.com/aya-prover/commonmark-java
GSON -- it's a PROJECT FROM GOOGLE so it's gonna be a disaster to depend on it. However, it supports jpms, so I think it's fine to use it (well but people are complaining google/gson#1315 (comment)).
JImGui -- it doesn't yet have jpms support, but I can add it in a minute since it's my project, so it's a small problem.

Also, I propose removing the tgbot subproject since it's useless.

More universe level related issues #2

Commit: f3b10ad

I'm trying to define Verb T = Quantifier (Event T).

(Why is the order of Quantifier's level params v, u, rather than u, v?)

universe u v

open data EventT : Type (lsuc u)
  | CarrierT (A : Type u)

def GetAgentT (T : EventT {universe u}) : Type u
  | CarrierT A => A

struct Event (T : EventT {universe u}) : Type u
  | agent : GetAgentT T

def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v

def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v)) => Quantifier {universe v, u} (Event T)

Tyck order

Opened during Walpurgis night

Agda or Lean style generalization

As title. Agda has some technical slides, I think we could learn from that.

Inline comment delimiter requires a space after it

--def f : Type 1 => Type 0

Paper reading activity

Anybody wanna read some papers with me?

Plans:

Swapping `def x` and `def y` of implicit2.aya causes NPE

implicit2.aya:

open data Unit : Set | unit

def y : Pi {a : Unit} -> Unit => \{a} => a
def x : Pi {a : Unit} -> Unit => y
def z : Pi {a : Unit} -> Unit => x

It does not typecheck as expected.

But a slightly different version causes NPE

open data Unit : Set | unit

def x : Pi {a : Unit} -> Unit => y
def y : Pi {a : Unit} -> Unit => \{a} => a
def z : Pi {a : Unit} -> Unit => x

stacktrace:

    java.lang.NullPointerException
        at java.base/java.util.Objects.requireNonNull(Objects.java:208)
        at org.aya.core.def.Def.defLevels(Def.java:39)
        at org.aya.tyck.ExprTycker.levelStuffs(ExprTycker.java:277)
        at org.aya.tyck.ExprTycker.defCall(ExprTycker.java:265)
        at org.aya.tyck.ExprTycker.inferRef(ExprTycker.java:231)
        at org.aya.tyck.ExprTycker.doVisitRef(ExprTycker.java:223)
        at org.aya.tyck.ExprTycker.visitRef(ExprTycker.java:212)
        at org.aya.tyck.ExprTycker.visitRef(ExprTycker.java:57)
        at org.aya.concrete.Expr$RefExpr.doAccept(Expr.java:244)
        at org.aya.concrete.Expr.accept(Expr.java:41)
        at org.aya.tyck.ExprTycker.checkNoZonk(ExprTycker.java:125)
        at org.aya.tyck.ExprTycker.lambda$checkNoZonk$2(ExprTycker.java:123)
        at org.aya.tyck.LocalCtx.with(LocalCtx.java:62)
        at org.aya.tyck.LocalCtx.with(LocalCtx.java:47)
        at org.aya.tyck.ExprTycker.checkNoZonk(ExprTycker.java:122)
        at org.aya.tyck.ExprTycker.checkExpr(ExprTycker.java:135)
        at org.aya.tyck.StmtTycker.lambda$visitFn$8(StmtTycker.java:184)
        at kala.control.Either$Left.map(Either.java:166)
        at org.aya.tyck.StmtTycker.visitFn(StmtTycker.java:183)
        at org.aya.tyck.StmtTycker.visitFn(StmtTycker.java:43)
        at org.aya.concrete.stmt.Decl$FnDecl.doAccept(Decl.java:324)
        at org.aya.concrete.stmt.Decl.accept(Decl.java:70)
        at org.aya.concrete.stmt.Decl.tyck(Decl.java:61)
        at org.aya.concrete.resolve.module.FileModuleLoader.tyckModule(FileModuleLoader.java:99)
        at org.aya.cli.single.SingleFileCompiler.compile(SingleFileCompiler.java:51)
        at org.aya.test.TestRunner.runFile(TestRunner.java:66)
        at org.aya.test.TestRunner.lambda$runDir$2(TestRunner.java:55)
        at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
        at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
        at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
        at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
        at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
        at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1845)
        at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
        at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
        at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
        at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
        at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
        at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
        at org.aya.test.TestRunner.runDir(TestRunner.java:55)
        at org.aya.test.TestRunner.runAllAyaTests(TestRunner.java:44)

Normalization problem

Commit: 1707136

Given the following code:

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : ooType
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : ooType => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
  => arcoe eq.at x i

bind = looser application

open data Unit : Set 0 | unit

open data Entity : Set 0
  | john

struct EventT : Set 1
  | agentT : Set 0

def getAgentT (t : EventT) : Set 0 => t.agentT
def setAgentT (x : Set 0) (t : EventT) : EventT
  => new EventT { | agentT => x }
def agentT-inv {t : EventT} {u : Set 0} : (setAgentT u t).agentT = u
  => idp u

struct Event (t : EventT) : Set 2
  | agent : t.agentT

def getAgent (t : EventT) (e : Event t) : t.agentT => e.agent

open data RunImpl (ag : Entity) : Set 0
  | john => run1

def Run (e : Event (new EventT { | agentT => Entity })) : Set 3
  => RunImpl e.agent

def mkVerb {t : EventT} (p : Event t -> Set 3) : (Event t -> Set 3) -> Set 3
  => \f => Sig (e : Event t) ** (Sig (p e) ** (f e))

def run : (Event (new EventT { | agentT => Entity }) -> Set 3) -> Set 3
  => mkVerb {new EventT { | agentT => Entity }} Run

def mkTheta
  (getT : EventT -> Set 0)
  (get : Pi (t : EventT) -> Event t -> getT t)
  (setT : Set 0 -> EventT -> EventT)
  (invariant : Pi {t : EventT} {u : Set 0} -> u = getT (setT u t))
  : Pi {u : Set 0} {t : EventT}
  -> ((u -> ooType 3) -> ooType 3)
  -> ((Event (setT u t) -> ooType 3) -> ooType 3)
  -> (Event (setT u t) -> ooType 3) -> ooType 3
  => \{u} {t} => \q p => \f =>
    q (\x => p (\e => Sig (get (setT u t) e = coe invariant x right) ** (f e)))

def agent' :
  Pi {u : Set 0} {t : EventT}
  -> ((u -> ooType 3) -> ooType 3)
  -> ((Event (setAgentT u t) -> ooType 3) -> ooType 3)
  -> (Event (setAgentT u t) -> ooType 3) -> ooType 3
  => \{u} {t} => mkTheta getAgentT getAgent setAgentT (\{t'} {u'} => agentT-inv {t'} {u'}) {u} {t}

def mkConst {t : Set} (x : t) : (t -> ooType 3) -> ooType 3
  => \f => f x

def john' : (Entity -> ooType 3) -> ooType 3
  => mkConst john

def mkSentence {t : EventT} (p : (Event t -> ooType 3) -> ooType 3) : ooType 3
  => p (\x => Unit)

def john-runs : ooType 3 =>
  mkSentence {new EventT { | agentT => Entity }}
    (agent' {Entity} {new EventT { | agentT => Unit }} john' run)

def proof-john-runs-event : Event (new EventT { | agentT => Entity })
  => new Event (new EventT { | agentT => Entity }) { | agent => john }

This code doesn't type check because the function body can't be typed:

def proof-john-runs : john-runs => (proof-john-runs-event, (run1, (idp john, unit)))

The type expected by the compiler was:

Σ (e : Event new { | agentT ⇒ Entity }) ** (_ : Σ (_1 : RunImpl
       e.agent) ** (_ : Σ (_7 : Path (λ i ⇒ Entity) e.agent john) ** (_ : Unit)))

So I wrote this, which type checks:

def proof-john-runs-impl
  : Sig (e : Event (new EventT { | agentT ⇒ Entity }))
    ** Sig (RunImpl e.agent)
      ** (Sig (Path (\i => Entity) e.agent john) ** Unit)
  => (proof-john-runs-event, (run1, (idp john, unit)))

However, this still doesn't type check:

def proof-john-runs : john-runs => proof-john-runs-impl

(Sorry, I couldn't simplify this example; it's too difficult for me.)

More universe level related issues #1

~~I plan to post all level related issues here in the future.~~

Commit: d2ef653

universe u

open data EventT : Type (lsuc u)
  | CarrierT (A : Type u)

def GetAgentT (T : EventT) : Type u
  | CarrierT A => A


struct Event (T : EventT) : Type (lsuc (lsuc u))
  | agent : GetAgentT T


universe v

def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v


def Verb (T : EventT) : Type (lsuc (lsuc u)) => Quantifier (Event T)

def mkVerb {T : EventT} (p : Event T -> Type v) : Verb T
  => \f => Sig (e : Event T) (s : p e) ** (f e)

(Apart from the level error, it's strange that the level parameter (lsuc (lsuc u)) of the type of Event can be omitted)

(I'm trying to make the program I wrote before level-polymorphic)
(Would there be a way to specify the level parameters for functions manully?)

Replace some visitors with pattern matching?

Question: allow overwriting fields that have default values?

fields that have default values are called FieldImpl in Aya source code.
Are we going to allow overwriting the field impls? for example

\struct Cross : \Set
  | base : Nat
  | plus1 => suc base

The plus1 has a value which depends on base. So we can use this syntax to create Cross:

\new Cross { | base => zero }

where the plus1 should be suc zero

Should we allow this new operation ?

\new Cross { | base => zero | plus1 => zero }

I think we should because we will have extends in the future which also overwrites fields.
What do you think?

aya-prover / aya-dev Goto Github PK

aya-dev's Introduction

What to expect?

Contributing to Aya

Use as a library

aya-dev's People

Stargazers

Watchers

Forkers

aya-dev's Issues

Recommend Projects

Recommend Topics

Recommend Org