FPL Core: Fundamental Data Elements for Flight Planning

import LeanSpec.lib.Util
import LeanSpec.lib.Geo

namespace Core

def maxTextLength := 200

def FreeText := Str 1 maxTextLength
deriving DecidableEq

def AircraftIdentification := Str 2 7
deriving DecidableEq

def SsrCode := Str 4 4
deriving DecidableEq

inductive FlightRule
  | ifr  -- instrument flight rules
  | vfr  -- visual flight rules
deriving DecidableEq

inductive FlightRules
  | i  -- IFR throughout
  | v  -- VFR throughout
  | y  -- IFR first, then changing to VFR
  | z  -- VFR first, then changing to IFR
deriving DecidableEq

inductive TypeOfFlight
  | s  -- Scheduled flight
  | n  -- Non-scheduled flight
  | g  -- General Aviation (GA)
  | m  -- Military
  | x  -- Other
deriving DecidableEq

inductive SpecialHandling
  | altrv
  | atfmx
  | ffr
  | fltck
  | hazmat
  | head
  | hosp
  | hum
  | marsa
  | medevac
  | nonrvsm
  | sar
  | state
deriving DecidableEq

def Registration := Str 2 7
deriving DecidableEq

def NumberOfAircraft := NatMN 2 99
deriving DecidableEq

def Doc8643.Designator := Str 2 4
deriving DecidableEq

inductive AircraftType
  | desig (_ : Doc8643.Designator)
  | name (_ : FreeText)
deriving DecidableEq

def AircraftAddress := Str 6 6
deriving DecidableEq

inductive AircraftPerformance
  | a | b | c | d | e | h
deriving DecidableEq

inductive WakeTurbulenceCategory
  | h  -- high
  | m  -- medium
  | l  -- low
deriving DecidableEq

inductive UnitOfVerticalDistance
  | feet
  | metres
deriving DecidableEq

inductive FlightLevelOrAltitude
  | flightLevel
  | altitude
deriving DecidableEq

structure VerticalPositionOfAircraft where
  value : Int
  uom   : UnitOfVerticalDistance
  type  : FlightLevelOrAltitude
deriving DecidableEq

inductive UnitOfHorizontalDistance
  | nm
deriving DecidableEq

structure HorizontalDistance where
  value : Nat
  uom   : UnitOfHorizontalDistance
deriving DecidableEq

inductive UnitOfSpeed
  | kt
  | kph
  | mach
deriving DecidableEq

inductive SpeedDatum
  | tas
  | ias
  | gspd
deriving DecidableEq

structure AircraftSpeed where
  value : Nat
  uom   : UnitOfSpeed
  datum : SpeedDatum
  inv   : -- Ground speed cannot be expressed as a mach number
          datum = .gspd → uom ≠ .mach
deriving DecidableEq

def TrueAirspeed := { spd : AircraftSpeed // spd.datum = .tas }
deriving DecidableEq

def Doc7910.Designator := Str 4 4
deriving DecidableEq

def Waypoint := Str 2 5
deriving DecidableEq

structure RelativePoint where
  point    : Waypoint
  bearing  : Geo.Direction
  distance : HorizontalDistance
deriving DecidableEq

inductive Position
  | geo (_ : Geo.Point)
  | wpt (_ : Waypoint)
  | rel (_ : RelativePoint)
deriving DecidableEq

def Position.waypointOf : Position → Option Waypoint
  | .wpt pt => pt
  | _       => none

structure NameAndPosition where
  name     : FreeText
  position : Position
deriving DecidableEq

inductive LandingSite
  | desig (_ : Doc7910.Designator)
  | namePos (_ : NameAndPosition)
deriving DecidableEq

def Doc7910.FIRDesignator := Str 4 4
deriving DecidableEq

inductive CommNavAppCode
  | s  | a  | b  | c  | d
  | e1 | e2 | e3
  | f  | g  | h  | i
  | j1 | j2 | j3 | j4 | j5 | j6 | j7
  | k  | l
  | m1 | m2 | m3
  | o
  | p1 | p2 | p3 | p4 | p5 | p6 | p7 | p8 | p9
  | r  | t  | u  | v  | w  | x  | y  | z
deriving DecidableEq

inductive SurveillanceCode
  | a  | c  | e  | h  | i  | l  | p  | s  | x
  | b1 | b2
  | u1 | u2
  | v1 | v2
  | d1 | g1
deriving DecidableEq

inductive PBNCode
  | a1
  | b1 | b2 | b3 | b4 | b5 | b6
  | c1 | c2 | c3 | c4
  | d1 | d2 | d3 | d4
  | l1
  | o1 | o2 | o3 | o4
  | s1 | s2
  | t1 | t2
deriving DecidableEq

def SelcalCode := Str 4 4
deriving DecidableEq

def RouteDesignator := Str 2 7
deriving DecidableEq

def ATSUnit := Str 4 4
deriving DecidableEq

def AFTNAddress := Str 8 8
deriving DecidableEq

end Core