diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/.ocamlformat (renamed from src/.ocamlformat) | 0 | ||||
| -rw-r--r-- | compiler/Assumed.ml (renamed from src/Assumed.ml) | 0 | ||||
| -rw-r--r-- | compiler/Collections.ml (renamed from src/Collections.ml) | 0 | ||||
| -rw-r--r-- | compiler/ConstStrings.ml (renamed from src/ConstStrings.ml) | 0 | ||||
| -rw-r--r-- | compiler/Contexts.ml (renamed from src/Contexts.ml) | 0 | ||||
| -rw-r--r-- | compiler/Cps.ml (renamed from src/Cps.ml) | 0 | ||||
| -rw-r--r-- | compiler/Crates.ml (renamed from src/Crates.ml) | 0 | ||||
| -rw-r--r-- | compiler/Errors.ml (renamed from src/Errors.ml) | 0 | ||||
| -rw-r--r-- | compiler/Expressions.ml (renamed from src/Expressions.ml) | 0 | ||||
| -rw-r--r-- | compiler/ExpressionsUtils.ml (renamed from src/ExpressionsUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/ExtractToFStar.ml (renamed from src/ExtractToFStar.ml) | 0 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml (renamed from src/FunsAnalysis.ml) | 0 | ||||
| -rw-r--r-- | compiler/Identifiers.ml (renamed from src/Identifiers.ml) | 0 | ||||
| -rw-r--r-- | compiler/Interpreter.ml (renamed from src/Interpreter.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml (renamed from src/InterpreterBorrows.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml (renamed from src/InterpreterBorrowsCore.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml (renamed from src/InterpreterExpansion.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml (renamed from src/InterpreterExpressions.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml (renamed from src/InterpreterPaths.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml (renamed from src/InterpreterProjectors.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml (renamed from src/InterpreterStatements.ml) | 0 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml (renamed from src/InterpreterUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/Invariants.ml (renamed from src/Invariants.ml) | 0 | ||||
| -rw-r--r-- | compiler/LlbcAst.ml (renamed from src/LlbcAst.ml) | 0 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml (renamed from src/LlbcAstUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/LlbcOfJson.ml (renamed from src/LlbcOfJson.ml) | 0 | ||||
| -rw-r--r-- | compiler/Logging.ml (renamed from src/Logging.ml) | 0 | ||||
| -rw-r--r-- | compiler/Meta.ml (renamed from src/Meta.ml) | 0 | ||||
| -rw-r--r-- | compiler/Names.ml (renamed from src/Names.ml) | 0 | ||||
| -rw-r--r-- | compiler/OfJsonBasic.ml (renamed from src/OfJsonBasic.ml) | 0 | ||||
| -rw-r--r-- | compiler/PrePasses.ml (renamed from src/PrePasses.ml) | 0 | ||||
| -rw-r--r-- | compiler/Print.ml (renamed from src/Print.ml) | 2 | ||||
| -rw-r--r-- | compiler/PrintPure.ml (renamed from src/PrintPure.ml) | 0 | ||||
| -rw-r--r-- | compiler/Pure.ml (renamed from src/Pure.ml) | 0 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml (renamed from src/PureMicroPasses.ml) | 0 | ||||
| -rw-r--r-- | compiler/PureToExtract.ml (renamed from src/PureToExtract.ml) | 0 | ||||
| -rw-r--r-- | compiler/PureTypeCheck.ml (renamed from src/PureTypeCheck.ml) | 0 | ||||
| -rw-r--r-- | compiler/PureUtils.ml (renamed from src/PureUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/Scalars.ml (renamed from src/Scalars.ml) | 0 | ||||
| -rw-r--r-- | compiler/StringUtils.ml (renamed from src/StringUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/Substitute.ml (renamed from src/Substitute.ml) | 0 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml (renamed from src/SymbolicAst.ml) | 0 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml (renamed from src/SymbolicToPure.ml) | 0 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml (renamed from src/SynthesizeSymbolic.ml) | 0 | ||||
| -rw-r--r-- | compiler/Translate.ml (renamed from src/Translate.ml) | 0 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml (renamed from src/TranslateCore.ml) | 0 | ||||
| -rw-r--r-- | compiler/Types.ml (renamed from src/Types.ml) | 0 | ||||
| -rw-r--r-- | compiler/TypesAnalysis.ml (renamed from src/TypesAnalysis.ml) | 0 | ||||
| -rw-r--r-- | compiler/TypesUtils.ml (renamed from src/TypesUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/Utils.ml (renamed from src/Utils.ml) | 0 | ||||
| -rw-r--r-- | compiler/Values.ml (renamed from src/Values.ml) | 0 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml (renamed from src/ValuesUtils.ml) | 0 | ||||
| -rw-r--r-- | compiler/aeneas.opam (renamed from aeneas.opam) | 0 | ||||
| -rw-r--r-- | compiler/driver.ml (renamed from src/driver.ml) | 0 | ||||
| -rw-r--r-- | compiler/dune (renamed from src/dune) | 0 | ||||
| -rw-r--r-- | compiler/dune-project (renamed from dune-project) | 0 | ||||
| -rw-r--r-- | compiler/fstar/Primitives.fst (renamed from fstar/Primitives.fst) | 0 |
57 files changed, 1 insertions, 1 deletions
diff --git a/src/.ocamlformat b/compiler/.ocamlformat index b0ae150e..b0ae150e 100644 --- a/src/.ocamlformat +++ b/compiler/.ocamlformat diff --git a/src/Assumed.ml b/compiler/Assumed.ml index cb089c08..cb089c08 100644 --- a/src/Assumed.ml +++ b/compiler/Assumed.ml diff --git a/src/Collections.ml b/compiler/Collections.ml index 0933b3e4..0933b3e4 100644 --- a/src/Collections.ml +++ b/compiler/Collections.ml diff --git a/src/ConstStrings.ml b/compiler/ConstStrings.ml index ae169a2e..ae169a2e 100644 --- a/src/ConstStrings.ml +++ b/compiler/ConstStrings.ml diff --git a/src/Contexts.ml b/compiler/Contexts.ml index 510976f4..510976f4 100644 --- a/src/Contexts.ml +++ b/compiler/Contexts.ml diff --git a/src/Cps.ml b/compiler/Cps.ml index c2c0363b..c2c0363b 100644 --- a/src/Cps.ml +++ b/compiler/Cps.ml diff --git a/src/Crates.ml b/compiler/Crates.ml index 844afb94..844afb94 100644 --- a/src/Crates.ml +++ b/compiler/Crates.ml diff --git a/src/Errors.ml b/compiler/Errors.ml index 31a53cf4..31a53cf4 100644 --- a/src/Errors.ml +++ b/compiler/Errors.ml diff --git a/src/Expressions.ml b/compiler/Expressions.ml index e2eaf1e7..e2eaf1e7 100644 --- a/src/Expressions.ml +++ b/compiler/Expressions.ml diff --git a/src/ExpressionsUtils.ml b/compiler/ExpressionsUtils.ml index c3ccfb15..c3ccfb15 100644 --- a/src/ExpressionsUtils.ml +++ b/compiler/ExpressionsUtils.ml diff --git a/src/ExtractToFStar.ml b/compiler/ExtractToFStar.ml index 5d212941..5d212941 100644 --- a/src/ExtractToFStar.ml +++ b/compiler/ExtractToFStar.ml diff --git a/src/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 248ad8b3..248ad8b3 100644 --- a/src/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml diff --git a/src/Identifiers.ml b/compiler/Identifiers.ml index b022b18d..b022b18d 100644 --- a/src/Identifiers.ml +++ b/compiler/Identifiers.ml diff --git a/src/Interpreter.ml b/compiler/Interpreter.ml index 7f51c5b9..7f51c5b9 100644 --- a/src/Interpreter.ml +++ b/compiler/Interpreter.ml diff --git a/src/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 30c3b221..30c3b221 100644 --- a/src/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml diff --git a/src/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index a5501712..a5501712 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml diff --git a/src/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 0ca34b43..0ca34b43 100644 --- a/src/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml diff --git a/src/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 62d9b80b..62d9b80b 100644 --- a/src/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml diff --git a/src/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index d54a046e..d54a046e 100644 --- a/src/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml diff --git a/src/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 064b8969..064b8969 100644 --- a/src/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml diff --git a/src/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 4e61e683..4e61e683 100644 --- a/src/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml diff --git a/src/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index e6033e9e..e6033e9e 100644 --- a/src/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml diff --git a/src/Invariants.ml b/compiler/Invariants.ml index 4a3364a6..4a3364a6 100644 --- a/src/Invariants.ml +++ b/compiler/Invariants.ml diff --git a/src/LlbcAst.ml b/compiler/LlbcAst.ml index 1b08f1ea..1b08f1ea 100644 --- a/src/LlbcAst.ml +++ b/compiler/LlbcAst.ml diff --git a/src/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 46711d0a..46711d0a 100644 --- a/src/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml diff --git a/src/LlbcOfJson.ml b/compiler/LlbcOfJson.ml index 79c9b756..79c9b756 100644 --- a/src/LlbcOfJson.ml +++ b/compiler/LlbcOfJson.ml diff --git a/src/Logging.ml b/compiler/Logging.ml index e83f25f8..e83f25f8 100644 --- a/src/Logging.ml +++ b/compiler/Logging.ml diff --git a/src/Meta.ml b/compiler/Meta.ml index f0e4ca04..f0e4ca04 100644 --- a/src/Meta.ml +++ b/compiler/Meta.ml diff --git a/src/Names.ml b/compiler/Names.ml index a27db161..a27db161 100644 --- a/src/Names.ml +++ b/compiler/Names.ml diff --git a/src/OfJsonBasic.ml b/compiler/OfJsonBasic.ml index 07daf03d..07daf03d 100644 --- a/src/OfJsonBasic.ml +++ b/compiler/OfJsonBasic.ml diff --git a/src/PrePasses.ml b/compiler/PrePasses.ml index a09ae476..a09ae476 100644 --- a/src/PrePasses.ml +++ b/compiler/PrePasses.ml diff --git a/src/Print.ml b/compiler/Print.ml index 03cab6ee..8f52b291 100644 --- a/src/Print.ml +++ b/compiler/Print.ml @@ -951,7 +951,7 @@ module LlbcAst = struct indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", " ^ T.VariantId.to_string variant_id ^ ")" - | A.Drop p -> indent ^ "drop(" ^ place_to_string fmt p ^ ")" + | A.Drop p -> indent ^ "drop " ^ place_to_string fmt p | A.Assert a -> let cond = operand_to_string fmt a.A.cond in if a.A.expected then indent ^ "assert(" ^ cond ^ ")" diff --git a/src/PrintPure.ml b/compiler/PrintPure.ml index a9e42f6c..a9e42f6c 100644 --- a/src/PrintPure.ml +++ b/compiler/PrintPure.ml diff --git a/src/Pure.ml b/compiler/Pure.ml index 77265f75..77265f75 100644 --- a/src/Pure.ml +++ b/compiler/Pure.ml diff --git a/src/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 3edae38a..3edae38a 100644 --- a/src/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml diff --git a/src/PureToExtract.ml b/compiler/PureToExtract.ml index 77c3afd4..77c3afd4 100644 --- a/src/PureToExtract.ml +++ b/compiler/PureToExtract.ml diff --git a/src/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index caad8a58..caad8a58 100644 --- a/src/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml diff --git a/src/PureUtils.ml b/compiler/PureUtils.ml index 39f3d76a..39f3d76a 100644 --- a/src/PureUtils.ml +++ b/compiler/PureUtils.ml diff --git a/src/Scalars.ml b/compiler/Scalars.ml index 03ca506c..03ca506c 100644 --- a/src/Scalars.ml +++ b/compiler/Scalars.ml diff --git a/src/StringUtils.ml b/compiler/StringUtils.ml index 0fd46136..0fd46136 100644 --- a/src/StringUtils.ml +++ b/compiler/StringUtils.ml diff --git a/src/Substitute.ml b/compiler/Substitute.ml index 5e5858de..5e5858de 100644 --- a/src/Substitute.ml +++ b/compiler/Substitute.ml diff --git a/src/SymbolicAst.ml b/compiler/SymbolicAst.ml index 604a7948..604a7948 100644 --- a/src/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml diff --git a/src/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index de4fb4c1..de4fb4c1 100644 --- a/src/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml diff --git a/src/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index a2256bdd..a2256bdd 100644 --- a/src/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml diff --git a/src/Translate.ml b/compiler/Translate.ml index 8f3b94c4..8f3b94c4 100644 --- a/src/Translate.ml +++ b/compiler/Translate.ml diff --git a/src/TranslateCore.ml b/compiler/TranslateCore.ml index a658147d..a658147d 100644 --- a/src/TranslateCore.ml +++ b/compiler/TranslateCore.ml diff --git a/src/Types.ml b/compiler/Types.ml index 326ef76f..326ef76f 100644 --- a/src/Types.ml +++ b/compiler/Types.ml diff --git a/src/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 60ce5149..60ce5149 100644 --- a/src/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml diff --git a/src/TypesUtils.ml b/compiler/TypesUtils.ml index 7531dd8b..7531dd8b 100644 --- a/src/TypesUtils.ml +++ b/compiler/TypesUtils.ml diff --git a/src/Utils.ml b/compiler/Utils.ml index a285e869..a285e869 100644 --- a/src/Utils.ml +++ b/compiler/Utils.ml diff --git a/src/Values.ml b/compiler/Values.ml index e404f40d..e404f40d 100644 --- a/src/Values.ml +++ b/compiler/Values.ml diff --git a/src/ValuesUtils.ml b/compiler/ValuesUtils.ml index 72d7abe0..72d7abe0 100644 --- a/src/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml diff --git a/aeneas.opam b/compiler/aeneas.opam index 4048f9a0..4048f9a0 100644 --- a/aeneas.opam +++ b/compiler/aeneas.opam diff --git a/src/driver.ml b/compiler/driver.ml index ae9d238a..ae9d238a 100644 --- a/src/driver.ml +++ b/compiler/driver.ml diff --git a/src/dune b/compiler/dune index e8b53fc5..e8b53fc5 100644 --- a/src/dune +++ b/compiler/dune diff --git a/dune-project b/compiler/dune-project index f8b418f2..f8b418f2 100644 --- a/dune-project +++ b/compiler/dune-project diff --git a/fstar/Primitives.fst b/compiler/fstar/Primitives.fst index b44fe9d1..b44fe9d1 100644 --- a/fstar/Primitives.fst +++ b/compiler/fstar/Primitives.fst |