Module Wp.ReprSource

High-Level Term Representation

Term & Predicate Introspection

Sourcetype tau = Lang.F.tau
Sourcetype var = Lang.F.var
Sourcetype field = Lang.field
Sourcetype lfun = Lang.lfun
Sourcetype term = Lang.F.term
Sourcetype pred = Lang.F.pred
Sourcetype repr =
  1. | True
  2. | False
  3. | And of term list
  4. | Or of term list
  5. | Not of term
  6. | Imply of term list * term
  7. | If of term * term * term
  8. | Var of var
  9. | Int of Z.t
  10. | Real of Q.t
  11. | Add of term list
  12. | Mul of term list
  13. | Div of term * term
  14. | Mod of term * term
  15. | Eq of term * term
  16. | Neq of term * term
  17. | Lt of term * term
  18. | Leq of term * term
  19. | Times of Z.t * term
  20. | Call of lfun * term list
  21. | Field of term * field
  22. | Record of (field * term) list
  23. | Cst of tau * term
  24. | Get of term * term
  25. | Set of term * term * term
  26. | HigherOrder
    (*

    See Lang.F.e_open and Lang.F.e_close

    *)
Sourceval term : term -> repr
Sourceval pred : pred -> repr
Sourceval lfun : lfun -> string
Sourceval field : field -> string