module mini_cecil.

import maps mini_cecil_abstract_syntax algebra visibles.

%%%% the evalsto relation for expressions
type	evalsto	expression -> value -> o.

(evalsto (intLiteral N) (inInteger N)).

(evalsto true (inTruthValue tt)).

(evalsto false (inTruthValue ff)).

 ((mappred evalsto Exprs Vs),
  (evaluate_in_algebra algebraVIS MsgName Vs Ans))
=> % ---------------------------------
 (evalsto (msgExpr MsgName Exprs) Ans).