cleanup of lospec lib

dune-project

@@ -1,5 +1,5 @@
-(lang dune 3.6)
-(using menhir 2.0)
+(lang dune 3.13)
+(using menhir 3.0)
 (using dune_site 0.1)
 
 (wrapped_executables false)

easycrypt.opam

@@ -6,7 +6,7 @@ depends: [
   "camlp-streams" {>= "5"}
   "camlzip"
   "cmdliner"
-  "dune" {>= "3.6" & >= "3.6"}
+  "dune" {>= "3.13" & >= "3.6"}
   "dune-build-info"
   "dune-site"
   "hex"

libs/lospecs/ast.ml

@@ -16,7 +16,10 @@ end = struct
   let id ((_, i) : ident) : int = i
 end
 
-module IdentMap = Map.Make(struct type t = Ident.ident let compare a b = (Ident.id a) - (Ident.id b) end) 
+module IdentMap = Map.Make(struct
+  type t = Ident.ident
+  let compare a b = (Ident.id a) - (Ident.id b)
+end) 
 
 (* -------------------------------------------------------------------- *)
 type ident = Ident.ident [@@deriving yojson]

libs/lospecs/circuit_spec.ml

@@ -6,6 +6,13 @@ open Aig
 let rec log2 n =
   if n <= 1 then 0 else 1 + log2 (n asr 1)
 
+
+(* ==================================================================== *)
+let load_from_file ~(filename : string) =
+  let specs = File.with_file_in filename (Io.parse filename) in
+  let specs = Typing.tt_program Typing.Env.empty specs in
+  specs
+
 (* ==================================================================== *)
 module Env : sig
   type env
@@ -60,7 +67,7 @@ end
 type env = Env.env
 
 (* ==================================================================== *)
-let circuit_of_spec (rs : reg list) (p : adef) : reg =
+let circuit_of_specification (rs : reg list) (p : adef) : reg =
   assert (List.length rs = List.length p.arguments);
   assert (List.for_all2 (fun r (_, `W n) -> List.length r = n) rs p.arguments);
 

libs/lospecs/circuit_spec.mli

@@ -1,19 +1,3 @@
-val log2 : int -> int
-module Env :
-  sig
-    type env
-    val empty : env
-    module Fun :
-      sig
-        val get : env -> Ast.ident -> Ast.aargs * Ast.aexpr
-        val bind : env -> Ast.ident -> Ast.aargs * Ast.aexpr -> env
-      end
-    module Var :
-      sig
-        val get : env -> Ast.ident -> Aig.reg
-        val bind : env -> Ast.ident -> Aig.reg -> env
-        val bindall : env -> (Ast.ident * Aig.reg) list -> env
-      end
-  end
-type env = Env.env
-val circuit_of_spec : Aig.reg list -> Ast.adef -> Aig.reg
+(* ==================================================================== *)
+val circuit_of_specification : Aig.reg list -> Ast.adef -> Aig.reg
+val load_from_file : filename:string -> (string * Ast.adef) list

libs/lospecs/dune

@@ -3,37 +3,18 @@
  (sites easycrypt))
 
 (library
- (name lospecs)
- (public_name easycrypt.lospecs)
- (flags
-  (:standard -open Batteries))
- (modules :standard config \ lospecs_test circuit_test)
- (preprocess
-  (pps ppx_deriving_yojson))
- (foreign_stubs
-  (language cxx)
-  (flags :standard -std=c++17 -mavx -mavx2)
-  (names avx2_runtime))
- (libraries batteries dune-site menhirLib zarith ppx_deriving_yojson.runtime bitwuzla))
-
-(executable
- (name lospecs_test)
- (flags
-  (:standard -open Batteries))
- (modules lospecs_test)
- (promote (until-clean))
- (libraries batteries cmdliner lospecs))
-
-(executable
- (name circuit_test)
- (flags
-  (:standard -open Batteries))
- (modules circuit_test)
- (promote (until-clean))
- (libraries batteries hex iter lospecs progress))
+  (name lospecs)
+  (public_name easycrypt.lospecs)
+  (flags
+    (:standard -open Batteries))
+  (modules :standard config)
+  (preprocess
+    (pps ppx_deriving_yojson))
+  (libraries batteries dune-site menhirLib zarith ppx_deriving_yojson.runtime bitwuzla))
 
 (ocamllex lexer)
 
 (menhir
- (modules parser)
- (flags --table --explain))
+  (modules parser)
+  (explain true)
+  (flags --table))