From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/dune | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 6785cad4..db099c3c 100644 --- a/compiler/dune +++ b/compiler/dune @@ -12,6 +12,7 @@ (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) (libraries charon core_unix unionFind ocamlgraph) (modules + AssociatedTypes Assumed Collections Config -- cgit v1.2.3 From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 15:28:06 +0200 Subject: Map some globals like u32::MAX to standard definitions --- compiler/dune | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index db099c3c..2f5a0a44 100644 --- a/compiler/dune +++ b/compiler/dune @@ -22,6 +22,7 @@ Expressions ExpressionsUtils Extract + ExtractAssumed ExtractBase FunsAnalysis Identifiers -- cgit v1.2.3 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 2f5a0a44..4ec46b70 100644 --- a/compiler/dune +++ b/compiler/dune @@ -22,8 +22,8 @@ Expressions ExpressionsUtils Extract - ExtractAssumed ExtractBase + ExtractBuiltin FunsAnalysis Identifiers InterpreterBorrowsCore -- cgit v1.2.3 From ece74df70f12790bab7ecfe0c590c2c637e89801 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 11:40:31 +0200 Subject: Update following the addition of raw pointers --- compiler/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 4ec46b70..a4b09df4 100644 --- a/compiler/dune +++ b/compiler/dune @@ -92,4 +92,4 @@ -g ;-dsource -warn-error - -5-8-9-11-14-33-20-21-26-27-39))) + -5@8-9-11-14-33-20-21-26-27-39))) -- cgit v1.2.3 From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 18:44:28 +0200 Subject: Make the hashmap files typecheck again in Lean --- compiler/dune | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index a4b09df4..648c7325 100644 --- a/compiler/dune +++ b/compiler/dune @@ -24,6 +24,7 @@ Extract ExtractBase ExtractBuiltin + ExtractTypes FunsAnalysis Identifiers InterpreterBorrowsCore -- cgit v1.2.3 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/dune | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 648c7325..bc3cc718 100644 --- a/compiler/dune +++ b/compiler/dune @@ -57,6 +57,7 @@ Pure PureTypeCheck PureUtils + RegionsHierarchy ReorderDecls SCC Scalars -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/dune | 1 - 1 file changed, 1 deletion(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index bc3cc718..8a1edd02 100644 --- a/compiler/dune +++ b/compiler/dune @@ -47,7 +47,6 @@ LlbcOfJson Logging Meta - Names PrePasses Print PrintPure -- cgit v1.2.3 From 4972f21e4b25cc16e0839dc3d4a4a2d0552f872d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:17:50 +0100 Subject: Rename Driver.ml to Main.ml --- compiler/dune | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 8a1edd02..43ce86c8 100644 --- a/compiler/dune +++ b/compiler/dune @@ -1,9 +1,9 @@ (executable - (name driver) - (public_name aeneas_driver) + (name main) + (public_name aeneas_main) (package aeneas) (libraries aeneas) - (modules Driver)) + (modules Main)) (library (name aeneas) ;; The name as used in the project -- cgit v1.2.3 From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: Use the name matcher implemented in Charon --- compiler/dune | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 43ce86c8..39ad6260 100644 --- a/compiler/dune +++ b/compiler/dune @@ -10,7 +10,7 @@ (public_name aeneas) ;; The name as revealed to the projects importing this library (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) - (libraries charon core_unix unionFind ocamlgraph) + (libraries charon core_unix unionFind ocamlgraph str) (modules AssociatedTypes Assumed @@ -24,6 +24,7 @@ Extract ExtractBase ExtractBuiltin + ExtractName ExtractTypes FunsAnalysis Identifiers -- cgit v1.2.3 From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 12:15:37 +0100 Subject: Rename PrimitiveValues to Values --- compiler/dune | 2 -- 1 file changed, 2 deletions(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 39ad6260..4bba6a08 100644 --- a/compiler/dune +++ b/compiler/dune @@ -51,8 +51,6 @@ PrePasses Print PrintPure - PrimitiveValues - PrimitiveValuesUtils PureMicroPasses Pure PureTypeCheck -- cgit v1.2.3 From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 13:55:46 +0100 Subject: Add an `is_local` field to declarations --- compiler/dune | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 4bba6a08..0d0a8017 100644 --- a/compiler/dune +++ b/compiler/dune @@ -84,7 +84,7 @@ -g ;-dsource -warn-error - -5@8-9-11-14-33-20-21-26-27-39)) + -5@8-11-14-33-20-21-26-27-39)) (release (flags :standard @@ -92,4 +92,4 @@ -g ;-dsource -warn-error - -5@8-9-11-14-33-20-21-26-27-39))) + -5@8-11-14-33-20-21-26-27-39))) -- cgit v1.2.3 From d163bb804f3418ea8e2c89fe6e8d1c0587fd544b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 22 Nov 2023 14:52:15 +0100 Subject: Fix an issue with the nix flake and update the flake.lock --- compiler/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/dune') diff --git a/compiler/dune b/compiler/dune index 0d0a8017..3a40e086 100644 --- a/compiler/dune +++ b/compiler/dune @@ -1,6 +1,6 @@ (executable (name main) - (public_name aeneas_main) + (public_name aeneas) (package aeneas) (libraries aeneas) (modules Main)) -- cgit v1.2.3