Commit be8a06f3 authored by Laszlo Domoszlai's avatar Laszlo Domoszlai
Browse files

KnuthBendix works now

parent 86ee1b4c
......@@ -9,3 +9,6 @@ App5 !f a1 a2 a3 a4 a5 = f a1 a2 a3 a4 a5
string_usize !str = _Tuple2 (string_size str) str
string_uselect !str !pos::I = _Tuple2 (string_select str pos) str
string_replace !str !idx::I !ch::C = _Tuple2 (string_select str idx) (string_update str idx ch)
second !f !s = s
trace !str a = second (_trace str) a
\ No newline at end of file
......@@ -13,7 +13,7 @@
#define instackb(addr) ((char*)addr >= (char*) &stack_b[0] && (char*)addr < (char*) &stack_b[STACK_SIZE_B])
#define follow_thunk(thunk) if (thunk->desc == (Desc*) __FORWARD_PTR__) thunk = thunk->_forward_ptr;
#define follow_thunk(thunk) while (thunk->desc == (Desc*) __FORWARD_PTR__) thunk = thunk->_forward_ptr;
#define forward_thunk(thunk, frame_ptr) \
Thunk* dst = get_dst(frame_ptr); \
......@@ -173,6 +173,12 @@ void exec(Code* expr, int frame_ptr, int root_frame_ptr)
switch (expr->type) {
case CT_APP_PRIM1:
if(get_dst(root_frame_ptr) == NULL)
Thunk* tmp = (Thunk*) alloc_heap(sizeof(Thunk));
set_return(root_frame_ptr, tmp);
case 1:
......@@ -195,6 +201,11 @@ void exec(Code* expr, int frame_ptr, int root_frame_ptr)
case CT_APP_PRIM2:
if(get_dst(root_frame_ptr) == NULL)
Thunk* tmp = (Thunk*) alloc_heap(sizeof(Thunk));
set_return(root_frame_ptr, tmp);
// careful, "exec" may trigger garbage collection
// read local variables only after the last exec
......@@ -247,6 +258,12 @@ void exec(Code* expr, int frame_ptr, int root_frame_ptr)
if(get_dst(root_frame_ptr) == NULL)
Thunk* tmp = (Thunk*) alloc_heap(sizeof(Thunk));
set_return(root_frame_ptr, tmp);
PrimEntry* desc = (PrimEntry*) ((AppEntry*) expr)->f;
int argmask = 1;
......@@ -299,7 +316,7 @@ void exec(Code* expr, int frame_ptr, int root_frame_ptr)
case CT_APP_FUN:
Desc* slice = ((AppEntry*) expr)->f;
int new_frame_ptr = stack_top_a;
int argmask = 1;
......@@ -470,7 +487,8 @@ void exec(Code* expr, int frame_ptr, int root_frame_ptr)
Thunk* arg = local(frame_ptr, ((VarEntry*) expr)->index);
// no need to check for array length, thunks in HNF are never overwritten
......@@ -46,12 +46,13 @@ void init_mem() {
void* alloc_desc(int size) {
size = ((size + 3) / 4) * 4;
desc_alloc += size;
return malloc(size);
void* alloc_code(int size) {
code_alloc += size;
code_alloc += ((size + 3) / 4) * 4;
return malloc(size);
#include <string.h>
#include <stdio.h>
#include "prim.h"
#include "desc.h"
......@@ -109,6 +110,12 @@ void __C2I(int dst_idx) {
target->_int = readC(arg(1));
void __I2C(int dst_idx) {
Thunk* target = get_dst(dst_idx);
target->desc = (Desc*) __CHAR__;
target->_int = (char) readI(arg(1));
void __string_size(int dst_idx)
Thunk* target = get_dst(dst_idx);
......@@ -345,6 +352,39 @@ void __eqS(int dst_idx)
target->_int = eq;
void __C2S(int dst_idx) {
Thunk* target = get_dst(dst_idx);
Thunk* ch = arg(1);
target = string_create(target, 1);
target->_array._chars[0] = (char) ch->_int;
set_return(dst_idx, target);
void __trace(int dst_idx)
Thunk* str = arg(1);
int length;
char* chars;
if(str->desc == (Desc*) __STRING_PTR__)
chars = str->_string_ptr->chars;
length = str->_string_ptr->length;
chars = str->_array._chars;
length = str->_array.length;
for(int i=0; i<length; i++)
printf("%c", chars[i]);
void add_prim(int arity, int boxingMap, char* name, void (*exec)(int)) {
int nameLength = strlen(name);
......@@ -386,7 +426,8 @@ void init_prim() {
add_prim(2, 0b011, "and", &__and);
add_prim(2, 0b011, "or", &__or);
add_prim(2, 0b011, "mod", &__mod);
add_prim(1, 0b001, "C2I", &__C2I);
add_prim(1, 0b001, "C2I", &__C2I);
add_prim(1, 0b001, "I2C", &__I2C);
add_prim(1, 0b000, "string_size", &__string_size);
add_prim(2, 0b010, "string_select", &__string_select);
......@@ -396,4 +437,7 @@ void init_prim() {
add_prim(3, 0b110, "string_slice", &__string_slice);
add_prim(2, 0b000, "string_append", &__string_append);
add_prim(2, 0b000, "eqS", &__eqS);
add_prim(1, 0b001, "C2S", &__C2S);
add_prim(1, 0b000, "_trace", &__trace);
......@@ -38,7 +38,7 @@ typedef struct __attribute__((packed)) Thunk {
union {
Thunk* _forward_ptr;
int _int; // also char and bool
double _real; // TODO: move "real" out of here, too long (at least on 32 bits)
double _real;
struct CleanString* _string_ptr; // For CT_THUNK
struct Array _array;
Thunk* _args[];
......@@ -47,7 +47,7 @@ typedef struct __attribute__((packed)) Thunk {
#pragma pack(pop)
#define thunk_size_f(arity) max(sizeof (Thunk), sizeof (Desc*) + sizeof (Thunk*) * arity);
#define thunk_size_f(arity) ((max(sizeof (Thunk), sizeof (Desc*) + sizeof (Thunk*) * arity) + 3) / 4) * 4
#ifdef DEBUG
......@@ -3,13 +3,13 @@ module precompiler
import Sapl.SaplParser
import Sapl.SaplTokenizer
import StdBool, StdList, StdOrdList, StdFile, StdDebug
import StdBool, StdList, StdOrdList, StdFile, StdFunc, StdArray, StdDebug
import Text.StringAppender, Text
import Data.Map
import Text.Unicode.Encodings.JS
from Text.Unicode.UChar import instance toChar UChar
from Text.Unicode.UChar import instance toChar UChar, instance toInt UChar
import System.CommandLine
import System.File
......@@ -144,9 +144,16 @@ genDefs [f:fs] a = a <++ textSize fstr <++ " " <++ fstr <++ genDefs fs
fstr = toString (sFunc newContext f newAppender)
encodeString :: UString -> String
encodeString us = {c \\ c <- map (convert o toInt) us}
convert cc
| cc > 255 = '?'
= toChar cc
instance Appendable Literal
(<++) a (LString lit) = a <++ "S" <++ sText (toJSLiteral lit)
(<++) a (LString lit) = a <++ "S" <++ sText (encodeString lit)
(<++) a (LInt lit) = a <++ "I" <++ sNum lit
(<++) a (LReal lit) = a <++ "R" <++ sNum lit
(<++) a (LChar [c]) = a <++ "C" <++ toString (toChar c)
Using equations:
(0 + X) = X
(-(X) + X) = 0
((X + Y) + Z) = (X + (Y + Z))
-((B + A)) -> (-(A) + -(B))
-(0) -> 0
-(-(A)) -> A
(A + -(A)) -> 0
(B + (-(B) + A)) -> A
(A + 0) -> A
(-(B) + (B + A)) -> A
((C + B) + A) -> (C + (B + A))
(-(A) + A) -> 0
(0 + A) -> A
\ No newline at end of file
main = KnuthBendix.Start
KnuthBendix.Start::I = if (KnuthBendix.checkEquations KnuthBendix.eqns KnuthBendix.sig) (KnuthBendix.emitStr (Flite.str "Using equations:\n") (KnuthBendix.emitStr (KnuthBendix.showEqns KnuthBendix.sig KnuthBendix.eqns) (KnuthBendix.emitStr (KnuthBendix.showResult (KnuthBendix.complete KnuthBendix.sig KnuthBendix.eqns) KnuthBendix.sig) 0))) (KnuthBendix.emitStr (Flite.str "Ill-formed equation\n") 0)
Flite.str !_x_0 = select _x_0 ("" -> Flite.Nil) (_ -> Flite.Cons (Flite.char (string_select _x_0 0)) (Flite.str (<{StdString.%_10}> _x_0 (_Tuple2 1 (string_size _x_0)))))
<{StdString.%_10}> !str_0 !_x_1 = select _x_1 (_Tuple2 a b -> string_slice str_0 a b)
Flite.char::I !c_0::C = C2I c_0
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
KnuthBendix.emitStr !_x_0 k_1 = select _x_0 (Flite.Nil -> k_1) (Flite.Cons c_1_0 cs_1_1 -> Flite.emit c_1_0 (KnuthBendix.emitStr cs_1_1 k_1))
Flite.emit !c_0::I k_1 = StdDebug.trace (<{StdOverloaded.toString;}> C2S) (I2C c_0) k_1
:: <{StdOverloaded.toString;}> = {StdOverloaded.toString}
StdDebug.trace !_vtoString_0 !message_1 a_2 = trace (StdOverloaded.get_toString_25 _vtoString_0 message_1) a_2
StdOverloaded.get_toString_25 rec = select rec (<{StdOverloaded.toString;}> a1 -> a1)
KnuthBendix.sig = Flite.Cons (Flite.Pair (Flite.str "+") (Flite.Pair 2 True)) (Flite.Cons (Flite.Pair (Flite.str "-") (Flite.Pair 1 False)) (Flite.Cons (Flite.Pair (Flite.str "0") (Flite.Pair 0 False)) Flite.Nil))
:: Flite.Pair = Flite.Pair a1 a2
KnuthBendix.eqns = Flite.Cons (Flite.Pair ( "+" (Flite.Cons ( "0" Flite.Nil) (Flite.Cons (KnuthBendix.var "X") Flite.Nil))) (KnuthBendix.var "X")) (Flite.Cons (Flite.Pair ( "+" (Flite.Cons ( "-" (Flite.Cons (KnuthBendix.var "X") Flite.Nil)) (Flite.Cons (KnuthBendix.var "X") Flite.Nil))) ( "0" Flite.Nil)) (Flite.Cons (Flite.Pair ( "+" (Flite.Cons ( "+" (Flite.Cons (KnuthBendix.var "X") (Flite.Cons (KnuthBendix.var "Y") Flite.Nil))) (Flite.Cons (KnuthBendix.var "Z") Flite.Nil))) ( "+" (Flite.Cons (KnuthBendix.var "X") (Flite.Cons ( "+" (Flite.Cons (KnuthBendix.var "Y") (Flite.Cons (KnuthBendix.var "Z") Flite.Nil))) Flite.Nil)))) Flite.Nil))
KnuthBendix.var x_0 = KnuthBendix.Var (Flite.str x_0)
:: KnuthBendix.E = KnuthBendix.Fun a1 a2 | KnuthBendix.Var a1 x_0 y_1 = KnuthBendix.Fun (Flite.str x_0) y_1
KnuthBendix.complete sig_0 !trs_1 = KnuthBendix.completionLoop KnuthBendix.variables 0 trs_1 Flite.Nil
KnuthBendix.variables = let variety_1_0 = Flite.Cons Flite.Nil (KnuthBendix.concatMap KnuthBendix.variations variety_1_0) in KnuthBendix.tail variety_1_0
KnuthBendix.tail !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> xs_1_1)
KnuthBendix.variations v_0 = (KnuthBendix.flip Flite.Cons v_0) (Flite.str "ABCDEFGHIJKLMNOPQRSTUVWXYZ")
KnuthBendix.flip !f_0 x_1 y_2 = f_0 y_2 x_1 f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons (f_0 x_1_0) ( f_0 xs_1_1))
KnuthBendix.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> KnuthBendix.append (f_0 x_1_0) (KnuthBendix.concatMap f_0 xs_1_1))
KnuthBendix.append !_x_0 ys_1 = select _x_0 (Flite.Nil -> ys_1) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (KnuthBendix.append xs_1_1 ys_1))
KnuthBendix.completionLoop vs_0 n_1::I !_x_2 rules_3 = select _x_2 (Flite.Nil -> Flite.Just rules_3) (Flite.Cons _x_1_0 rest_1_1 -> select _x_1_0 (Flite.Pair l_2_0 r_2_1 -> <{KnuthBendix._c;230;3_157}> (eqI n_1 1000) vs_0 l_2_0 r_2_1 n_1 rest_1_1 rules_3) )
<{KnuthBendix._c;230;3_157}> !_x_0::B vs_1 l_2 r_3 n_4::I rest_5 rules_6 = select _x_0 (True -> Flite.Nothing) (False -> <{KnuthBendix._c;232;12_156}> (KnuthBendix.renameNew vs_1 (Flite.Pair l_2 r_3)) n_4 rest_5 rules_6)
KnuthBendix.renameNew !vs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> <{KnuthBendix._c;213;3_145}> (KnuthBendix.zipWithRemRight (KnuthBendix.curry (KnuthBendix.cross KnuthBendix.Var)) (KnuthBendix.vars l_1_0) vs_0) l_1_0 r_1_1)
KnuthBendix.vars !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons v_1_0 Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.foldr (KnuthBendix.unionBy KnuthBendix.equalStrings_133) Flite.Nil ( KnuthBendix.vars ts_1_1))
KnuthBendix.equalStrings_133::B !_x_0 !_x_1 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_1 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> KnuthBendix.con (eqI x_1_0 y_2_0) (KnuthBendix.equalStrings_133 xs_1_1 ys_2_1)) )
KnuthBendix.con::B !_x_0::B q_1::B = if _x_0 q_1 False
KnuthBendix.unionBy e_0 !xs_1 !ys_2 = KnuthBendix.foldr (KnuthBendix.insBy e_0) xs_1 ys_2
KnuthBendix.insBy e_0 x_1 !ys_2 = if (KnuthBendix.elemBy e_0 x_1 ys_2) ys_2 (Flite.Cons x_1 ys_2)
KnuthBendix.elemBy::B e_0 x_1 !_x_2 = select _x_2 (Flite.Nil -> False) (Flite.Cons y_1_0 ys_1_1 -> if (e_0 x_1 y_1_0) True (KnuthBendix.elemBy e_0 x_1 ys_1_1))
KnuthBendix.foldr f_0 z_1 !_x_2 = select _x_2 (Flite.Nil -> z_1) (Flite.Cons x_1_0 xs_1_1 -> f_0 x_1_0 (KnuthBendix.foldr f_0 z_1 xs_1_1)) !x_0 = x_0
KnuthBendix.cross f_0 g_1 !_x_2 = select _x_2 (Flite.Pair x_1_0 y_1_1 -> Flite.Pair (f_0 x_1_0) (g_1 y_1_1))
KnuthBendix.curry !f_0 x_1 y_2 = f_0 (Flite.Pair x_1 y_2)
KnuthBendix.zipWithRemRight f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Pair Flite.Nil (Flite.Cons y_2_0 ys_2_1)) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> <{KnuthBendix._c;208;3_144}> (KnuthBendix.zipWithRemRight f_0 xs_1_1 ys_2_1) f_0 x_1_0 y_2_0) )
<{KnuthBendix._c;208;3_144}> !_x_0 f_1 x_2 y_3 = select _x_0 (Flite.Pair rest_1_0 rem_1_1 -> Flite.Pair (Flite.Cons (f_1 x_2 y_3) rest_1_0) rem_1_1)
<{KnuthBendix._c;213;3_145}> !_x_0 l_1 r_2 = select _x_0 (Flite.Pair sub_1_0 rest_1_1 -> Flite.Pair (Flite.Pair (KnuthBendix.subst sub_1_0 l_1) (KnuthBendix.subst sub_1_0 r_2)) rest_1_1)
KnuthBendix.subst s_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> <{KnuthBendix._c;501;24_141}> s_0 v_1_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.Fun f_1_0 ( (KnuthBendix.subst s_0) ts_1_1))
<{KnuthBendix._c;501;24_141}> !s_0 v_1 = select s_0 (Flite.Nil -> KnuthBendix.Var v_1) (Flite.Cons _x_1_0 rest_1_1 -> select _x_1_0 (Flite.Pair w_2_0 t_2_1 -> if (KnuthBendix.equalStrings_133 v_1 w_2_0) t_2_1 (KnuthBendix.subst rest_1_1 (KnuthBendix.Var v_1))) )
<{KnuthBendix._c;232;12_156}> !_x_0 n_1::I rest_2 rules_3 = select _x_0 (Flite.Pair newEqn_1_0 ws_1_1 -> <{KnuthBendix._c;233;30_155}> (KnuthBendix.orient newEqn_1_0) ws_1_1 n_1 rest_2 rules_3)
KnuthBendix.orient !_x_0 = select _x_0 (Flite.Pair t1_1_0 t2_1_1 -> if (KnuthBendix.order t1_1_0 t2_1_1) (Flite.Just (Flite.Pair t1_1_0 t2_1_1)) (if (KnuthBendix.order t2_1_1 t1_1_0) (Flite.Just (Flite.Pair t2_1_1 t1_1_0)) Flite.Nothing))
:: Flite.Maybe = Flite.Nothing | Flite.Just a1
KnuthBendix.order = KnuthBendix.kbGreaterThan KnuthBendix.weights
KnuthBendix.weights = KnuthBendix.Weights 1 (Flite.Cons (Flite.Pair (Flite.str "0") 1) (Flite.Cons (Flite.Pair (Flite.str "+") 0) (Flite.Cons (Flite.Pair (Flite.str "-") 0) Flite.Nil)))
:: KnuthBendix.Weights = KnuthBendix.Weights a1 a2
KnuthBendix.kbGreaterThan::B !w_0 !t_1 !s_2 = let wt_1_0 = KnuthBendix.termWeight w_0 t_1, ws_1_1 = KnuthBendix.termWeight w_0 s_2, vs_1_2 = KnuthBendix.unionBy KnuthBendix.equalStrings_133 (KnuthBendix.vars t_1) (KnuthBendix.vars s_2), ns_1_3 = KnuthBendix.snd (KnuthBendix.varCounts s_2 vs_1_2), nt_1_4 = KnuthBendix.snd (KnuthBendix.varCounts t_1 vs_1_2) in KnuthBendix.dis (KnuthBendix.con (KnuthBendix.inv (<{KnuthBendix.<=_137}> wt_1_0 ws_1_1)) (KnuthBendix.compareAll <{KnuthBendix.<=_138}> ns_1_3 nt_1_4)) (KnuthBendix.con (KnuthBendix.con (eqI wt_1_0 ws_1_1) (KnuthBendix.compareAll eqI nt_1_4 ns_1_3)) (KnuthBendix.dis (KnuthBendix.powerOf (KnuthBendix.last (KnuthBendix.funSequence w_0)) t_1 s_2) (KnuthBendix.funcAfter w_0 t_1 s_2)))
KnuthBendix.funcAfter::B w_0 !_x_1 !_x_2 = select _x_1 (KnuthBendix.Var v_1_0 -> select _x_2 (KnuthBendix.Var x_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> False) ) (KnuthBendix.Fun f_1_0 ts_1_1 -> select _x_2 (KnuthBendix.Var x_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> if (KnuthBendix.equalStrings_133 f_1_0 g_2_0) (KnuthBendix.orderLex (KnuthBendix.kbGreaterThan w_0) ts_1_1 us_2_1) (KnuthBendix.before_139 (KnuthBendix.funSequence w_0) g_2_0 f_1_0)) )
KnuthBendix.funSequence !_x_0 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> KnuthBendix.fst fws_1_1)
KnuthBendix.fst !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> x_1_0)
KnuthBendix.before_139::B !_x_0 !x_1 y_2 = select _x_0 (Flite.Cons h_1_0 t_1_1 -> KnuthBendix.dis (KnuthBendix.equalStrings_133 h_1_0 x_1) (KnuthBendix.con (KnuthBendix.inv (KnuthBendix.equalStrings_133 h_1_0 y_2)) (KnuthBendix.before_139 t_1_1 x_1 y_2)))
KnuthBendix.inv::B !_x_0::B = if _x_0 False True
KnuthBendix.dis::B !_x_0::B q_1::B = if _x_0 True q_1
KnuthBendix.orderLex::B f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> if (KnuthBendix.equalTerms x_1_0 y_2_0) (KnuthBendix.orderLex f_0 xs_1_1 ys_2_1) (f_0 x_1_0 y_2_0)) )
KnuthBendix.equalTerms::B !_x_0 !_x_1 = select _x_0 (KnuthBendix.Var v_1_0 -> select _x_1 (KnuthBendix.Var w_2_0 -> KnuthBendix.equalStrings_133 v_1_0 w_2_0) (KnuthBendix.Fun g_2_0 us_2_1 -> False) ) (KnuthBendix.Fun f_1_0 ts_1_1 -> select _x_1 (KnuthBendix.Var w_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> KnuthBendix.con (KnuthBendix.equalStrings_133 f_1_0 g_2_0) (KnuthBendix.and (KnuthBendix.zipWith KnuthBendix.equalTerms ts_1_1 us_2_1))) )
KnuthBendix.zipWith f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Nil) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons (f_0 x_1_0 y_2_0) (KnuthBendix.zipWith f_0 xs_1_1 ys_2_1)) )
KnuthBendix.and::B !xs_0 = KnuthBendix.foldr KnuthBendix.con True xs_0
KnuthBendix.last !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (KnuthBendix.null xs_1_1) x_1_0 (KnuthBendix.last xs_1_1))
KnuthBendix.null::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False)
KnuthBendix.powerOf::B fn_0 !_x_1 u_2 = select _x_1 (KnuthBendix.Var v_1_0 -> False) (KnuthBendix.Fun f_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> False) (Flite.Cons x_2_0 xs_2_1 -> KnuthBendix.con (KnuthBendix.con (KnuthBendix.isVar u_2) (KnuthBendix.equalStrings_133 f_1_0 fn_0)) (KnuthBendix.con (KnuthBendix.null xs_2_1) (KnuthBendix.pow fn_0 x_2_0))) )
KnuthBendix.pow::B fn_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 _x_1_1 -> select _x_1_1 (Flite.Cons z_2_0 zs_2_1 -> KnuthBendix.con (KnuthBendix.equalStrings_133 f_1_0 fn_0) (KnuthBendix.con (KnuthBendix.null zs_2_1) (KnuthBendix.pow fn_0 z_2_0))) )
KnuthBendix.isVar::B !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 ts_1_1 -> False)
KnuthBendix.compareAll::B f_0 !xs_1 !ys_2 = KnuthBendix.and (KnuthBendix.zipWith f_0 xs_1 ys_2)
<{KnuthBendix.<=_138}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{KnuthBendix.<=_137}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
KnuthBendix.varCounts !t_0 !vs_1 = KnuthBendix.foldr KnuthBendix.tally_136 ( vs_1 (KnuthBendix.repeat 0)) (KnuthBendix.concatMap (KnuthBendix.varAt t_0) (KnuthBendix.positions t_0))
KnuthBendix.positions !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons Flite.Nil Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> Flite.Cons Flite.Nil (KnuthBendix.concatMap (KnuthBendix.argPositions ts_1_1) (KnuthBendix.enumFromTo 1 (KnuthBendix.len ts_1_1))))
KnuthBendix.len::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> KnuthBendix.incr (KnuthBendix.len xs_1_1))
KnuthBendix.incr::I !i_0::I = addI i_0 1
KnuthBendix.enumFromTo !m_0::I !n_1::I = if (<{KnuthBendix.<=_131}> m_0 n_1) (Flite.Cons m_0 (KnuthBendix.enumFromTo (KnuthBendix.incr m_0) n_1)) Flite.Nil
<{KnuthBendix.<=_131}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
KnuthBendix.argPositions !ts_0 !n_1::I = (Flite.Cons n_1) (KnuthBendix.positions (KnuthBendix.elemAt ts_0 (KnuthBendix.decr n_1)))
KnuthBendix.decr::I !i_0::I = subI i_0 1
KnuthBendix.elemAt !_x_0 !n_1::I = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (eqI n_1 0) x_1_0 (KnuthBendix.elemAt xs_1_1 (KnuthBendix.decr n_1)))
KnuthBendix.varAt !t_0 !p_1 = <{KnuthBendix._c;365;15_143}> (KnuthBendix.subterm t_0 p_1)
KnuthBendix.subterm !t_0 !_x_1 = select _x_1 (Flite.Nil -> t_0) (Flite.Cons p1_1_0 pRest_1_1 -> <{KnuthBendix._c;524;31_142}> t_0 p1_1_0 pRest_1_1)
<{KnuthBendix._c;524;31_142}> !t_0 !p1_1::I !pRest_2 = select t_0 (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.subterm (KnuthBendix.elemAt ts_1_1 (KnuthBendix.decr p1_1)) pRest_2)
<{KnuthBendix._c;365;15_143}> !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons v_1_0 Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> Flite.Nil)
KnuthBendix.repeat x_0 = Flite.Cons x_0 (KnuthBendix.repeat x_0) = KnuthBendix.zipWith Flite.Pair
KnuthBendix.tally_136 k_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons _x_1_0 xs_1_1 -> select _x_1_0 (Flite.Pair x_2_0 nx_2_1 -> if (KnuthBendix.equalStrings_133 k_0 x_2_0) (Flite.Cons (Flite.Pair x_2_0 (KnuthBendix.incr nx_2_1)) xs_1_1) (Flite.Cons (Flite.Pair x_2_0 nx_2_1) (KnuthBendix.tally_136 k_0 xs_1_1))) )
KnuthBendix.snd !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> y_1_1)
KnuthBendix.termWeight::I !w_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> KnuthBendix.varWeight w_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> addI (KnuthBendix.funWeight_135 w_0 f_1_0) (KnuthBendix.sum ( (KnuthBendix.termWeight w_0) ts_1_1)))
KnuthBendix.sum::I !xs_0 = KnuthBendix.foldr KnuthBendix.plus_132 0 xs_0
KnuthBendix.plus_132::I !a_0::I !b_1::I = addI a_0 b_1
KnuthBendix.funWeight_135 !_x_0 !f_1 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> KnuthBendix.fromJust (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 fws_1_1))
KnuthBendix.lookUpBy e_0 x_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Nothing) (Flite.Cons _x_1_0 yvs_1_1 -> select _x_1_0 (Flite.Pair y_2_0 v_2_1 -> if (e_0 x_1 y_2_0) (Flite.Just v_2_1) (KnuthBendix.lookUpBy e_0 x_1 yvs_1_1)) )
KnuthBendix.fromJust !_x_0 = select _x_0 (Flite.Just x_1_0 -> x_1_0)
KnuthBendix.varWeight !_x_0 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> vw_1_0)
<{KnuthBendix._c;233;30_155}> !_x_0 ws_1 n_2::I rest_3 rules_4 = select _x_0 (Flite.Nothing -> Flite.Nothing) (Flite.Just newRule_1_0 -> KnuthBendix.completionWith ws_1 (KnuthBendix.incr n_2) rest_3 newRule_1_0 rules_4)
KnuthBendix.completionWith vs_0 n_1::I !rest_2 newRule_3 !rules_4 = <{KnuthBendix._c;242;7_158}> (KnuthBendix.simplifyRules KnuthBendix.sig newRule_3 rules_4) vs_0 n_1 newRule_3 rules_4 rest_2
KnuthBendix.simplifyRules sig_0 rule_1 !trs_2 = <{KnuthBendix._c;262;3_150}> (KnuthBendix.reduceSplit sig_0 rule_1 trs_2) rule_1
KnuthBendix.reduceSplit sig_0 rule_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons _x_1_0 rs_1_1 -> select _x_1_0 (Flite.Pair l_2_0 r_2_1 -> <{KnuthBendix._c;280;3_149}> (KnuthBendix.reduceSplit sig_0 rule_1 rs_1_1) rule_1 l_2_0 r_2_1) )
<{KnuthBendix._c;280;3_149}> !_x_0 rule_1 !l_2 r_3 = select _x_0 (Flite.Pair eqns_1_0 rules_1_1 -> let reducedl_2_0 = KnuthBendix.reduce (Flite.Cons rule_1 Flite.Nil) l_2 in if (KnuthBendix.dis (KnuthBendix.null reducedl_2_0) (KnuthBendix.reducible (Flite.Cons (Flite.Pair l_2 r_3) Flite.Nil) (KnuthBendix.left rule_1))) (Flite.Pair eqns_1_0 (Flite.Cons (Flite.Pair l_2 r_3) rules_1_1)) (Flite.Pair (Flite.Cons (Flite.Pair (KnuthBendix.head reducedl_2_0) r_3) eqns_1_0) rules_1_1))
KnuthBendix.head !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> x_1_0)
KnuthBendix.left = KnuthBendix.fst
KnuthBendix.reducible::B trs_0 !t_1 = KnuthBendix.inv (KnuthBendix.null (KnuthBendix.reduce trs_0 t_1))
KnuthBendix.reduce trs_0 !t_1 = KnuthBendix.concatMap (KnuthBendix.reduceAt trs_0 t_1) (KnuthBendix.positions t_1)
KnuthBendix.reduceAt trs_0 !t_1 !p_2 = if (KnuthBendix.isVar (KnuthBendix.subterm t_1 p_2)) Flite.Nil (KnuthBendix.concatMap (KnuthBendix.reduceAtWith t_1 p_2) trs_0)
KnuthBendix.reduceAtWith t_0 p_1 !_x_2 = select _x_2 (Flite.Pair l_1_0 r_1_1 -> <{KnuthBendix._c;493;3_148}> (KnuthBendix.match l_1_0 (KnuthBendix.subterm t_0 p_1)) r_1_1 p_1 t_0)
KnuthBendix.match !t1_0 t2_1 = KnuthBendix.matchWith (Flite.Cons t1_0 Flite.Nil) (Flite.Cons t2_1 Flite.Nil) Flite.Nil
KnuthBendix.matchWith !_x_0 !_x_1 sub_2 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> Flite.Just sub_2) ) (Flite.Cons _x_1_0 ts1_1_1 -> select _x_1_0 (KnuthBendix.Var v_2_0 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> if (KnuthBendix.elemBy KnuthBendix.equalStrings_133 v_2_0 ( KnuthBendix.fst sub_2)) (if (KnuthBendix.equalTerms t_3_0 (KnuthBendix.subst sub_2 (KnuthBendix.Var v_2_0))) (KnuthBendix.matchWith ts1_1_1 ts2_3_1 sub_2) Flite.Nothing) (KnuthBendix.matchWith ts1_1_1 ts2_3_1 (Flite.Cons (Flite.Pair v_2_0 t_3_0) sub_2))) ) (KnuthBendix.Fun f_2_0 ts_2_1 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> <{KnuthBendix._c;465;3_146}> t_3_0 f_2_0 ts_2_1 ts1_1_1 ts2_3_1 sub_2) ) )
<{KnuthBendix._c;465;3_146}> !t_0 f_1 ts_2 ts1_3 ts2_4 sub_5 = select t_0 (KnuthBendix.Var v_1_0 -> Flite.Nothing) (KnuthBendix.Fun g_1_0 us_1_1 -> if (KnuthBendix.equalStrings_133 f_1 g_1_0) (KnuthBendix.matchWith (KnuthBendix.append ts_2 ts1_3) (KnuthBendix.append us_1_1 ts2_4) sub_5) Flite.Nothing)
<{KnuthBendix._c;493;3_148}> !_x_0 r_1 p_2 t_3 = select _x_0 (Flite.Nothing -> Flite.Nil) (Flite.Just sub_1_0 -> Flite.Cons (KnuthBendix.placeAt (KnuthBendix.subst sub_1_0 r_1) p_2 t_3) Flite.Nil)
KnuthBendix.placeAt t_0 !_x_1 u_2 = select _x_1 (Flite.Nil -> t_0) (Flite.Cons p_1_0 pRest_1_1 -> <{KnuthBendix._c;529;32_147}> u_2 t_0 pRest_1_1 p_1_0)
<{KnuthBendix._c;529;32_147}> !u_0 t_1 pRest_2 p_3::I = select u_0 (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.Fun f_1_0 (KnuthBendix.applyToIndex (KnuthBendix.placeAt t_1 pRest_2) (KnuthBendix.decr p_3) ts_1_1))
KnuthBendix.applyToIndex f_0 !n_1::I !_x_2 = select _x_2 (Flite.Cons x_1_0 xs_1_1 -> if (eqI n_1 0) (Flite.Cons (f_0 x_1_0) xs_1_1) (Flite.Cons x_1_0 (KnuthBendix.applyToIndex f_0 (KnuthBendix.decr n_1) xs_1_1)))
<{KnuthBendix._c;262;3_150}> !_x_0 rule_1 = select _x_0 (Flite.Pair newEqns_1_0 remainingRules_1_1 -> Flite.Pair newEqns_1_0 (KnuthBendix.uniqueRules ( (KnuthBendix.normRhs (Flite.Cons rule_1 remainingRules_1_1)) (Flite.Cons rule_1 remainingRules_1_1))))
KnuthBendix.normRhs trs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> Flite.Pair l_1_0 (KnuthBendix.norm trs_0 r_1_1))
KnuthBendix.norm trs_0 !t_1 = KnuthBendix.head (KnuthBendix.normalForms trs_0 t_1)
KnuthBendix.normalForms trs_0 !t_1 = let reduced_1_0 = KnuthBendix.reduce trs_0 t_1 in if (KnuthBendix.null reduced_1_0) (Flite.Cons t_1 Flite.Nil) (KnuthBendix.concatMap (KnuthBendix.normalForms trs_0) reduced_1_0)
KnuthBendix.uniqueRules = KnuthBendix.nubBy KnuthBendix.equivPair
KnuthBendix.equivPair::B !_x_0 !_x_1 = select _x_0 (Flite.Pair a_1_0 b_1_1 -> select _x_1 (Flite.Pair c_2_0 d_2_1 -> KnuthBendix.dis (KnuthBendix.con (KnuthBendix.equiv a_1_0 c_2_0) (KnuthBendix.equiv b_1_1 d_2_1)) (KnuthBendix.con (KnuthBendix.equiv a_1_0 d_2_1) (KnuthBendix.equiv b_1_1 c_2_0))) )
KnuthBendix.equiv::B !t_0 !u_1 = KnuthBendix.con (KnuthBendix.isJust (KnuthBendix.match t_0 u_1)) (KnuthBendix.isJust (KnuthBendix.match u_1 t_0))
KnuthBendix.isJust::B !_x_0 = select _x_0 (Flite.Nothing -> False) (Flite.Just x_1_0 -> True)
KnuthBendix.nubBy e_0 !xs_1 = KnuthBendix.nubBySans Flite.Nil e_0 xs_1
KnuthBendix.nubBySans ss_0 e_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (KnuthBendix.elemBy e_1 x_1_0 ss_0) (KnuthBendix.nubBySans ss_0 e_1 xs_1_1) (Flite.Cons x_1_0 (KnuthBendix.nubBySans (Flite.Cons x_1_0 ss_0) e_1 xs_1_1)))
<{KnuthBendix._c;242;7_158}> !_x_0 vs_1 n_2::I newRule_3 rules_4 !rest_5 = select _x_0 (Flite.Pair eqs_1_0 rls_1_1 -> KnuthBendix.completionLoop vs_1 n_2 (KnuthBendix.simplifyEquations KnuthBendix.sig (Flite.Cons newRule_3 rules_4) (KnuthBendix.append rest_5 (KnuthBendix.append eqs_1_0 (KnuthBendix.getCriticalPairs (Flite.Cons newRule_3 rules_4) newRule_3)))) (KnuthBendix.uniqueRules rls_1_1))
KnuthBendix.getCriticalPairs trs_0 !r_1 = KnuthBendix.append (KnuthBendix.selfCriticalPairs trs_0 r_1) (KnuthBendix.concatMap (KnuthBendix.duoCriticalPairs trs_0 r_1) trs_0)
KnuthBendix.duoCriticalPairs trs_0 !_x_1 !_x_2 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> select _x_2 (Flite.Pair l2_2_0 r2_2_1 -> KnuthBendix.append (KnuthBendix.criticalPairs trs_0 True (Flite.Pair l1_1_0 r1_1_1) (Flite.Pair l2_2_0 r2_2_1)) (KnuthBendix.criticalPairs trs_0 False (Flite.Pair l2_2_0 r2_2_1) (Flite.Pair l1_1_0 r1_1_1))) )
KnuthBendix.criticalPairs trs_0 !allowRootPos_1::B !_x_2 !_x_3 = select _x_2 (Flite.Pair l1_1_0 r1_1_1 -> select _x_3 (Flite.Pair l2_2_0 r2_2_1 -> KnuthBendix.concatMap (KnuthBendix.criticalPairsAt trs_0 (Flite.Pair l1_1_0 r1_1_1) (Flite.Pair l2_2_0 r2_2_1)) (<{KnuthBendix._c;299;14_154}> allowRootPos_1 l1_1_0)) )
<{KnuthBendix._c;299;14_154}> !allowRootPos_0::B !l1_1 = select allowRootPos_0 (True -> KnuthBendix.positions l1_1) (False -> KnuthBendix.filter (KnuthBendix.non KnuthBendix.null) (KnuthBendix.positions l1_1))
KnuthBendix.non::B !f_0 x_1 = KnuthBendix.inv (f_0 x_1)
KnuthBendix.filter p_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (p_0 x_1_0) (Flite.Cons x_1_0 (KnuthBendix.filter p_0 xs_1_1)) (KnuthBendix.filter p_0 xs_1_1))
KnuthBendix.criticalPairsAt trs_0 !_x_1 !_x_2 !p_3 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> select _x_2 (Flite.Pair l2_2_0 r2_2_1 -> let t_3_0 = KnuthBendix.subterm l1_1_0 p_3 in <{KnuthBendix._c;308;7_153}> (KnuthBendix.isVar t_3_0) t_3_0 l2_2_0 trs_0 r1_1_1 r2_2_1 p_3 l1_1_0) )
<{KnuthBendix._c;308;7_153}> !_x_0::B t_1 l2_2 trs_3 r1_4 r2_5 p_6 l1_7 = select _x_0 (True -> Flite.Nil) (False -> <{KnuthBendix._c;310;16_152}> (KnuthBendix.unify t_1 l2_2) trs_3 r1_4 r2_5 p_6 l1_7)
KnuthBendix.unify !t1_0 !t2_1 = KnuthBendix.unifyWith (Flite.Cons t1_0 Flite.Nil) (Flite.Cons t2_1 Flite.Nil) Flite.Nil
KnuthBendix.unifyWith !_x_0 !_x_1 sub_2 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> Flite.Just sub_2) ) (Flite.Cons _x_1_0 ts1_1_1 -> select _x_1_0 (KnuthBendix.Var v_2_0 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> if (KnuthBendix.equalTerms t_3_0 (KnuthBendix.Var v_2_0)) (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 sub_2) (let vi_4_0 = KnuthBendix.subst sub_2 (KnuthBendix.Var v_2_0) in if (KnuthBendix.equalTerms vi_4_0 (KnuthBendix.Var v_2_0)) (let ti_5_0 = KnuthBendix.subst sub_2 t_3_0 in if (KnuthBendix.elemBy KnuthBendix.equalStrings_133 v_2_0 (KnuthBendix.vars ti_5_0)) Flite.Nothing (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 (KnuthBendix.substAdd (Flite.Cons (Flite.Pair v_2_0 ti_5_0) Flite.Nil) sub_2))) (let ti_5_0 = KnuthBendix.subst sub_2 t_3_0, mgu_5_1 = KnuthBendix.unify vi_4_0 ti_5_0 in if (KnuthBendix.isJust mgu_5_1) (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 (KnuthBendix.substAdd (KnuthBendix.fromJust mgu_5_1) sub_2)) Flite.Nothing))) ) (KnuthBendix.Fun f_2_0 ts_2_1 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> <{KnuthBendix._c;443;3_151}> t_3_0 ts2_3_1 f_2_0 ts_2_1 ts1_1_1 sub_2) ) )
<{KnuthBendix._c;443;3_151}> !t_0 ts2_1 f_2 ts_3 ts1_4 sub_5 = select t_0 (KnuthBendix.Var v_1_0 -> KnuthBendix.unifyWith (Flite.Cons (KnuthBendix.Var v_1_0) ts2_1) (Flite.Cons (KnuthBendix.Fun f_2 ts_3) ts1_4) sub_5) (KnuthBendix.Fun g_1_0 us_1_1 -> if (KnuthBendix.equalStrings_133 f_2 g_1_0) (KnuthBendix.unifyWith (KnuthBendix.append ts_3 ts1_4) (KnuthBendix.append us_1_1 ts2_1) sub_5) Flite.Nothing)
KnuthBendix.substAdd !subNew_0 subOld_1 = KnuthBendix.append subNew_0 ( (KnuthBendix.cross (KnuthBendix.subst subNew_0)) subOld_1)
<{KnuthBendix._c;310;16_152}> !_x_0 trs_1 r1_2 r2_3 p_4 l1_5 = select _x_0 (Flite.Nothing -> Flite.Nil) (Flite.Just sub_1_0 -> KnuthBendix.criticalPairsFrom (KnuthBendix.norm trs_1 (KnuthBendix.subst sub_1_0 r1_2)) (KnuthBendix.norm trs_1 (KnuthBendix.placeAt (KnuthBendix.subst sub_1_0 r2_3) p_4 (KnuthBendix.subst sub_1_0 l1_5))))
KnuthBendix.criticalPairsFrom !cpl_0 !cpr_1 = if (KnuthBendix.equalTerms cpl_0 cpr_1) Flite.Nil (Flite.Cons (Flite.Pair cpl_0 cpr_1) Flite.Nil)
KnuthBendix.selfCriticalPairs trs_0 !_x_1 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> KnuthBendix.criticalPairs trs_0 False (Flite.Pair l1_1_0 r1_1_1) (KnuthBendix.rename (Flite.Pair l1_1_0 r1_1_1)))
KnuthBendix.rename !_x_0 = select _x_0 (Flite.Pair l_1_0 r_1_1 -> let oldVars_2_0 = KnuthBendix.vars l_1_0, sub_2_1 = oldVars_2_0 ( KnuthBendix.Var (KnuthBendix.filter (KnuthBendix.non (KnuthBendix.flip (KnuthBendix.elemBy KnuthBendix.equalStrings_133) oldVars_2_0)) KnuthBendix.variables)) in Flite.Pair (KnuthBendix.subst sub_2_1 l_1_0) (KnuthBendix.subst sub_2_1 r_1_1))
KnuthBendix.simplifyEquations sig_0 trs_1 !eqns_2 = KnuthBendix.filter (KnuthBendix.non (KnuthBendix.uncurry KnuthBendix.equalTerms)) (KnuthBendix.uniqueRules ( (KnuthBendix.normEqn trs_1) eqns_2))
KnuthBendix.normEqn trs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> Flite.Pair (KnuthBendix.norm trs_0 l_1_0) (KnuthBendix.norm trs_0 r_1_1))
KnuthBendix.uncurry !f_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> f_0 x_1_0 y_1_1)
KnuthBendix.showResult !_x_0 sig_1 = select _x_0 (Flite.Just trs_1_0 -> KnuthBendix.append (Flite.str "\nSuccess\n") (KnuthBendix.showRules sig_1 ( KnuthBendix.rn trs_1_0))) (Flite.Nothing -> Flite.str "\nFailure\n")
KnuthBendix.rn !_x_0 = select _x_0 (Flite.Pair l_1_0 r_1_1 -> let sub_2_0 = (KnuthBendix.vars l_1_0) ( KnuthBendix.Var KnuthBendix.variables) in Flite.Pair (KnuthBendix.subst sub_2_0 l_1_0) (KnuthBendix.subst sub_2_0 r_1_1))
KnuthBendix.showRules sig_0 !rules_1 = KnuthBendix.unlines ( (KnuthBendix.showRule sig_0) rules_1)
KnuthBendix.showRule sig_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.append (KnuthBendix.showTerm sig_0 x_1_0) (KnuthBendix.append (Flite.str " -> ") (KnuthBendix.showTerm sig_0 y_1_1)))
KnuthBendix.showTerm sig_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> v_1_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> if (KnuthBendix.isInfix_134 sig_0 f_1_0) (KnuthBendix.append (Flite.str "(") (KnuthBendix.append (KnuthBendix.showTerm sig_0 (KnuthBendix.elemAt ts_1_1 0)) (KnuthBendix.append (Flite.str " ") (KnuthBendix.append f_1_0 (KnuthBendix.append (Flite.str " ") (KnuthBendix.append (KnuthBendix.showTerm sig_0 (KnuthBendix.elemAt ts_1_1 1)) (Flite.str ")"))))))) (if (KnuthBendix.null ts_1_1) f_1_0 (KnuthBendix.append f_1_0 (KnuthBendix.append (Flite.str "(") (KnuthBendix.append (KnuthBendix.concatStrings (KnuthBendix.intersperse (Flite.str ",") ( (KnuthBendix.showTerm sig_0) ts_1_1))) (Flite.str ")"))))))
KnuthBendix.intersperse i_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> Flite.Cons x_1_0 Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons x_1_0 (Flite.Cons i_0 (KnuthBendix.intersperse i_0 (Flite.Cons y_2_0 ys_2_1)))) )
KnuthBendix.concatStrings !ss_0 = KnuthBendix.foldr KnuthBendix.append Flite.Nil ss_0
KnuthBendix.isInfix_134::B !sig_0 f_1 = KnuthBendix.maybe False KnuthBendix.snd (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 sig_0)
KnuthBendix.maybe n_0 j_1 !_x_2 = select _x_2 (Flite.Nothing -> n_0) (Flite.Just x_1_0 -> j_1 x_1_0)
KnuthBendix.unlines !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons s_1_0 ss_1_1 -> KnuthBendix.append s_1_0 (Flite.Cons (Flite.char '\n') (KnuthBendix.unlines ss_1_1)))
KnuthBendix.showEqns sig_0 !eqns_1 = KnuthBendix.unlines ( (KnuthBendix.showEqn sig_0) eqns_1)
KnuthBendix.showEqn sig_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.append (KnuthBendix.showTerm sig_0 x_1_0) (KnuthBendix.append (Flite.str " = ") (KnuthBendix.showTerm sig_0 y_1_1)))
KnuthBendix.checkEquations::B !es_0 sig_1 = KnuthBendix.all (KnuthBendix.both (KnuthBendix.checkTerm sig_1)) es_0
KnuthBendix.checkTerm::B sig_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.con (eqI (KnuthBendix.len ts_1_1) (KnuthBendix.arity_140 sig_0 f_1_0)) (KnuthBendix.all (KnuthBendix.checkTerm sig_0) ts_1_1))
KnuthBendix.all::B p_0 !xs_1 = KnuthBendix.and ( p_0 xs_1)
KnuthBendix.arity_140::I !sig_0 f_1 = KnuthBendix.maybe (subI 0 1) KnuthBendix.fst (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 sig_0)
KnuthBendix.both::B !p_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.con (p_0 x_1_0) (p_0 y_1_1))
Markdown is supported
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