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
}

然后，2 cent：

如果你要有 heavy search 的话，别像 coq/ACL2 这样傻傻的每次都重新 search，保存下来（所以 design 的时候要有 incrementality in mind）

提供一个好的 system for normalization，比如说会自动的 break /\ \/ exists（包括 forall 里面的/\，这Coq就很疼），然后用户可以自己 register 新的，比如说 perm ++ 的 split。这里有一些 subtle point，比如说顺序：你希望先执行生成 0subgoal 的，然后执行生成 1subgoal 的，然后 2subgoal……这也很难用户自己搞

programming by refinement 跟 property base testing/普通unit test 之间提供 native 融合，做到 assert 一个p roperty，subgoal 界面自动出现反例提示，或者 unit test 能证明。然后 higher order theorem 的 admit 可以用 contract。

Interactive 方法的改革也很好，比如说用计算机执行 N 个 Search，然后人类可以调节 focus 进那个 search，比 Coq 更 compact 的 subgoal representation（很多时候两个 subgoal 有一推一样的 hypothesis，这样用 sharing，能更好的同时表达两个 subgoal），外接 machine learning 的东西，并让用户手动写某种 extractor（extract 一个 goal 里面的某些属性，比如有多少 list concatenation，然后 feed 进 NN），说不定会有奇效。

最后，如果可以的话用 Haskell friendly language，这样我以后说不定能外接 DDF 上去

用个简单点的对普通语言也适用的例子说明为啥吧：Higher Order Unification不完备，所以如果语言支持sophisticated HOU，就会疼-天知道那天更改HOU算法，会不会破坏向后兼容性

不过，如果你保存下inferenced type，每次编译都事先去查找之（或者更漂亮，程序是binary文件），就完全不担心

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

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