aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 8 Pull Requests 2 Packages Projects Releases 1 Wiki Activity
155 Commits 8 Branches 16 Tags 1.3 MiB
Commit Graph

50 Commits

Author SHA1 Message Date
Leni Aniva f42a27e036
feat(lib): Expose goal state interface 2024-03-10 08:13:10 -07:00
Leni Aniva d958dbed9d
feat(lib): CoreM execution function 2024-03-10 06:41:35 -07:00
Leni Aniva ca89d671cc
refactor: Move some functions to `Library.lean` 2024-03-09 20:37:48 -08:00
Leni Aniva 863c6d9e7d
feat(lib): Catalog command FFI 2024-03-09 16:50:36 -08:00
Leni Aniva 021d0b5b7d
feat: Add exported version function 2024-03-08 23:50:44 -08:00
Leni Aniva 9a5ee49778
feat: Print parent expression assignment 2024-01-24 18:19:04 -08:00
Leni Aniva 22789436bd
chore: Move environment functions to its own file 
Symbol.lean is now subsumed
 2023-12-15 13:40:36 -05:00
Leni Aniva aca7dc9811
refactor: env. operations into its own file 2023-12-15 13:37:55 -05:00
Leni Aniva 3b83c81540
fix: Force instantiate all mvars in env.add 2023-12-15 13:07:59 -05:00
Leni Aniva 6c25cca46a
test: env.add 2023-12-14 11:11:24 -08:00
Leni Aniva 2f3a91562a
fix: env_add monads 2023-12-14 05:52:12 -08:00
Leni Aniva 09f5792d4a
Merge branch 'dev' into env/add-decl 2023-12-14 05:48:49 -08:00
Leni Aniva 02889510b2
feat: env_add command 2023-12-13 19:35:32 -08:00
Leni Aniva 12544b81ee
chore: Rename lib. commands to env. 
This is done to improve clarity and align with Lean's terminology
 2023-12-12 18:56:25 -08:00
Leni Aniva ab1b309c72
feat: Use CoreM as the main interaction monad 2023-12-12 18:39:02 -08:00
Leni Aniva 1fb189a38f
fix: Consolidate TermElabM blocks 2023-12-08 17:31:25 -08:00
Leni Aniva c76751861a
fix: Change the main interaction monad to MetaM 2023-12-08 16:17:16 -08:00
Leni Aniva 2dc7657e2a
doc: getUsedConstants bug about projections 2023-12-06 15:05:04 -08:00
Leni Aniva da74258dd1
feat!: Display public name only if name is private 2023-12-05 20:20:08 -08:00
Leni Aniva 9f2b07757f
feat: Display whether a symbol is private 2023-12-05 19:07:00 -08:00
Leni Aniva 7b59937853
feat: Read dependencies of library symbols 2023-11-25 15:07:56 -08:00
Leni Aniva 2a9931c134
fix: Rectify error format 2023-11-09 22:24:17 -08:00
Leni Aniva 8218d3f004
fix: Do not show parent state in continue 2023-11-07 13:10:14 -08:00
Leni Aniva 736e68639f
fix: New goal state not inserted correctly 2023-11-07 13:07:50 -08:00
Leni Aniva 764be6d14b
fix: Remove the error prone SemihashMap 2023-11-07 12:09:54 -08:00
Leni Aniva 7076669c3d
chore: Code formatting 2023-11-06 12:20:08 -08:00
Leni Aniva 245e76b2f1
feat: Print the root mvar name 2023-11-06 11:51:31 -08:00
Leni Aniva dbace9f2d5
fix: Use Lean's built in name parser 
The `str_to_name` parser cannot handle numerical names and escapes.
 2023-11-06 10:45:11 -08:00
Leni Aniva db706070ad
feat: Add goal.continue command 2023-11-04 15:51:09 -07:00
Leni Aniva 427d819349
feat: Add REPL function for root expression 2023-10-27 15:41:12 -07:00
Leni Aniva 82f5494718
feat: Add REPL command for assigning an expression 2023-10-27 15:32:59 -07:00
Leni Aniva e98fb77f33
refactor: Separate goal printing and processing 
Added a test for delta proof variables
 2023-10-26 22:47:42 -07:00
Leni Aniva 9447d29e37
Store states instead of goals 
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)

Documentations pending
 2023-10-15 17:15:23 -07:00
Leni Aniva 8c93d30ab7
Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00
Leni Aniva 46347d8244
Add SemihashMap interface, rename proof commands to goal commands, allow deletion 2023-08-30 19:16:33 -07:00
Leni Aniva 80ad7a2bd0
Rename proof commands to goal commands 2023-08-27 19:58:52 -07:00
Leni Aniva 0c5f439067
Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00
Leni Aniva 81702d12ef Remove the obsolete name field from proof tree structure 2023-08-26 18:50:15 -07:00
Leni Aniva 95d26a2f50
Classify JSON error as command error 
Also add documentation for this
 2023-08-24 22:51:40 -07:00
Leni Aniva 7160f8aa61
Merge branch 'dev' into io/serial 2023-08-23 13:25:08 -07:00
Leni Aniva 85440e0278
Unify json and unknown error into command error 2023-08-23 13:00:11 -07:00
Leni Aniva 1d1fa60175
Move all json-string functions to Main.lean 2023-08-22 09:54:37 -07:00
Leni Aniva ddf7ec21c8 Add compressed json print option; Rearrange commands into hierarchy 2023-08-16 19:25:32 -07:00
Leni Aniva 0e61093f47 Add proof variable delta; Bump version to 0.2.1 2023-08-15 15:40:54 -07:00
Leni Aniva d476354a4a Add expression sexp printing (2/2) 2023-08-14 21:43:40 -07:00
Leni Aniva 19c57ada1e Add expression sexp printing (1/2, tests pending) 2023-08-14 17:07:53 -07:00
Leni Aniva d705cdf0e5 version bump, restructure 2023-08-13 21:19:06 -07:00
Leni Ven 3cb0795bb6 Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
Leni Aniva 0b2db92b4a Separate commands into its own file 2023-05-09 18:01:09 -07:00
Leni Aniva 9bba78eb1d Initial commit 2023-05-07 15:19:45 -07:00