From 79f5ad08070e158f79a0b805d4386e1f0ee54b8b Mon Sep 17 00:00:00 2001 From: John Tristan Date: Mon, 9 Sep 2024 08:54:16 -0400 Subject: [PATCH] Refactoring AST --- SHerLOC/AST/Basic.lean | 13 -- SHerLOC/AST/Constants.lean | 58 ------ SHerLOC/AST/Functions.lean | 25 --- SHerLOC/AST/Identifiers.lean | 22 --- SHerLOC/AST/Modules.lean | 21 -- SHerLOC/AST/Numbers.lean | 161 ---------------- SHerLOC/AST/Operations.lean | 55 ------ SHerLOC/AST/Programs.lean | 18 -- SHerLOC/AST/Types.lean | 96 ---------- SHerLOC/AST1.lean | 309 ++++++++++++++++++++++++++++++ SHerLOC/Basic.lean | 2 +- SHerLOC/Parsing/Constants.lean | 2 +- SHerLOC/Parsing/Functions.lean | 2 +- SHerLOC/Parsing/Identifiers.lean | 2 +- SHerLOC/Parsing/Intermediate.lean | 2 +- SHerLOC/Parsing/Modules.lean | 2 +- SHerLOC/Parsing/Numbers.lean | 2 +- SHerLOC/Parsing/Operations.lean | 2 +- SHerLOC/Parsing/Parser.lean | 2 +- SHerLOC/Parsing/Programs.lean | 2 +- SHerLOC/Parsing/Types.lean | 2 +- 21 files changed, 320 insertions(+), 480 deletions(-) delete mode 100644 SHerLOC/AST/Basic.lean delete mode 100644 SHerLOC/AST/Constants.lean delete mode 100644 SHerLOC/AST/Functions.lean delete mode 100644 SHerLOC/AST/Identifiers.lean delete mode 100644 SHerLOC/AST/Modules.lean delete mode 100644 SHerLOC/AST/Numbers.lean delete mode 100644 SHerLOC/AST/Operations.lean delete mode 100644 SHerLOC/AST/Programs.lean delete mode 100644 SHerLOC/AST/Types.lean create mode 100644 SHerLOC/AST1.lean diff --git a/SHerLOC/AST/Basic.lean b/SHerLOC/AST/Basic.lean deleted file mode 100644 index e24fa04..0000000 --- a/SHerLOC/AST/Basic.lean +++ /dev/null @@ -1,13 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Numbers -import SHerLOC.AST.Types -import SHerLOC.AST.Identifiers -import SHerLOC.AST.Constants -import SHerLOC.AST.Operations -import SHerLOC.AST.Functions -import SHerLOC.AST.Modules -import SHerLOC.AST.Programs diff --git a/SHerLOC/AST/Constants.lean b/SHerLOC/AST/Constants.lean deleted file mode 100644 index 49c8688..0000000 --- a/SHerLOC/AST/Constants.lean +++ /dev/null @@ -1,58 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Numbers -import SHerLOC.AST.Types - -/-! -# Constants - --/ - -namespace StableHLO - -structure Constant where - literal : Literal - typ : Option SType - deriving Repr, Inhabited, Nonempty - --- structure IntegerConstant where --- literal : IntegerLiteral --- type : IntegerType --- deriving Repr, Inhabited, Nonempty - --- structure FloatConstant where --- literal : FloatLiteral --- type : FloatType --- deriving Repr, Inhabited, Nonempty - --- structure NumberConstant where --- literal : FloatLiteral --- type : NumberType --- deriving Repr, Inhabited, Nonempty - --- structure ComplexConstant where --- literal : ComplexLiteral --- type : ComplexType --- deriving Repr, Inhabited, Nonempty - --- structure TensorConstant where --- literal : TensorLiteral --- type : TensorType --- deriving Repr, Inhabited, Nonempty - --- inductive Constant where --- | booleanConstant (literal : BooleanLiteral) --- | integerConstant (constant : IntegerConstant) --- | floatConstant (constant : FloatConstant) --- | numberConsant (constant : NumberConstant) --- | complexConstant (constant : ComplexConstant) --- | tensorConstant (constant : TensorConstant) --- | stringConstant (literal : String) --- | enumConstant (literal : EnumLiteral) --- | special -- For complicated dictionnary properties we do not parse yet --- deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST/Functions.lean b/SHerLOC/AST/Functions.lean deleted file mode 100644 index a49005f..0000000 --- a/SHerLOC/AST/Functions.lean +++ /dev/null @@ -1,25 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Types -import SHerLOC.AST.Identifiers -import SHerLOC.AST.Operations - -/-! -# Functions - --/ - -namespace StableHLO - -structure Function where - funcId : FuncId - funcArgAttrs : List (List Attribute) - funcResAttrs : List (List Attribute) - funcType : FunctionType - funcBody : InputFunc - deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST/Identifiers.lean b/SHerLOC/AST/Identifiers.lean deleted file mode 100644 index e99897a..0000000 --- a/SHerLOC/AST/Identifiers.lean +++ /dev/null @@ -1,22 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ - -/-! -# Identifiers - --/ - -namespace StableHLO - -abbrev FuncId := String - -abbrev ValueId := String - -abbrev UnusedId := String - -abbrev AttrId := String - -end StableHLO diff --git a/SHerLOC/AST/Modules.lean b/SHerLOC/AST/Modules.lean deleted file mode 100644 index 52fd59a..0000000 --- a/SHerLOC/AST/Modules.lean +++ /dev/null @@ -1,21 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Functions - -/-! -# Modules - --/ - -namespace StableHLO - -structure Module where - modId : Option FuncId - modAttrs : List Attribute - modFuncs : List Function - deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST/Numbers.lean b/SHerLOC/AST/Numbers.lean deleted file mode 100644 index fa7bdf3..0000000 --- a/SHerLOC/AST/Numbers.lean +++ /dev/null @@ -1,161 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Identifiers - -/-! -# Numbers - --/ - -namespace StableHLO - -inductive Signedness where - | signed - | unsigned - deriving Repr, Inhabited, Nonempty - -inductive IntegerSize where - | b2 - | b4 - | b8 - | b16 - | b32 - | b64 - deriving Repr, Inhabited, Nonempty - -inductive Sign where - | plus - | minus - deriving Repr, Inhabited, Nonempty - -structure IntegerLiteral where - sign : Sign - decimal : Nat - deriving Repr, Inhabited, Nonempty - -structure FloatLiteralDecimal where - integerPart : IntegerLiteral - fractionalPart : IntegerLiteral - scientificPart : IntegerLiteral - deriving Repr, Inhabited, Nonempty - -inductive FloatLiteral where - | decimal (literal : FloatLiteralDecimal) - | hexaDecimal (literal : Nat) - deriving Repr, Inhabited, Nonempty - -inductive BooleanLiteral where - | true - | false - deriving Repr, Inhabited, Nonempty - -structure ComplexLiteral where - real : FloatLiteral - imaginary : FloatLiteral - deriving Repr, Inhabited, Nonempty - -inductive ElementLiteral where - | booleanLiteral (literal : BooleanLiteral) - | floatLiteral (literal : FloatLiteral) - | complexLiteral (literal : ComplexLiteral) - deriving Repr, Inhabited, Nonempty - -inductive DenseLiteral where - | denseDimension (literal : List DenseLiteral) - | denseElements (literal : List ElementLiteral) - deriving Repr, Inhabited, Nonempty - -abbrev TensorLiteral := DenseLiteral - -inductive ComparisonDirection where - | eq - | ne - | ge - | gt - | le - | lt - deriving Repr, Inhabited, Nonempty - -inductive CompareType where - | float - | totalOrder - | signed - | unsigned - deriving Repr, Inhabited, Nonempty - -inductive PrecisionConfig where - | default - | high - | highest - deriving Repr, Inhabited, Nonempty - -inductive FftType where - | fft - | ifft - | rfft - | irfft - deriving Repr, Inhabited, Nonempty - -inductive ChannelType where - | deviceToDevice - | hostToDevice - deriving Repr, Inhabited, Nonempty - -inductive RngDistribution where - | uniform - | normal - deriving Repr, Inhabited, Nonempty - -inductive RngAlgorithm where - | default - | threeFry - | philox - deriving Repr, Inhabited, Nonempty - -inductive TransposeA where - | noTranspose - | transpose - | adjoint - deriving Repr, Inhabited, Nonempty - -inductive EnumLiteral where - | comparisonDirection (enum : ComparisonDirection) - | compareType (enum : CompareType) - | precisionConfig (enum : PrecisionConfig) - | fftType (enum : FftType) - | channelType (enum : ChannelType) - | rngDistribution (enum : RngDistribution) - | rngAlgorithm (enum : RngAlgorithm) - | transposeA (enum : TransposeA) - deriving Repr, Inhabited, Nonempty - -inductive ArrayLiteral where - | array64 (literal : List IntegerLiteral) - | array1 (literal : List BooleanLiteral) - deriving Repr, Inhabited, Nonempty - -structure ChannelHandle where - handle : Nat - typ : Nat - deriving Repr, Inhabited, Nonempty - -inductive Literal where - | enum (literal : EnumLiteral) - | element (literal : ElementLiteral) - | tensor (literal : TensorLiteral) - | string (literal : String) - - | use_global_device_ids - | array (literal : ArrayLiteral) - | special - | channelHandle (literal : ChannelHandle) - | experiment1 (literal : List FuncId) - | experiment2 (literal : List (List FuncId)) - | experiment3 (literal : List EnumLiteral) - | func (literal : FuncId) - deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST/Operations.lean b/SHerLOC/AST/Operations.lean deleted file mode 100644 index 5b5fa77..0000000 --- a/SHerLOC/AST/Operations.lean +++ /dev/null @@ -1,55 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Constants -import SHerLOC.AST.Identifiers -import SHerLOC.AST.Types - -/-! -# Operations - --/ - -namespace StableHLO - -structure Attribute where - id : AttrId - constant : Constant - deriving Repr, Inhabited, Nonempty - -structure FuncInput where - id : FuncId - typ : ValueType - deriving Repr, Inhabited, Nonempty - -mutual - - inductive InputFunc where - | mk - (funcInputs : List FuncInput) - (body : List Operation) - deriving Repr, Inhabited, Nonempty - - inductive Operation where - | stablehlo - (name : String) - (inputValues : List ValueId) - (inputFunctions : List InputFunc) - (inputAttributes : List Attribute) - (outputs : List ValueId) - (signature : FunctionType) - | return - (operands : List ValueId) - (signature : FunctionType) - | call - (callee : FuncId) - (inputValues : List ValueId) - (outputs : List ValueId) - (signature : FunctionType) - deriving Repr, Inhabited, Nonempty - -end - -end StableHLO diff --git a/SHerLOC/AST/Programs.lean b/SHerLOC/AST/Programs.lean deleted file mode 100644 index b806ea0..0000000 --- a/SHerLOC/AST/Programs.lean +++ /dev/null @@ -1,18 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Modules - -/-! -# Programs - --/ - -namespace StableHLO - -def Program := List Module - deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST/Types.lean b/SHerLOC/AST/Types.lean deleted file mode 100644 index 5872f90..0000000 --- a/SHerLOC/AST/Types.lean +++ /dev/null @@ -1,96 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SHerLOC.AST.Numbers - -/-! -# Types - --/ - -namespace StableHLO - -structure IntegerType where - sign : Signedness - size : IntegerSize - deriving Repr, Inhabited, Nonempty - -inductive FloatType where - | f8E4M3FN - | f8E5M2 - | f8E4M3FNUZ - | f8E5M2FNUZ - | f8E4M3B11FNUZ - | bf16 - | f16 - | f32 - | f64 - | tf32 - deriving Repr, Inhabited, Nonempty - -inductive NumberType where - | integerType (type : IntegerType) - | floatType (type: FloatType) - deriving Repr, Inhabited, Nonempty - -inductive ComplexType where - | f32 - | f64 - deriving Repr, Inhabited, Nonempty - -inductive TensorElementType where - | booleanType - | integerType (t : IntegerType) - | floatType (t: FloatType) - | complexType (t: ComplexType) - deriving Repr, Inhabited, Nonempty - -structure QuantizationParameter where - quantizationScale : FloatLiteral - quantizationZeroPoint: IntegerLiteral - deriving Repr, Inhabited, Nonempty - -structure QuantizedTensorElementType where - quantizationStorageType : IntegerType - quantizationStorageMinMax : Option (IntegerLiteral × IntegerLiteral) - quantizationExpressedType : FloatType - quantizationDimension : Option IntegerLiteral - quantizationParameters : List QuantizationParameter - deriving Repr, Inhabited, Nonempty - -inductive TensorElementTypeGen where - | classic (t : TensorElementType) - | quantized (t : QuantizedTensorElementType) - deriving Repr, Inhabited, Nonempty - -structure TensorType where - shape : List Nat - tensorElementTypeGen : TensorElementTypeGen - deriving Repr, Inhabited, Nonempty - -inductive ValueType where - | tensorType (tensor : TensorType) - | tokenType - | tupleType (elements : List ValueType) - deriving Repr, Inhabited, Nonempty - -structure FunctionType where - domain : List ValueType - range : List ValueType - deriving Repr, Inhabited, Nonempty - -inductive NonValueType where - | tensorElementType (t : TensorElementType) - | quantizedTensorElementType (t: QuantizedTensorElementType) - | functionType (t : FunctionType) - | stringType - deriving Repr, Inhabited, Nonempty - -inductive SType where - | valueType (t : ValueType) - | nonValueType (t : NonValueType) - deriving Repr, Inhabited, Nonempty - -end StableHLO diff --git a/SHerLOC/AST1.lean b/SHerLOC/AST1.lean new file mode 100644 index 0000000..3849c79 --- /dev/null +++ b/SHerLOC/AST1.lean @@ -0,0 +1,309 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jean-Baptiste Tristan +-/ + +/-! +# AST resulting from parsing + +-/ + +namespace StableHLO + +abbrev FuncId := String + +abbrev ValueId := String + +abbrev UnusedId := String + +abbrev AttrId := String + +inductive Signedness where + | signed + | unsigned + deriving Repr, Inhabited, Nonempty + +inductive IntegerSize where + | b2 + | b4 + | b8 + | b16 + | b32 + | b64 + deriving Repr, Inhabited, Nonempty + +inductive Sign where + | plus + | minus + deriving Repr, Inhabited, Nonempty + +structure IntegerLiteral where + sign : Sign + decimal : Nat + deriving Repr, Inhabited, Nonempty + +structure FloatLiteralDecimal where + integerPart : IntegerLiteral + fractionalPart : IntegerLiteral + scientificPart : IntegerLiteral + deriving Repr, Inhabited, Nonempty + +inductive FloatLiteral where + | decimal (literal : FloatLiteralDecimal) + | hexaDecimal (literal : Nat) + deriving Repr, Inhabited, Nonempty + +inductive BooleanLiteral where + | true + | false + deriving Repr, Inhabited, Nonempty + +structure ComplexLiteral where + real : FloatLiteral + imaginary : FloatLiteral + deriving Repr, Inhabited, Nonempty + +inductive ElementLiteral where + | booleanLiteral (literal : BooleanLiteral) + | floatLiteral (literal : FloatLiteral) + | complexLiteral (literal : ComplexLiteral) + deriving Repr, Inhabited, Nonempty + +inductive DenseLiteral where + | denseDimension (literal : List DenseLiteral) + | denseElements (literal : List ElementLiteral) + deriving Repr, Inhabited, Nonempty + +abbrev TensorLiteral := DenseLiteral + +inductive ComparisonDirection where + | eq + | ne + | ge + | gt + | le + | lt + deriving Repr, Inhabited, Nonempty + +inductive CompareType where + | float + | totalOrder + | signed + | unsigned + deriving Repr, Inhabited, Nonempty + +inductive PrecisionConfig where + | default + | high + | highest + deriving Repr, Inhabited, Nonempty + +inductive FftType where + | fft + | ifft + | rfft + | irfft + deriving Repr, Inhabited, Nonempty + +inductive ChannelType where + | deviceToDevice + | hostToDevice + deriving Repr, Inhabited, Nonempty + +inductive RngDistribution where + | uniform + | normal + deriving Repr, Inhabited, Nonempty + +inductive RngAlgorithm where + | default + | threeFry + | philox + deriving Repr, Inhabited, Nonempty + +inductive TransposeA where + | noTranspose + | transpose + | adjoint + deriving Repr, Inhabited, Nonempty + +inductive EnumLiteral where + | comparisonDirection (enum : ComparisonDirection) + | compareType (enum : CompareType) + | precisionConfig (enum : PrecisionConfig) + | fftType (enum : FftType) + | channelType (enum : ChannelType) + | rngDistribution (enum : RngDistribution) + | rngAlgorithm (enum : RngAlgorithm) + | transposeA (enum : TransposeA) + deriving Repr, Inhabited, Nonempty + +inductive ArrayLiteral where + | array64 (literal : List IntegerLiteral) + | array1 (literal : List BooleanLiteral) + deriving Repr, Inhabited, Nonempty + +structure ChannelHandle where + handle : Nat + typ : Nat + deriving Repr, Inhabited, Nonempty + +inductive Literal where + | enum (literal : EnumLiteral) + | element (literal : ElementLiteral) + | tensor (literal : TensorLiteral) + | string (literal : String) + + | use_global_device_ids + | array (literal : ArrayLiteral) + | special + | channelHandle (literal : ChannelHandle) + | experiment1 (literal : List FuncId) + | experiment2 (literal : List (List FuncId)) + | experiment3 (literal : List EnumLiteral) + | func (literal : FuncId) + deriving Repr, Inhabited, Nonempty + +structure IntegerType where + sign : Signedness + size : IntegerSize + deriving Repr, Inhabited, Nonempty + +inductive FloatType where + | f8E4M3FN + | f8E5M2 + | f8E4M3FNUZ + | f8E5M2FNUZ + | f8E4M3B11FNUZ + | bf16 + | f16 + | f32 + | f64 + | tf32 + deriving Repr, Inhabited, Nonempty + +inductive NumberType where + | integerType (type : IntegerType) + | floatType (type: FloatType) + deriving Repr, Inhabited, Nonempty + +inductive ComplexType where + | f32 + | f64 + deriving Repr, Inhabited, Nonempty + +inductive TensorElementType where + | booleanType + | integerType (t : IntegerType) + | floatType (t: FloatType) + | complexType (t: ComplexType) + deriving Repr, Inhabited, Nonempty + +structure QuantizationParameter where + quantizationScale : FloatLiteral + quantizationZeroPoint: IntegerLiteral + deriving Repr, Inhabited, Nonempty + +structure QuantizedTensorElementType where + quantizationStorageType : IntegerType + quantizationStorageMinMax : Option (IntegerLiteral × IntegerLiteral) + quantizationExpressedType : FloatType + quantizationDimension : Option IntegerLiteral + quantizationParameters : List QuantizationParameter + deriving Repr, Inhabited, Nonempty + +inductive TensorElementTypeGen where + | classic (t : TensorElementType) + | quantized (t : QuantizedTensorElementType) + deriving Repr, Inhabited, Nonempty + +structure TensorType where + shape : List Nat + tensorElementTypeGen : TensorElementTypeGen + deriving Repr, Inhabited, Nonempty + +inductive ValueType where + | tensorType (tensor : TensorType) + | tokenType + | tupleType (elements : List ValueType) + deriving Repr, Inhabited, Nonempty + +structure FunctionType where + domain : List ValueType + range : List ValueType + deriving Repr, Inhabited, Nonempty + +inductive NonValueType where + | tensorElementType (t : TensorElementType) + | quantizedTensorElementType (t: QuantizedTensorElementType) + | functionType (t : FunctionType) + | stringType + deriving Repr, Inhabited, Nonempty + +inductive SType where + | valueType (t : ValueType) + | nonValueType (t : NonValueType) + deriving Repr, Inhabited, Nonempty + +structure Constant where + literal : Literal + typ : Option SType + deriving Repr, Inhabited, Nonempty + +structure Attribute where + id : AttrId + constant : Constant + deriving Repr, Inhabited, Nonempty + +structure FuncInput where + id : FuncId + typ : ValueType + deriving Repr, Inhabited, Nonempty + +mutual + + inductive InputFunc where + | mk + (funcInputs : List FuncInput) + (body : List Operation) + deriving Repr, Inhabited, Nonempty + + inductive Operation where + | stablehlo + (name : String) + (inputValues : List ValueId) + (inputFunctions : List InputFunc) + (inputAttributes : List Attribute) + (outputs : List ValueId) + (signature : FunctionType) + | return + (operands : List ValueId) + (signature : FunctionType) + | call + (callee : FuncId) + (inputValues : List ValueId) + (outputs : List ValueId) + (signature : FunctionType) + deriving Repr, Inhabited, Nonempty + +end + +structure Function where + funcId : FuncId + funcArgAttrs : List (List Attribute) + funcResAttrs : List (List Attribute) + funcType : FunctionType + funcBody : InputFunc + deriving Repr, Inhabited, Nonempty + +structure Module where + modId : Option FuncId + modAttrs : List Attribute + modFuncs : List Function + deriving Repr, Inhabited, Nonempty + +def Program := List Module + deriving Repr, Inhabited, Nonempty + +end StableHLO diff --git a/SHerLOC/Basic.lean b/SHerLOC/Basic.lean index 6fd9fa4..77b5d18 100644 --- a/SHerLOC/Basic.lean +++ b/SHerLOC/Basic.lean @@ -3,5 +3,5 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Basic diff --git a/SHerLOC/Parsing/Constants.lean b/SHerLOC/Parsing/Constants.lean index d61c9d2..171bcb7 100644 --- a/SHerLOC/Parsing/Constants.lean +++ b/SHerLOC/Parsing/Constants.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Types diff --git a/SHerLOC/Parsing/Functions.lean b/SHerLOC/Parsing/Functions.lean index 69ca490..26251ed 100644 --- a/SHerLOC/Parsing/Functions.lean +++ b/SHerLOC/Parsing/Functions.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Operations import SHerLOC.Parsing.Intermediate diff --git a/SHerLOC/Parsing/Identifiers.lean b/SHerLOC/Parsing/Identifiers.lean index 3bee842..bb98791 100644 --- a/SHerLOC/Parsing/Identifiers.lean +++ b/SHerLOC/Parsing/Identifiers.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser namespace StableHLO diff --git a/SHerLOC/Parsing/Intermediate.lean b/SHerLOC/Parsing/Intermediate.lean index bd0f28f..b47a30c 100644 --- a/SHerLOC/Parsing/Intermediate.lean +++ b/SHerLOC/Parsing/Intermediate.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Identifiers import SHerLOC.Parsing.Types diff --git a/SHerLOC/Parsing/Modules.lean b/SHerLOC/Parsing/Modules.lean index 8b8f6e7..158d004 100644 --- a/SHerLOC/Parsing/Modules.lean +++ b/SHerLOC/Parsing/Modules.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Operations import SHerLOC.Parsing.Functions diff --git a/SHerLOC/Parsing/Numbers.lean b/SHerLOC/Parsing/Numbers.lean index 5d4e87e..ee4beae 100644 --- a/SHerLOC/Parsing/Numbers.lean +++ b/SHerLOC/Parsing/Numbers.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Identifiers diff --git a/SHerLOC/Parsing/Operations.lean b/SHerLOC/Parsing/Operations.lean index 571f02e..00c2e64 100644 --- a/SHerLOC/Parsing/Operations.lean +++ b/SHerLOC/Parsing/Operations.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Constants import SHerLOC.Parsing.Identifiers diff --git a/SHerLOC/Parsing/Parser.lean b/SHerLOC/Parsing/Parser.lean index 3427f5e..cffe6d6 100644 --- a/SHerLOC/Parsing/Parser.lean +++ b/SHerLOC/Parsing/Parser.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 namespace StableHLO diff --git a/SHerLOC/Parsing/Programs.lean b/SHerLOC/Parsing/Programs.lean index f57e5a4..8390cc2 100644 --- a/SHerLOC/Parsing/Programs.lean +++ b/SHerLOC/Parsing/Programs.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Modules diff --git a/SHerLOC/Parsing/Types.lean b/SHerLOC/Parsing/Types.lean index 2970531..73ad340 100644 --- a/SHerLOC/Parsing/Types.lean +++ b/SHerLOC/Parsing/Types.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SHerLOC.AST.Basic +import SHerLOC.AST1 import SHerLOC.Parsing.Parser import SHerLOC.Parsing.Numbers