// GeologMeta: A homoiconic representation of geolog theories
//
// An instance of GeologMeta IS a collection of geolog theories, complete with
// signatures, axioms, and well-formedness constraints.
//
// Key design principles:
// - All elements identified by UUID; human-readable names in separate NamingIndex
// - Child pointers go from parent to children (no products in domains)
// - Binding uses upward pointers from variable to binder
// - Transitive closure (ancestor) via Datalog-style axioms
// - Srt/theory, Func/theory enables multi-theory instances and theory parameters
//
// Naming convention: DomainSort/descriptor
// - Embeddings: VarT/term, EqF/formula (target sort)
// - Parent pointers: Srt/theory, Field/prod (container sort)
// - Projections: EqF/lhs, ProjT/field (field reference)

theory GeologMeta {

  // ============================================================
  // THEORIES
  // ============================================================

  Theory : Sort;

  // Theory parameters: (N : PetriNet) means N is a Param
  Param : Sort;
  Param/theory : Param -> Theory;        // which theory has this parameter
  Param/type : Param -> Theory;          // must instantiate this theory

  // ============================================================
  // SORTS (renamed to Srt to avoid keyword conflict)
  // ============================================================

  Srt : Sort;
  Srt/theory : Srt -> Theory;

  // ============================================================
  // DERIVED SORTS (Base | Product)
  // ============================================================

  DSort : Sort;

  // Base case: wraps a Sort
  BaseDS : Sort;
  BaseDS/dsort : BaseDS -> DSort;
  BaseDS/srt : BaseDS -> Srt;

  // Product case: [x: A, y: B, ...]
  ProdDS : Sort;
  ProdDS/dsort : ProdDS -> DSort;

  // Product fields (recursive: field type is DSort)
  Field : Sort;
  Field/prod : Field -> ProdDS;
  Field/type : Field -> DSort;

  // ============================================================
  // FUNCTION SYMBOLS
  // ============================================================

  Func : Sort;
  Func/theory : Func -> Theory;
  Func/dom : Func -> DSort;
  Func/cod : Func -> DSort;

  // ============================================================
  // RELATION SYMBOLS (predicates, no codomain)
  // ============================================================

  Rel : Sort;
  Rel/theory : Rel -> Theory;
  Rel/dom : Rel -> DSort;

  // ============================================================
  // BINDERS (for variable scoping)
  // ============================================================
  // Variables point UP to their binder. Binders are introduced by
  // Exists quantifiers or context variables.

  Binder : Sort;
  Binder/type : Binder -> DSort;

  // ============================================================
  // TERMS
  // ============================================================

  Term : Sort;

  // Variable reference (points to binder)
  VarT : Sort;
  VarT/term : VarT -> Term;
  VarT/binder : VarT -> Binder;       // UPWARD pointer to introducing binder

  // Function application (unary - argument may be a record)
  AppT : Sort;
  AppT/term : AppT -> Term;
  AppT/func : AppT -> Func;
  AppT/arg : AppT -> Term;

  // Record construction [x = t1, y = t2, ...]
  RecordT : Sort;
  RecordT/term : RecordT -> Term;

  RecEntry : Sort;
  RecEntry/record : RecEntry -> RecordT;
  RecEntry/val : RecEntry -> Term;
  RecEntry/field : RecEntry -> Field;     // which field this entry is for

  // Projection t.field
  ProjT : Sort;
  ProjT/term : ProjT -> Term;
  ProjT/base : ProjT -> Term;
  ProjT/field : ProjT -> Field;           // which field to project

  // ============================================================
  // FORMULAS
  // ============================================================

  Formula : Sort;

  // Relation application `t R`
  RelF : Sort;
  RelF/formula : RelF -> Formula;
  RelF/arg : RelF -> Term;
  RelF/rel : RelF -> Rel;

  // Truth
  TrueF : Sort;
  TrueF/formula : TrueF -> Formula;

  // Falsity
  FalseF : Sort;
  FalseF/formula : FalseF -> Formula;

  // Equality t1 = t2
  EqF : Sort;
  EqF/formula : EqF -> Formula;
  EqF/lhs : EqF -> Term;
  EqF/rhs : EqF -> Term;

  // Conjunction (n-ary via arms)
  ConjF : Sort;
  ConjF/formula : ConjF -> Formula;

  ConjArm : Sort;
  ConjArm/conj : ConjArm -> ConjF;
  ConjArm/child : ConjArm -> Formula;

  // Disjunction (n-ary via arms)
  DisjF : Sort;
  DisjF/formula : DisjF -> Formula;

  DisjArm : Sort;
  DisjArm/disj : DisjArm -> DisjF;
  DisjArm/child : DisjArm -> Formula;

  // Existential quantification
  ExistsF : Sort;
  ExistsF/formula : ExistsF -> Formula;
  ExistsF/binder : ExistsF -> Binder;     // introduces this binder
  ExistsF/body : ExistsF -> Formula;

  // ============================================================
  // SEQUENTS (axioms)
  // ============================================================

  Sequent : Sort;
  Sequent/theory : Sequent -> Theory;
  Sequent/premise : Sequent -> Formula;
  Sequent/conclusion : Sequent -> Formula;

  // Context variables (universal quantification at sequent level)
  CtxVar : Sort;
  CtxVar/sequent : CtxVar -> Sequent;
  CtxVar/binder : CtxVar -> Binder;       // introduces this binder

  // ============================================================
  // NODE UNIVERSE (for ancestry/scoping)
  // ============================================================
  // Unified sort for tracking parent-child in formula trees

  Node : Sort;
  Term/node : Term -> Node;
  Formula/node : Formula -> Node;

  // ============================================================
  // CHILD RELATION
  // ============================================================
  // child(p, c) means c is an immediate child of p in the AST

  child : [parent: Node, child: Node] -> Prop;

  // ============================================================
  // ANCESTOR RELATION (transitive closure of child)
  // ============================================================

  ancestor : [anc: Node, desc: Node] -> Prop;

  // Datalog-style transitive closure axioms
  ax/anc/base : forall p : Node, c : Node.
    [parent: p, child: c] child |- [anc: p, desc: c] ancestor;

  ax/anc/step : forall a : Node, p : Node, c : Node.
    [anc: a, desc: p] ancestor, [parent: p, child: c] child |- [anc: a, desc: c] ancestor;

  // ============================================================
  // CHILD AXIOMS (populate child from structure)
  // ============================================================

  // EqF children
  ax/child/eq/lhs : forall e : EqF, t : Term.
    e EqF/lhs = t |- [parent: e EqF/formula Formula/node, child: t Term/node] child;
  ax/child/eq/rhs : forall e : EqF, t : Term.
    e EqF/rhs = t |- [parent: e EqF/formula Formula/node, child: t Term/node] child;

  // ExistsF body
  ax/child/exists : forall e : ExistsF, f : Formula.
    e ExistsF/body = f |- [parent: e ExistsF/formula Formula/node, child: f Formula/node] child;

  // ConjF arms
  ax/child/conj : forall a : ConjArm, c : ConjF, f : Formula.
    a ConjArm/conj = c, a ConjArm/child = f |-
      [parent: c ConjF/formula Formula/node, child: f Formula/node] child;

  // DisjF arms
  ax/child/disj : forall a : DisjArm, d : DisjF, f : Formula.
    a DisjArm/disj = d, a DisjArm/child = f |-
      [parent: d DisjF/formula Formula/node, child: f Formula/node] child;

  // RelF argument
  ax/child/rel : forall r : RelF, t : Term.
    r RelF/arg = t |- [parent: r RelF/formula Formula/node, child: t Term/node] child;

  // AppT argument
  ax/child/app : forall a : AppT, t : Term.
    a AppT/arg = t |- [parent: a AppT/term Term/node, child: t Term/node] child;

  // ProjT base
  ax/child/proj : forall p : ProjT, t : Term.
    p ProjT/base = t |- [parent: p ProjT/term Term/node, child: t Term/node] child;

  // RecEntry value
  ax/child/rec : forall e : RecEntry, r : RecordT, t : Term.
    e RecEntry/record = r, e RecEntry/val = t |-
      [parent: r RecordT/term Term/node, child: t Term/node] child;

  // ============================================================
  // IN-SEQUENT RELATION (for context variable scoping)
  // ============================================================

  in_seq : [node: Node, seq: Sequent] -> Prop;

  ax/in_seq/premise : forall s : Sequent, f : Formula.
    s Sequent/premise = f |- [node: f Formula/node, seq: s] in_seq;

  ax/in_seq/conclusion : forall s : Sequent, f : Formula.
    s Sequent/conclusion = f |- [node: f Formula/node, seq: s] in_seq;

  ax/in_seq/desc : forall n : Node, m : Node, s : Sequent.
    [node: n, seq: s] in_seq, [anc: n, desc: m] ancestor |- [node: m, seq: s] in_seq;

  // ============================================================
  // BINDING WELL-FORMEDNESS CONSTRAINTS
  // ============================================================
  // These axioms ensure variables point to valid binders.
  // An instance satisfies these iff scoping is correct.

  // Exists-bound: binder's exists must be an ancestor of the var
  ax/wf/exists : forall v : VarT, b : Binder, e : ExistsF.
    v VarT/binder = b, e ExistsF/binder = b |-
      [anc: e ExistsF/formula Formula/node, desc: v VarT/term Term/node] ancestor;

  // Context-bound: var must be in the same sequent as the ctx var
  ax/wf/ctx : forall v : VarT, b : Binder, cv : CtxVar, s : Sequent.
    v VarT/binder = b, cv CtxVar/binder = b, cv CtxVar/sequent = s |-
      [node: v VarT/term Term/node, seq: s] in_seq;

  // ============================================================
  // COMMITS (version control checkpoints)
  // ============================================================
  // Commits form a DAG. Each commit represents a point-in-time
  // snapshot of all name bindings.

  Commit : Sort;
  Commit/parent : Commit -> Commit;  // previous commit (optional for initial)
  // Note: For merge commits, we'd need a relation for multiple parents

  // ============================================================
  // NAME BINDINGS (mutable pointers via append-only log)
  // ============================================================
  // A NameBinding records that, as of a given commit, a name
  // points to a specific theory or instance version.
  //
  // Names are strings stored in NamingIndex (by UUID).
  // The "current" binding for a name is the most recent one
  // reachable from HEAD commit.

  NameBinding : Sort;
  NameBinding/commit : NameBinding -> Commit;  // when this binding was made

  // What the name points to (exactly one of these is defined):
  NameBinding/theory : NameBinding -> Theory;
  NameBinding/instance : NameBinding -> Instance;

  // ============================================================
  // INSTANCES (immutable, patch-based versioning)
  // ============================================================
  // An Instance is an immutable snapshot. "Modifying" an instance
  // creates a new Instance with parent pointer and delta.
  //
  // To materialize: chase parent chain, union additions, apply retractions.

  Instance : Sort;
  Instance/parent : Instance -> Instance;   // base version (optional for v0)
  Instance/theory : Instance -> Theory;     // which theory this instantiates

  // ============================================================
  // INSTANCE ELEMENTS (delta: additions)
  // ============================================================
  // Elements added in a specific instance version.
  // The actual UUID is tracked via the element's Luid in Universe.

  Elem : Sort;
  Elem/instance : Elem -> Instance;   // which version introduced this
  Elem/sort : Elem -> Srt;            // which sort of the theory

  // ============================================================
  // ELEMENT RETRACTIONS (delta: tombstones)
  // ============================================================
  // Marks an element as retracted in a specific version.
  // The element still exists in the log, but is filtered from materialized view.

  ElemRetract : Sort;
  ElemRetract/instance : ElemRetract -> Instance;  // which version retracted
  ElemRetract/elem : ElemRetract -> Elem;          // what was retracted

  // ============================================================
  // FUNCTION VALUES (delta: additions)
  // ============================================================
  // Records a function value: func(arg) = result

  FuncVal : Sort;
  FuncVal/instance : FuncVal -> Instance;  // which version defined this
  FuncVal/func : FuncVal -> Func;          // which function
  FuncVal/arg : FuncVal -> Elem;           // domain element (or product elem)
  FuncVal/result : FuncVal -> Elem;        // codomain element

  // NOTE: No FuncValRetract sort - function values are IMMUTABLE.
  // To "change" a function value, retract the domain element and create a new one.
  // This ensures the Monotonic Submodel Property (see incremental_index_design.md).

  // ============================================================
  // RELATION TUPLES (delta: additions)
  // ============================================================
  // Records a relation tuple: rel(args...) holds
  //
  // All relations use product-domain encoding uniformly (even unary).
  // Each tuple has RelTupleArg entries for each position in the domain.

  RelTuple : Sort;
  RelTuple/instance : RelTuple -> Instance;  // which version asserted this
  RelTuple/rel : RelTuple -> Rel;            // which relation

  // Relation tuple argument components (one per domain field)
  RelTupleArg : Sort;
  RelTupleArg/tuple : RelTupleArg -> RelTuple;  // which tuple this belongs to
  RelTupleArg/elem : RelTupleArg -> Elem;       // element value for this position
  RelTupleArg/position : RelTupleArg -> Field;  // which field of the domain product

  // NOTE: No RelTupleRetract sort - relation tuples are IMMUTABLE.
  // Relations are boolean-valued functions: R(a,b) is defined at element creation time.
  // To "change" a relation value, retract the involved elements and create new ones.
  // This ensures the Monotonic Submodel Property (see incremental_index_design.md).

  // ============================================================
  // THEORY VERSIONING (same pattern as instances)
  // ============================================================
  // Theories are also immutable and patch-based.
  // Theory/parent allows incremental theory extension.

  Theory/parent : Theory -> Theory;  // base version (optional for v0)

  // Theory element retractions (for removing sorts/funcs/rels)
  SrtRetract : Sort;
  SrtRetract/theory : SrtRetract -> Theory;
  SrtRetract/srt : SrtRetract -> Srt;

  FuncRetract : Sort;
  FuncRetract/theory : FuncRetract -> Theory;
  FuncRetract/func : FuncRetract -> Func;

  RelRetract : Sort;
  RelRetract/theory : RelRetract -> Theory;
  RelRetract/rel : RelRetract -> Rel;

  SequentRetract : Sort;
  SequentRetract/theory : SequentRetract -> Theory;
  SequentRetract/sequent : SequentRetract -> Sequent;
}