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
ecSymbols.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
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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 = Pervasives.compare
(* -------------------------------------------------------------------- *)
module SymCmp = struct
type t = symbol
let compare = (Pervasives.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 rec 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)