aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity
178 Commits 6 Branches 17 Tags 1.3 MiB
Commit Graph

67 Commits

Author SHA1 Message Date
Leni Aniva e79e386b39 test: Catalog has no numeric symbols 2024-03-28 20:44:09 -07:00
Leni Aniva 8fa1a7d383 feat: Stop cataloging internal/detail dependencies 2024-03-28 19:49:44 -07:00
Leni Aniva 9e68a9cae4 test: Elimination of aux lemmas 2024-03-28 19:27:45 -07:00
Leni Aniva a698a4250f feat: Unfold aux lemmas when printing root expr 2024-03-28 18:56:42 -07:00
Leni Aniva 516ab15961 feat: Bump toolchain version 2024-03-28 00:06:35 -07:00
Leni Aniva e6dbf88ce2 fix: Use Arrays only in the ABI 2024-03-14 22:40:14 -07:00
Leni Aniva 111781816f test: Delayed metavariable assignment 2024-02-15 14:47:09 -08:00
Leni Aniva fe5c1eda7d feat: Prevent crash during rootExpr call 2024-01-30 17:22:20 -08:00
Leni Aniva 25f3a2f19d feat: Print parent expression assignment 2024-01-24 18:19:04 -08:00
Leni Aniva 50ac2fea4b feat: Print constructor and recursor info 2024-01-16 14:11:52 -08:00
Leni Aniva 6fb1b2e787 feat: Print inductives in env.inspect 2024-01-16 13:29:30 -08:00
Leni Aniva 6692303da6 test: Simplify monad execution 2024-01-07 14:14:20 -08:00
Leni Aniva 1c370ef2ae refactor: Rename Test/{Catalog,Environment} 2023-12-26 12:22:57 -05:00
Leni Aniva dc90b6b73e chore: Move environment functions to its own file 
Symbol.lean is now subsumed
 2023-12-15 13:40:36 -05:00
Leni Aniva aef93cf506 fix: Force instantiate all mvars in env.add 2023-12-15 13:07:59 -05:00
Leni Aniva a540dd4540 test: env.add 2023-12-14 11:11:24 -08:00
Leni Aniva 69be7c3920 Merge branch 'dev' into env/add-decl 2023-12-14 05:48:49 -08:00
Leni Aniva ff4671cdd0 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 085b12c255 feat: Use CoreM as the main interaction monad 2023-12-12 18:39:02 -08:00
Leni Aniva 2fe4fa9bc4 fix: Change the main interaction monad to MetaM 2023-12-08 16:17:16 -08:00
Leni Aniva 3c2d93259f Merge branch 'dev' into library/catalog 2023-12-05 20:21:22 -08:00
Leni Aniva dbfee00420 feat!: Display public name only if name is private 2023-12-05 20:20:08 -08:00
Leni Aniva cdb1e8576f feat: Display whether a symbol is private 2023-12-05 19:07:00 -08:00
Leni Aniva 35f411041e feat: Remove printing projections 2023-12-04 16:21:02 -08:00
Leni Aniva e654613182 fix: New goal state not inserted correctly 2023-11-07 13:07:50 -08:00
Leni Aniva ce585f7288 feat: Print the root mvar name 2023-11-06 11:51:31 -08:00
Leni Aniva 32fedede6a Merge branch 'dev' into goal/continuation 2023-11-06 11:45:24 -08:00
Leni Aniva 8182da436d chore: Remove unnecessary unsafe's 2023-11-06 11:43:57 -08:00
Leni Aniva ce1cb13e54 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 4be9dbc84a feat: Goal continuation fails if target has goals 2023-11-04 15:53:57 -07:00
Leni Aniva 333355a85d feat: Partial state continuation 2023-11-04 15:33:53 -07:00
Leni Aniva 4a4a33cea7 test: Separate mvar coupling tests 2023-11-04 15:01:41 -07:00
Leni Aniva 59ac83f0b7 bug: Fix quote escape problem 2023-10-30 14:45:43 -07:00
Leni Aniva d1c0dc376f feat: Print metavariable name in goal 2023-10-30 14:44:06 -07:00
Leni Aniva 60854525b9 feat: Simplify printing of function applications 2023-10-29 12:50:36 -07:00
Leni Aniva de250eafd0 feat: Print names in one segment separated with . 2023-10-29 11:56:56 -07:00
Leni Aniva c0dfa04b18 feat: Simplify name printing 2023-10-29 11:18:35 -07:00
Leni Aniva 045181356c feat: Add REPL function for root expression 2023-10-27 15:41:12 -07:00
Leni Aniva 3b1746490d feat: Add REPL command for assigning an expression 2023-10-27 15:32:59 -07:00
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 7a5fe554ba Add holes test stub 
Move tests into their own namespaces
 2023-10-06 17:31:36 -07:00
Leni Aniva 13f3460e9a Fix test failures 2023-10-05 17:51:41 -07:00
Leni Aniva 6d15d1e670 Use makefile instead of ad-hoc script 2023-10-02 10:26:19 -07:00
Leni Aniva a86af1bc57 Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00