using System.Text using Nemerle.Collections using Nemerle.Utility using Nemerle.Logging using Nemerle.Imperative set namespace Fx7 public class Trew type E = ProofGen.E type Lemma = ProofGen.Lemma // fn_symbols : Hashtable [string * int, object] = Hashtable () fn_sb : StringBuilder = StringBuilder () dumped_terms : Hashtable [bool * Term, int] = Hashtable () term_sb : StringBuilder = StringBuilder () main_sb : StringBuilder = StringBuilder () core : Core current_qvars : Hashtable [Term, int] = Hashtable () mutable final_clause : Clause mutable final_clause_name : string Encode (name : string, quant = false) : string _ = quant name TermToString (t : Term, prop : bool, expand = false) : string def sb = StringBuilder () def say (s) _ = sb.Append (s) def say_term (t, prop, expand, deep_expand) def expand = Driver.ExpandProofs || expand || deep_expand match (t.Name) | "true" => //assert (prop) say ("true") | "false" => //assert (prop) say ("false") | "$@true" => say ("true") | "not" => assert (prop) say ("(not ") say_term (t.OnlyChild, true, false, deep_expand) say (")") | _ when t.Arity > 0 && !expand => unless (dumped_terms.Contains ((prop, t))) def id = dumped_terms.Count dumped_terms [(prop, t)] = id _ = term_sb.Append ($"(let t$id $(TermToString (t, prop, expand = true)))\n") say ($ "t$(dumped_terms[(prop, t)])") | "implies" | "iff" | "and" | "or" => def sym = t.Name assert (prop) def loop (_) | [a] => say_term (a, true, true, true) | x :: xs => say ($"($sym ") say_term (x, true, true, true) //say (TermToString (x, true, false)) say (" ") loop (xs) say (")") | [] => assert (false) if (t.Arity == 0) if (t.Name == "and") say ("true") else if (t.Name == "or") say ("false") else assert (false) else if (deep_expand) loop (t.Children) else match (t.Children) | [x] => log (WARN, $"single-argument $(t.Name)") say_term (x, true, false, false) | x :: xs => say ($"($sym ") say_term (x, true, false, false) say (" ") def t = match (xs) | [t] => t | _ => core.TermPool.Get (t.Name, xs) say_term (t, true, false, false) say (")") | [] => assert (false) | "=" | "<=" | ">=" | ">" | "<" => //assert (prop, $ "t = $t") if (t.Child_1of2 === core.TermPool.True && t.Child_2of2 === core.TermPool.True) say ("true") else say ($"($(t.Name) ") say_term (t.Child_1of2, false, false, deep_expand) say (" ") say_term (t.Child_2of2, false, false, deep_expand) say (")") | "exists" \ | "forall" => assert (prop) match (t.Children) | [vars, _, body] \ | [vars, body] => foreach (v in vars.Children) if (current_qvars.Contains (v)) current_qvars [v]++ else current_qvars [v] = 1 foreach (v in vars.Children) say ($"($(t.Name) (\\ $(Encode (v.Name, quant = true)) ") say_term (body, true, true, true) foreach (_ in vars.Children) say ("))") foreach (v in vars.Children) current_qvars [v]-- | _ => assert (false) | "distinct" => assert (prop) def loop (_) | [x] => say_term (x, false, false, deep_expand) | x :: xs => say ("(distinct ") say_term (x, false, false, deep_expand) say (" ") loop (xs) say (")") | [] => assert (false) loop (t.Children) | _ when prop => //say ("(= ") say_term (t, false, false, deep_expand) //say (" ") //say_term (core.TermPool.True, false, false, deep_expand) //say (")") | name => if (current_qvars.Contains (t) && current_qvars [t] > 0) say (Encode (t.Name, quant = true)) else /* unless (fn_symbols.Contains (name, t.Arity)) def arity = $["obj" | _ in [0 .. t.Arity]].ToString (" -> ") def suf = if (t.Arity == 0) "" else $"'$(t.Arity)" _ = fn_sb.Append ($ "Parameter $(Encode (name))$suf : $(arity).\n") fn_symbols [(name, t.Arity)] = null */ if (t.Arity > 0) say ("(") say (Encode (name)) // + $"'$(t.Arity) ") say (" ") NString.SeparatedCalls (" ", t.Children, say_term (_, false, false, deep_expand), sb) say (")") else say (Encode (name)) say_term (t, prop, expand, false) sb.ToString () Dump (lemmas : list [Lemma]) : StringBuilder def main_sb = StringBuilder () def say (s) _ = main_sb.Append (s) def say_clause (c) def lits = c.Lits foreach (i in [0 .. lits.Length - 1]) say ("(implies ") say (TermToString ((~ lits [i]).ToTerm (), prop = true)) say (" ") say ("false") foreach (_ in [0 .. lits.Length - 1]) say (")") mutable funs = 0 def say_e (_ : E) | Lit (l) => say (TermToString (l.ToTerm (), prop = true)) | InfTerm => say ("") | Term (t, prop) => say (TermToString (t, prop)) | Ref (hd) => say (hd) | Lambda (x, body) => say ($"(\\ $x ") say_e (body) say (")") | App (hd, children) => say ($"($hd") foreach (c in children) | InfTerm => {} | _ => say (" ") say_e (c) say (")") | Fun (parms, body) => funs++ foreach ((name, ty) in parms) say ("(assume ") say_e (ty) say ($ " (\\ $name ") say_e (body) foreach (_ in parms) say ("))") | GenApp (Comp (t1, t2), t3) => say_e (E.GenApp (t1, E.GenApp (t2, t3))) | Comp (Id, t) | Comp (t, Id) | GenApp (Id, t) => say_e (t) | Id => say ("id") | GenApp (t1, t2) => say ("(") say_e (t1) say (" ") say_e (t2) say (")") | Comp (t1, t2) => say ("(compose ") say_e (t1) say (" ") say_e (t2) say (")") | Let (name, val, body) => say ($ "(let $name ") say_e (val) say ("\n ") say_e (body) say (")") | RawClause (c) => say_clause (c) foreach (lemma in lemmas) when (lemma.clause === final_clause) final_clause_name = lemma.name if (lemma.proof == null) if (lemma.name == "c0") if (lemma.clause.Lits [0].IsNeg) say ("(let c0 (absurd_x2 initial))\n") else say ("(let c0 (absurd_x initial))\n") else say ($"(let $(lemma.name) (%known ") if (lemma.clause == null) say_e (E.Term (lemma.formula, true)) else say_clause (lemma.clause) say ("))") say ($" ; $(lemma.comment)\n") else funs = 0 if (lemma.name == "skol") say ("(print proving_skolemization)\n(initial\n") else say ($"(let $(lemma.name) ; $(lemma.comment)\n ") if (lemma.name == "skol") say_e (lemma.proof) say ("\n ") say_e (E.Term (lemma.formula.Child_1of2, prop = true)) say ("\n") else if (lemma.clause != null) when (lemma.clause.Proof is Rule.TheoryConflict) say ($"; $(lemma.clause)\n ") say_e (lemma.proof) else say_e (lemma.proof) say (")\n") if (lemma.name == "skol") say ($"(assert_ok (is_form initial $(TermToString(lemma.formula.Child_2of2, true))))\n" "(print skolemization_OK)\n") else if (lemma.clause != null) say ($"(assert_ok (is_form $(lemma.name) \n") say_clause (lemma.clause) say ("))\n") when (Driver.PrintDoneForProofs) say ($"(print $(lemma.name)_done/$funs)\n") else {} main_sb lemmas : list [Lemma] public this (l : list [Lemma], c : Core) core = c lemmas = l public DumpProof (root : Clause, initial : Clause) : string final_clause = root def cl = Dump (ProofGen (core).Run (lemmas, root, initial)) _ = fn_sb.Append ("\n").Append (term_sb).Append ("\n").Append (cl) \ .Append ($"(final $(final_clause_name))\n\n; -- EOF --\n") fn_sb.ToString ()