; ============================================================
; Lojban egglog schema — mirrors jbo_syntax.rs and jbo_prop.rs
;
; Because many sorts are mutually recursive we first declare
; all sort names with bare (sort …), then add constructors.
; Self-contained (datatype …) blocks are used only for sorts
; whose constructors reference only primitive sorts (i64, String)
; or sorts already declared earlier in this file.
; ============================================================
; ---- Step 1: declare all user-defined sort names -----------
(sort JboTagUnit)
(sort LogConn)
(sort DecTagUnit)
(sort DecTagList)
(sort JboTag)
(sort JboConn)
(sort JboMex)
(sort MexList)
(sort JboOperator)
(sort JboTerm)
(sort TermList)
(sort JboRel)
(sort JboModalOp)
(sort JboQuantifier)
(sort JboProp)
(sort TexList)
(sort Texticule)
; ---- Step 2: add constructors for each sort ----------------
; LogConn — bool-encoded connective (b1 letter b2)
(constructor LogConnMk (i64 String i64) LogConn)
; JboTagUnit variants
(constructor TenseCmavo (String) JboTagUnit)
(constructor CAhA (String) JboTagUnit)
(constructor BAI (String) JboTagUnit)
(constructor FAhA (i64 String) JboTagUnit) ; has_mohi, cmavo
(constructor TAhE_ZAhO (i64 String) JboTagUnit) ; is_space, cmavo
(constructor ROI (String i64 JboMex) JboTagUnit) ; cmavo is_space quant
(constructor FIhO_tag (String) JboTagUnit) ; opaque brivla name
(constructor KI () JboTagUnit)
(constructor CUhE (String) JboTagUnit)
; DecTagUnit
(constructor DecTagUnitMk (String i64 i64 JboTagUnit) DecTagUnit)
; nahe-or-empty se-or-0 nai unit
; DecTagList
(constructor DTNil () DecTagList)
(constructor DTCons (DecTagUnit DecTagList) DecTagList)
; JboTag
(constructor DecoratedTagUnits (DecTagList) JboTag)
(constructor ConnectedTag (JboConn JboTag JboTag) JboTag)
; JboConn
(constructor JboConnLog (JboTag LogConn) JboConn)
(constructor JboConnLogNoTag (LogConn) JboConn)
(constructor JboConnJoik (JboTag String) JboConn)
(constructor JboConnJoikNoTag (String) JboConn)
; JboOperator (declared before JboMex so JboMex can reference it)
(constructor OpVUhU (String) JboOperator)
(constructor OpPermuted (i64 JboOperator) JboOperator)
(constructor OpScalarNeg (String JboOperator) JboOperator)
(constructor OpMex (JboMex) JboOperator)
; MexList
(constructor MLNil () MexList)
(constructor MLCons (JboMex MexList) MexList)
; JboMex
(constructor MexInt (i64) JboMex)
(constructor MexSumti (JboTerm) JboMex)
(constructor MexArray (MexList) JboMex)
(constructor MexOp (JboOperator MexList) JboMex)
; JboTerm
(constructor BoundVar (i64) JboTerm)
(constructor Var (i64) JboTerm)
(constructor Named (String) JboTerm) ; la NAME
(constructor NonAnaph (String) JboTerm) ; mi, do, ti, …
(constructor Unfilled () JboTerm)
(constructor Valsi (String) JboTerm) ; bare word
(constructor JboQuoteT (TexList) JboTerm) ; quoted text as term
(constructor JoikedTerms (String JboTerm JboTerm) JboTerm)
(constructor QualifiedTerm (String JboTerm) JboTerm)
; TermList
(constructor TNil () TermList)
(constructor TCons (JboTerm TermList) TermList)
; JboRel
(constructor Brivla (String) JboRel)
(constructor Equal () JboRel)
(constructor Among (JboTerm) JboRel)
(constructor Tanru (JboRel JboRel) JboRel)
(constructor PermutedRel (i64 JboRel) JboRel)
(constructor RVar (i64) JboRel)
(constructor BoundRVar (i64) JboRel)
(constructor RAss (i64) JboRel)
(constructor ScalarNegRel (String JboRel) JboRel)
(constructor AbsPropRel (String JboProp) JboRel)
(constructor TagRel (JboTag) JboRel)
(constructor ModalRel (JboModalOp JboRel) JboRel)
; JboModalOp
(constructor NonVeridical () JboModalOp)
(constructor WithEventAs (JboTerm) JboModalOp)
(constructor QTruthModal () JboModalOp)
(constructor Tagged (JboTag JboTerm) JboModalOp)
(constructor TaggedNoTerm (JboTag) JboModalOp)
; JboQuantifier
(constructor MexQuant (JboMex) JboQuantifier)
(constructor Exists () JboQuantifier)
(constructor Forall () JboQuantifier)
(constructor Exactly (i64) JboQuantifier)
(constructor QuestionQ () JboQuantifier)
(constructor RelQuant (JboQuantifier) JboQuantifier)
; JboProp
(constructor Eet () JboProp)
(constructor PNot (JboProp) JboProp)
(constructor PAnd (JboProp JboProp) JboProp)
(constructor POr (JboProp JboProp) JboProp)
(constructor PImpl (JboProp JboProp) JboProp)
(constructor PEquiv (JboProp JboProp) JboProp)
(constructor PNonLog (String JboProp JboProp) JboProp)
(constructor PModal (JboModalOp JboProp) JboProp)
; PQuant: quant, restr_id (0=none), body, bound-var-index
(constructor PQuant (JboQuantifier i64 JboProp i64) JboProp)
(constructor PRel (JboRel TermList) JboProp)
; Texticule
(constructor TexticuleProp (JboProp) Texticule)
(constructor TexticuleFragTerms (TermList) Texticule)
(constructor TexticuleSideBracketed (Texticule) Texticule)
(constructor TexticuleSideDiscursive (Texticule) Texticule)
; TexList
(constructor XNil () TexList)
(constructor XCons (Texticule TexList) TexList)
; ---- Top-level relation ------------------------------------
; TextTexticule(text_id, position, texticule)
(relation TextTexticule (i64 i64 Texticule))