From cc991aee7d91e0451ad7550b8fb5ec2323ae05f5 Mon Sep 17 00:00:00 2001 From: John Tristan Date: Tue, 20 Aug 2024 18:05:30 -0400 Subject: [PATCH] AST --- SHerLOC/Basic.lean | 2 +- SHerLOC/Syntax/Basic.lean | 11 --- SHerLOC/Syntax/Constants.lean | 25 ------ SHerLOC/Syntax/Functions.lean | 23 ----- SHerLOC/Syntax/Identifiers.lean | 18 ---- SHerLOC/Syntax/Operations.lean | 149 -------------------------------- SHerLOC/Syntax/Programs.lean | 17 ---- SHerLOC/Syntax/README.md | 1 - SHerLOC/Syntax/Types.lean | 77 ----------------- 9 files changed, 1 insertion(+), 322 deletions(-) delete mode 100644 SHerLOC/Syntax/Basic.lean delete mode 100644 SHerLOC/Syntax/Constants.lean delete mode 100644 SHerLOC/Syntax/Functions.lean delete mode 100644 SHerLOC/Syntax/Identifiers.lean delete mode 100644 SHerLOC/Syntax/Operations.lean delete mode 100644 SHerLOC/Syntax/Programs.lean delete mode 100644 SHerLOC/Syntax/README.md delete mode 100644 SHerLOC/Syntax/Types.lean diff --git a/SHerLOC/Basic.lean b/SHerLOC/Basic.lean index 952c72f..ca1ed6a 100644 --- a/SHerLOC/Basic.lean +++ b/SHerLOC/Basic.lean @@ -3,4 +3,4 @@ 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.Syntax.Basic +import SHerLOC.AST.Basic diff --git a/SHerLOC/Syntax/Basic.lean b/SHerLOC/Syntax/Basic.lean deleted file mode 100644 index cb25c1b..0000000 --- a/SHerLOC/Syntax/Basic.lean +++ /dev/null @@ -1,11 +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.Syntax.Types -import SHerLOC.Syntax.Identifiers -import SHerLOC.Syntax.Constants -import SHerLOC.Syntax.Operations -import SHerLOC.Syntax.Functions -import SHerLOC.Syntax.Programs diff --git a/SHerLOC/Syntax/Constants.lean b/SHerLOC/Syntax/Constants.lean deleted file mode 100644 index 4e0b149..0000000 --- a/SHerLOC/Syntax/Constants.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.Syntax.Types - -/-! -# Constants - --/ - -namespace STableHLO - -inductive Constant where - | booleanConstant (literal : Bool) - | integerConstant (literal : Int) (type : IntegerType) - | floatConstant (literal : Float) (type : FloatType) - | complexConstant (real imaginary : ComplexType) - | tensorConstant - | quantizedTensorConstant - | stringConstant (literal : String) - | enumConstant (choices : List String) - -end STableHLO diff --git a/SHerLOC/Syntax/Functions.lean b/SHerLOC/Syntax/Functions.lean deleted file mode 100644 index 5c4c153..0000000 --- a/SHerLOC/Syntax/Functions.lean +++ /dev/null @@ -1,23 +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.Syntax.Types -import SHerLOC.Syntax.Identifiers -import SHerLOC.Syntax.Operations - -/-! -# Functions - --/ - -namespace StableHLO - -structure Function where - funcId : FuncId - funcInputs : List (ValueId × ValueType) - funcOutputs : List ValueType - funcBody : List Operation - -end StableHLO diff --git a/SHerLOC/Syntax/Identifiers.lean b/SHerLOC/Syntax/Identifiers.lean deleted file mode 100644 index fbee4eb..0000000 --- a/SHerLOC/Syntax/Identifiers.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 --/ - -/-! -# Identifiers - --/ - -namespace StableHLO - -def FuncId := Nat -def ValueId := Nat -def UnusedId := Nat - -end StableHLO diff --git a/SHerLOC/Syntax/Operations.lean b/SHerLOC/Syntax/Operations.lean deleted file mode 100644 index 613c338..0000000 --- a/SHerLOC/Syntax/Operations.lean +++ /dev/null @@ -1,149 +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.Syntax.Constants -import SHerLOC.Syntax.Identifiers -import SHerLOC.Syntax.Types - -/-! -# Operations - --/ - -namespace StableHLO - -inductive OpName where - | abs - | add - | after_all - | all_gather - | all_reduce - | all_to_all - | and - | atan2 - | batch_norm_grad - | batch_norm_inference - | batch_norm_training - | bitcast_convert - | broadcast_in_dim - | case - | cbrt - | ceil - | cholesky - | clamp - | collective_broadcast - | collective_permute - | compare - | complex - | composite - | concatenate - | constant - | convert - | convolution - | cosine - | count_leading_zeros - | custom_call - | divide - | dot_general - | dynamic_broadcast_in_dim - | dynamic_conv - | dynamic_gather - | dynamic_iota - | dynamic_pad - | dynamic_reshape - | dynamic_slice - | dynamic_update_slice - | exponential - | exponential_minus_one - | fft - | floor - | gather - | get_dimension_size - | get_tuple_element - | if - | imag - | infeed - | iota - | is_finite - | log - | log_plus_one - | logistic - | map - | maximum - | minimum - | multiply - | negate - | not - | optimization_barrier - | or - | outfeed - | pad - | partition_id - | popcnt - | power - | real - | recv - | reduce - | reduce_precision - | reduce_scatter - | reduce_window - | remainder - | replica_id - | reshape - | reverse - | rng - | rng_bit_generator - | round_nearest_afz - | round_nearest_even - | rsqrt - | scatter - | select - | select_and_scatter - | send - | shift_left - | shift_right_arithmetic - | shift_right_logical - | sign - | sine - | slice - | sort - | sqrt - | subtract - | tan - | tanh - | transpose - | triangular_solve - | tuple - | uniform_dequantize - | uniform_quantize - | while - | xor - -mutual - - inductive InputFunc where - | mk - (id : UnusedId) - (funcInputs : List ValueId) - (body : List Operation) - - inductive Operation where - | stable - (name : OpName)(inputValues : List ValueId) - (inputFunctions : List InputFunc) - (inputAttributes : List Constant) - (outputs : List ValueId) - (signature : FunctionType) - | return - (operands : ValueId) - (signature : ValueType) - | call - (callee : FuncId) - (arguments : ValueId) - (signature : FunctionType) - -end - -end StableHLO diff --git a/SHerLOC/Syntax/Programs.lean b/SHerLOC/Syntax/Programs.lean deleted file mode 100644 index fe304b3..0000000 --- a/SHerLOC/Syntax/Programs.lean +++ /dev/null @@ -1,17 +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.Syntax.Functions - -/-! -# Programs - --/ - -namespace StableHLO - -def Program := List Function - -end StableHLO diff --git a/SHerLOC/Syntax/README.md b/SHerLOC/Syntax/README.md deleted file mode 100644 index 01dbcd3..0000000 --- a/SHerLOC/Syntax/README.md +++ /dev/null @@ -1 +0,0 @@ -# Notes diff --git a/SHerLOC/Syntax/Types.lean b/SHerLOC/Syntax/Types.lean deleted file mode 100644 index 8ff0b15..0000000 --- a/SHerLOC/Syntax/Types.lean +++ /dev/null @@ -1,77 +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 --/ - -/-! -# Types - --/ - -namespace StableHLO - -inductive Signedness where - | signed - | unsigned - -inductive IntegerSize where - | b2 - | b4 - | b8 - | b16 - | b32 - | b64 - -structure IntegerType where - sign : Signedness - size : IntegerSize - -inductive FloatType where - | f8E4M3FN - | f8E5M2 - | f8E4M3FNUZ - | f8E5M2FNUZ - | f8E4M3B11FNUZ - | bf16 - | f16 - | f32 - | f64 - | tf32 - -inductive ComplexType where - | f32 - | f64 - -inductive TensorElementType where - | booleanType - | integerType (t : IntegerType) - | floatType (t: FloatType) - | complexType (t: ComplexType) - -inductive QuantizedTensorElementType where - | quant : Signedness → IntegerSize → Int → Int → FloatSize → Int → List (Float × Int) → QuantizedTensorElementType - -inductive ValueType where - | tensorType (shape : List Int) (typ : TensorElementType) - | quantizedTensorType (shape : List Int) (typ : QuantizedTensorElementType) - | tokenType - | tupleType (elements : List Valuetype) - -inductive StringType where - -structure FunctionType where - domain : List ValueType - range : List ValueType - -inductive NonValueType where - | tensorElementType (t : TensorElementType) - | quantizedTensorElementType (t: QuantizedTensorElementType) - | functionType (t : FunctionType) - | stringType (t : StringType) - -inductive SType where - | valueType (t : ValueType) - | nonValueType (t : NonValueType) - -end StableHLO