Skip to content

Commit d31c0ce

Browse files
loutrloutr
authored
Merge branch 'EasyCrypt:main' into reworked-lazy-eager-logic-squashed
2 parents 0c06051 + 48a21c3 commit d31c0ce

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

76 files changed

+1852
-758
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ jobs:
2222
- name: Install EasyCrypt dependencies
2323
run: |
2424
opam pin add -n easycrypt .
25+
opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
2526
opam install --deps-only easycrypt
2627
- name: Compile EasyCrypt
2728
run: opam exec -- make PROFILE=ci
@@ -61,6 +62,7 @@ jobs:
6162
- name: Install EasyCrypt dependencies
6263
run: |
6364
opam pin add -n easycrypt .
65+
opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
6466
opam install --deps-only easycrypt
6567
- name: Compile EasyCrypt
6668
run: opam exec -- make
@@ -128,6 +130,7 @@ jobs:
128130
- name: Install EasyCrypt dependencies
129131
run: |
130132
opam pin add -n easycrypt easycrypt
133+
opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
131134
opam install --deps-only easycrypt
132135
- name: Compile & Install EasyCrypt
133136
run: opam exec -- make -C easycrypt build install

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@
55

66
/_build
77
/result
8-
/etc
98
/theories/attic
109

1110
/ec.*

‎3rdparty/inifiles-1.2/dune‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
(library
2+
(name inifiles)
3+
(public_name easycrypt.inifiles)
4+
(modules :standard)
5+
(libraries pcre2 unix))
6+
7+
(ocamllex inilexer)
8+
(ocamlyacc parseini)

‎3rdparty/inifiles-1.2/inifiles.ml‎

Lines changed: 267 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,267 @@
1+
(* A small library to read and write .ini files
2+
3+
Copyright (C) 2004 Eric Stokes, and The California State University
4+
at Northridge
5+
6+
This library is free software; you can redistribute it and/or
7+
modify it under the terms of the GNU Lesser General Public
8+
License as published by the Free Software Foundation; either
9+
version 2.1 of the License, or (at your option) any later version.
10+
11+
This library is distributed in the hope that it will be useful,
12+
but WITHOUT ANY WARRANTY; without even the implied warranty of
13+
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14+
Lesser General Public License for more details.
15+
16+
You should have received a copy of the GNU Lesser General Public
17+
License along with this library; if not, write to the Free Software
18+
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
19+
*)
20+
21+
22+
module Pcre = Pcre2
23+
24+
open Pcre
25+
open Parseini
26+
open Inilexer
27+
28+
exception Invalid_section of string
29+
exception Invalid_element of string
30+
exception Missing_section of string
31+
exception Missing_element of string
32+
exception Ini_parse_error of (int * string)
33+
34+
type attribute_specification = {
35+
atr_name: string;
36+
atr_required: bool;
37+
atr_default: (string list) option;
38+
atr_validator: Pcre.regexp option;
39+
}
40+
41+
type section_specification = {
42+
sec_name: string;
43+
sec_required: bool;
44+
sec_attributes: attribute_specification list;
45+
}
46+
47+
type specification = section_specification list
48+
49+
let comment = regexp "^#.*$"
50+
51+
module Ordstr =
52+
struct
53+
type t = string
54+
let compare (x:t) (y:t) =
55+
String.compare (String.lowercase_ascii x) (String.lowercase_ascii y)
56+
end
57+
58+
module Strset = Set.Make(Ordstr)
59+
60+
let setOfList list =
61+
let rec dosetOfList list set =
62+
match list with
63+
a :: tail -> dosetOfList tail (Strset.add a set)
64+
| [] -> set
65+
in
66+
dosetOfList list Strset.empty
67+
68+
let rec filterfile ?(buf=Buffer.create 500) f fd =
69+
try
70+
let theline = input_line fd in
71+
if f theline then begin
72+
Buffer.add_string buf (theline ^ "\n");
73+
filterfile ~buf f fd
74+
end
75+
else
76+
filterfile ~buf f fd
77+
with End_of_file -> Buffer.contents buf
78+
79+
let read_inifile file fd tbl =
80+
let lxbuf =
81+
Lexing.from_string
82+
(filterfile
83+
(fun line -> not (Pcre.pmatch ~rex:comment line))
84+
fd)
85+
in
86+
try
87+
let parsed_file = inifile lexini lxbuf in
88+
List.iter
89+
(fun (section, values) ->
90+
Hashtbl.add tbl section
91+
(List.fold_left
92+
(fun tbl (key, value) -> Hashtbl.add tbl key value;tbl)
93+
(Hashtbl.create 10)
94+
values))
95+
parsed_file
96+
with Parsing.Parse_error | Failure _ ->
97+
raise (Ini_parse_error (lxbuf.Lexing.lex_curr_p.Lexing.pos_lnum, file))
98+
99+
let write_inifile fd tbl =
100+
Hashtbl.iter
101+
(fun k v ->
102+
output_string fd "[";output_string fd k;output_string fd "]\n";
103+
(Hashtbl.iter
104+
(fun k v ->
105+
output_string fd k;output_string fd " = ";output_string fd v;
106+
output_string fd "\n") v);
107+
output_string fd "\n")
108+
tbl
109+
110+
class inifile ?(spec=[]) file =
111+
object (self)
112+
val file = file
113+
val data = Hashtbl.create 50
114+
115+
initializer
116+
let inch = open_in file in
117+
(try read_inifile file inch data
118+
with exn -> close_in inch;raise exn);
119+
close_in inch;
120+
self#validate
121+
122+
method private validate =
123+
match spec with
124+
[] -> ()
125+
| spec ->
126+
List.iter
127+
(fun {sec_name=name;sec_required=required;
128+
sec_attributes=attrs} ->
129+
try
130+
let sec =
131+
try Hashtbl.find data name
132+
with Not_found -> raise (Missing_section name)
133+
in
134+
List.iter
135+
(fun {atr_name=name;atr_required=req;
136+
atr_default=def;atr_validator=validator} ->
137+
try
138+
let attr_val =
139+
try Hashtbl.find sec name
140+
with Not_found -> raise (Missing_element name)
141+
in
142+
(match validator with
143+
Some rex ->
144+
if not (Pcre.pmatch ~rex:rex attr_val) then
145+
raise
146+
(Invalid_element
147+
(name ^ ": validation failed"))
148+
| None -> ())
149+
with Missing_element elt ->
150+
if req then raise (Missing_element elt)
151+
else match def with
152+
Some def -> List.iter (Hashtbl.add sec name) def
153+
| None -> ())
154+
attrs
155+
with Missing_section s ->
156+
if required then raise (Missing_section s))
157+
spec
158+
159+
method getval sec elt =
160+
try Hashtbl.find
161+
(try (Hashtbl.find data sec)
162+
with Not_found -> raise (Invalid_section sec))
163+
elt
164+
with Not_found -> raise (Invalid_element elt)
165+
166+
method getaval sec elt =
167+
try Hashtbl.find_all
168+
(try (Hashtbl.find data sec)
169+
with Not_found -> raise (Invalid_section sec))
170+
elt
171+
with Not_found -> raise (Invalid_element elt)
172+
173+
method setval sec elt v =
174+
(Hashtbl.add
175+
(try Hashtbl.find data sec
176+
with Not_found ->
177+
let h = Hashtbl.create 10 in
178+
Hashtbl.add data sec h;h)
179+
elt v);
180+
try self#validate
181+
with exn -> Hashtbl.remove data elt;raise exn
182+
183+
method delval sec elt =
184+
let valu =
185+
try
186+
Some
187+
(Hashtbl.find
188+
(try Hashtbl.find data sec
189+
with Not_found -> raise (Invalid_section sec))
190+
elt)
191+
with Not_found -> None
192+
in
193+
match valu with
194+
Some v ->
195+
((Hashtbl.remove
196+
(try Hashtbl.find data sec
197+
with Not_found -> raise (Invalid_section sec))
198+
elt);
199+
try self#validate
200+
with exn ->
201+
(Hashtbl.add
202+
(try Hashtbl.find data sec
203+
with Not_found -> raise (Invalid_section sec))
204+
elt v);
205+
raise exn)
206+
| None -> ()
207+
208+
209+
method sects =
210+
(Hashtbl.fold
211+
(fun k _v keys -> k :: keys)
212+
data [])
213+
214+
method iter func sec =
215+
(Hashtbl.iter func
216+
(try Hashtbl.find data sec
217+
with Not_found -> raise (Invalid_section sec)))
218+
219+
method attrs sec =
220+
(Strset.elements
221+
(setOfList
222+
(Hashtbl.fold
223+
(fun k _v attrs -> k :: attrs)
224+
(try Hashtbl.find data sec
225+
with Not_found -> raise (Invalid_section sec))
226+
[])))
227+
228+
method save ?(file = file) () =
229+
let outch = open_out file in
230+
write_inifile outch data;
231+
flush outch;
232+
end
233+
234+
let readdir path =
235+
let dir = Unix.handle_unix_error Unix.opendir path in
236+
let rec do_read dir =
237+
try
238+
let current = Unix.readdir dir in
239+
current :: (do_read dir)
240+
with End_of_file -> []
241+
in
242+
let lst = do_read dir in
243+
Unix.closedir dir;
244+
lst
245+
246+
let fold func path initial =
247+
let check_file path =
248+
match
249+
(path,
250+
(try (Unix.stat path).Unix.st_kind
251+
with Unix.Unix_error (_,_,_) -> Unix.S_DIR))
252+
with
253+
(_name, Unix.S_REG) when
254+
(Pcre.pmatch ~rex:(Pcre.regexp "^.*\\.ini$") path) ->
255+
true
256+
| _ -> false
257+
in
258+
(List.fold_left
259+
func
260+
initial
261+
(List.rev_map
262+
(fun x -> new inifile x)
263+
(List.filter
264+
check_file
265+
(List.rev_map
266+
(fun p -> (path ^ "/" ^ p))
267+
(readdir path)))))

0 commit comments

Comments
 (0)