Skip to content

Rename DL folder to Dialects #247

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.

Sign up for GitHub

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

Open
keyboardDrummer wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Rename DL folder to Dialects #247

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions Strata.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ import Strata.DDM.Integration.Lean
import Strata.DDM.Ion

/- Dialect Library -/
import Strata.DL.SMT.SMT
import Strata.DL.Lambda.Lambda
import Strata.DL.Imperative.Imperative
import Strata.Dialects.SMT.SMT
import Strata.Dialects.Lambda.Lambda
import Strata.Dialects.Imperative.Imperative

/- Boogie -/
import Strata.Languages.Boogie.Examples.Examples
Expand Down
2 changes: 1 addition & 1 deletion Strata/Backends/CBMC/BoogieToCBMC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import Lean.Data.Json
import Strata.Languages.Boogie.Env
import Strata.Languages.Boogie.DDMTransform.Parse
import Strata.Languages.Boogie.DDMTransform.Translate
import Strata.DL.Util.Map
import Strata.Dialects.Util.Map
import Strata.Languages.Boogie.Boogie
import Strata.Backends.CBMC.Common

Expand Down
2 changes: 1 addition & 1 deletion Strata/Backends/CBMC/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
-/

import Lean.Data.Json
import Strata.DL.Util.Map
import Strata.Dialects.Util.Map

-------------------------------------------------------------------------------

Expand Down
2 changes: 1 addition & 1 deletion Strata/Backends/CBMC/StrataToCBMC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
-/

import Lean.Data.Json
import Strata.DL.Util.Map
import Strata.Dialects.Util.Map
import Strata.Languages.C_Simp.C_Simp
import Strata.Languages.C_Simp.Verify
import Strata.Backends.CBMC.Common
Expand Down
22 changes: 0 additions & 22 deletions Strata/DL/Imperative/Imperative.lean
View file
Open in desktop

This file was deleted.

15 changes: 0 additions & 15 deletions Strata/DL/SMT/SMT.lean
View file
Open in desktop

This file was deleted.

8 changes: 4 additions & 4 deletions Strata/DL/Imperative/Cmd.lean → Strata/Dialects/Imperative/Cmd.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.PureExpr
import Strata.DL.Imperative.MetaData
import Strata.DL.Imperative.HasVars
import Strata.DL.Lambda.LExpr
import Strata.Dialects.Imperative.PureExpr
import Strata.Dialects.Imperative.MetaData
import Strata.Dialects.Imperative.HasVars
import Strata.Dialects.Lambda.LExpr

---------------------------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Imperative/CmdEval.lean → Strata/Dialects/Imperative/CmdEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@



import Strata.DL.Imperative.Cmd
import Strata.DL.Imperative.EvalContext
import Strata.Dialects.Imperative.Cmd
import Strata.Dialects.Imperative.EvalContext

namespace Imperative
open Std (ToFormat Format format)
Expand Down
8 changes: 4 additions & 4 deletions Strata/DL/Imperative/CmdSemantics.lean → Strata/Dialects/Imperative/CmdSemantics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.Stmt
import Strata.DL.Imperative.HasVars
import Strata.DL.Util.Map
import Strata.DL.Util.ListUtils
import Strata.Dialects.Imperative.Stmt
import Strata.Dialects.Imperative.HasVars
import Strata.Dialects.Util.Map
import Strata.Dialects.Util.ListUtils

---------------------------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Imperative/CmdType.lean → Strata/Dialects/Imperative/CmdType.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@



import Strata.DL.Imperative.Cmd
import Strata.DL.Imperative.TypeContext
import Strata.Dialects.Imperative.Cmd
import Strata.Dialects.Imperative.TypeContext

namespace Imperative
open Std (ToFormat Format format)
Expand Down
10 changes: 5 additions & 5 deletions Strata/DL/Imperative/EvalContext.lean → Strata/Dialects/Imperative/EvalContext.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@



import Strata.DL.Imperative.Cmd
import Strata.DL.Imperative.EvalError
import Strata.DL.Imperative.MetaData
import Strata.DL.Util.ListMap
import Strata.DL.Util.Maps
import Strata.Dialects.Imperative.Cmd
import Strata.Dialects.Imperative.EvalError
import Strata.Dialects.Imperative.MetaData
import Strata.Dialects.Util.ListMap
import Strata.Dialects.Util.Maps

namespace Imperative
open Std (ToFormat Format format)
Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/EvalError.lean → Strata/Dialects/Imperative/EvalError.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@



import Strata.DL.Imperative.PureExpr
import Strata.Dialects.Imperative.PureExpr

namespace Imperative
open Std (ToFormat Format format)
Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/HasVars.lean → Strata/Dialects/Imperative/HasVars.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.PureExpr
import Strata.Dialects.Imperative.PureExpr

-- open Imperative Boogie
namespace Imperative
Expand Down
22 changes: 22 additions & 0 deletions Strata/Dialects/Imperative/Imperative.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
/-
Copyright Strata Contributors

SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.Dialects.Imperative.PureExpr
import Strata.Dialects.Imperative.HasVars
import Strata.Dialects.Imperative.MetaData

import Strata.Dialects.Imperative.CmdEval
import Strata.Dialects.Imperative.CmdType
import Strata.Dialects.Imperative.CmdSemantics
import Strata.Dialects.Imperative.StmtSemantics
import Strata.Dialects.Imperative.StmtSemanticsSmallStep

import Strata.Dialects.Imperative.NondetStmt
import Strata.Dialects.Imperative.NondetStmtSemantics

import Strata.Dialects.Imperative.SemanticsProps

import Strata.Dialects.Imperative.SMTUtils
4 changes: 2 additions & 2 deletions Strata/DL/Imperative/MetaData.lean → Strata/Dialects/Imperative/MetaData.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.PureExpr
import Strata.DL.Util.DecidableEq
import Strata.Dialects.Imperative.PureExpr
import Strata.Dialects.Util.DecidableEq

namespace Imperative

Expand Down
6 changes: 3 additions & 3 deletions Strata/DL/Imperative/NondetStmt.lean → Strata/Dialects/Imperative/NondetStmt.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,9 @@



import Strata.DL.Imperative.MetaData
import Strata.DL.Imperative.Stmt
import Strata.DL.Imperative.HasVars
import Strata.Dialects.Imperative.MetaData
import Strata.Dialects.Imperative.Stmt
import Strata.Dialects.Imperative.HasVars

---------------------------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions ...ta/DL/Imperative/NondetStmtSemantics.lean → ...lects/Imperative/NondetStmtSemantics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.CmdSemantics
import Strata.DL.Imperative.NondetStmt
import Strata.Dialects.Imperative.CmdSemantics
import Strata.Dialects.Imperative.NondetStmt

---------------------------------------------------------------------

Expand Down
0 Strata/DL/Imperative/PureExpr.lean → Strata/Dialects/Imperative/PureExpr.lean
View file
Open in desktop
File renamed without changes.
6 changes: 3 additions & 3 deletions Strata/DL/Imperative/SMTUtils.lean → Strata/Dialects/Imperative/SMTUtils.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.SMT.SMT
import Strata.DL.Imperative.PureExpr
import Strata.DL.Imperative.EvalContext
import Strata.Dialects.SMT.SMT
import Strata.Dialects.Imperative.PureExpr
import Strata.Dialects.Imperative.EvalContext

namespace Imperative
open Std (ToFormat Format format)
Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Imperative/SemanticsProps.lean → ...a/Dialects/Imperative/SemanticsProps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.CmdSemantics
import Strata.DL.Imperative.StmtSemantics
import Strata.Dialects.Imperative.CmdSemantics
import Strata.Dialects.Imperative.StmtSemantics

namespace Imperative

Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/Stmt.lean → Strata/Dialects/Imperative/Stmt.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@



import Strata.DL.Imperative.Cmd
import Strata.Dialects.Imperative.Cmd

namespace Imperative
---------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/StmtSemantics.lean → ...ta/Dialects/Imperative/StmtSemantics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@



import Strata.DL.Imperative.CmdSemantics
import Strata.Dialects.Imperative.CmdSemantics

---------------------------------------------------------------------

Expand Down
2 changes: 1 addition & 1 deletion ...DL/Imperative/StmtSemanticsSmallStep.lean → ...ts/Imperative/StmtSemanticsSmallStep.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Imperative.CmdSemantics
import Strata.Dialects.Imperative.CmdSemantics

---------------------------------------------------------------------

Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/ToCProverGOTO.lean → ...ta/Dialects/Imperative/ToCProverGOTO.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
-/

import Strata.Backends.CBMC.GOTO.Program
import Strata.DL.Imperative.Imperative
import Strata.Dialects.Imperative.Imperative

open Std (ToFormat Format format)

Expand Down
2 changes: 1 addition & 1 deletion Strata/DL/Imperative/TypeContext.lean → Strata/Dialects/Imperative/TypeContext.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@



import Strata.DL.Imperative.Cmd
import Strata.Dialects.Imperative.Cmd

namespace Imperative
open Std (ToFormat Format format)
Expand Down
12 changes: 6 additions & 6 deletions Strata/DL/Lambda/Factory.lean → Strata/Dialects/Lambda/Factory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,21 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LExprWF
import Strata.DL.Lambda.LTy
import Strata.DL.Util.ListMap
import Strata.Dialects.Lambda.LExprWF
import Strata.Dialects.Lambda.LTy
import Strata.Dialects.Util.ListMap

/-!
## Lambda's Factory

This module formalizes Lambda's _factory_, which is a mechanism to extend the
type checker (see `Strata.DL.Lambda.LExprT`) and partial evaluator (see
`Strata.DL.Lambda.LExprEval`) by providing a map from operations to their types
type checker (see `Strata.Dialects.Lambda.LExprT`) and partial evaluator (see
`Strata.Dialects.Lambda.LExprEval`) by providing a map from operations to their types
and optionally, denotations. The factory allows adding type checking and
evaluation support for new operations without modifying the implementation of
either or any core ASTs.

Also see `Strata.DL.Lambda.IntBoolFactory` for a concrete example of a factory.
Also see `Strata.Dialects.Lambda.IntBoolFactory` for a concrete example of a factory.
-/


Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Lambda/Identifiers.lean → Strata/Dialects/Lambda/Identifiers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@



import Strata.DL.Lambda.LTy
import Strata.DL.Util.Map
import Strata.Dialects.Lambda.LTy
import Strata.Dialects.Util.Map

---------------------------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Lambda/IntBoolFactory.lean → Strata/Dialects/Lambda/IntBoolFactory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LState
import Strata.Dialects.Lambda.LState

/-! ## A Minimal Factory with Support for Unbounded Integer and Boolean Operations

See also `Strata.DL.Lambda.Factory`.
See also `Strata.Dialects.Lambda.Factory`.
-/

---------------------------------------------------------------------
Expand Down
10 changes: 5 additions & 5 deletions Strata/DL/Lambda/LExpr.lean → Strata/Dialects/Lambda/LExpr.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LTy
import Strata.DL.Lambda.Identifiers
import Strata.DL.Lambda.MetaData
import Strata.DL.Util.DecidableEq
import Strata.Dialects.Lambda.LTy
import Strata.Dialects.Lambda.Identifiers
import Strata.Dialects.Lambda.MetaData
import Strata.Dialects.Util.DecidableEq

/-! ## Lambda Expressions with Quantifiers

Lambda expressions are formalized by the inductive type `LExpr`. Type
formalization is described in `Strata.DL.Lambda.LTy`.
formalization is described in `Strata.Dialects.Lambda.LTy`.
-/

---------------------------------------------------------------------
Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Lambda/LExprEval.lean → Strata/Dialects/Lambda/LExprEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LExprWF
import Strata.DL.Lambda.LState
import Strata.Dialects.Lambda.LExprWF
import Strata.Dialects.Lambda.LState

/-! ## Partial evaluator for Lambda expressions

Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Lambda/LExprT.lean → Strata/Dialects/Lambda/LExprT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LExprTypeEnv
import Strata.DL.Lambda.LExprWF
import Strata.Dialects.Lambda.LExprTypeEnv
import Strata.Dialects.Lambda.LExprWF

/-! ## Type Inference Transform for Lambda Expressions.

Expand Down
4 changes: 2 additions & 2 deletions Strata/DL/Lambda/LExprType.lean → Strata/Dialects/Lambda/LExprType.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@
SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import Strata.DL.Lambda.LExprTypeSpec
import Strata.DL.Lambda.LExprT
import Strata.Dialects.Lambda.LExprTypeSpec
import Strata.Dialects.Lambda.LExprT
Loading
Loading