Overview  Index  Help 

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.

         
Type summary

type ident = ProofAst.ident
          identifiers as string (numeroted for alpha-conversion).

type typed_term = tterm * expType

 
Datatype summary

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.

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.

 
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.

   

 
Type detail

ident

type ident = ProofAst.ident

identifiers as string (numeroted for alpha-conversion).


typed_term

type typed_term = tterm * expType

 
Datatype detail

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.

 
DataConstructor detail

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

   


Overview  Index  Help