TmTypeApply (TmValue (TypeAbstraction (TmValue (Abstraction (TmValue (Abstraction (TmApply (TmVariable...
can get a little difficult to debug
More symbolic representations can make reading and writing expressions much more intuitive
eg the whole statement from above written symbolically is just
(template ((t_ --> t_) /-> (t_v /-> (v_v <: v_))) <:: {Int})
Request:
At least conditional removal of the Show in deriving(Eq, Show), so that I may implement my own.
But perhaps further, adding an alias syntax to the grammar, and autogenerating Show implementations and Construction operators.
namespace VarValue: Term
sort Term
inh ctx VarValue
| TmVariable (x@ctx)
| TmApply (t1: Term) (t2: Term) as "t1 <=: t2"
| TmAbstraction (t: Term) [z: VarValue] as "z /-> t"
would generate
instance Show Term where
show (TmVariable v) = "TmVariable " ++ show v
show (TmApply t1 t2) = show t1 ++ " <=: " ++ show t2
show (TmAbstraction v t) = show v ++ " /-> " ++ show t
(/->) :: Variable -> Term -> Term
var /-> term = TmAbstraction var term
(<=:) :: Term -> Term -> Term
func <=: arg = TmApply func arg
TmTypeApply (TmValue (TypeAbstraction (TmValue (Abstraction (TmValue (Abstraction (TmApply (TmVariable...
can get a little difficult to debugMore symbolic representations can make reading and writing expressions much more intuitive eg the whole statement from above written symbolically is just
(template ((t_ --> t_) /-> (t_v /-> (v_v <: v_))) <:: {Int})
Request:
At least conditional removal of the Show in deriving(Eq, Show), so that I may implement my own.
But perhaps further, adding an alias syntax to the grammar, and autogenerating Show implementations and Construction operators.
would generate