https://github.com/EasyCrypt/easycrypt
Revision ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC, committed by Pierre-Yves Strub on 12 June 2018, 05:34:41 UTC
The tactic statically unroll while loops of the form
x <- int-constant
while (guard) {
body (does not write x);
x <- f(x);
}
where "guard" and "f" can be statically evaluated at each
iteration. The code is then replaced by the while loop
fully unrolled.
The tactic does not terminate if the unrolling leads to
a infinite process.
1 parent 43fd7aa
Tip revision: ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC
New tactic for static unrolling of "for-loops"
New tactic for static unrolling of "for-loops"
Tip revision: ba545a9
ecSubst.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcIdent
open EcPath
open EcModules
open EcTypes
open EcTheory
open EcDecl
open EcCoreFol
(* -------------------------------------------------------------------- *)
type subst_name_clash = [
| `Ident of EcIdent.t
]
exception SubstNameClash of subst_name_clash
exception InconsistentSubst
(* -------------------------------------------------------------------- *)
type subst
val empty : subst
val is_empty : subst -> bool
(* -------------------------------------------------------------------- *)
val add_module : subst -> EcIdent.t -> mpath -> subst
val add_path : subst -> src:path -> dst:path -> subst
val add_tydef : subst -> path -> (EcIdent.t list * ty) -> subst
val add_opdef : subst -> path -> (EcIdent.t list * expr) -> subst
val add_pddef : subst -> path -> (EcIdent.t list * form) -> subst
(* -------------------------------------------------------------------- *)
val freshen_type : (ty_params * ty) -> (ty_params * ty)
(* -------------------------------------------------------------------- *)
val subst_theory : subst -> theory -> theory
val subst_ax : subst -> axiom -> axiom
val subst_op : subst -> operator -> operator
val subst_tydecl : subst -> tydecl -> tydecl
val subst_tc : subst -> typeclass -> typeclass
val subst_ctheory : subst -> ctheory -> ctheory
(* -------------------------------------------------------------------- *)
val subst_path : subst -> path -> path
val subst_mpath : subst -> mpath -> mpath
val subst_function : subst -> function_ -> function_
val subst_module : subst -> module_expr -> module_expr
val subst_module_comps : subst -> module_comps -> module_comps
val subst_modtype : subst -> module_type -> module_type
val subst_modsig : ?params:(ident list) -> subst -> module_sig -> module_sig
val subst_modsig_body : subst -> module_sig_body -> module_sig_body
(* -------------------------------------------------------------------- *)
val subst_genty : subst -> (ty_params * ty) -> (ty_params * ty)
val subst_ty : subst -> ty -> ty
val subst_form : subst -> form -> form
Computing file changes ...
