Overview  Index  Help 

FunTranslation


The First-Order LoopW Proof Checker translator into functional syntax. The functional translator converts imperative programs into functional terms.

Opened structures

ProofAst

ProofAstUtils

               
Value summary

val mkTuple
           builds a typed singleton tuple from a term and a type.

val omega2tuple
           translates an imperative sequence type into a function tuple type.

val order
           orders an environment according to a given variable list.

val orderSubst
           orders a substitution according to a given variable list.

val translateExpression
           translate an imperative expression into a functional typed term.

val translateProgram : ProofAst.sequence -> FunAst.typed_term
           translate a complete imperative program into a functional typed term.

val translateSequence
           translate an imperative sequence into a functional typed term.

val translateType
           translates imperative types into functional types.

val translateValue
           translate an imperative value into a functional typed term.

 

       
Value detail

mkTuple

fun mkTuple tterm typ

builds a typed singleton tuple from a term and a type.

Parameters:
tterm
the term.
typ
the type.
Returns:
the tuple (tterm):(typ).

order

fun order xl omega

orders an environment according to a given variable list.

Parameters:
xl
the variable list [x1, ..., xn].
omega
the environment [xi:ti]*.
Returns:
the ordered environment [x1:t1, ..., xn:tn].
Exception:
Fail
if length mismatch.

orderSubst

fun orderSubst xl subst

orders a substitution according to a given variable list.

Parameters:
xl
the variable list [x1, ..., xn].
subst
the substitution [xi <- ti]*.
Returns:
the ordered substitution [x1 <- t1, ..., xn <- tn].
Exception:
Fail
if length mismatch.

translateType

fun translateType t

translates imperative types into functional types.

Parameters:
t
the imperative type.
Returns:
the functional type t*.

omega2tuple

fun omega2tuple (j, om)

translates an imperative sequence type into a function tuple type.

Parameters:
j
the identifier list of existential quantification.
om
the formula list.
Returns:
the functional type Exist j.om* (TTuple (j, om* )).

translateValue

fun translateValue (v, tau)

translate an imperative value into a functional typed term.

Parameters:
v
the imperative value.
tau
the type of v.
Returns:
the functional term v*.

translateExpression

fun translateExpression (e, tau)

translate an imperative expression into a functional typed term.

Parameters:
e
the imperative expression.
tau
the type of e.
Returns:
the functional term e*.

translateSequence

fun translateSequence (seq, (j, omega)) z

translate an imperative sequence into a functional typed term.

Parameters:
seq
the imperative sequence.
j
the identifier list of existential quantification.
omega
the existentialy quantified formula list typing seq.
z
the output variable vector.
Returns:
the functional term (s)*_z.

translateProgram

fun translateProgram p : ProofAst.sequence -> FunAst.typed_term

translate a complete imperative program into a functional typed term.

Parameters:
p
the imperative program.
Returns:
the functional term p*.

 


Overview  Index  Help