{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.Domain where

open import SemanticExplanation.Base
open import SemanticExplanation.IR using (AtomSurface ; ExprSurface)
open import Agda.Builtin.Reflection using (Name ; primQNameEquality)

data ArgRole : Set where
  semanticExpression : ArgRole
  infrastructureArgument : ArgRole

record EntityRule : Set where
  constructor entity-rule
  field
    ruleId : String
    head : Name
    roles : List ArgRole
    word : String

record PredicateRule : Set where
  constructor predicate-rule
  field
    ruleId : String
    head : Name
    roles : List ArgRole
    surface : AtomSurface

record ExpressionRule : Set where
  constructor expression-rule
  field
    ruleId : String
    head : Name
    roles : List ArgRole
    surface : ExprSurface

record InfrastructureRule : Set where
  constructor infrastructure-rule
  field
    ruleId : String
    head : Name

record DomainSpec : Set where
  constructor domain-spec
  field
    domainId : String
    entities : List EntityRule
    predicates : List PredicateRule
    expressions : List ExpressionRule
    infrastructure : List InfrastructureRule
    transparentAliases : List Name
    reductionFuel : Nat

nameEq : Name → Name → Bool
nameEq = primQNameEquality

findEntity : Name → List EntityRule → Maybe EntityRule
findEntity name [] = nothing
findEntity name (rule ∷ rules) with nameEq name (EntityRule.head rule)
... | true = just rule
... | false = findEntity name rules

findPredicate : Name → List PredicateRule → Maybe PredicateRule
findPredicate name [] = nothing
findPredicate name (rule ∷ rules) with nameEq name (PredicateRule.head rule)
... | true = just rule
... | false = findPredicate name rules

findExpression : Name → List ExpressionRule → Maybe ExpressionRule
findExpression name [] = nothing
findExpression name (rule ∷ rules) with nameEq name (ExpressionRule.head rule)
... | true = just rule
... | false = findExpression name rules

findInfrastructure : Name → List InfrastructureRule → Maybe InfrastructureRule
findInfrastructure name [] = nothing
findInfrastructure name (rule ∷ rules) with nameEq name (InfrastructureRule.head rule)
... | true = just rule
... | false = findInfrastructure name rules

memberName : Name → List Name → Bool
memberName name [] = false
memberName name (candidate ∷ names) with nameEq name candidate
... | true = true
... | false = memberName name names