Revision 4388214acf75d0162f5a29c2c42230f44f6c8187 authored by Pierre-Yves Strub on 12 December 2015, 19:59:46 UTC, committed by Pierre-Yves Strub on 12 December 2015, 20:03:33 UTC
Syntax is `[~*]`. The full syntax of this i-p is now: `move=> [int?~?/?*]`
1 parent c09a98a
ecPrinting.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcIdent
open EcSymbols
open EcPath
open EcTypes
open EcFol
open EcDecl
open EcModules
open EcTheory
(* -------------------------------------------------------------------- *)
module PPEnv : sig
type t
val ofenv : EcEnv.env -> t
val add_locals : ?force:bool -> t -> EcIdent.t list -> t
end
(* -------------------------------------------------------------------- *)
type 'a pp = Format.formatter -> 'a -> unit
val pp_id : 'a pp -> 'a pp
val pp_if : bool -> 'a pp -> 'a pp -> 'a pp
val pp_maybe : bool -> ('a pp -> 'a pp) -> 'a pp -> 'a pp
val pp_enclose:
pre:('a, 'b, 'c, 'd, 'd, 'a) format6
-> post:('a, 'b, 'c, 'd, 'd, 'a) format6
-> 'a pp -> 'a pp
val pp_paren : 'a pp -> 'a pp
val pp_list : ('a, 'b, 'c, 'd, 'd, 'a) format6 -> 'a pp -> 'a list pp
(* -------------------------------------------------------------------- *)
val pp_pv : PPEnv.t -> prog_var pp
val pp_local : ?fv:Sid.t -> PPEnv.t -> ident pp
val pp_opname : PPEnv.t -> path pp
val pp_funname : PPEnv.t -> xpath pp
val pp_topmod : PPEnv.t -> mpath pp
val pp_form : PPEnv.t -> form pp
val pp_type : PPEnv.t -> ty pp
val pp_tyname : PPEnv.t -> path pp
val pp_mem : PPEnv.t -> EcIdent.t pp
val pp_tyvar : PPEnv.t -> ident pp
val pp_tyunivar : PPEnv.t -> EcUid.uid pp
val pp_path : path pp
(* -------------------------------------------------------------------- *)
val pp_typedecl : PPEnv.t -> (path * tydecl ) pp
val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator) pp
val pp_added_op : PPEnv.t -> operator pp
val pp_axiom : ?long:bool -> PPEnv.t -> (path * axiom ) pp
val pp_theory : PPEnv.t -> (path * (ctheory * thmode) ) pp
val pp_modtype : PPEnv.t -> (module_type * mod_restr ) pp
val pp_modexp : PPEnv.t -> (mpath * module_expr ) pp
val pp_modsig : PPEnv.t -> (path * module_sig ) pp
(* -------------------------------------------------------------------- *)
val pp_hoareS : PPEnv.t -> hoareS pp
val pp_bdhoareS : PPEnv.t -> bdHoareS pp
val pp_equivS : PPEnv.t -> equivS pp
val pp_stmt : PPEnv.t -> stmt pp
val pp_instr : PPEnv.t -> instr pp
(* -------------------------------------------------------------------- *)
type ppgoal = (EcBaseLogic.hyps * EcFol.form) * [
| `One of int
| `All of (EcBaseLogic.hyps * EcFol.form) list
]
val pp_goal : PPEnv.t -> ppgoal pp
(* -------------------------------------------------------------------- *)
module ObjectInfo : sig
val pr_ty : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_op : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_th : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_ax : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_mod : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_mty : Format.formatter -> EcEnv.env -> qsymbol -> unit
val pr_any : Format.formatter -> EcEnv.env -> qsymbol -> unit
end
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...