Skip to content

Commit

Permalink
Merge pull request #727 from hacspec/refactor-concrete-ident-generated
Browse files Browse the repository at this point in the history
fix(engine): `Concrete_ident_generated`: `name` -> `t`, derive more
  • Loading branch information
W95Psp authored Jul 1, 2024
2 parents 0da8372 + d7cdcc8 commit 7be21f5
Show file tree
Hide file tree
Showing 6 changed files with 19 additions and 14 deletions.
8 changes: 4 additions & 4 deletions engine/backends/proverif/proverif_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -147,20 +147,20 @@ module Make (Options : OPTS) : MAKE = struct

(* TODO: Give definitions for core / known library functions, cf issues #447, #448 *)
let library_functions :
(Concrete_ident_generated.name * (AST.expr list -> document)) list =
(Concrete_ident_generated.t * (AST.expr list -> document)) list =
[]

let library_constructors :
(Concrete_ident_generated.name
(Concrete_ident_generated.t
* ((global_ident * AST.expr) list -> document))
list =
[]

let library_constructor_patterns :
(Concrete_ident_generated.name * (field_pat list -> document)) list =
(Concrete_ident_generated.t * (field_pat list -> document)) list =
[]

let library_types : (Concrete_ident_generated.name * document) list = []
let library_types : (Concrete_ident_generated.t * document) list = []

let assoc_known_name name (known_name, _) =
Global_ident.eq_name known_name name
Expand Down
3 changes: 2 additions & 1 deletion engine/lib/concrete_ident/concrete_ident.ml
Original file line number Diff line number Diff line change
Expand Up @@ -420,7 +420,8 @@ module T = struct
let hash x = [%hash: Imported.def_id] x.def_id
let hash_fold_t s x = Imported.hash_fold_def_id s x.def_id

type name = Concrete_ident_generated.name
type name = Concrete_ident_generated.t
[@@deriving show, yojson, compare, sexp, eq, hash]

let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k

Expand Down
4 changes: 3 additions & 1 deletion engine/lib/concrete_ident/concrete_ident.mli
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
type t [@@deriving show, yojson, compare, sexp, eq, hash]
type name = Concrete_ident_generated.name

type name = Concrete_ident_generated.t
[@@deriving show, yojson, compare, sexp, eq, hash]

module ImplInfoStore : sig
val init : (Types.def_id * Types.impl_infos) list -> unit
Expand Down
4 changes: 2 additions & 2 deletions engine/lib/phases/phase_simplify_question_marks.ml
Original file line number Diff line number Diff line change
Expand Up @@ -106,8 +106,8 @@ module%inlined_contents Make (FA : Features.T) = struct
Some call

let mk_pconstruct ~is_struct ~is_record ~span ~typ
(constructor : Concrete_ident_generated.name)
(fields : (Concrete_ident_generated.name * pat) list) =
(constructor : Concrete_ident_generated.t)
(fields : (Concrete_ident_generated.t * pat) list) =
let name =
Global_ident.of_name (Constructor { is_struct }) constructor
in
Expand Down
8 changes: 4 additions & 4 deletions engine/lib/phases/phase_specialize.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ module Make (F : Features.T) =
open Concrete_ident_generated

type pattern = {
fn : name;
fn_replace : name;
fn : t;
fn_replace : t;
args : (expr -> bool) list;
ret : ty -> bool;
}
Expand All @@ -30,7 +30,7 @@ module Make (F : Features.T) =

(** Constructs a predicate out of predicates and names *)
let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
(fn : name) (fn_replace : name) : pattern =
(fn : t) (fn_replace : t) : pattern =
let args = List.map ~f:(fun p x -> p x |> Option.is_some) args in
let ret t = ret t |> Option.is_some in
{ fn; fn_replace; args; ret }
Expand All @@ -51,7 +51,7 @@ module Make (F : Features.T) =
fun ~eq x x' -> if eq x x' then Some x' else None

let eq_global_ident :
name -> (Ast.Global_ident.t, Ast.Global_ident.t) predicate =
t -> (Ast.Global_ident.t, Ast.Global_ident.t) predicate =
eq ~eq:Ast.Global_ident.eq_name

let erase : 'a. ('a, unit) predicate = fun _ -> Some ()
Expand Down
6 changes: 4 additions & 2 deletions engine/names/extract/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,14 +91,16 @@ fn reader_to_str(s: String) -> String {
const TAB: &str = " ";
let mut result = String::new();
result += &format!(
"type name = \n{TAB} {}\n",
"type t = \n{TAB} {}[@@deriving show, yojson, compare, sexp, eq, hash]\n",
def_ids
.iter()
.map(|(_, def_name)| format!("{def_name}"))
.collect::<Vec<_>>()
.join(&format!("\n{TAB}| "))
);

result += "\n";
result += "include (val Base.Comparator.make ~compare ~sexp_of_t)";
result += "\n";
result += "module Values = struct\n";
for (json, name) in &def_ids {
Expand All @@ -107,7 +109,7 @@ fn reader_to_str(s: String) -> String {
result += "end\n\n";

result += &format!(
"let def_id_of: name -> Types.def_id = function\n{TAB} {}\n\n",
"let def_id_of: t -> Types.def_id = function\n{TAB} {}\n\n",
def_ids
.iter()
.map(|(_, n)| format!("{n} -> Values.parsed_{n}"))
Expand Down

0 comments on commit 7be21f5

Please sign in to comment.