https://github.com/EasyCrypt/easycrypt
Tip revision: 8e47fe3d10d154d0653552a905fee3a3113265d4 authored by Pierre-Yves Strub on 03 December 2021, 16:11:39 UTC
Fix bug that prevents `rewrite //= in h` to simplify in `h`
Fix bug that prevents `rewrite //= in h` to simplify in `h`
Tip revision: 8e47fe3
ecSymbols.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
type symbol = string
type qsymbol = symbol list * symbol
type msymbol = (symbol * msymbol list) list
let sym_equal : symbol -> symbol -> bool = (=)
let sym_compare : symbol -> symbol -> int = Stdlib.compare
(* -------------------------------------------------------------------- *)
module SymCmp = struct
type t = symbol
let compare = (Stdlib.compare : t -> t -> int)
end
module Msym = EcMaps.Map.Make(SymCmp)
module Ssym = EcMaps.Set.MakeOfMap(Msym)
(* -------------------------------------------------------------------- *)
module MMsym : sig
type +'a t
val empty : 'a t
val add : symbol -> 'a -> 'a t -> 'a t
val last : symbol -> 'a t -> 'a option
val all : symbol -> 'a t -> 'a list
val fold : (symbol -> 'a list -> 'b -> 'b) -> 'a t -> 'b -> 'b
val map_at : ('a list -> 'a list) -> symbol -> 'a t -> 'a t
val iter : (symbol -> 'a -> unit) -> 'a t -> unit
end = struct
type 'a t = ('a list) Msym.t
let empty : 'a t = Msym.empty
let add (x : symbol) (v : 'a) (m : 'a t) =
Msym.change
(fun crt -> Some (v :: (EcUtils.odfl [] crt))) x m
let last (x : symbol) (m : 'a t) =
match Msym.find_opt x m with
| None -> None
| Some [] -> None
| Some (v :: _) -> Some v
let all (x : symbol) (m : 'a t) =
EcUtils.odfl [] (Msym.find_opt x m)
let fold f m x = Msym.fold f m x
let map_at f (x : symbol) (m : 'a t) =
Msym.change
(fun v ->
match f (EcUtils.odfl [] v) with
| [] -> None
| v -> Some v)
x m
let iter f (m:'a t) =
Msym.iter (fun s -> List.iter (f s)) m
end
(* -------------------------------------------------------------------- *)
let pp_symbol fmt s = Format.fprintf fmt "%s" s
let rec string_of_qsymbol = function
| ([] , x) -> Printf.sprintf "%s" x
| (n :: p, x) -> Printf.sprintf "%s.%s" n (string_of_qsymbol (p, x))
let pp_qsymbol fmt qn =
Format.fprintf fmt "%s" (string_of_qsymbol qn)
let rec string_of_msymbol (mx : msymbol) =
match mx with
| [] ->
""
| [(x, [])] ->
x
| [(x, args)] ->
Printf.sprintf "%s(%s)"
x (String.concat ", " (List.map string_of_msymbol args))
| nm :: x ->
Printf.sprintf "%s.%s"
(string_of_msymbol [nm])
(string_of_msymbol x)
let pp_msymbol fmt x =
Format.fprintf fmt "%s" (string_of_msymbol x)