gebn / expressioncompiler Goto Github PK

This can be done easily using aggressive pattern matching (resulting in lots of cases), but a more concise proof would be preferable.

Assigned to @RenuAB and @gcywong.

Assigned to @mikeyt103 and @sam066.

The -' and +' functions carry out the same functionality with a different operator. Given multiplication and division operations will require similar logic, it makes sense to abstract this out into a single function with a signature along the lines of ∀ {a} {A : Set a} → Maybe A → Maybe A → (A → A → A) → Maybe A, which takes two Maybe types along with an operator, and applies the operator if and only if both parameters are not nothing. It could be called like so:

maybeOp (⟦ E ⟧ σ) (⟦ E' ⟧ σ) _+_ -- for addition
maybeOp (⟦ E ⟧ σ) (⟦ E' ⟧ σ) _∸_ -- for subtraction

Assigned to @RenuAB and @gcywong.

It would be good to say exactly what we've done - new operators, proofs etc. in a little summary, and where they can be found - e.g. "Our proof for soundness can be found in Proofs.Soundness" - just to make marking that little bit easier.

Assigned to @RenuAB and @gcywong.

Assigned to @sam066 and @mikeyt103.