Commit b99c7e3c authored by jfschaefer's avatar jfschaefer
Browse files

first logic support (with bugs)

parent 4db3a65c
......@@ -18,15 +18,4 @@ incomplete concrete FGrammarI of FGrammar = {
fexpression_row expr = wrap_mml "mrow" expr;
apply_bin_rel rel a b = wrap_mml "mrow" (a ++ (wrap_mml "mo" rel) ++ b);
fstatement_to_statement fstmt = lin Cl { s = table {
Pres => table {
Simul => table { CPos => table { _ => "$" ++ fstmt ++ "$" }; _ => table { _ => "???" } };
_ => table { _ => table { _ => "???" } } };
_ => table { _ => table { _ => table { _ => "???" } } } } };
fcomplexidentifier_to_identifer fci = { s = "$" ++ fci ++ "$"; m = one };
fexpr_fbinrel_fcid_fbinrel_fexpr_to_identifier a r1 b r2 c =
{ s = "$" ++ (wrap_mml "mrow" (a ++ (wrap_mml "mo" r1) ++ b ++ (wrap_mml "mo" r2) ++ c)) ++ "$"; m = one };
}
concrete FGrammarLog of FGrammar = MCatsLog ** {
lincat
FIdentifier = Str;
FNumeral = Str;
FBinRelation = Str;
FComplexIdentifier = Str;
FExpression = Str;
FStatement = Str;
lin
fidentifier_to_fcomplexidentifier i = i;
fnumeral_to_fexpression n = n;
fcomplexidentifier_to_fexpression c = c;
fexpression_row expr = expr;
apply_bin_rel rel a b = rel ++ "(" ++ a ++ "," ++ b ++ ")";
fstatement_to_statement fstmt = fstmt;
fcomplexidentifier_to_identifer fci = {
formula = "";
core = fci;
hasFormula = false;
};
fexpr_fbinrel_fcid_fbinrel_fexpr_to_identifier a r1 b r2 c = {
formula = r1 ++ "(" ++ a ++ "," ++ b ++ ")" ++ "∧" ++ r2 ++ "(" ++ b ++ "," ++ c ++ ")";
core = b;
hasFormula = true;
};
}
concrete FLexiconLog of FLexicon = FGrammarLog ** {
lin
n_FIdentifier = "n";
m_FIdentifier = "m";
A_FIdentifier = "A";
a_FIdentifier = "a";
one_FNumeral = "1";
two_FNumeral = "2";
lessThan_FBinRelation = "less";
divides_FBinRelation = "divides";
}
concrete MCatsLog of MCats = {
param
boolean = true | false;
multiplicity = one | many;
lincat
-- natural language
PosNegPol = boolean;
MObj = Str;
MObjProp = Str;
Statement = Str;
-- statement as sentence or relative sentence ("such that ...")
StatementFin = Str;
Definition = Str;
Declaration = Str;
Utterance = Str;
-- formulae
MathCN = Str;
Identifier = { formula : Str; core : Str; hasFormula : boolean };
}
concrete MNlpLog of MNlp = NLexiconLog, NGrammarLog, FGrammarLog, FLexiconLog ** {
}
......@@ -27,7 +27,7 @@ concrete NGrammarEng of NGrammar = MCatsEng, GrammarEng, ExtraEng ** open Syntax
--
def_mobj_mobjprop obj id prop = mkS (mkCl
(DetCN aSg_Det (mobjToCN obj id)) -- (mkNP aSg_Det (mobjToCN obj))
(PastPartAP (mkVPSlash (mkV2A (mkV "call" "calls" "called" "called" "calling") noPrep) prop)));
(PastPartAP (mkVPSlash call_V2A prop)));
-- -- iff_definition defi condition = lin S { s = "iff" }; -- better solution for this?
iff_definition defi condition = lin S { s = defi.s ++ "iff" ++ condition.s.s }; -- better solution for this?
-- def_defmobj_defmobj a b = mkCl a b;
......
concrete NGrammarLog of NGrammar = MCatsLog ** {
oper
ofx : Str -> Str = \s -> s ++ "(" ++ "x" ++ ")";
lwrap : Str -> Str = \f -> "(" ++ "λx." ++ f ++ ")";
inp : Str -> Str = \s -> "(" ++ s ++ ")";
and_formula : Identifier -> Str = \id -> table {true => "∧" ++ id.formula; false => ""} ! id.hasFormula;
lin
PosPol = true;
NegPol = false;
no_identifier = { formula = ""; core = "x0"; hasFormula = false };
restrict_mobj prop obj = prop ++ "∧" ++ obj;
mobj_such_that obj restr = obj ++ "∧" ++ restr;
exists_statement obj id = inp("∃" ++ id.core ++ "." ++ lwrap(obj) ++ id.core ++ and_formula(id));
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");
let_id_be_a_mobj id obj = "declare"; -- TODO: Figure out how to deal with this
utter_statement s = s;
utter_declaration s = s;
utter_definition s = s;
}
concrete NLexiconLog of NLexicon = MCatsLog, NLexiconMObjLog ** {
lin
-- integer_MObj = mkCN (mkN "integer");
-- set_MObj = mkCN (mkN "set");
-- alphabet_MObj = mkCN (mkN "alphabet");
finite_MObjProp = "finite" ++ "(" ++ "x" ++ ")";
empty_MObjProp = "empty" ++ "(" ++ "x" ++ ")";
even_MObjProp = "even" ++ "(" ++ "x" ++ ")";
positive_MObjProp = "positive" ++ "(" ++ "x" ++ ")";
prime_MObjProp = "prime" ++ "(" ++ "x" ++ ")";
}
concrete NLexiconMObjLog of NLexiconMObj = MCatsLog ** {
lin
set_MObj = "set" ++ "(" ++ "x" ++ ")";
function_MObj = "function" ++ "(" ++ "x" ++ ")";
case_MObj = "case" ++ "(" ++ "x" ++ ")";
space_MObj = "space" ++ "(" ++ "x" ++ ")";
form_MObj = "form" ++ "(" ++ "x" ++ ")";
point_MObj = "point" ++ "(" ++ "x" ++ ")";
group_MObj = "group" ++ "(" ++ "x" ++ ")";
result_MObj = "result" ++ "(" ++ "x" ++ ")";
sequence_MObj = "sequence" ++ "(" ++ "x" ++ ")";
operator_MObj = "operator" ++ "(" ++ "x" ++ ")";
map_MObj = "map" ++ "(" ++ "x" ++ ")";
number_MObj = "number" ++ "(" ++ "x" ++ ")";
algebra_MObj = "algebra" ++ "(" ++ "x" ++ ")";
solution_MObj = "solution" ++ "(" ++ "x" ++ ")";
constant_MObj = "constant" ++ "(" ++ "x" ++ ")";
vector_MObj = "vector" ++ "(" ++ "x" ++ ")";
measure_MObj = "measure" ++ "(" ++ "x" ++ ")";
system_MObj = "system" ++ "(" ++ "x" ++ ")";
time_MObj = "time" ++ "(" ++ "x" ++ ")";
matrix_MObj = "matrix" ++ "(" ++ "x" ++ ")";
metric_MObj = "metric" ++ "(" ++ "x" ++ ")";
class_MObj = "class" ++ "(" ++ "x" ++ ")";
product_MObj = "product" ++ "(" ++ "x" ++ ")";
field_MObj = "field" ++ "(" ++ "x" ++ ")";
graph_MObj = "graph" ++ "(" ++ "x" ++ ")";
structure_MObj = "structure" ++ "(" ++ "x" ++ ")";
element_MObj = "element" ++ "(" ++ "x" ++ ")";
polynomial_MObj = "polynomial" ++ "(" ++ "x" ++ ")";
boundary_MObj = "boundary" ++ "(" ++ "x" ++ ")";
subset_MObj = "subset" ++ "(" ++ "x" ++ ")";
probability_MObj = "probability" ++ "(" ++ "x" ++ ")";
manifold_MObj = "manifold" ++ "(" ++ "x" ++ ")";
state_MObj = "state" ++ "(" ++ "x" ++ ")";
family_MObj = "family" ++ "(" ++ "x" ++ ")";
basis_MObj = "basis" ++ "(" ++ "x" ++ ")";
action_MObj = "action" ++ "(" ++ "x" ++ ")";
limit_MObj = "limit" ++ "(" ++ "x" ++ ")";
value_MObj = "value" ++ "(" ++ "x" ++ ")";
representation_MObj = "representation" ++ "(" ++ "x" ++ ")";
way_MObj = "way" ++ "(" ++ "x" ++ ")";
vertex_MObj = "vertex" ++ "(" ++ "x" ++ ")";
process_MObj = "process" ++ "(" ++ "x" ++ ")";
norm_MObj = "norm" ++ "(" ++ "x" ++ ")";
integer_MObj = "integer" ++ "(" ++ "x" ++ ")";
}
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