FunTranslation
-
The First-Order LoopW Proof Checker translator into functional syntax.
The functional translator converts imperative programs into functional terms.
-
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.
|
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*.