def Esolangs.Cornucopia.Prog.HasModel (prog : Prog) : Prop

Equations

• prog.HasModel = ∃ (fs : Map String (List ℕ → ℕ)), prog.Compatible fs

def Esolangs.Cornucopia.Prog.HasUniqueModel (prog : Prog) : Prop

Equations

• prog.HasUniqueModel = ∃! fs : Map String (List ℕ → ℕ), prog.Compatible fs

class Esolangs.Cornucopia.ProgInfo (prog : Prog) : Type

• name : String
• defNames : List String
• has_model : Bool
• has_unique_model : Bool
• h_defNames : prog.defs.keys.Perm (List.map Builtin.name builtins ++ defNames prog)
• h_wf' : prog.WF'
• h_has_model : prog.HasModel ↔ has_model prog = true
• h_has_unique_model : prog.HasUniqueModel ↔ has_unique_model prog = true

@[irreducible]

def Esolangs.Cornucopia.Expr.show (e : Expr) (argNames : Array String) : String

Equations

• (Esolangs.Cornucopia.Expr.arg i).show argNames = argNames[i]!
• (Esolangs.Cornucopia.Expr.call t args).show argNames = t ++ if args.length = 0 then "" else "(" ++ ", ".intercalate (List.map (fun (x : Esolangs.Cornucopia.Expr) => x.show argNames) args) ++ ")"

def Esolangs.Cornucopia.Def.show (d : Def) (name : String) : String

Equations

• d.show name = (name ++ if d.arity = 0 then "" else "(" ++ ", ".intercalate (mkList d.arity fun (i : ℕ) => String.ofList [Char.ofNat (97 + i)]) ++ ")") ++ " := " ++ d.expr.show { toList := mkList d.arity fun (i : ℕ) => String.ofList [Char.ofNat (97 + i)] }

def Esolangs.Cornucopia.ProgInfo.showWF {prog : Prog} [info : ProgInfo prog] : String

Equations

• Esolangs.Cornucopia.ProgInfo.showWF = if (!Esolangs.Cornucopia.ProgInfo.has_model prog) = true then "no model" else if (!Esolangs.Cornucopia.ProgInfo.has_unique_model prog) = true then "multiple models" else "unique model"

def Esolangs.Cornucopia.Prog.show (prog : Prog) [info : ProgInfo prog] : String

Equations

• prog.show = "".intercalate ["-- ", Esolangs.Cornucopia.ProgInfo.showWF, "\n", "\n".intercalate (List.map (fun (name : String) => (prog.def name).show name) (Esolangs.Cornucopia.ProgInfo.defNames prog))]