cv_trans_deep_embedding

cv_transLib.cv_trans_deep_embedding : conv -> thm -> unit

Translates equations defining a deeply embedded AST to the cv_compute subset of HOL.

This function is similar to cv_transLib.cv_trans, but can only translate constants. It is designed for the translation of large deep embeddings to :cv functions. It takes as an argument a conversion which must evaluate terms such as from <deep_embedding> (e.g. computeLib.EVAL).

Failure

When the input term is not a constant defining a suitable deep embedding.

Example

> Datatype:
   exp = Const num | Add exp exp
  End
> Definition sem_def:
   sem (Const n) = n ∧
   sem (Add e1 e2) = sem e1 + sem e2
  End
val sem_def =
   ⊢ (∀n. sem (Const n) = n) ∧ ∀e1 e2. sem (Add e1 e2) = sem e1 + sem e2: thm
> Definition deep_def:
   deep = Add (Const 5) (Add (Const 2) (Const 3))
  End
val deep_def = ⊢ deep = Add (Const 5) (Add (Const 2) (Const 3)): thm
> cv_transLib.cv_trans sem_def;
Finished translating sem, stored in cv_sem_thm
val it = (): unit
> cv_transLib.cv_trans_deep_embedding EVAL deep_def;
val it = (): unit
> cv_transLib.cv_eval “sem deep”;
val it = ⊢ sem deep = 10: thm

Comments

Designed to produce definitions suitable for evaluation by cv_transLib.cv_eval.

See also

cv_transLib.cv_trans, cv_transLib.cv_eval