Overview  Index  Help 

ProofAst


The First-Order LoopW Proof Checker proof abstract syntax. The proof abstract syntax is used to represent annotated LoopW programs, i.e. iCND proofs.

Opened structures

Error

         
Type summary

type block =
     (i_sequence * (ident list * (ident * formula) list)) *
     (ident list * (ident * formula) list)

          blocks { s |> {i'}x':tau' }{i}x:tau.

type expression = i_expression * formula
          typed expressions e : tau.

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

type program = sequence
          programs

type sequence = i_sequence * (ident list * (ident * formula) list)
          typed sequences s |> {i}x:tau.

type value = i_value * formula
          typed values v : tau.

 
Datatype summary

datatype command =
         Block of block
       | For of ident * ident * expression * formula * block
       | Affect of ident * formula * expression
       | Inc of ident * formula
       | Dec of ident * formula
       | ProcCall of
         
         expression *
         formula *
          (expression * formula) list *
          (ident * term) list *
          (ident * formula) list
       | Label of ident * formula * block
       | Jump of
         
         expression *
         formula *
         (expression * formula) list *
         (ident * term) list *
         (ident * formula) list
       | CommRegion of command * region

          commands.

datatype formula =
         TNat of term
       | TProc of ident list * formula list * ident list * formula list
       | TEqual of term * term
       | TBot
       | TVar of ident

          first-order formulas.

datatype i_expression =
         Id of ident
       | Val of value
       | ESubst of  expression *  formula *  ident *  expression * formula
       | Lemma of formula list * formula
       | ExpRegion of i_expression * region

          untyped expressions.

datatype i_sequence =
         Empty of (ident * term) list
       | Comm of command * sequence
       | Cst of ident * formula * expression * sequence
       | Var of ident * formula * expression * sequence
       | SSubst of
          sequence *  (ident * formula) list *  ident *  expression * formula
       | SeqRegion of i_sequence * region

          untyped sequences.

datatype i_value =
         Star
       | Int of int
       | Proc of
         
         ident list *
         (ident * formula) list *
          ident list *
         (ident * formula) list *
          block
       | ValRegion of i_value * region

          untyped values.

datatype term = FId of ident | FZero | FFun of ident * term list
          terms in the logic.

 
DataConstructor summary

constructor Affect : ident * formula * expression -> command
          assignment: x : tau := e.

constructor Block : block -> command
          block: { s }{i}x:tau

constructor Comm : command * sequence -> i_sequence
          composed command: c; s.

constructor CommRegion : command * region -> command

constructor Cst : ident * formula * expression * sequence -> i_sequence
          constant declaration: cst x : tau = e; s.

constructor Dec : ident * formula -> command
          decrementation: dec(x : tau).

constructor Empty : (ident * term) list -> i_sequence
          empty sequence : [n/j] "substitution used for existential introduction".

constructor ESubst
            :  expression *  formula *  ident *  expression * formula ->
                i_expression

          expression substitution: e :> {i/tau[i]} [e' : (n = m)].

constructor ExpRegion : i_expression * region -> i_expression

constructor FFun : ident * term list -> term
          n-ary function (s and p will be instances of this): f(tl)

constructor FId : ident -> term
          identifier.

constructor For : ident * ident * expression * formula * block -> command
          for-loop: for I : nat(i) := e : tau { s }{j}x:tau[i].

constructor FZero : term
          zero: Z

constructor Id : ident -> i_expression
          identifier.

constructor Inc : ident * formula -> command
          incrementation: inc(x : tau).

constructor Int : int -> i_value
          natural number: n.

constructor Jump
            : 
              expression *
              formula *
              (expression * formula) list *
              (ident * term) list *
              (ident * formula) list ->
                command

          jump to a label: jump(k : ~tau [subst], etl)x:tau.

constructor Label : ident * formula * block -> command
          label definition: k : {i}~tau :{ s }{i}x:tau.

constructor Lemma : formula list * formula -> i_expression
          lemma (equation over term in a context): G |- n = m.

constructor Proc
            : 
              ident list *
              (ident * formula) list *
               ident list *
              (ident * formula) list *
               block ->
                i_value

          anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.

constructor ProcCall
            : 
              expression *
              formula *
               (expression * formula) list *
               (ident * term) list *
               (ident * formula) list ->
                command

          procedure call: p:tau(etl [subst], itl).

constructor SeqRegion : i_sequence * region -> i_sequence

constructor SSubst
            : 
              sequence *
               (ident * formula) list *
               ident *
               expression *
              formula ->
                i_sequence

          sequence substitution: s :> {i/({j}Omega)[i]} [e : (n = m)].

constructor Star : i_value
          null value: *.

constructor TBot : formula
          absurd: _|_.

constructor TEqual : term * term -> formula
          equality predicate over terms: t = t'.

constructor TNat : term -> formula
          nat predicate: nat(t) corresponds to "t in nat".

constructor TProc
            : ident list * formula list * ident list * formula list -> formula

          procedures: proc(il, fl, jl, hl) corresponds to "forall il.(fl => exists jl.hl)".

constructor TVar : ident -> formula
          formula meta-variable (only used in input programs).

constructor Val : value -> i_expression
          value.

constructor ValRegion : i_value * region -> i_value

constructor Var : ident * formula * expression * sequence -> i_sequence
          variable declaration: var x : tau := e; s.

   

 
Type detail

ident

type ident = string * int

identifiers as string (numeroted for alpha-conversion).


sequence

type sequence = i_sequence * (ident list * (ident * formula) list)

typed sequences s |> {i}x:tau.


expression

type expression = i_expression * formula

typed expressions e : tau.


value

type value = i_value * formula

typed values v : tau.


block

type block =
     (i_sequence * (ident list * (ident * formula) list)) *
     (ident list * (ident * formula) list)

blocks { s |> {i'}x':tau' }{i}x:tau.


program

type program = sequence

programs

 
Datatype detail

term

datatype term = FId of ident | FZero | FFun of ident * term list

terms in the logic.


formula

datatype formula =
         TNat of term
       | TProc of ident list * formula list * ident list * formula list
       | TEqual of term * term
       | TBot
       | TVar of ident

first-order formulas.


command

datatype command =
         Block of block
       | For of ident * ident * expression * formula * block
       | Affect of ident * formula * expression
       | Inc of ident * formula
       | Dec of ident * formula
       | ProcCall of
         (* p : proc(tau[i], sig) *)
         expression *
         formula *
         (* (e1 : tau1[u], ..., en : taun[u]; *) (expression * formula) list *
         (* [u/i] *) (ident * term) list *
         (* r1 : sig1, ..., rp : sigp) *) (ident * formula) list
       | Label of ident * formula * block
       | Jump of
         (* k : ~tau *)
         expression *
         formula *
         (expression * formula) list *
         (ident * term) list *
         (ident * formula) list
       | CommRegion of command * region

commands.


i_sequence

datatype i_sequence =
         Empty of (ident * term) list
       | Comm of command * sequence
       | Cst of ident * formula * expression * sequence
       | Var of ident * formula * expression * sequence
       | SSubst of
         (* s *)
         sequence *
         (* ({j}Omega)[i] *) (ident * formula) list *
         (* i *) ident *
         (* e : (n = m) *) expression *
         formula
       | SeqRegion of i_sequence * region

untyped sequences.


i_expression

datatype i_expression =
         Id of ident
       | Val of value
       | ESubst of
         (* e *)
         expression *
         (* tau[i] *) formula *
         (* i *) ident *
         (* e' : (n = m) *) expression *
         formula
       | Lemma of formula list * formula
       | ExpRegion of i_expression * region

untyped expressions.


i_value

datatype i_value =
         Star
       | Int of int
       | Proc of
         (* {il} in x:fl *)
         ident list *
         (ident * formula) list *
         (* {jl} out y:fl' *) ident list *
         (ident * formula) list *
         (* { s }{jl}yfl *) block
       | ValRegion of i_value * region

untyped values.

 
DataConstructor detail

FId

constructor FId : ident -> term

identifier.


FZero

constructor FZero : term

zero: Z


FFun

constructor FFun : ident * term list -> term

n-ary function (s and p will be instances of this): f(tl)


TNat

constructor TNat : term -> formula

nat predicate: nat(t) corresponds to "t in nat".


TProc

constructor TProc
            : ident list * formula list * ident list * formula list -> formula

procedures: proc(il, fl, jl, hl) corresponds to "forall il.(fl => exists jl.hl)".


TEqual

constructor TEqual : term * term -> formula

equality predicate over terms: t = t'.


TBot

constructor TBot : formula

absurd: _|_.


TVar

constructor TVar : ident -> formula

formula meta-variable (only used in input programs).


Block

constructor Block : block -> command

block: { s }{i}x:tau


For

constructor For : ident * ident * expression * formula * block -> command

for-loop: for I : nat(i) := e : tau { s }{j}x:tau[i].


Affect

constructor Affect : ident * formula * expression -> command

assignment: x : tau := e.


Inc

constructor Inc : ident * formula -> command

incrementation: inc(x : tau).


Dec

constructor Dec : ident * formula -> command

decrementation: dec(x : tau).


ProcCall

constructor ProcCall
            : (* p : proc(tau[i], sig) *)
              expression *
              formula *
              (* (e1 : tau1[u], ..., en : taun[u]; *) (expression * formula) list *
              (* [u/i] *) (ident * term) list *
              (* r1 : sig1, ..., rp : sigp) *) (ident * formula) list ->
                command

procedure call: p:tau(etl [subst], itl).


Label

constructor Label : ident * formula * block -> command

label definition: k : {i}~tau :{ s }{i}x:tau.


Jump

constructor Jump
            : (* k : ~tau *)
              expression *
              formula *
              (expression * formula) list *
              (ident * term) list *
              (ident * formula) list ->
                command

jump to a label: jump(k : ~tau [subst], etl)x:tau.


CommRegion

constructor CommRegion : command * region -> command


Empty

constructor Empty : (ident * term) list -> i_sequence

empty sequence : [n/j] "substitution used for existential introduction".


Comm

constructor Comm : command * sequence -> i_sequence

composed command: c; s.


Cst

constructor Cst : ident * formula * expression * sequence -> i_sequence

constant declaration: cst x : tau = e; s.


Var

constructor Var : ident * formula * expression * sequence -> i_sequence

variable declaration: var x : tau := e; s.


SSubst

constructor SSubst
            : (* s *)
              sequence *
              (* ({j}Omega)[i] *) (ident * formula) list *
              (* i *) ident *
              (* e : (n = m) *) expression *
              formula ->
                i_sequence

sequence substitution: s :> {i/({j}Omega)[i]} [e : (n = m)].


SeqRegion

constructor SeqRegion : i_sequence * region -> i_sequence


Id

constructor Id : ident -> i_expression

identifier.


Val

constructor Val : value -> i_expression

value.


ESubst

constructor ESubst
            : (* e *)
              expression *
              (* tau[i] *) formula *
              (* i *) ident *
              (* e' : (n = m) *) expression *
              formula ->
                i_expression

expression substitution: e :> {i/tau[i]} [e' : (n = m)].


Lemma

constructor Lemma : formula list * formula -> i_expression

lemma (equation over term in a context): G |- n = m.


ExpRegion

constructor ExpRegion : i_expression * region -> i_expression


Star

constructor Star : i_value

null value: *.


Int

constructor Int : int -> i_value

natural number: n.


Proc

constructor Proc
            : (* {il} in x:fl *)
              ident list *
              (ident * formula) list *
              (* {jl} out y:fl' *) ident list *
              (ident * formula) list *
              (* { s }{jl}yfl *) block ->
                i_value

anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.


ValRegion

constructor ValRegion : i_value * region -> i_value

   


Overview  Index  Help