Start generating documentation

6 files changed, 101 insertions, 73 deletions

diff --git a/Makefile b/Makefile
index c59aec01..3b822802 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,8 @@ CHARON_TESTS_DIR =
 CHARON_OPTIONS =
 CHARON_TESTS_SRC =
 
+AENEAS_DRIVER = src/driver.exe
+
 # The user can specify additional translation options for Aeneas:
 OPTIONS ?=
 
@@ -29,8 +31,15 @@ build-tests-verify: build tests verify
 
 # Build the project
 .PHONY: build
-build:
-	dune build src/main.exe
+build: build-driver build-lib
+
+.PHONY: build-driver
+build-driver:
+	dune build $(AENEAS_DRIVER)
+
+.PHONY: build-lib
+build-lib:
+	dune build src/aeneas.cmxs
 
 # Test the project by translating test files to F*
 .PHONY: tests
@@ -91,10 +100,10 @@ trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
 trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
 trans-polonius-%: gen-llbc-polonius-%
-	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+	dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 trans-%: gen-llbc-%
-	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+	dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 .PHONY: doc
 doc:
diff --git a/aeneas.opam b/aeneas.opam
new file mode 100644
index 00000000..4048f9a0
--- /dev/null
+++ b/aeneas.opam
@@ -0,0 +1,29 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+synopsis: ""
+description: ""
+maintainer: ["son.ho@inria.fr"]
+authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"]
+license: "Apache-2.0"
+homepage: "https://github.com/AeneasVerif/aeneas"
+bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
+depends: [
+  "dune" {>= "2.8"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/AeneasVerif/aeneas.git"
diff --git a/dune-project b/dune-project
index c2e46604..f8b418f2 100644
--- a/dune-project
+++ b/dune-project
@@ -1 +1,24 @@
 (lang dune 2.8)
+
+(name aeneas)
+
+(version 0.1)
+
+(generate_opam_files true)
+
+(formatting)
+
+(source
+ (uri git+https://github.com/AeneasVerif/aeneas.git))
+
+(homepage "https://github.com/AeneasVerif/aeneas")
+
+(bug_reports "https://github.com/AeneasVerif/aeneas/issues")
+
+(authors
+  "Son Ho"
+  "Jonathan Protzenko"
+  "Aymeric Fromherz"
+  "Sidney Congard")
+
+(license Apache-2.0)
\ No newline at end of file
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
deleted file mode 100644
index 37b7555e..00000000
--- a/src/PrintSymbolicAst.ml
+++ /dev/null
@@ -1,59 +0,0 @@
-(** Printing utilities for symbolic AST.
-
-    We don't put this in [Print] because:
-    - [Print] is getting quite big
-    - if we do so we have a dependency cycle...
- *)
-
-open Errors
-open Identifiers
-open FunIdentifier
-module T = Types
-module TU = TypesUtils
-module V = Values
-module E = Expressions
-module A = LlbcAst
-module C = Contexts
-open SymbolicAst
-module P = Print
-module PT = Print.Types
-
-type formatting_ctx = {
-  type_context : C.type_context;
-  fun_context : A.fun_decl FunDeclId.Map.t;
-  type_vars : T.type_var list;
-}
-
-type formatter = P.Values.value_formatter
-
-let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter =
-  (* We shouldn't use [rvar_to_string] *)
-  let rvar_to_string _ = failwith "Unexpected use of rvar_to_string" in
-  let r_to_string r = PT.region_id_to_string r in
-
-  let type_var_id_to_string vid =
-    let v = T.TypeVarId.nth ctx.type_vars vid in
-    v.name
-  in
-  let type_decl_id_to_string def_id =
-    let def = T.TypeDeclId.Map.find def_id ctx.type_context.type_decls in
-    P.name_to_string def.name
-  in
-  let adt_variant_to_string =
-    P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
-  in
-  (* We shouldn't use [var_id_to_string] *)
-  let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in
-
-  let adt_field_names =
-    P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
-  in
-  {
-    rvar_to_string;
-    r_to_string;
-    type_var_id_to_string;
-    type_decl_id_to_string;
-    adt_variant_to_string;
-    var_id_to_string;
-    adt_field_names;
-  }
diff --git a/src/main.ml b/src/driver.ml
index 05e96af9..ae9d238a 100644
--- a/src/main.ml
+++ b/src/driver.ml
@@ -1,12 +1,15 @@
-open LlbcOfJson
-open Logging
-open Print
-module T = Types
-module A = LlbcAst
-module I = Interpreter
+open Aeneas.LlbcOfJson
+open Aeneas.Logging
+open Aeneas.Print
+module T = Aeneas.Types
+module A = Aeneas.LlbcAst
+module I = Aeneas.Interpreter
 module EL = Easy_logging.Logging
-module TA = TypesAnalysis
-module Micro = PureMicroPasses
+module TA = Aeneas.TypesAnalysis
+module Micro = Aeneas.PureMicroPasses
+module Print = Aeneas.Print
+module PrePasses = Aeneas.PrePasses
+module Translate = Aeneas.Translate
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
diff --git a/src/dune b/src/dune
index ccf726c9..e8b53fc5 100644
--- a/src/dune
+++ b/src/dune
@@ -1,10 +1,33 @@
 ;; core: for Core.Unix.mkdir_p
 
 (executable
- (name main)
+ (name driver)
+ (public_name aeneas_driver)
+ (package aeneas)
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries ppx_deriving yojson zarith easy_logging core_unix))
+ (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas)
+ (modules driver))
+
+(library
+ (name aeneas) ;; The name as used in the project
+ (public_name aeneas) ;; The name as revealed to the projects importing this library
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
+ (libraries ppx_deriving yojson zarith easy_logging core_unix)
+ (modules Assumed Collections ConstStrings Contexts Cps Crates Errors
+   Expressions ExpressionsUtils ExtractToFStar FunsAnalysis Identifiers
+   InterpreterBorrowsCore InterpreterBorrows InterpreterExpansion
+   InterpreterExpressions Interpreter InterpreterPaths InterpreterProjectors
+   InterpreterStatements InterpreterUtils Invariants LlbcAst LlbcAstUtils
+   LlbcOfJson Logging Meta Names OfJsonBasic PrePasses Print PrintPure
+   PureMicroPasses Pure PureToExtract PureTypeCheck PureUtils Scalars
+   StringUtils Substitute SymbolicAst SymbolicToPure SynthesizeSymbolic
+   TranslateCore Translate TypesAnalysis Types TypesUtils Utils Values
+   ValuesUtils))
+
+(documentation
+ (package aeneas))
 
 (env
  (dev