Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CN: Error on unused modules #780

Merged
merged 1 commit into from
Dec 20, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion backend/cn/bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(public_name cn)
(package cn)
(flags
(:standard -w -37 -open Monomorphic.Int))
(:standard -w @60 -open Monomorphic.Int))
(libraries
cerb_backend
cerb_frontend
Expand Down
3 changes: 0 additions & 3 deletions backend/cn/lib/core_to_mucore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module Ctype = CF.Ctype
module BT = BaseTypes
module C = Compile
module IT = IndexTerms
module IdMap = Map.Make (Id)
module SBT = BaseTypes.Surface
module Mu = Mucore

Expand Down Expand Up @@ -849,9 +848,7 @@ let rec n_expr
| Eexcluded _ -> assert_error loc !^"core_anormalisation: Eexcluded"


module RT = ReturnTypes
module AT = ArgumentTypes
module LRT = LogicalReturnTypes
module LAT = LogicalArgumentTypes

let rec lat_of_arguments f_i = function
Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/definition.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
module IT = IndexTerms
module AT = ArgumentTypes
module LAT = LogicalArgumentTypes

module Function = struct
Expand Down
2 changes: 1 addition & 1 deletion backend/cn/lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(name cn)
(public_name cn)
(flags
(:standard -w -37 -open Monomorphic.Int))
(:standard -w @60 -open Monomorphic.Int))
(libraries
cerb_backend
cerb_frontend
Expand Down
6 changes: 0 additions & 6 deletions backend/cn/lib/explain.ml
Original file line number Diff line number Diff line change
@@ -1,16 +1,10 @@
open Report
module IT = IndexTerms
module BT = BaseTypes
module Res = Resource
module Def = Definition
module Req = Request
module LC = LogicalConstraints
module LF = Definition.Function
module LAT = LogicalArgumentTypes
module StringMap = Map.Make (String)
module C = Context
module Loc = Locations
module S = Solver
open Request
open IndexTerms
open Pp
Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/request.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
open Pp.Infix
module IT = IndexTerms
module BT = BaseTypes

let pp_maybe_oargs = function None -> Pp.empty | Some oargs -> Pp.parens (IT.pp oargs)

Expand Down
4 changes: 0 additions & 4 deletions backend/cn/lib/solver.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
module SMT = Simple_smt
module IT = IndexTerms
open IndexTerms
module BT = BaseTypes
open BaseTypes
module LC = LogicalConstraints
open LogicalConstraints
Expand All @@ -17,8 +15,6 @@ module Int_BT_Table = Map.Make (struct
BT.compare bt1 bt2
end)

module BT_Table = Hashtbl.Make (BT)

module IntWithHash = struct
(* For compatability with older ocamls *)
include Int
Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/testGeneration/genCodeGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ module Utils = Executable_spec_utils
module BT = BaseTypes
module IT = IndexTerms
module LC = LogicalConstraints
module GT = GenTerms
module GR = GenRuntime

let mk_expr = Utils.mk_expr
Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/testGeneration/genCompile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ module GBT = GenBaseTypes
module GT = GenTerms
module GD = GenDefinitions
module Config = TestGenConfig
module CtA = Cn_internal_to_ail

type s = GD.context

Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/testGeneration/genDistribute.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ module IT = IndexTerms
module LC = LogicalConstraints
module GT = GenTerms
module GD = GenDefinitions
module GA = GenAnalysis
module Config = TestGenConfig

let generated_size (bt : BT.t) : int =
Expand Down
1 change: 0 additions & 1 deletion backend/cn/lib/testGeneration/specTests.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module CF = Cerb_frontend
module A = CF.AilSyntax
module C = CF.Ctype
module BT = BaseTypes
module AT = ArgumentTypes
module LAT = LogicalArgumentTypes
module CtA = Cn_internal_to_ail
Expand Down
2 changes: 0 additions & 2 deletions backend/cn/lib/typing.ml
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
open Context
module IT = IndexTerms
module ITSet = Set.Make (IT)
module Req = Request
module Res = Resource
open TypeErrors

type solver = Solver.solver
Expand Down