Skip to content

GitLab

Commit 612c6131 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

bugfix in simp function

parent 08c457e3
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 823 additions and 10 deletions
trs/main.ml
View file @ 612c6131
......@@ -4,8 +4,12 @@ let tree_of_string s = Parser.input Lexer.token (Lexing.from_string s)
let () =
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "APPEND NIL (CONS NIL NIL)\n"))); *)
(tree_of_string "HDEQ SA SA\n"))); *)
Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "PCP NIL\n")))
(tree_of_string "PCP (CONS (PAIR SB SAA) (CONS ((PAIR SAAA SB)) (CONS (PAIR SA SAB) NIL)))\n")))
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "EQ SB SB\n"))) *)
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "TLL (CONS ((PAIR SA SB)) (CONS (PAIR SA SA) NIL))\n"))) *)
(* Printf.printf "%s\n" (Core.a_term_to_string (List.hd (List.rev reduction))); *)
trslib/core.ml
View file @ 612c6131
......@@ -9,7 +9,8 @@ type trs_symbol =
HDA | HDB | HDEQ | EQP | EQ | PREFIXP | PREFIX | NIL |
CONS | HDL | TLL | ISNIL | APPENDP | APPEND |
SIMPP | SIMP | PVALID | FINDEQP | FINDEQ | CMB |
MAPCMBP | MAPCMB | CROSSCMBP | CROSSCMB | PCPP | PCP
MAPCMBP | MAPCMB | CROSSCMBP | CROSSCMB | PCPP | PCP |
SA | SB | SAA | SAB | SBA | SBB | SAAA
type trs_term =
S of trs_symbol | FA of trs_term * trs_term
......@@ -62,6 +63,13 @@ let trs_symbol_to_string symbol =
| CROSSCMB -> "CROSSCMB"
| PCPP -> "PCPP"
| PCP -> "PCP"
| SA -> "SA"
| SB -> "SB"
| SAA -> "SAA"
| SAB -> "SAB"
| SBA -> "SBA"
| SBB -> "SBB"
| SAAA -> "SAAA"
let rec _trs_term_to_string term =
match term with
......@@ -69,6 +77,7 @@ let rec _trs_term_to_string term =
(
match a,b with
| FA _, FA _ -> "(" ^ (_trs_term_to_string a) ^ ") (" ^ (_trs_term_to_string b) ^ ")"
| _, FA _ -> (_trs_term_to_string a) ^ " (" ^ (_trs_term_to_string b) ^ ")"
| FA _, _ -> "(" ^ (_trs_term_to_string a) ^ ") " ^ (_trs_term_to_string b)
| _, _ -> (_trs_term_to_string a) ^ " " ^ (_trs_term_to_string b)
)
......@@ -83,9 +92,10 @@ let itetruefalse = FA (FA (S ITE, S FALSE), S TRUE)
let rec _reduce_lo term =
match term with
| FA (FA (S TRUE, a), b) -> a
| FA (FA (S FALSE, a), b) -> b
| FA (S Y, a) -> ( FA (a, FA (S Y, a)) )
| FA (S NIL, x) -> x
| FA (S TLL, x) -> x
| FA (S AT, a) -> S TRUE
| FA (S AF, a) -> S FALSE
| FA (S ISNIL, a) -> ( FA (S FST, a) )
......@@ -94,20 +104,26 @@ let rec _reduce_lo term =
| FA (S HDA, s) -> ( FA (FA(FA(s, S FALSE), S AT), S AF) )
| FA (S HDB, s) -> ( FA (FA(FA(s, S FALSE), S AF), S AT) )
| FA (S ISEMPTY, s) -> (FA( FA( FA(s, S TRUE), S AF) ,S AF))
| FA (S HDL, z) -> (FA(S FST, FA(S SND, z)))
| FA (S HDL, z) -> FA(S FST, FA(S SND, z))
| FA (S TLL, z) -> FA(S SND, FA(S SND, z))
| FA (S NEXTA, x) -> ( FA (FA(S PAIR, FA(S PREPA, FA(S FST, x))), FA(S FST, x)) )
| FA (S NEXTB, x) -> ( FA (FA(S PAIR, FA(S PREPB, FA(S FST, x))), FA(S FST, x)) )
| FA (S TLSTR, s) -> ( FA(S SND, FA(FA(FA(s, FA(FA(S PAIR, S EMPTY), S EMPTY)), S NEXTA), S NEXTB)) )
| FA (FA (S CONS, x), y) -> ( FA(FA(S PAIR, S FALSE), FA(FA(S PAIR,x),y) ))
| FA (FA (S AND, a), b) -> ( FA (FA (a, b), a) )
| FA (FA (S OR, a), b) -> ( FA (FA (a, a), b) )
| FA (FA (S TRUE, a), b) -> a
| FA (FA (S FALSE, a), b) -> b
| FA (FA (S MKPAIR, a), b) -> (FA(FA(S PAIR,a),b))
| FA (FA (S MKPAIR, a), b) -> FA(FA(S PAIR,a),b)
| FA (FA (S HDEQ, a), b) -> (FA(FA(S OR, FA(FA(S AND, FA(S HDA, a)),FA(S HDA, b))), FA(FA(S AND, FA(S HDB, a)),FA(S HDB, b))))
| FA (FA (S APPEND, a), b) -> (FA(FA(FA(S Y, S APPENDP),a),b))
| FA (FA (FA (S APPENDP, r), x), y) -> (FA(FA(FA(S ITE, FA(S ISNIL,x)),y),FA(FA(S CONS,FA(S HDL, x)),FA(r,FA(FA(S TLL, x),y)))))
| FA (FA (FA (S EMPTY, x), a), b) -> x
| FA (FA (FA (S SA, x), a), b) -> FA(a,x)
| FA (FA (FA (S SB, x), a), b) -> FA(b,x)
| FA (FA (FA (S SAA, x), a), b) -> FA(a,FA(a,x))
| FA (FA (FA (S SAB, x), a), b) -> FA(a,FA(b,x))
| FA (FA (FA (S SBA, x), a), b) -> FA(b,FA(a,x))
| FA (FA (FA (S SBB, x), a), b) -> FA(b,FA(b,x))
| FA (FA (FA (S SAAA, x), a), b) -> FA(a,FA(a,FA(a,x)))
| FA (FA (FA (S ITE, c), a), b) -> ( FA (FA (c, a), b) )
| FA (FA (FA (S PAIR, a), b), c) -> ( FA (FA (c, a), b) )
| FA (FA (FA (S EQP, f), x), y) -> ( FA(FA(FA(S ITE, FA(FA(S OR,FA(S ISEMPTY, x)),FA(S ISEMPTY, y))),FA(FA(S AND,FA(S ISEMPTY, x)),FA(S ISEMPTY, y))), FA(FA(S AND, FA(FA(S HDEQ, x), y)),FA(FA(f, FA(S TLSTR, x)),FA(S TLSTR, y)))) )
......@@ -118,8 +134,8 @@ let rec _reduce_lo term =
| FA (FA (FA (S PREFIXP, r), x), y) -> (FA(FA(FA(S ITE, FA(S ISEMPTY, x)),S TRUE),
FA(FA(S AND,FA(FA(S HDEQ, x), y)),FA(FA(r,FA(S TLSTR, x)),FA(S TLSTR, y)))))
| FA (FA (S PREFIX, a), b) -> (FA(FA(FA(S Y, S PREFIXP),a),b))
| FA (FA(FA(S SIMPP,r), x),y) -> FA(FA(FA(S ITE, FA(FA(S OR,FA(S ISEMPTY, x)),FA(S ISEMPTY, y))),FA(FA(S MKPAIR,x),y)),FA(FA(r,FA(S TLSTR, x)),FA(S TLSTR, y)))
| FA (S SIMP, p) -> FA(FA(FA(S Y, S SIMPP),FA(S FST, p)),FA(S FST, p))
| FA (FA(FA(S SIMPP,r), x),y) -> FA(FA(FA(S ITE, FA(FA(S OR,FA(S ISEMPTY, x)),FA(S ISEMPTY, y))),FA(FA(S MKPAIR,x),y)),FA(FA(r,FA(S TLSTR,x)),FA(S TLSTR,y)))
| FA (S SIMP, p) -> FA(FA(FA(S Y, S SIMPP),FA(S FST, p)),FA(S SND, p))
| FA (S PVALID, x) -> FA(FA(S OR,FA(FA(S PREFIX,FA(S FST, x)),FA(S SND, x))),FA(FA(S PREFIX,FA(S SND, x)),FA(S FST,x)))
| FA (FA (S FINDEQP, r), x) -> FA(FA(FA(S ITE,FA(S ISNIL,x)),S FALSE),FA(FA(S OR,FA(FA(S EQ,FA(S FST,FA(S HDL,x))),FA(S SND,FA(S HDL, x)))),FA(r,FA(S TLL, x))))
| FA (S FINDEQ, x) -> FA(FA(S Y, S FINDEQP),x)
......
trslib/lexer.mll
View file @ 612c6131
......@@ -57,4 +57,11 @@ rule token = parse
| "CROSSCMB" { CROSSCMB }
| "PCPP" { PCPP }
| "PCP" { PCP }
| "SAAA" { SAAA }
| "SAA" { SAA }
| "SAB" { SAB }
| "SBA" { SBA }
| "SBB" { SBB }
| "SA" { SA }
| "SB" { SB }
| eof { raise Eof }
trslib/parser.mly
View file @ 612c6131
......@@ -8,6 +8,7 @@
%token EMPTY ISEMPTY CONCAT PREPA PREPB NEXTA NEXTB TLSTR HDA HDB HDEQ EQP EQ PREFIXP PREFIX
%token NIL CONS HDL TLL ISNIL APPENDP APPEND
%token SIMPP SIMP PVALID FINDEQP FINDEQ CMB MAPCMBP MAPCMB CROSSCMBP CROSSCMB PCPP PCP
%token SA SB SAA SAB SBA SBB SAAA
%token LPAREN RPAREN
%token EOF
%token BLANK
......@@ -71,6 +72,13 @@ T :
| CROSSCMB { S CROSSCMB }
| PCPP { S PCPP }
| PCP { S PCP }
| SAAA { S SAAA }
| SBB { S SBB }
| SBA { S SBA }
| SAB { S SAB }
| SAA { S SAA }
| SB { S SB }
| SA { S SA }
| T BLANK T { FA($1, $3) }
| LPAREN T RPAREN { $2 }
;
......
zmp.txt 0 → 100644
View file @ 612c6131
This diff is collapsed.
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