diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/PrintSymbolicAst.ml | 59 | ||||
| -rw-r--r-- | src/driver.ml (renamed from src/main.ml) | 19 | ||||
| -rw-r--r-- | src/dune | 27 |
3 files changed, 36 insertions, 69 deletions
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. @@ -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 |