Documentation

Cedar.SymCC.Symbolizer

This file contains functions to encode a concrete Env into a SymEnv, which can also be thought of as an "inverse" of concretization.

source
def Cedar.Spec.Prim.symbolize :
Prim → SymCC.Term
Equations
Instances For
    source
    @[irreducible]
    def Cedar.Spec.Value.symbolize? (v : Value) (ty : Validation.CedarType) :
    Option SymCC.Term

    Encodes a Value as a Term assuming it is of a certain type

    Equations
    Instances For
      source
      @[irreducible]
      def Cedar.Spec.Value.symbolize?.symbolizeAttr? (rec : Data.Map Attr Value) (a : Attr) (qty : Validation.QualifiedType) :
      Option (Attr × SymCC.Term)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cedar.Spec.Request.symbolize? (req : Request) (Γ : Validation.TypeEnv) (var : SymCC.TermVar) :
        Option SymCC.Term

        The variable ids here should match the variables in SymRequest.ofRequestType.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cedar.Spec.defaultEidOf (Γ : Validation.TypeEnv) (ety : EntityType) :
          String
          Equations
          Instances For
            source
            def Cedar.Spec.defaultLitWithDefaultEid (Γ : Validation.TypeEnv) (ty : SymCC.TermType) :
            SymCC.Term
            Equations
            Instances For
              source
              def Cedar.Spec.Entities.symbolizeAttrs? (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) (entry : Validation.EntitySchemaEntry) (uuf : SymCC.UUF) :
              Option SymCC.UDF

              Generates an interpretation of the attribute map.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cedar.Spec.Entities.symbolizeAttrs?.udf (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) (entry : Validation.EntitySchemaEntry) :
                SymCC.UDF
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Cedar.Spec.Entities.symbolizeTags? (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) (entry : Validation.EntitySchemaEntry) (uuf : SymCC.UUF) :
                  Option SymCC.UDF

                  Generates interpretations for the tag key and value maps.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cedar.Spec.Entities.symbolizeTags?.keysUDF (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) :
                    SymCC.UDF
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Cedar.Spec.Entities.symbolizeTags?.valsUDF (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) (tagTy : Validation.CedarType) :
                      SymCC.UDF
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Cedar.Spec.Entities.symbolizeAncs? (entities : Entities) (Γ : Validation.TypeEnv) (ety : EntityType) (entry : Validation.EntitySchemaEntry) (uuf : SymCC.UUF) :
                        Option SymCC.UDF

                        Generates an interpretation for the ancestor map.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Cedar.Spec.Entities.symbolizeAncs?.udf (entities : Entities) (Γ : Validation.TypeEnv) (ety ancTy : EntityType) :
                          SymCC.UDF
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Cedar.Spec.Entities.symbolize? (entities : Entities) (Γ : Validation.TypeEnv) (uuf : SymCC.UUF) :
                            Option SymCC.UDF

                            Symbolizes a concrete Entities into (part of) an Interpretation of SymEnv.ofEnv Γ. The UUF ids here should match those in SymEntityData.ofStandardEntityType.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Cedar.Spec.Env.symbolize? (env : Env) (Γ : Validation.TypeEnv) :
                              SymCC.Interpretation

                              Converts an Env (assumed to be a well-typed instance of TypeEnv) into an Interpretation of SymEnv.ofEnv Γ.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For