Commit 721efd67 authored by jfschaefer's avatar jfschaefer
Browse files

fix known bugs in Log grammar

parent b99c7e3c
......@@ -14,7 +14,7 @@ concrete MCatsLog of MCats = {
Statement = Str;
-- statement as sentence or relative sentence ("such that ...")
StatementFin = Str;
Definition = Str;
Definition = { pref : Str; postf : Str } ; -- {pref: "(forall x. prime(x)"; postf: ")"} (allows to add further conditions)
Declaration = Str;
Utterance = Str;
......
......@@ -18,9 +18,18 @@ concrete NGrammarLog of NGrammar = MCatsLog ** {
not_exists_statement obj id = inp("¬" ++ "∃" ++ id.core ++ "." ++ lwrap(obj) ++ id.core ++ and_formula(id));
state stmt pol = table { true => stmt; false => "¬" ++ stmt } ! pol;
def_mobj_mobjprop obj id prop = inp("∀" ++ id.core ++ "." ++ inp(lwrap(obj) ++ id.core ++ and_formula(id)) ++ "⇒" ++ prop);
iff_definition defi condition = defi ++ "⇔" ++ condition; -- TODO: This is wrong!!
def_mobj_is_mobj definiendum definiens = inp("∀" ++ "x0" ++ "." ++ lwrap(definiens) ++ "x0" ++ "⇒" ++ lwrap(definiendum) ++ "x0");
def_mobj_mobjprop obj id prop = {
pref = "∀" ++ id.core ++ "." ++ inp(lwrap(obj) ++ id.core ++ and_formula(id)) ++ "⇒" ++ "(" ++ lwrap(prop) ++ id.core;
postf = ")";
};
iff_definition defi condition = {
pref = defi.pref ++ "⇔" ++ condition;
postf = defi.postf;
};
def_mobj_is_mobj definiendum definiens = {
pref = "∀" ++ "x0" ++ "." ++ lwrap(definiens) ++ "x0" ++ "⇒" ++ "(" ++ lwrap(definiendum) ++ "x0";
postf = ")";
};
......@@ -28,5 +37,5 @@ concrete NGrammarLog of NGrammar = MCatsLog ** {
utter_statement s = s;
utter_declaration s = s;
utter_definition s = s;
utter_definition s = inp(s.pref ++ s.postf);
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment