Slava Pestov
0571b65cb8
RequirementMachine: Move protocol linear order from ProtocolGraph to RewriteContext
2021-10-21 19:00:10 -04:00
Slava Pestov
77b8dfeeb2
RequirementMachine: Homotopy reduction prefers to delete less-canonical rules
...
Instead of deleting lower numbered rules, compare the LHS, and if they're
equal, compare the RHS, then use that to pick the rule to delete.
2021-10-15 15:13:22 -04:00
Slava Pestov
6441b8bd73
RequirementMachine: Extract some verification logic out of minimizeRewriteSystem()
2021-10-14 15:03:08 -04:00
Slava Pestov
3ee99d6619
RequirementMachine: NFC cleanups for generating conformances
2021-10-09 19:11:15 -04:00
Slava Pestov
371366eb4b
RequirementMachine: Assert that non-redundant rules are fully resolved
2021-10-08 14:28:27 -04:00
Slava Pestov
b8177995df
RequirementMachine: Sort requirements and canonicalize same-type requirements
2021-10-08 14:28:27 -04:00
Slava Pestov
566971dbc2
RequirementMachine: Add some comments and assertions around state transitions
2021-10-08 14:28:27 -04:00
Slava Pestov
2db676d41a
RequirementMachine: Homotopy reduction deletes rules with unresolved name symbols first
2021-10-01 00:57:44 -04:00
Slava Pestov
86ee6c2f55
RequirementMachine: Add some comments
2021-10-01 00:56:50 -04:00
Slava Pestov
a46a7b893f
RequirementMachine: Check that homotopy reduction was able to eliminate all redundant conformances
2021-10-01 00:56:50 -04:00
Slava Pestov
34592cb2fa
RequirementMachine: Fix generating conformances algorithm for rules of the form [P].[P] => [P]
2021-10-01 00:56:50 -04:00
Slava Pestov
64d1931e15
RequirementMachine: Sketch out "generating conformances" algorithm
2021-09-27 19:04:16 -04:00
Slava Pestov
5f3d781ed3
RequirementMachine: Homotopy reduction tweaks
...
- Skip permanent rules (there's no point, we'll add them back next time)
- Skip conformance rules (these will be handled separately)
- Delete 3-cells that are entirely "in-context" (but don't quote me on
this one, I'm not quite yet convinced it's correct, but it feels right)
2021-09-27 19:03:34 -04:00
Slava Pestov
2b068b3c48
RequirementMachine: Encapsulate 3-cells in a new HomotopyGenerator data type
2021-09-24 08:59:51 -04:00
Slava Pestov
5210e5d475
RequirementMachine: Remove some debugging code
2021-09-24 08:59:51 -04:00
Slava Pestov
67fad897ab
RequirementMachine: Compute left canonical forms of paths
2021-09-24 08:59:51 -04:00
Slava Pestov
5f03c737d2
RequirementMachine: Preliminary implementation of homotopy reduction
2021-09-24 08:59:50 -04:00
