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

308 Commits

Author SHA1 Message Date
Leni Aniva d846210b9e Merge pull request 'feat: Print structural projection as application' (#35) from io/serial into dev 
Reviewed-on: #35
 2023-12-05 20:20:51 -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 c80d7567b6 feat: Expose _private names 2023-12-04 23:36:09 -08:00
Leni Aniva f72a82a4c9 feat: Remove stem deduce 
Some private subproofs are not shown in the catalog and this breaks
dependencies
 2023-12-04 16:40:15 -08:00
Leni Aniva 35f411041e feat: Remove printing projections 2023-12-04 16:21:02 -08:00
Leni Aniva 860d2e239a feat: Remove | in symbol output 2023-11-27 09:54:41 -08:00
Leni Aniva e0cfdfaf16 chore: Version bump to 0.2.9 2023-11-26 23:48:47 -08:00
Leni Aniva fe850ded98 feat: Shorter symbol category 2023-11-26 22:14:58 -08:00
Leni Aniva aaebb6b121 feat: Read dependencies of library symbols 2023-11-25 15:07:56 -08:00
Leni Aniva a1d991f5db fix: Rectify error format 2023-11-09 22:24:17 -08:00
Leni Aniva cc9e659c06 Merge pull request 'feat: Allow selective continuation of goals' (#27) from goal/continuation into dev 
Reviewed-on: #27
 2023-11-07 16:49:55 -08:00
Leni Aniva a491316541 fix: Do not show parent state in continue 2023-11-07 13:10:14 -08:00
Leni Aniva e654613182 fix: New goal state not inserted correctly 2023-11-07 13:07:50 -08:00
Leni Aniva d35803791e Merge branch 'dev' into goal/continuation 2023-11-07 12:11:14 -08:00
Leni Aniva d9745094fa fix: Remove the error prone SemihashMap 2023-11-07 12:09:54 -08:00
Leni Aniva 53b63bf46c fix: Remove the error prone SemihashMap 2023-11-07 12:04:17 -08:00
Leni Aniva 4396da3e65 chore: Code formatting 2023-11-06 12:20:08 -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 c6bb4be597 chore: Update documentation 2023-11-06 11:04:28 -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 a5b5e01858 chore: Version bump to 0.2.8 2023-11-04 15:54:28 -07:00
Leni Aniva 4be9dbc84a feat: Goal continuation fails if target has goals 2023-11-04 15:53:57 -07:00
Leni Aniva 97d658cfc5 feat: Add goal.continue command 2023-11-04 15:51:09 -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 1638c308a9 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev 
Reviewed-on: #26
 2023-10-30 14:47: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 6cf328a84f Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev 
Reviewed-on: #25
 2023-10-29 13:08:05 -07:00
Leni Aniva 1a99a2e7b2 fix: Sanitize name in universe levels 2023-10-29 13:03:48 -07:00
Leni Aniva 60854525b9 feat: Simplify printing of function applications 2023-10-29 12:50:36 -07:00
Leni Aniva e523e8bcc6 chore: Version bump (breaking change) 2023-10-29 11:57:24 -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 4ce932eb3b Merge pull request 'Enable handling of m-Coupled goals' (#20) from goal/dependency into dev 
Reviewed-on: #20
 2023-10-27 19:30:20 -07:00
Leni Aniva 045181356c feat: Add REPL function for root expression 2023-10-27 15:41:12 -07:00
Leni Aniva 41e1f64d44 Merge branch 'dev' into goal/dependency 2023-10-27 15:33:47 -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 a9294e0338 Add documentation about flake 2023-10-20 12:54:35 -07:00
Leni Aniva 3d7d5d6b4d feat: Add nix flake 2023-10-20 12:41:56 -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