https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecMatching.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 EcMaps
open EcUid
open EcParsetree
open EcIdent
open EcTypes
open EcModules
open EcFol
open EcUnify
open EcEnv
open EcGenRegexp
(* -------------------------------------------------------------------- *)
module Zipper : sig
type ipath =
| ZTop
| ZWhile of expr * spath
| ZIfThen of expr * spath * stmt
| ZIfElse of expr * stmt * spath
and spath = (instr list * instr list) * ipath
type zipper = {
z_head : instr list; (* instructions on my left (rev) *)
z_tail : instr list; (* instructions on my right (me incl.) *)
z_path : ipath ; (* path (zipper) leading to me *)
}
exception InvalidCPos
(* Create a codepos1 from a top-level absolute position *)
val cpos : int -> codepos1
(* Split a statement from a top-level position (codepos1) *)
val find_by_cpos1 : ?rev:bool -> codepos1 -> stmt -> instr list * instr * instr list
val split_at_cpos1 : codepos1 -> stmt -> instr list * instr list
(* Split a statement from an optional top-level position (codepos1) *)
val may_split_at_cpos1 : ?rev:bool -> codepos1 option -> stmt -> instr list * instr list
(* [zipper] soft constructor *)
val zipper : instr list -> instr list -> ipath -> zipper
(* Return the zipper for the stmt [stmt] at code position [codepos].
* Raise [InvalidCPos] if [codepos] is not valid for [stmt]. *)
val zipper_of_cpos : codepos -> stmt -> zipper
(* Zip the zipper, returning the corresponding statement *)
val zip : zipper -> stmt
(* [after ~strict zpr] returns all the statements that come after the
* zipper cursor. They are returned as a list of statements, where the head
* is the list of instructions coming directly after the cursor at the
* same level, the next element is the ones coming after the cursor
* parent block, and so forth. The cursor is included iff [strict] is [true].
*)
val after : strict:bool -> zipper -> instr list list
type ('a, 'state) folder = 'a -> 'state -> instr -> 'state * instr list
(* [fold cl cpos f state s] create the zipper for [s] at [cpos], and apply
* [f] to it, along with [v] and the state [state]. [f] must return the
* new [state] and a new [zipper]. These last are directly returned.
*
* Raise [InvalidCPos] if [cpos] is not valid for [s], or any exception
* raised by [f].
*)
val fold : 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
end
(* -------------------------------------------------------------------- *)
(* Formulas rigid unification *)
(* -------------------------------------------------------------------- *)
type 'a evmap
module EV : sig
val empty : 'a evmap
val of_idents : ident list -> 'a evmap
val add : ident -> 'a evmap -> 'a evmap
val mem : ident -> 'a evmap -> bool
val isset : ident -> 'a evmap -> bool
val set : ident -> 'a -> 'a evmap -> 'a evmap
val get : ident -> 'a evmap -> [`Unset | `Set of 'a] option
val doget : ident -> 'a evmap -> 'a
val fold : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b
val filled : 'a evmap -> bool
end
(* -------------------------------------------------------------------- *)
type mevmap = {
evm_form : form evmap;
evm_mem : EcMemory.memory evmap;
evm_mod : EcPath.mpath evmap;
}
(* -------------------------------------------------------------------- *)
module MEV : sig
type item = [
| `Form of form
| `Mem of EcMemory.memory
| `Mod of EcPath.mpath
]
type kind = [ `Form | `Mem | `Mod ]
val empty : mevmap
val of_idents : ident list -> kind -> mevmap
val add : ident -> kind -> mevmap -> mevmap
val mem : ident -> kind -> mevmap -> bool
val isset : ident -> kind -> mevmap -> bool
val set : ident -> item -> mevmap -> mevmap
val get : ident -> kind -> mevmap -> [`Unset | `Set of item] option
val filled : mevmap -> bool
val fold : (ident -> item -> 'a -> 'a) -> mevmap -> 'a -> 'a
val assubst: EcUnify.unienv -> mevmap -> EcFol.f_subst
end
(* -------------------------------------------------------------------- *)
exception MatchFailure
type fmoptions = {
fm_delta : bool;
fm_conv : bool;
fm_horder : bool;
}
val fmsearch : fmoptions
val fmrigid : fmoptions
val fmdelta : fmoptions
val fmnotation : fmoptions
val f_match_core :
fmoptions
-> EcEnv.LDecl.hyps
-> unienv * mevmap
-> ptn:form
-> form
-> unienv * mevmap
val f_match :
fmoptions
-> EcEnv.LDecl.hyps
-> unienv * mevmap
-> ptn:form
-> form
-> unienv * (uid -> ty option) * mevmap
(* -------------------------------------------------------------------- *)
type ptnpos = private [`Select of int | `Sub of ptnpos] Mint.t
type occ = [`Inclusive | `Exclusive] * Sint.t
exception InvalidPosition
exception InvalidOccurence
module FPosition : sig
type select = [`Accept of int | `Continue]
val empty : ptnpos
val is_empty : ptnpos -> bool
val tostring : ptnpos -> string
val select : ?o:occ -> (Sid.t -> form -> select) -> form -> ptnpos
val select_form : ?xconv:EcReduction.xconv ->
LDecl.hyps -> occ option -> form -> form -> ptnpos
val is_occurences_valid : Sint.t -> ptnpos -> bool
val occurences : ptnpos -> int
val filter : occ -> ptnpos -> ptnpos
val map : ptnpos -> (form -> form) -> form -> form
val topattern : ?x:EcIdent.t -> ptnpos -> form -> EcIdent.t * form
end
(* -------------------------------------------------------------------- *)
type cptenv = CPTEnv of f_subst
val can_concretize : mevmap -> EcUnify.unienv -> bool
(* -------------------------------------------------------------------------- *)
type regexp_instr = regexp1_instr gen_regexp
and regexp1_instr =
| RAssign
| RSample
| RCall
| RIf of regexp_instr * regexp_instr
| RWhile of regexp_instr
module RegexpStmt : sig
type regexp = regexp_instr
type subject = instr list
type matches = subject Mstr.t
val search : regexp -> subject -> matches option
end