FunAst
-
The First-Order LoopW Proof Checker functional programs abstract syntax.
The functionnal abstract syntax is used to represent annotated functional programs, i.e. CND proofs.
-
DataConstructor summary
|
constructor Abs : (ident * expType) list * typed_term -> tterm
Abstraction: fn (x1 : f1, ..., xp : fp) => t.
|
constructor App : typed_term * ProofAst.term list * typed_term -> tterm
Application: (t[a1, ..., an] u) as universal instantiation.
|
constructor Callcc : ident * typed_term -> tterm
Catch operator: call/cc (fn k => t).
|
constructor Id : ident -> tterm
identifier.
|
constructor Lemma : expType list * expType -> tterm
Lemma: f1, ..., fn |- f
|
constructor LetIn : (ident * expType) list * typed_term * typed_term -> tterm
Let binding: let (x1 : f1 = u1, ..., xp : fp = up) in t (as existential elimination).
|
constructor Pred : typed_term -> tterm
Pred function.
|
constructor Rec : typed_term * typed_term * typed_term -> tterm
Primitive recursion: rec(t1, t2, t3).
|
constructor S : typed_term -> tterm
successor constructor.
|
constructor Subst : typed_term * expType * ident * typed_term -> tterm
Substitution: t {x/f[x]}[u : a = b]
|
constructor Succ : typed_term -> tterm
Succ function.
|
constructor TBot : expType
absurd: _|_.
|
constructor TEqual : ProofAst.term * ProofAst.term -> expType
equality predicate over terms: t = t'.
|
constructor TFun : ident list * expType * expType -> expType
functions: [i1, ..., in](f1 -> f2) corresponds to "forall i1...in.(f1 => f2)".
|
constructor Throw : typed_term * ProofAst.term list * typed_term -> tterm
Throw: throw t [a1, ..., an] u (with universal elimination).
|
constructor TNat : ProofAst.term -> expType
nat predicate: nat(t) corresponds to "t in nat".
|
constructor TTuple : ident list * expType list -> expType
tuples: [i1, ..., in](f1, ..., fm) corresponds to "exists i1...in.(f1 & ...
|
constructor Tuple : ProofAst.term list * typed_term list -> tterm
term tuples: [a1, ..., an](t1, ..., tm) (as existential introduction).
|
constructor TVar : ident -> expType
type variables
|
constructor Z : tterm
zero.
|
ident
type ident = ProofAst.ident
-
identifiers as string (numeroted for alpha-conversion).
-
typed_term
type typed_term = tterm * expType
expType
datatype expType =
TBot
| TNat of ProofAst.term
| TEqual of ProofAst.term * ProofAst.term
| TTuple of ident list * expType list
| TFun of ident list * expType * expType
| TVar of ident
-
first-order formulas.
-
tterm
datatype tterm =
Id of ident
| Tuple of ProofAst.term list * typed_term list
| Z
| S of typed_term
| Succ of typed_term
| Pred of typed_term
| App of typed_term * ProofAst.term list * typed_term
| Abs of (ident * expType) list * typed_term
| Rec of typed_term * typed_term * typed_term
| LetIn of (ident * expType) list * typed_term * typed_term
| Callcc of ident * typed_term
| Throw of typed_term * ProofAst.term list * typed_term
| Subst of typed_term * expType * ident * typed_term
| Lemma of expType list * expType
-
functional terms.
-
TBot
constructor TBot : expType
-
absurd: _|_.
-
TNat
constructor TNat : ProofAst.term -> expType
-
nat predicate: nat(t) corresponds to "t in nat".
-
TEqual
constructor TEqual : ProofAst.term * ProofAst.term -> expType
-
equality predicate over terms: t = t'.
-
TTuple
constructor TTuple : ident list * expType list -> expType
-
tuples: [i1, ..., in](f1, ..., fm) corresponds to "exists i1...in.(f1 & ... & fn)".
-
TFun
constructor TFun : ident list * expType * expType -> expType
-
functions: [i1, ..., in](f1 -> f2) corresponds to "forall i1...in.(f1 => f2)".
-
TVar
constructor TVar : ident -> expType
-
type variables
-
Id
constructor Id : ident -> tterm
-
identifier.
-
Tuple
constructor Tuple : ProofAst.term list * typed_term list -> tterm
-
term tuples: [a1, ..., an](t1, ..., tm) (as existential introduction).
-
Z
constructor Z : tterm
-
zero.
-
S
constructor S : typed_term -> tterm
-
successor constructor.
-
Succ
constructor Succ : typed_term -> tterm
-
Succ function.
-
Pred
constructor Pred : typed_term -> tterm
-
Pred function.
-
App
constructor App : typed_term * ProofAst.term list * typed_term -> tterm
-
Application: (t[a1, ..., an] u) as universal instantiation.
-
Abs
constructor Abs : (ident * expType) list * typed_term -> tterm
-
Abstraction: fn (x1 : f1, ..., xp : fp) => t.
-
Rec
constructor Rec : typed_term * typed_term * typed_term -> tterm
-
Primitive recursion: rec(t1, t2, t3).
-
LetIn
constructor LetIn : (ident * expType) list * typed_term * typed_term -> tterm
-
Let binding: let (x1 : f1 = u1, ..., xp : fp = up) in t (as existential elimination).
-
Callcc
constructor Callcc : ident * typed_term -> tterm
-
Catch operator: call/cc (fn k => t).
-
Throw
constructor Throw : typed_term * ProofAst.term list * typed_term -> tterm
-
Throw: throw t [a1, ..., an] u (with universal elimination).
-
Subst
constructor Subst : typed_term * expType * ident * typed_term -> tterm
-
Substitution: t {x/f[x]}[u : a = b]
-
Lemma
constructor Lemma : expType list * expType -> tterm
-
Lemma: f1, ..., fn |- f
-