{-# OPTIONS --safe --cubical #-}

module OWL2.Elab.Policy where

open import OWL2.Prelude

data ImportMode : Type₀ where
  strict :
    ImportMode
  compatibility :
    ImportMode
  annotationOnly :
    ImportMode

record ImportPolicy : Type₀ where
  constructor importPolicy
  field
    mode :
      ImportMode
    allowUnknownPropertyKinds :
      Bool
    allowUnresolvedReferences :
      Bool
    allowLossyMappings :
      Bool

open ImportPolicy public

strictPolicy : ImportPolicy
strictPolicy =
  importPolicy strict false false false

compatibilityPolicy : ImportPolicy
compatibilityPolicy =
  importPolicy compatibility true false true

annotationOnlyPolicy : ImportPolicy
annotationOnlyPolicy =
  importPolicy annotationOnly true true false

record ImportPolicyEvidence (policy : ImportPolicy) : Type₀ where
  constructor importPolicyEvidence
  field
    recordedMode :
      ImportMode
    recordedAllowUnknownPropertyKinds :
      Bool
    recordedAllowUnresolvedReferences :
      Bool
    recordedAllowLossyMappings :
      Bool
    modeRecorded :
      recordedMode ≡ mode policy
    unknownPropertyKindsRecorded :
      recordedAllowUnknownPropertyKinds ≡ allowUnknownPropertyKinds policy
    unresolvedReferencesRecorded :
      recordedAllowUnresolvedReferences ≡ allowUnresolvedReferences policy
    lossyMappingsRecorded :
      recordedAllowLossyMappings ≡ allowLossyMappings policy

open ImportPolicyEvidence public

trivialPolicyEvidence : (policy : ImportPolicy) → ImportPolicyEvidence policy
trivialPolicyEvidence policy =
  importPolicyEvidence
    (mode policy)
    (allowUnknownPropertyKinds policy)
    (allowUnresolvedReferences policy)
    (allowLossyMappings policy)
    refl
    refl
    refl
    refl