PROPOSAL -- TT syntax

gistfile1.txt

-- Totalscript syntax
Module -> Imports (Access? Declaration | Access Name | Access? OperatorDecl | Definition | Mutual)*
Access -> ("public" | "private") ("definition" | "function" | "lemma" | "theorem")?
Program -> (Declaration | Definition | Mutual)*

Imports -> Import*
Import  -> "import" Name* "from" String

OperatorDecl -> "operator" Operator NumberLiteral ("left" | "right" | "none") "=" Access

DeclBlock    -> "{" Declaration* "}"
DefBlock     -> "{" Definition* "}"
ProgramBlock -> "{" Program "}"

Declaration -> SimpleDecl | InductiveDecl | InterfaceDecl | InstanceDecl | Coercion
SimpleDecl  -> Name ":" Term
Param       -> Name | "(" SimpleDecl ")"
InductiveDecl -> "inductive" SimpleDecl "where" DeclBlock
InterfaceDecl -> "interface" SimpleDecl Param+ "where" ProgramBlock
InstanceDecl  -> "instance" (Name ":")? Term "where" ProgramBlock
Coercion      -> "implicit" SimpleDecl

Definition -> (SimpleDef | ViewDef) ("where" ProgramBlock)?
SimpleDef  -> Name Pattern* "=" Term
ViewDef    -> Name Pattern* "with" Term+ DefBlock

Term       -> If | Case | Expr1
If         -> "if" Term "then" Term "else" Term
Case       -> "case" Term "of" "{" (Pattern "->" Term)* "}"
Expr1      -> Expr
            | Param "->" Expr1                  # Pi
            | Expr "|" Expr1                    # Interface Pi
            | "(" SimpleDecl ("&" Expr1)+ ")"  # Sigma
            | Expr "<|" Expr1                   # Low-priority call
            | Expr1 "|>" Expr                   # Low-priority call, RTL
Expr       -> Factor | Expr InfixL Factor | Factor InfixR Factor
Factor     -> Primitive | Factor Primitive
Primitive  -> Access | Literal | Do | Tactic | "(" Term ")" | "[" Term* "]"

Access     -> Name | Access "." Name
Do         -> "do" "{" (Pattern "<-" Term | Term)* "}"
Tactic     -> ("tactic" | "proof") "{" (Pattern "<-" Term | Term)* "}"

Pattern    -> Name | Name Pattern* | "(" Pattern ")" | "(" Name "|" Pattern ")"

Name       -> ......
Literal    -> ......

sample.tt

inductive Tree : Type -> Type where {
    Leaf : a -> Tree a
    Branch : a -> Tree a -> Tree a -> Tree a
}

public instance Eq a | Eq (Tree a) where {
    equal (Leaf a) (Leaf b) = equal a b
    equal (Branch x1 l1 r1) (Branch x2 l2 r2) = (equal x1 x2) && (equal l1 l2) && (equal r1 r2)
    equal p q = false
}

operator (@) 500 right = map
interface Functor (f : Type -> Type) where {
    map : (a -> b) -> f a -> f b
}

public instance (Functor Tree) where {
    map f (Leaf a) = Leaf (f a)
    map f (Branch x l r) = Branch (f x) (map f l) (map f r)
}

public flipTree : Tree a -> Tree a
flipTree (x | Leaf a) = x
flipTree (Branch x l r) = Branch x (flipTree r) (flipTree l)

theorem flipTreeSym (t : Tree a) -> t === (flipTree <| flipTree a)
flipTreeSym = proof {
    a <- intro
    t <- intro
    induct t
    refl
    rewrite ind_Branch_l
    rewrite ind_Branch_r
    refl
}

我的重点是 design 的时候就要考虑这些东西，到后期搞成插件为时已晚（当然，除非你做得很 flexible 啥都可以替换，但是既然这样为啥不直接写进去）

自举听上去很帅，不过要小心 non-termination，不知道你打算怎么避免 PFPL SystemT*Eval 出现的对角线？