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

module OWL2.Raw.Provenance where

open import Agda.Builtin.String using (primShowNat)
open import OWL2.Prelude

record SourcePath : Type₀ where
  constructor sourcePath
  field
    segments : List String

open SourcePath public

rootPath : SourcePath
rootPath =
  sourcePath []

fieldPath : String → SourcePath → SourcePath
fieldPath label path =
  sourcePath (segments path ++ label ∷ [])

indexPath : ℕ → SourcePath → SourcePath
indexPath index path =
  sourcePath (segments path ++ primShowNat index ∷ [])

record SourceHash : Type₀ where
  constructor mkSourceHash
  field
    algorithm : String
    digest    : String

open SourceHash public

record SourceProvenance : Type₀ where
  constructor sourceProvenance
  field
    sourceId   : String
    sourceHash : Optional SourceHash

open SourceProvenance public

anonymousSource : SourceProvenance
anonymousSource =
  sourceProvenance "" absent