package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Smtml.RewriteSource

Module that performs two 'important' rewritings:

1. Replace symbols' Ty_none with the correct type specified in declare-const.

2. Propagate the correct theory encoding for Unop, Binop, Relop, and Triop.

3. Inlines Let_in binders into a single big expr

module Symb_map : sig ... end
Sourceval debug : ('a, Format.formatter, unit) format -> ('a -> unit) -> unit
Sourceval unify_types : Ty.t list -> Ty.t
Sourceval rewrite_ty : Ty.t -> Ty.t list -> Ty.t
Sourceval rewrite_expr : (Ty.t Symb_map.t * Expr.t Symb_map.t) -> Expr.t -> Expr.t

Propagates types in type_map and inlines Let_in binders

Sourceval rewrite_cmd : Ty.t Symb_map.t -> Ast.t -> Ty.t Symb_map.t * Ast.t

Acccumulates types of symbols in type_map and calls rewrite_expr

Sourceval rewrite : Ast.t list -> Ast.t list