Skip to content

Commit 86b798a

Browse files
fsestinifsestini
authored
Merge pull request #1718 from fsestini/uoaim
[uoaim] Implement tool
2 parents e45326f + d7cdbf2 commit 86b798a

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

+3523
-38
lines changed

‎gen/critical.ml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@
2020
"./critical n" outputs critical tests on n procs.
2121
*)
2222

23-
open Misc
2423
open Printf
2524
open Archs
2625

‎gen/diycross.ml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
1515
(****************************************************************************)
1616

17-
open Misc
1817
open Printf
1918

2019
module type Config = sig
@@ -74,7 +73,7 @@ module Make (Config:Config) (M:Builder.S) =
7473
let ess = List.map expand_edges ess in
7574
let ess = varatom_ess ess in
7675
D.all (gen ess)
77-
with Fatal msg ->
76+
with Misc.Fatal msg ->
7877
eprintf "Fatal error: %s\n" msg ;
7978
exit 2
8079
end

‎gen/diyone.ml‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
1515
(****************************************************************************)
1616

17-
open Misc
1817
open Printf
1918

2019
module type Config = sig
@@ -156,7 +155,7 @@ module Make(O:Config) (M:Builder.S) =
156155
let mk_scope _ = st in
157156
Some (kont es D.no_info mk_name mk_scope k0)
158157
with
159-
| Fatal msg | UserError msg ->
158+
| Misc.Fatal msg | Misc.UserError msg ->
160159
Warn.warn_always "%s on line '%s'" msg line ;
161160
Some k0
162161
with
@@ -167,7 +166,7 @@ module Make(O:Config) (M:Builder.S) =
167166
do_rec in
168167
D.all gen
169168
| _ -> dump name_opt es
170-
end with Fatal msg ->
169+
end with Misc.Fatal msg ->
171170
eprintf "%s: Fatal error: %s\n" Config.prog msg ;
172171
exit 2
173172

‎lib/misc.ml‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -834,3 +834,60 @@ let group_by_int get_key env =
834834
(IntMap.fold
835835
(fun _ env_p k -> List.rev env_p::k)
836836
m []))
837+
838+
(************************************)
839+
(* Stdlib shims and other utilities *)
840+
(************************************)
841+
842+
module List = struct
843+
include List
844+
845+
let empty = []
846+
let concat_map f l = concat (map f l)
847+
let is_empty = function
848+
| [] -> true
849+
| _ -> false
850+
851+
let singleton x = [ x ]
852+
let uniq ~eq l =
853+
let rec uniq eq acc l =
854+
match l with
855+
| [] -> List.rev acc
856+
| x :: xs when List.exists (eq x) xs -> uniq eq acc xs
857+
| x :: xs -> uniq eq (x :: acc) xs
858+
in
859+
uniq eq [] l
860+
861+
862+
let fold_left_map f accu l =
863+
let rec aux accu l_accu = function
864+
| [] -> accu, rev l_accu
865+
| x :: l ->
866+
let accu, x = f accu x in
867+
aux accu (x :: l_accu) l in
868+
aux accu [] l
869+
870+
module Syntax = struct
871+
let (let*) = fun l f -> concat_map f l
872+
end
873+
874+
let apply (fs : ('a -> 'b) list) (xs : 'a list) : 'b list =
875+
let open Syntax in
876+
let* f = fs in
877+
let* x = xs in
878+
[ f x ]
879+
end
880+
881+
module Option = struct
882+
include Option
883+
884+
let get_or_exn exn = function
885+
| Some x -> x
886+
| None -> raise exn
887+
888+
let apply f_opt x_opt =
889+
let (let*) = Option.bind in
890+
let* f = f_opt in
891+
let* x = x_opt in
892+
Some (f x)
893+
end

‎lib/misc.mli‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -363,3 +363,41 @@ val mix : int -> int -> int -> int
363363
(*********************************)
364364

365365
val group_by_int : ('k -> int option) -> ('k * 'v) list -> ('k * 'v) list list
366+
367+
(************************************)
368+
(* Stdlib shims and other utilities *)
369+
(************************************)
370+
371+
module List : sig
372+
include module type of List
373+
374+
val apply : ('a -> 'b) t -> 'a t -> 'b t
375+
val empty : 'a t
376+
val concat_map : ('a -> 'b list) -> 'a list -> 'b list
377+
val is_empty : 'a list -> bool
378+
val singleton : 'a -> 'a t
379+
(** [singleton x] returns the one-element list [[x]].
380+
For compatibility with OCaml < 5.4. *)
381+
382+
val uniq : eq:('a -> 'a -> bool) -> 'a t -> 'a t
383+
(** [uniq ~eq l] removes duplicates in [l] w.r.t the equality predicate [eq].
384+
Complexity is quadratic in the length of the list, but the order
385+
of elements is preserved. *)
386+
387+
val fold_left_map :
388+
('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
389+
(** [fold_left_map] is a combination of [fold_left] and [map] that threads an
390+
accumulator through calls to [f].
391+
For compatibility with OCaml < 4.11. *)
392+
393+
module Syntax : sig
394+
val (let*) : 'a list -> ('a -> 'b list) -> 'b list
395+
end
396+
end
397+
398+
module Option : sig
399+
include module type of Option
400+
401+
val apply : ('a -> 'b) t -> 'a t -> 'b t
402+
val get_or_exn : exn -> 'a option -> 'a
403+
end

‎tools/mcompare.ml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
1515
(****************************************************************************)
1616

17-
open Misc
1817
open Printf
1918

2019
(*****************************)
@@ -1172,7 +1171,7 @@ let format_int_string s =
11721171
let dump_cond_chan txt chan = List.iter (fprintf chan "%s\n") txt in
11731172
let dump_cond txt o = match o with
11741173
| None -> ()
1175-
| Some name -> output_protect (dump_cond_chan txt) name in
1174+
| Some name -> Misc.output_protect (dump_cond_chan txt) name in
11761175
dump_cond !pos_cond Config.cond_pos ;
11771176
dump_cond !neg_cond Config.cond_neg ;
11781177
()

‎tools/miaou.ml‎

Lines changed: 1 addition & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -68,43 +68,14 @@ module Make
6868

6969
open AST
7070

71-
let toalpha s =
72-
let buff = Buffer.create 10 in
73-
for k=0 to String.length s-1 do
74-
match s.[k] with
75-
| 'a'..'z'|'A'..'Z' as c ->
76-
Buffer.add_char buff c
77-
| _ -> ()
78-
done ;
79-
Buffer.contents buff
80-
81-
let vocabulary =
82-
StringMap.empty
83-
|> StringMap.add "dmb.full" "DMBFULL"
84-
|> StringMap.add "dmb.st" "DMBST"
85-
|> StringMap.add "dmb.ld" "DMBLD"
86-
|> StringMap.add "dsb.full" "DSBFULL"
87-
|> StringMap.add "dsb.st" "DSBST"
88-
|> StringMap.add "dsb.ld" "DSBLD"
89-
|> StringMap.add "iico_order" "iicoorder"
90-
|> StringMap.add "iico_data" "iicodata"
91-
|> StringMap.add "iico_ctrl" "iicoctrl"
92-
|> StringMap.add "iico_control" "iicoctrl"
93-
|> StringMap.add "hw-reqs" "hwreqs"
94-
|> StringMap.add "sca-class" "sca"
95-
|> StringMap.add "Instr-read-ordered-before" "Instrreadob"
96-
|> StringMap.add "id" "sameEffect"
71+
let tr_id = MiaouNames.to_csname
9772

9873
let defs =
9974
match O.texfile with
10075
| None -> None
10176
| Some fname ->
10277
Some (LexMiaou.csnames (libfind fname))
10378

104-
let tr_id s =
105-
try StringMap.find s vocabulary
106-
with Not_found -> toalpha s
107-
10879
let get_id_type =
10980
match defs with
11081
| None -> fun _ -> None

‎tools/miaouNames.ml‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
(****************************************************************************)
2+
(* The Diy toolsuite *)
3+
(* *)
4+
(* Jade Alglave, University College London, UK. *)
5+
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
6+
(* *)
7+
(* Copyright 2023-present Institut National de Recherche en Informatique et *)
8+
(* en Automatique and the authors. All rights reserved. *)
9+
(* *)
10+
(* This software is governed by the CeCILL-B license under French law and *)
11+
(* abiding by the rules of distribution of free software. You can use, *)
12+
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
13+
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
14+
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
15+
(****************************************************************************)
16+
17+
(** Name handling for miaou and back *)
18+
19+
20+
let toalpha s =
21+
let buff = Buffer.create 10 in
22+
for k=0 to String.length s-1 do
23+
match s.[k] with
24+
| 'a'..'z'|'A'..'Z' as c ->
25+
Buffer.add_char buff c
26+
| _ -> ()
27+
done ;
28+
Buffer.contents buff
29+
30+
let vocabulary =
31+
StringMap.empty
32+
|> StringMap.add "dmb.full" "DMBFULL"
33+
|> StringMap.add "dmb.st" "DMBST"
34+
|> StringMap.add "dmb.ld" "DMBLD"
35+
|> StringMap.add "dsb.full" "DSBFULL"
36+
|> StringMap.add "dsb.st" "DSBST"
37+
|> StringMap.add "dsb.ld" "DSBLD"
38+
|> StringMap.add "iico_order" "iicoorder"
39+
|> StringMap.add "iico_data" "iicodata"
40+
|> StringMap.add "iico_ctrl" "iicoctrl"
41+
|> StringMap.add "iico_control" "iicoctrl"
42+
|> StringMap.add "hw-reqs" "hwreqs"
43+
|> StringMap.add "sca-class" "sca"
44+
|> StringMap.add "Instr-read-ordered-before" "Instrreadob"
45+
|> StringMap.add "L" "REL"
46+
|> StringMap.add "id" "sameEffect"
47+
48+
let to_csname s =
49+
try StringMap.find s vocabulary
50+
with Not_found -> toalpha s

‎tools/miaouNames.mli‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
(****************************************************************************)
2+
(* The Diy toolsuite *)
3+
(* *)
4+
(* Jade Alglave, University College London, UK. *)
5+
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
6+
(* *)
7+
(* Copyright 2023-present Institut National de Recherche en Informatique et *)
8+
(* en Automatique and the authors. All rights reserved. *)
9+
(* *)
10+
(* This software is governed by the CeCILL-B license under French law and *)
11+
(* abiding by the rules of distribution of free software. You can use, *)
12+
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
13+
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
14+
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
15+
(****************************************************************************)
16+
17+
(** Name handling for miaou and back *)
18+
19+
(* Translate name to a valid LaTeX command name *)
20+
val to_csname : string -> string

‎tools/uoaim/.ocamlformat‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
disable = false

0 commit comments

Comments
 (0)