feat: cleanup FSM code to contain real abstractions instead of directly applying low-level functions. #667
Conversation
| internal carry state of this FSM has -/ | ||
| ( σ : Type ) -- Why is σ also not an index? |
There was a problem hiding this comment.
| internal carry state of this FSM has -/ | |
| ( σ : Type ) -- Why is σ also not an index? | |
| internal carry state of this FSM has. -/ | |
| ( σ : Type ) -- Why is σ also not an index? |
| a finite bitvector whose width is given by the arity of `p.σ` -/ | ||
| abbrev State (p : FSM arity): Type := BoolProd p.σ |
There was a problem hiding this comment.
| a finite bitvector whose width is given by the arity of `p.σ` -/ | |
| abbrev State (p : FSM arity): Type := BoolProd p.σ | |
| a finite bitvector whose width is given by the arity of `p.σ`. -/ | |
| abbrev State (p : FSM arity): Type := BoolProd p.σ |
|
|
||
|
|
||
| end FSM |
There was a problem hiding this comment.
| end FSM | |
| end FSM |
|
|
||
|
|
||
| def StateStream (p : FSM arity) := ℕ → p.State |
There was a problem hiding this comment.
| def StateStream (p : FSM arity) := ℕ → p.State | |
| def StateStream (p : FSM arity) := ℕ → p.State |
| /-- `p.carryStream inputStream` computes the stream of carries, from the stream of inputs -/ | ||
| def carryStream (inputStream : BitStreamProd arity) : p.StateStream := fun n => |
There was a problem hiding this comment.
| /-- `p.carryStream inputStream` computes the stream of carries, from the stream of inputs -/ | |
| def carryStream (inputStream : BitStreamProd arity) : p.StateStream := fun n => | |
| /-- `p.carryStream inputStream` computes the stream of carries, from the stream of inputs. -/ | |
| def carryStream (inputStream : BitStreamProd arity) : p.StateStream := fun n => |
| /-- An `arity` indexed product of Booleans. -/ | ||
| def BoolProd (arity : Type) : Type := arity → Bool |
There was a problem hiding this comment.
If we're going to refactor this, I think I'd prefer to just pay the cost once, change arity to a Nat, and use BitVec w
| fun a => (x a).eval y | ||
|
|
||
| /-- A 'arity' indexed product of `Bitstream`s. -/ | ||
| def BitStreamProd (arity : Type) : Type := arity → BitStream |
There was a problem hiding this comment.
| def BitStreamProd (arity : Type) : Type := arity → BitStream | |
| def BitStreams (arity : Nat) : Type := Fin arity → BitStream |
There was a problem hiding this comment.
Although I fully admit I'm being self-contradictory, given my previous crusade against semantically similar definitions having a <= 1 edit distance, somehow singular vs plural feels like a safe exception to that rule.
Otherwise, I'd be more comfortable even calling it a BitStreamVec(tor) --- although that is tempting confusion with BitVectors (aagh, why is naming so hard). In my mind, Prod means binary product, an n-ary product is a Vector
| def BitStreamProd.head (x : BitStreamProd arity) : BoolProd arity := | ||
| fun i => (x i).head | ||
|
|
||
| def BitStreamProd.tail (x : BitStreamProd arity) : BitStreamProd arity := | ||
| fun a => (x a).tail |
There was a problem hiding this comment.
These could use some docstring explicitly explaining you're doing head/tail on the constituent bitstreams! I was a bit confused by the arity being the same on both sides at first.
bollu
changed the title
…o fsm-abstractions
Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Siddharth <[email protected]>
…eMachine Co-authored-by: Siddharth <[email protected]>
|
Alive Statistics: 76 / 93 (17 failed) |
Let's not continue this
|
Alive Statistics: 76 / 93 (17 failed) |
Co-authored-by: Siddharth <[email protected]> Co-authored-by: Luisa Cicolini <[email protected]>
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
1 similar comment
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
| If the set of states R is closed under the inverse image of next state, | ||
| and if every state in the set R produces a true next output, | ||
| and furthermore, if our initial state is not R, | ||
| the the value at the initial state is zero, and furthermore, the state will not enter into R in the next state |
There was a problem hiding this comment.
| the the value at the initial state is zero, and furthermore, the state will not enter into R in the next state | |
| the value at the initial state is zero, and furthermore, the state will not enter into R in the next state |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
1 similar comment
|
Alive Statistics: 76 / 93 (17 failed) |
|
This has now been superseeded, I guess. |
No description provided.