https://github.com/EasyCrypt/easycrypt
Tip revision: 0dd57f714852f6f779d230c5bbf3e98e4594f41f authored by François Dupressoir on 06 December 2019, 09:55:55 UTC
OneMap-PRP: a PRP with a single map and lemmas to switch
OneMap-PRP: a PRP with a single map and lemmas to switch
Tip revision: 0dd57f7
ecTransMatching.ml
(* --------------------------------------------------------------------
* 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 EcUtils
open EcParsetree
open EcMatching
open EcGenRegexp
(* -------------------------------------------------------------------- *)
let default_start_name = "$start"
let default_end_name = "$end"
let default_name = "$default"
(*-------------------------------------------------------------------- *)
let any_stmt = Repeat (Any, (None, None), `Greedy)
let any_block = (With_anchor, With_anchor), IM_Any
let set_default_name pattern = Named (pattern, default_name)
let default_start_without_anchor =
Named (Repeat (Any, (None, None), `Lazy), default_start_name)
let default_end_without_anchor =
Named (Repeat (Any, (None, None), `Greedy), default_end_name)
(*-------------------------------------------------------------------- *)
let default_stmt x = odfl any_stmt x
(*-------------------------------------------------------------------- *)
let add_default_names (at_begin, at_end) pattern =
let pattern_sequence = [ set_default_name pattern ] in
let pattern_sequence =
if at_begin = With_anchor
then Named (Seq [], default_start_name) :: pattern_sequence
else default_start_without_anchor :: pattern_sequence in
let pattern_sequence =
if at_end = With_anchor
then pattern_sequence @ [Named (Seq [], default_end_name)]
else pattern_sequence @ [default_end_without_anchor] in
pattern_sequence
(*-------------------------------------------------------------------- *)
let add_anchors (at_begin, at_end) pattern_sequence =
let pattern =
if at_begin = With_anchor then Anchor Start :: pattern_sequence
else pattern_sequence in
if at_end = With_anchor then pattern @ [Anchor End]
else pattern
(*-------------------------------------------------------------------- *)
let rec trans_block (anchors, pattern_parsed) =
let pattern = trans_stmt pattern_parsed in
match pattern with
| Seq ps -> Seq (add_anchors anchors ps)
| _ -> Seq (add_anchors anchors [ pattern ])
(*-------------------------------------------------------------------- *)
and trans_stmt = function
| IM_Any -> any_stmt
| IM_Parens r -> trans_stmt r
| IM_Assign -> Base RAssign
| IM_Sample -> Base RSample
| IM_Call -> Base RCall
| IM_If (bt, bf) ->
let branch_true = trans_block (odfl any_block bt) in
let branch_false = trans_block (odfl any_block bf) in
Base (RIf (branch_true, branch_false))
| IM_While b ->
let branch = odfl any_block b in
let branch = trans_block branch in
Base (RWhile branch)
| IM_Named (s, r) ->
let r = odfl IM_Any r in
let r = trans_stmt r in
Named (r, EcLocation.unloc s)
| IM_Repeat ((a,b),c) ->
trans_repeat ((a,b),c)
| IM_Seq l ->
Seq (List.map trans_stmt l)
| IM_Choice l ->
Choice (List.map trans_stmt l)
(*-------------------------------------------------------------------- *)
and trans_repeat ((is_greedy, repeat_kind), r) =
match r with
| IM_Any -> begin
let greed = if is_greedy then `Greedy else `Lazy in
match repeat_kind with
| IM_R_Repeat info -> Repeat (Any, info, greed)
| IM_R_May info -> Repeat (Any, (None, info), greed)
end
| IM_Named (s, r) ->
let r = odfl IM_Any r in
let r = trans_repeat ((is_greedy, repeat_kind), r) in
Named (r, EcLocation.unloc s)
| _ -> begin
let r = trans_stmt r in
let greed = if is_greedy then `Greedy else `Lazy in
match repeat_kind with
| IM_R_Repeat info -> Repeat (r, info, greed)
| IM_R_May info -> Repeat (r, (None, info), greed)
end
(*-------------------------------------------------------------------- *)
let trans_block (anchors, pattern_parsed) =
let pattern = trans_stmt pattern_parsed in
Seq (add_anchors anchors (add_default_names anchors pattern))