Commit Graph

293 Commits

Author SHA1 Message Date
Leni Aniva f064bb21a4 feat: Assigning a goal with an expression 2023-10-27 15:15:22 -07:00
Leni Aniva 269e5c707c refactor: Separate goal printing and processing
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva c852db2f46 test: m-coupled goals 2023-10-26 11:22:02 -07:00
Leni Aniva 8029298db7 feat: Display user name in Goal structure
1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression
2023-10-25 22:18:59 -07:00
Leni Aniva d991533170 feat: Add proof continue and root extraction 2023-10-25 16:03:45 -07:00
Leni Aniva 538ba6e7d7 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 41db295ff5 Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00
Leni Aniva 35b391881e Add ready message to indicate the main loop is up 2023-10-02 10:14:03 -07:00
Leni Aniva f538f580bd Merge branch 'dev' into tactic/book 2023-08-30 19:17:25 -07:00
Leni Aniva f1f1c20ff9 Add SemihashMap interface, rename proof commands to goal commands, allow deletion 2023-08-30 19:16:33 -07:00
Leni Aniva 6b96f7893f Separate max and imax in sort level 2023-08-27 22:50:18 -07:00
Leni Aniva b98304f78a Version bump to 0.2.4 due to breaking change 2023-08-27 19:59:31 -07:00
Leni Aniva a6e337a89e Rename proof commands to goal commands 2023-08-27 19:58:52 -07:00
Leni Aniva a86af1bc57 Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00
Leni Aniva 9c4c43a9f1 Remove the obsolete name field from proof tree structure 2023-08-26 18:50:15 -07:00
Leni Aniva 59c046efc6 Add proper printing of sorts 2023-08-23 12:51:06 -07:00
Leni Aniva 96cbbf2551 Add compressed json print option; Rearrange commands into hierarchy 2023-08-16 19:25:32 -07:00
Leni Aniva b2ba26528d Add proof variable delta; Bump version to 0.2.1 2023-08-15 15:40:54 -07:00
Leni Aniva 7771408de1 Add expression sexp printing (2/2) 2023-08-14 21:43:40 -07:00
Leni Aniva 9eadd1d4d4 Add expression sexp printing (1/2, tests pending) 2023-08-14 17:07:53 -07:00
Leni Aniva 5cedb9d88c version bump, restructure 2023-08-13 21:19:06 -07:00
Leni Aniva 622aa7f969 Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
Leni Aniva 4613777607 Add json goal printing 2023-05-27 23:10:39 -07:00
Leni Aniva 3e05722d1e Add back the clear command to reset state 2023-05-26 16:55:33 -07:00
Leni Aniva 068a188fea Add expr.type 2023-05-25 13:40:03 -07:00
Leni Aniva e0c5f76451 Rename tactic failure mode to avoid confusion
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva 95ed7d115c Add expression binding printing and import Lean 2023-05-24 00:54:48 -07:00
Leni Aniva 1fed222f56 Use TermElabM as the main monad stack instead of IO 2023-05-23 05:12:46 -07:00
Leni Aniva 94bc3355a2 Save core state in proofs 2023-05-22 22:48:48 -07:00
Leni Aniva ba779766c0 Rename ids so they are consistent 2023-05-22 19:51:16 -07:00
Leni Aniva 0f8df08dd5 Add module name for symbol 2023-05-22 16:00:41 -07:00
Leni Aniva 116c7ff4c6 Add option id handling with ? 2023-05-22 14:56:43 -07:00
Leni Aniva 6a71dad389 Add option format for proof output and test cases 2023-05-22 14:49:56 -07:00
Leni Aniva 46ccad1669 Add default arguments for Json 2023-05-22 00:49:37 -07:00
Leni Aniva 083ec8beec Add REPL tactics 2023-05-21 17:41:39 -07:00
Leni Aniva 15aab3d31f Remove ExceptT from main monad
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva 2a4d348aab Add expression IO stub for constant types 2023-05-20 14:04:09 -07:00
Leni Aniva 8127e9ba06 Add alternative command input format and IO stub 2023-05-20 13:03:12 -07:00
Leni Aniva e246fd961f Add tactic state manipulation 2023-05-17 21:58:03 -07:00
Leni Aniva 4d636ec12b Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
Leni Aniva d3af535652 Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
Leni Aniva b5cb464694 Add README and catalog functions 2023-05-09 22:51:19 -07:00
Leni Aniva f6a520c7a0 Separate commands into its own file 2023-05-09 18:01:09 -07:00