Remove 'TypeEncodingKind'

ateleris · Sep 9, 2024 · c44f2b4 · c44f2b4
1 parent 40137f6
commit c44f2b4
Show file tree

Hide file tree

Showing 6 changed files with 120 additions and 210 deletions.
diff --git a/BackendAst/DAstACN.fs b/BackendAst/DAstACN.fs
diff --git a/BackendAst/DAstUPer.fs b/BackendAst/DAstUPer.fs
diff --git a/CommonTypes/FsUtils.fs b/CommonTypes/FsUtils.fs
@@ -393,8 +393,8 @@ module List =
         match xs with
         | [] -> None
         | x :: xs ->
-            match f(x) with
-            | Some(b) -> Some(b)
+            match f x with
+            | Some b -> Some b
             | None -> tryFindMap f xs
 
     let foldBackWith (f: 'a -> 's -> 's) (init: 'a -> 's) (xs: 'a list): 's =

diff --git a/FrontEndAst/DAst.fs b/FrontEndAst/DAst.fs
@@ -382,26 +382,8 @@ type Asn1IntegerEncodingType =
     | UnconstrainedMax of bigint
     | Unconstrained
 
-type TypeEncodingKind = // TODO: Alignment???
-    | Asn1IntegerEncodingType of Asn1IntegerEncodingType option // None if range min = max
-    | Asn1RealEncodingType of Asn1AcnAst.RealClass
-    | AcnIntegerEncodingType of AcnIntegerEncodingType
-    | AcnRealEncodingType of AcnRealEncodingType
-    | AcnBooleanEncodingType of AcnBooleanEncoding option
-    | AcnNullEncodingType of PATTERN_PROP_VALUE option
-    | AcnStringEncodingType of Asn1AcnAst.StringAcnEncodingClass
-    | AcnOctetStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
-    | AcnBitStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
-    | SequenceOfEncodingType of TypeEncodingKind * Asn1AcnAst.SizeableAcnEncodingClass
-    | SequenceEncodingType of TypeEncodingKind option list
-    | ChoiceEncodingType of TypeEncodingKind option list
-    | ReferenceEncodingType of string
-    | OptionEncodingType of TypeEncodingKind
-    | Placeholder
-
 /////////////////////////////////////////////////////////////////////
 
-
 type NestingScope = {
     acnOuterMaxSize: bigint
     uperOuterMaxSize: bigint
@@ -429,7 +411,6 @@ type UPERFuncBodyResult = {
     bValIsUnReferenced  : bool
     bBsIsUnReferenced   : bool
     resultExpr          : string option
-    typeEncodingKind    : TypeEncodingKind option
     auxiliaries         : string list
 }
 type UPerFunction = {
@@ -457,7 +438,6 @@ type AcnFuncBodyResult = {
     bValIsUnReferenced  : bool
     bBsIsUnReferenced   : bool
     resultExpr          : string option
-    typeEncodingKind    : TypeEncodingKind option
     auxiliaries         : string list
     icdResult           : IcdArgAux option
 }
@@ -843,7 +823,6 @@ and Asn1Child = {
     isEqualBodyStats            : CallerScope -> CallerScope -> (string*(LocalVariable list)) option
     Type                        : Asn1Type
     Optionality                 : Asn1AcnAst.Asn1Optionality option
-    // acnArgs                     : RelativePath list
     Comments                    : string array
 } with
     member this.toAsn1AcnAst: Asn1AcnAst.Asn1Child =
@@ -854,7 +833,6 @@ and Asn1Child = {
             _ada_name = this._ada_name
             Type = this.Type.toAsn1AcnAst
             Optionality = this.Optionality
-            // acnArgs = this.acnArgs
             asn1Comments = this.Comments |> Array.toList
             acnComments = []
         }

diff --git a/FrontEndAst/Language.fs b/FrontEndAst/Language.fs
@@ -55,18 +55,6 @@ type UncheckedAccessKind =
     | FullAccess // unwrap all selection, including the last one
     | PartialAccess // unwrap all but the last selection
 
-// TODO: Remove?
-type TypeInfo = {
-    uperMaxSizeBits: bigint
-    acnMaxSizeBits: bigint
-    typeKind: TypeEncodingKind option
-} with
-    member this.maxSize (enc: Asn1Encoding): bigint =
-        match enc with
-        | ACN -> this.acnMaxSizeBits
-        | UPER -> this.uperMaxSizeBits
-        | _ -> raise (BugErrorException $"Unexpected encoding: {enc}")
-
 type SequenceChildProps = {
     info: Asn1AcnAst.SeqChildInfo
     sel: Selection
@@ -100,9 +88,6 @@ type SequenceProofGen = {
         | UPER -> this.uperSiblingMaxSize
         | _ -> raise (BugErrorException $"Unexpected encoding: {enc}")
 
-    // member this.maxSize (enc: Asn1Encoding): BigInteger =
-    //     this.children |> List.map (fun c -> c.typeInfo.maxSize enc) |> List.sum
-
     member this.outerMaxSize (enc: Asn1Encoding): bigint =
         match enc with
         | ACN -> this.acnOuterMaxSize
@@ -183,7 +168,6 @@ type SequenceOfLikeProofGen = {
     nestingIx: bigint
     acnMaxOffset: bigint
     uperMaxOffset: bigint
-    typeInfo: TypeInfo
     nestingScope: NestingScope
     cs: CallerScope
     encDec: string option

diff --git a/StgScala/acn_scala.stg b/StgScala/acn_scala.stg
@@ -554,7 +554,6 @@ locally {
         assert(codec.base.bitStream.bitIndex \<= oldCodec.base.bitStream.bitIndex + <nSizeInBits>L)
         BitStream.validateOffsetBitsIneqLemma(oldCodec.base.bitStream, codec.base.bitStream, <nRemainingMinBits>, <nSizeInBits>L)
         check(codec.base.bitStream.bitIndex \<= codec_0_1.base.bitStream.bitIndex + <nAbsOffset>L + <nSizeInBits>L)
-        //check(codec.base.bitStream.bitIndex \<= codec_<nLevel>_<nIx>.base.bitStream.bitIndex + <nOffset>L + <nSizeInBits>L)
     }
 }
 <soCallAux>
@@ -575,7 +574,6 @@ val <p>_nCount = locally {
         assert(codec.base.bitStream.bitIndex \<= oldCodec.base.bitStream.bitIndex + <nSizeInBits>L)
         BitStream.validateOffsetBitsIneqLemma(oldCodec.base.bitStream, codec.base.bitStream, <nRemainingMinBits>, <nSizeInBits>L)
         check(codec.base.bitStream.bitIndex \<= codec_0_1.base.bitStream.bitIndex + <nAbsOffset>L + <nSizeInBits>L)
-        //check(codec.base.bitStream.bitIndex \<= codec_<nLevel>_<nIx>.base.bitStream.bitIndex + <nOffset>L + <nSizeInBits>L)
     }
     <p>_nCount
 }