# Copyright (c) Meta Platforms, Inc. and affiliates.

schema hs.3 {
import src

predicate ModuleName : string

type Namespace = enum { var_ | datacon | tyvar | tycon }

predicate UnitName : string

predicate Module:
  {
    name: ModuleName,
    unit: UnitName,
  }

predicate ModuleSource:
  {
    mod: Module,
    file: src.File,
  }

predicate SourceModule:
  {
    file: src.File,
    mod: Module,
  }
  stored { File, Mod } where ModuleSource { Mod, File }

predicate OccName:
  {
    name: string,
    namespace_: Namespace,
  }

type NameSort =
  {
    external: {} |
      # An exported entity, uniquely identified by its OccName and Module.
    internal: src.ByteSpan |
      # A local binder, e.g. bound by a pattern-match, let. or where,
      # or a non-exported entity. These are uniquely identified by
      # the OccName, Module and ByteSpan.
  }

# Name: a unique key for an entity
predicate Name:
  {
    occ: OccName,
    mod: Module,
    sort: NameSort,
  }

# Types

type TupleSort = enum { boxed | unboxed | constraint }

type TyConSort =
  {
    normal: {} |
    tuple: { arity: nat, sort: TupleSort } |
    sum: { arity: nat } |
    equality: {} |
  }

predicate TyCon:
  {
    name: Name,
    sort: TyConSort,
    promoted: bool,
  }

type ArgFlag =
  {
    invisible: Specificity |
    requird: {}
  }

type Specificity = enum { inferred | specified }

predicate LitType:
  {
    num: nat |
    str: string |
    chr: nat |
  }

type TypeArg =
  {
    visible: bool,
    ty: Type,
  }

type TyVar = string

# Type variables
#
# In HieType a type variable is a Name. But these are always internal
# names, and they don't have a binding SrcSpan so we can't use sort =
# { internal = { span = .. }}. I considered adding a new NameSort: {
# unique: string }, but we don't really want to index uniques (they're
# too non-deterministic). Interestingly, when a HieType is rendered,
# we convert to IfaceType and we use only the OccName of the tyvars,
# discarding the uniques. This is probably wrong, strictly speaking,
# because there could be name clashes, but using a string here leaves
# room to rename the tyvars to disambiguate later.

predicate Type:
  {
    tyvar: TyVar |
    app: { fun: Type, args_: [TypeArg] } |
    tyconapp: { tycon: TyCon, args_: [TypeArg] } |
    forall: { name: TyVar, kind: Type, flag: ArgFlag, inner: Type } |
    fun: { mult: Type, arg: Type, res: Type } |
    qual: { pred: Type, res: Type } |
    lit: LitType |
    cast: Type |
    coercion: {}
  }

# Declarations / definitions

# A declaration, which may or may not define a Name.
type Declaration =
  {
    val: ValBind |
    typeFamily: TypeFamilyDecl |
    type_: TypeSynDecl |
    data: DataDecl |
    con: ConstrDecl |
    patSyn: PatSynDecl |
    class_: ClassDecl |
    method: MethDecl |
    instance: InstanceDecl |
    patBind: PatBind |
    tyVarBind: TyVarBind |
    field: RecordFieldDecl |
    sig: SigDecl |
  }

# Go from a Name to its definition, or vice versa.
predicate DeclarationOfName:
  {
    name: Name,
    decl: Declaration,
  }
  { N, { val = { name = N }}} |
  { N, { typeFamily = { name = N }}} |
  { N, { type_ = { name = N }}} |
  { N, { data = { name = N }}} |
  { N, { con = { name = N }}} |
  { N, { patSyn = { name = N }}} |
  { N, { class_ = { name = N }}} |
  { N, { method = { name = N }}} |
  { N, { patBind = { name = N }}} |
  { N, { tyVarBind = { name = N }}} |
  { N, { field = { name = N }}}

predicate ValBind:
  {
    name: Name,
    ty: maybe Type,
    # fixity
    sig: maybe SigDecl
  }

predicate InstanceBind:
  {
    name: Name,
    # ty: maybe Type,
    loc: src.FileLocation,
  }

# Maps an InstanceBind back to its containing decl
predicate InstanceBindToDecl:
  {
    bind: InstanceBind,
    decl: { inst: InstanceDecl | class_: ClassDecl }
  }

predicate SigDecl:
  {
    name: Name,
    loc: src.FileLocation,
  }

predicate TypeFamilyDecl:
  {
    name: Name,
  }

predicate TypeSynDecl:
  {
    name: Name,
  }

predicate DataDecl:
  {
    name: Name,
    constrs: [ConstrDecl]
  }

predicate ConstrDecl:
  {
    name: Name,
    data_: Name,  # the Name of the DataDecl
    fields: [RecordFieldDecl],  # empty if this is not a record
  }

predicate PatSynDecl:
  {
    name: Name,
  }

predicate ClassDecl:
  {
    name: Name,
    methods: [MethDecl],
    # superclass constraints
    defaults: [InstanceBind],
    # associated types / datatypes
    # associated type defaults
  }

predicate MethDecl:
  {
    name: Name,
    class_: Name,
    # type
    # default decl
  }

predicate InstanceDecl:
  {
    # class
    # parameters etc.
    methods: [InstanceBind],
    loc: src.FileLocation,
  }

predicate PatBind:
  {
    name: Name,
    ty: maybe Type,
  }

predicate TyVarBind:
  {
    name: Name,
  }

predicate RecordFieldDecl:
  {
    name: Name,
    con: Name,
    # type
  }

# From a Name to the location of its defining declaration
predicate DeclarationLocation:
  {
    name: Name,
    file: src.File,
    span: src.ByteSpan
  }

# From a Declaration to its location
predicate DeclarationSpan:
  {
    decl: Declaration,
    loc: src.FileLocation,
  }
  { Decl, Loc } where
    # it's either a definition, or it has a location
    (
      DeclarationOfName { Name, Decl };
      DeclarationLocation { Name, File, Span };
      Loc = { File, Span };
    ) | (
      Decl.sig?.loc = Loc;
    )

predicate ModuleDeclarations:
  {
    module: Module,
    names: set Name,
    # TODO: decls: [Declaration],
    exports: set Name,
  }

# References

type RefSpan =
  {
    kind: RefKind,
    span: src.ByteSpan,
  }

# It's useful to be able to distinguish import/export refs from code refs,
# because e.g. dead code can still have import/export refs.
type RefKind = enum { importref | exportref | coderef | tydecl | instbind }

type RefTarget =
  {
    name: Name |
    modName: ModuleName |
    # We would much prefer Module for the xref from an import
    # declaration, but the HieAST only provides ModuleName. We'll try
    # to resolve this to a Module in the codemarkup layer later.
  }

# Note that references are indexed by Name, so this supports
# find-references. Go-to-def is provided by FileXRefs, which gives all
# the references for a file.
predicate XRef:
  {
    target: RefTarget,
    file: src.File,
    refs: [RefSpan],
  }

predicate FileXRefs :
  {
    file : src.File,
    xrefs : [XRef],
  }

predicate OccNameLowerCase:
  {
    nameLowerCase: string,
    occName: OccName,
  }
  stored { prim.toLower Str, N } where N = OccName { name = Str }

}