From 21d139f8069521eed1678762b38aaa717dc6f8c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fredrik=20=C3=96hrstr=C3=B6m?= Date: Tue, 9 Jul 2024 19:37:32 +0200 Subject: [PATCH] Can read simple theory. --- .../viklauverk/eventbtools/TestInternals.java | 4 +- .../viklauverk/eventbtools/core/Canvas.java | 10 +- .../viklauverk/eventbtools/core/Formula.java | 15 +++ .../viklauverk/eventbtools/core/Pattern.java | 110 +++++++++++++++--- .../viklauverk/eventbtools/core/Prover.java | 4 +- .../eventbtools/core/RenderTheoryTeX.java | 5 + .../eventbtools/core/SymbolTable.java | 11 +- .../eventbtools/core/Templates.java | 9 ++ .../eventbtools/core/TestInternals.java | 4 +- .../viklauverk/eventbtools/core/Typing.java | 2 +- templates/TeXDefinitions | 9 ++ 11 files changed, 150 insertions(+), 33 deletions(-) diff --git a/src/main/java/com/viklauverk/eventbtools/TestInternals.java b/src/main/java/com/viklauverk/eventbtools/TestInternals.java index 83a6472..dd4ff7f 100644 --- a/src/main/java/com/viklauverk/eventbtools/TestInternals.java +++ b/src/main/java/com/viklauverk/eventbtools/TestInternals.java @@ -456,7 +456,7 @@ public static boolean testParserRenderer() public static boolean check(String in, String out, String out_with_types) { - SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC; + SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; Formula fo = Formula.fromString(in, fc); String ot = fo.toStringWithTypes(); @@ -484,7 +484,7 @@ public static boolean check(String in, String out, String out_with_types) public static boolean checkFail(String in) { - SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC; + SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; try { Formula f = Formula.fromString(in, fc); diff --git a/src/main/java/com/viklauverk/eventbtools/core/Canvas.java b/src/main/java/com/viklauverk/eventbtools/core/Canvas.java index 4b89470..138ee99 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Canvas.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Canvas.java @@ -655,7 +655,7 @@ public int lengthIgnoringAnsi(String s) */ public void stopAlignments() { - assert(alignments_active_ == true) : "Internal error: Expected alignments to be active when starting alignments, but it was already active!"; + assert(alignments_active_ == true) : "Internal error: Expected alignments to be active when stopping alignments, but it was inactive!"; alignments_active_ = false; append("¤flush¤\n"); @@ -1149,10 +1149,10 @@ public void constructor(String s) append(colorize(BGreen, s)); return; case TEX: - append("\\CNSTR{"+Util.texSafe(s)+"}"); + append("\\CNST{"+Util.texSafe(s)+"}"); return; case HTML: - append(" span(class=CNSTR)="+Util.quoteXMQ(s)+" "); + append(" span(class=CNST)="+Util.quoteXMQ(s)+" "); return; } assert (false) : "Unknown encoding "+render_target_; @@ -1169,10 +1169,10 @@ public void destructor(String s) append(colorize(BGreen, s)); return; case TEX: - append("\\DSTR{"+Util.texSafe(s)+"}"); + append("\\DEST{"+Util.texSafe(s)+"}"); return; case HTML: - append(" span(class=DSTR)="+Util.quoteXMQ(s)+" "); + append(" span(class=DEST)="+Util.quoteXMQ(s)+" "); return; } assert (false) : "Unknown encoding "+render_target_; diff --git a/src/main/java/com/viklauverk/eventbtools/core/Formula.java b/src/main/java/com/viklauverk/eventbtools/core/Formula.java index 3432c93..6abf620 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Formula.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Formula.java @@ -380,6 +380,21 @@ public boolean isPolymorphicDataType() return node_.isPolymorphicDataType(); } + public boolean isConstructor() + { + return node_.isConstructor(); + } + + public boolean isDestructor() + { + return node_.isDestructor(); + } + + public boolean isOperator() + { + return node_.isOperator(); + } + public boolean equals(Formula f) { if (this == f) return true; diff --git a/src/main/java/com/viklauverk/eventbtools/core/Pattern.java b/src/main/java/com/viklauverk/eventbtools/core/Pattern.java index 88b61dd..5b88a83 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Pattern.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Pattern.java @@ -48,6 +48,9 @@ public static class MatchResult public Map anys = new HashMap<>(); public Map numbers = new HashMap<>(); public Map polymorphic_data_types = new HashMap<>(); + public Map constructors = new HashMap<>(); + public Map destructors = new HashMap<>(); + public Map operators = new HashMap<>(); public void clear() { @@ -60,6 +63,9 @@ public void clear() anys.clear(); numbers.clear(); polymorphic_data_types.clear(); + constructors.clear(); + destructors.clear(); + operators.clear(); } } @@ -75,14 +81,17 @@ public void clear() * * The patterns are always parsed using a symbol table containing: * - * predicate symbols: PQR - * expression symbols: EFG - * set symbols: STU - * variable symbols: xyz - * constant_symbols:cdf - * any symbols: ABC - * number symbols: NM + * predicate symbols: P Q R + * expression symbols: E F G + * set symbols: S T U + * variable symbols: x y z + * constant_symbols:c d f + * any symbols: A B C + * number symbols: N M * polymorphic_data_types: H + * constructors: cx (two character symbol) + * destructors: dx (two character symbol) + * operators: op (two character symbol) */ public boolean match(Formula formula, String... pattern_strings) { @@ -109,7 +118,7 @@ private static Formula lookupMatchRule(String s) Formula f = match_rules_.get(s); if (f != null) return f; - f = Formula.fromString(s, SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC); + f = Formula.fromString(s, SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op); match_rules_.put(s, f); return f; } @@ -206,6 +215,24 @@ private static boolean tryMatch(Formula f, Formula p, MatchResult mr) if (!tryMetaMatch(f, p, mr)) return false; return okToAdd(f, p, mr.constants, "constants"); } + if (pt == Node.CONSTRUCTOR_SYMBOL) + { + if (!f.isConstructor()) return false; + if (!tryMetaMatch(f, p, mr)) return false; + return okToAdd(f, p, mr.constructors, "constructors"); + } + if (pt == Node.DESTRUCTOR_SYMBOL) + { + if (!f.isDestructor()) return false; + if (!tryMetaMatch(f, p, mr)) return false; + return okToAdd(f, p, mr.destructors, "destructors"); + } + if (pt == Node.OPERATOR_SYMBOL) + { + if (!f.isOperator()) return false; + if (!tryMetaMatch(f, p, mr)) return false; + return okToAdd(f, p, mr.operators, "operators"); + } if (pt == Node.NUMBER_SYMBOL) { if (!f.isNumber()) return false; @@ -353,6 +380,23 @@ public Set numberNames() return match_results_.numbers.keySet(); } + public Formula getAny(String a) + { + Formula f = match_results_.anys.get(a); + assert (f != null) : "Internal error, could not find any-symbol "+a+" in matched results."; + return f; + } + + public Formula tryGetAny(String a) + { + return match_results_.anys.get(a); + } + + public Set anyNames() + { + return match_results_.anys.keySet(); + } + public Formula getPolymorphicDataType(String v) { Formula f = match_results_.polymorphic_data_types.get(v); @@ -365,21 +409,40 @@ public Set polymorphicDataTypeNames() return match_results_.polymorphic_data_types.keySet(); } - public Formula getAny(String a) + public Formula getConstructor(String v) { - Formula f = match_results_.anys.get(a); - assert (f != null) : "Internal error, could not find any-symbol "+a+" in matched results."; + Formula f = match_results_.constructors.get(v); + assert (f != null) : "Internal error, could not find constructor "+v+" in matched results."; return f; } - public Formula tryGetAny(String a) + public Set constructorNames() { - return match_results_.anys.get(a); + return match_results_.constructors.keySet(); } - public Set anyNames() + public Formula getDestructor(String v) { - return match_results_.anys.keySet(); + Formula f = match_results_.destructors.get(v); + assert (f != null) : "Internal error, could not find destructor "+v+" in matched results."; + return f; + } + + public Set destructorNames() + { + return match_results_.destructors.keySet(); + } + + public Formula getOperator(String v) + { + Formula f = match_results_.operators.get(v); + assert (f != null) : "Internal error, could not find operator "+v+" in matched results."; + return f; + } + + public Set operatorNames() + { + return match_results_.operators.keySet(); } public String matchedRule() @@ -415,14 +478,27 @@ public String allMatches() { sb.append(n+"="+getNumber(n)+" "); } + for (String a : anyNames()) + { + sb.append(a+"="+getAny(a)+" "); + } for (String n : polymorphicDataTypeNames()) { sb.append(n+"="+getPolymorphicDataType(n)+" "); } - for (String a : anyNames()) + for (String n : constructorNames()) { - sb.append(a+"="+getAny(a)+" "); + sb.append(n+"="+getConstructor(n)+" "); + } + for (String n : destructorNames()) + { + sb.append(n+"="+getDestructor(n)+" "); } + for (String n : operatorNames()) + { + sb.append(n+"="+getOperator(n)+" "); + } + return sb.toString().trim(); } diff --git a/src/main/java/com/viklauverk/eventbtools/core/Prover.java b/src/main/java/com/viklauverk/eventbtools/core/Prover.java index fb49a4f..344a7f5 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Prover.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Prover.java @@ -1,6 +1,6 @@ /* Copyright (C) 2021 Viklauverk AB - + This program is free software: you can redistribute it and/or modify it under the terms of the GNU Affero General Public License as published by the Free Software Foundation, either version 3 of the License, or @@ -23,7 +23,7 @@ public class Prover { - SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC; + SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; // _a stands for antecedent // _c stands for consequent diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryTeX.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryTeX.java index fedc644..33e232a 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryTeX.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryTeX.java @@ -94,4 +94,9 @@ public void visit_PolymorphicDataTypesStart(Theory thr) cnvs().append("}\n"); } + @Override + public void visit_PolymorphicDataTypesEnd(Theory thr) + { + } + } diff --git a/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java b/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java index 62369f1..bffdb59 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java +++ b/src/main/java/com/viklauverk/eventbtools/core/SymbolTable.java @@ -712,8 +712,6 @@ public void addDefaults() set_symbols_.add("T"); set_symbols_.add("U"); - polymorphic_data_type_symbols_.add("H"); - variable_symbols_.add("x"); variable_symbols_.add("y"); variable_symbols_.add("z"); @@ -728,14 +726,19 @@ public void addDefaults() any_symbols_.add("A"); any_symbols_.add("B"); any_symbols_.add("C"); + + polymorphic_data_type_symbols_.add("H"); + constructor_symbols_.add("cx"); + destructor_symbols_.add("dx"); + operator_symbols_.add("op"); } - public static SymbolTable PQR_EFG_STU_xyz_cdf_NM_ABC; + public static SymbolTable PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; static { SymbolTable st = new SymbolTable("plain"); st.addDefaults(); - PQR_EFG_STU_xyz_cdf_NM_ABC = st; + PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op = st; } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/Templates.java b/src/main/java/com/viklauverk/eventbtools/core/Templates.java index cd594ee..6a3f8a6 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Templates.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Templates.java @@ -377,6 +377,9 @@ public class Templates { "\\definecolor{EvBCarrierSet}{HTML}{\\DarkGreen}%\n"+ "\\definecolor{EvBPrimitiveSet}{HTML}{000000}%\n"+ "\\definecolor{EvBPolymorphicDataType}{HTML}{000000}%\n"+ +"\\definecolor{EvBConstructor}{HTML}{000000}%\n"+ +"\\definecolor{EvBDestructor}{HTML}{000000}%\n"+ +"\\definecolor{EvBOperator}{HTML}{000000}%\n"+ "\\definecolor{EvBComment}{HTML}{000000}%\n"+ "\\definecolor{EvBLabel}{HTML}{0066cc}%\n"+ "\\definecolor{EvBNames}{HTML}{000000}%\n"+ @@ -397,6 +400,9 @@ public class Templates { "\\definecolor{EvBCarrierSet}{HTML}{000000}%\n"+ "\\definecolor{EvBPrimitiveSet}{HTML}{000000}%\n"+ "\\definecolor{EvBPolymorphicDataType}{HTML}{\\Cyan}%\n"+ +"\\definecolor{EvBConstructor}{HTML}{\\Cyan}%\n"+ +"\\definecolor{EvBDestructor}{HTML}{\\Cyan}%\n"+ +"\\definecolor{EvBOperator}{HTML}{\\Cyan}%\n"+ "\\definecolor{EvBComment}{HTML}{000000}%\n"+ "\\definecolor{EvBLabel}{HTML}{000000}%\n"+ "\\definecolor{EvBNames}{HTML}{000000}%\n"+ @@ -426,6 +432,9 @@ public class Templates { "\\newcommand{\\CSET}[1]{\\EVBTtextrm{\\EVBTcolor{EvBCarrierSet}#1}}%\n"+ "\\newcommand{\\PSET}[1]{\\EVBTtextrm{\\EVBTcolor{EvBPrimitiveSet}#1}}%\n"+ "\\newcommand{\\PDT}[1]{\\EVBTtextrm{\\EVBTcolor{EvBPolymorphicDataType}#1}}%\n"+ +"\\newcommand{\\CNST}[1]{\\EVBTtextrm{\\EVBTcolor{EvBConstructor}#1}}%\n"+ +"\\newcommand{\\DEST}[1]{\\EVBTtextrm{\\EVBTcolor{EvBDestructor}#1}}%\n"+ +"\\newcommand{\\OPER}[1]{\\EVBTtextrm{\\EVBTcolor{EvBOperator}#1}}%\n"+ "\\newcommand{\\EXPR}[1]{\\EVBTtexttt{\\EVBTcolor{EvBExpression}#1}}%\n"+ "\\newcommand{\\PRED}[1]{\\EVBTtexttt{\\EVBTcolor{EvBPredicate}#1}}%\n"+ "\\newcommand{\\NONF}[1]{\\EVBTmathit{\\EVBTcolor{EvBNonFree}#1}}%\n"+ diff --git a/src/main/java/com/viklauverk/eventbtools/core/TestInternals.java b/src/main/java/com/viklauverk/eventbtools/core/TestInternals.java index 43e8a82..7346a56 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/TestInternals.java +++ b/src/main/java/com/viklauverk/eventbtools/core/TestInternals.java @@ -1,6 +1,6 @@ /* Copyright (C) 2021 Viklauverk AB - + This program is free software: you can redistribute it and/or modify it under the terms of the GNU Affero General Public License as published by the Free Software Foundation, either version 3 of the License, or @@ -79,7 +79,7 @@ public static boolean testContainingCardinalitys() public static boolean testm(String in, String out, String out_with_metas, String out_with_types, String out_with_metas_and_types) { - SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC; + SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; Formula fo = Formula.fromString(in, fc); diff --git a/src/main/java/com/viklauverk/eventbtools/core/Typing.java b/src/main/java/com/viklauverk/eventbtools/core/Typing.java index 52af907..c8074c8 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Typing.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Typing.java @@ -195,7 +195,7 @@ else if (c == null) */ private void extractPossibleImplTypesFromPredicate(Formula predicate, SymbolTable symbols) { - SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC; + SymbolTable fc = SymbolTable.PQR_EFG_STU_xyz_cdf_NM_ABC_H_cx_dx_op; Formula fo = Formula.fromString("x:S", fc); boolean ok = pattern().match(predicate, "conjunction", "P & Q", diff --git a/templates/TeXDefinitions b/templates/TeXDefinitions index c07ffd2..305da4d 100644 --- a/templates/TeXDefinitions +++ b/templates/TeXDefinitions @@ -182,6 +182,9 @@ \definecolor{EvBCarrierSet}{HTML}{\DarkGreen}% \definecolor{EvBPrimitiveSet}{HTML}{000000}% \definecolor{EvBPolymorphicDataType}{HTML}{000000}% +\definecolor{EvBConstructor}{HTML}{000000}% +\definecolor{EvBDestructor}{HTML}{000000}% +\definecolor{EvBOperator}{HTML}{000000}% \definecolor{EvBComment}{HTML}{000000}% \definecolor{EvBLabel}{HTML}{0066cc}% \definecolor{EvBNames}{HTML}{000000}% @@ -202,6 +205,9 @@ \definecolor{EvBCarrierSet}{HTML}{000000}% \definecolor{EvBPrimitiveSet}{HTML}{000000}% \definecolor{EvBPolymorphicDataType}{HTML}{\Cyan}% +\definecolor{EvBConstructor}{HTML}{\Cyan}% +\definecolor{EvBDestructor}{HTML}{\Cyan}% +\definecolor{EvBOperator}{HTML}{\Cyan}% \definecolor{EvBComment}{HTML}{000000}% \definecolor{EvBLabel}{HTML}{000000}% \definecolor{EvBNames}{HTML}{000000}% @@ -231,6 +237,9 @@ \newcommand{\CSET}[1]{\EVBTtextrm{\EVBTcolor{EvBCarrierSet}#1}}% \newcommand{\PSET}[1]{\EVBTtextrm{\EVBTcolor{EvBPrimitiveSet}#1}}% \newcommand{\PDT}[1]{\EVBTtextrm{\EVBTcolor{EvBPolymorphicDataType}#1}}% +\newcommand{\CNST}[1]{\EVBTtextrm{\EVBTcolor{EvBConstructor}#1}}% +\newcommand{\DEST}[1]{\EVBTtextrm{\EVBTcolor{EvBDestructor}#1}}% +\newcommand{\OPER}[1]{\EVBTtextrm{\EVBTcolor{EvBOperator}#1}}% \newcommand{\EXPR}[1]{\EVBTtexttt{\EVBTcolor{EvBExpression}#1}}% \newcommand{\PRED}[1]{\EVBTtexttt{\EVBTcolor{EvBPredicate}#1}}% \newcommand{\NONF}[1]{\EVBTmathit{\EVBTcolor{EvBNonFree}#1}}%