Skip to content

GitLab

Commit 3ffa20f0 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

all bugs fixed, trs works

parent 612c6131
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 67 additions and 798 deletions
trs/main.ml
View file @ 3ffa20f0
......@@ -5,11 +5,21 @@ 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 "HDEQ SA SA\n"))); *)
Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(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 "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 "PCP 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"))) *)
(tree_of_string "PCP (CONS ((PAIR SA SABB)) (CONS (PAIR SBB SB) NIL))\n"))) *)
Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "PCP (CONS ((PAIR SA SABBB)) (CONS (PAIR SBB SB) NIL))\n")))
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "ITE (OR (ISEMPTY x) (ISEMPTY y)) (AND (ISEMPTY x) (ISEMPTY y)) (AND (HDEQ x y) (f (TLSTR x) (TLSTR y)))\n"))) *)
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "CROSSCMB (CONS ((PAIR EMPTY SB)) (CONS (PAIR SBB EMPTY) NIL)) (CONS ((PAIR SA SABB)) (CONS (PAIR SBB SB) NIL))\n"))) *)
(* Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "FINDEQ (CONS ((PAIR EMPTY EMPTY)) (CONS (PAIR SBB EMPTY) NIL))\n"))) *)
(* Printf.printf "%s\n" (Core.a_term_to_string (List.hd (List.rev reduction))); *)
trslib/cltrs.txt 0 → 100644
View file @ 3ffa20f0
(VAR f x y z a b c p)
(RULES
true(x,y) -> x
false(x,y) -> x
Y(f) -> f(Y(f))
)
trslib/core.ml
View file @ 3ffa20f0
......@@ -10,10 +10,10 @@ type trs_symbol =
CONS | HDL | TLL | ISNIL | APPENDP | APPEND |
SIMPP | SIMP | PVALID | FINDEQP | FINDEQ | CMB |
MAPCMBP | MAPCMB | CROSSCMBP | CROSSCMB | PCPP | PCP |
SA | SB | SAA | SAB | SBA | SBB | SAAA
SA | SB | SAA | SAB | SBA | SBB | SAAA | SABB
type trs_term =
S of trs_symbol | FA of trs_term * trs_term
V of string | S of trs_symbol | FA of trs_term * trs_term
let trs_symbol_to_string symbol =
match symbol with
......@@ -70,6 +70,15 @@ let trs_symbol_to_string symbol =
| SBA -> "SBA"
| SBB -> "SBB"
| SAAA -> "SAAA"
| SABB -> "SABB"
let rec _trs_term_to_string2 term =
match term with
| FA (a,b) -> "FA(" ^ (_trs_term_to_string2 a) ^ ", " ^ (_trs_term_to_string2 b) ^ ")"
| S a -> "S " ^ (trs_symbol_to_string a)
| V x -> x
let trs_term_to_string2 term = _trs_term_to_string2 term
let rec _trs_term_to_string term =
match term with
......@@ -83,6 +92,7 @@ let rec _trs_term_to_string term =
)
| S a -> trs_symbol_to_string a
| V x -> x
(** Convert a {e a_term} to string *)
let trs_term_to_string term = _trs_term_to_string term
......@@ -109,13 +119,14 @@ let rec _reduce_lo term =
| 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 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), S FALSE)
| FA (FA (S OR, a), b) -> FA (FA (a, S TRUE), 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 (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 (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(FA(r, FA(S TLL, x)), y)))
| FA (FA (S APPEND, a), b) -> FA(FA(FA(S Y, S APPENDP), a), b)
(* STRINGS *)
| 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)
......@@ -124,10 +135,11 @@ let rec _reduce_lo term =
| 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 SABB, x), a), b) -> FA(a,FA(b,FA(b,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)))) )
| FA (FA (S EQ, x), y) -> ( FA(FA(FA(S Y, S EQP),x),y) )
| 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))))
| FA (FA (S EQ, x), y) -> FA(FA(FA(S Y, S EQP),x),y)
| FA (FA (FA (FA (S PREPA, s), x), a), b) -> (FA(a,FA(FA(FA(s,x),a),b)))
| FA (FA (FA (FA (S PREPB, s), x), a), b) -> (FA(b,FA(FA(FA(s,x),a),b)))
| FA (FA (FA (FA (FA (S CONCAT, y), z), x), a), b) -> ( FA (FA( FA(y, FA( FA( FA(z, x), a), b)), a), b) )
......@@ -140,15 +152,26 @@ let rec _reduce_lo term =
| 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)
| FA (FA (S CMB, p), s) -> FA(FA(S MKPAIR, FA(FA(S CONCAT,FA(S FST, p)),FA(S FST, s))), FA(FA(S CONCAT,FA(S SND, p)),FA(S SND, s)) )
| FA (FA (FA (S MAPCMBP, r), x), y) -> FA(FA(FA(S ITE, FA(S ISNIL, y)),S NIL),
FA(FA(FA(S ITE,FA(S PVALID, FA(FA(S CMB,x),FA(S HDL,y)))), FA(FA(S CONS, FA(S SIMP, FA(FA(S CMB,x),FA(S HDL,y)))),FA(FA(r,x),FA(S TLL, y)))),FA(FA(r,x),FA(S TLL, y)))
)
| FA (FA (FA (S MAPCMBP, r), x), y) -> FA(FA(FA(S ITE, FA(S ISNIL, y)), S NIL), FA(FA(FA(S ITE, FA(S PVALID, FA(FA(S CMB, x), FA(S HDL, y)))), FA(FA(S CONS, FA(S SIMP, FA(FA(S CMB, x), FA(S HDL, y)))), FA(FA(r, x), FA(S TLL, y)))), FA(FA(r, x), FA(S TLL, y))))
| FA (FA (S MAPCMB, x), y) -> FA(FA(FA(S Y, S MAPCMBP),x),y)
| FA (FA (FA (S CROSSCMBP, r), x), y) -> FA(FA(FA(S ITE,FA(S ISNIL,x)),S NIL),FA(FA(S APPEND,FA(FA(S MAPCMB,FA(S HDL, x)),y)),FA(FA(r,FA(S TLL, x)),y)))
| FA (FA (FA (S CROSSCMBP, r), x), y) ->
FA(FA(FA(S ITE,
(* ISNIL x *)
FA(S ISNIL, x)
),
(* NIL *)
S NIL
),
(* (APPEND (MAP CMB (HD L x) y) (r (TL L x) y)) *)
FA(FA(S APPEND, FA(FA(S MAPCMB,FA(S HDL, x)),y)),
FA(FA(r,FA(S TLL, x)),y)
)
)
| FA (FA (S CROSSCMB, x), y) -> FA(FA(FA(S Y, S CROSSCMBP),x),y)
| FA (FA (FA (S PCPP, r), x), y) -> FA(FA(FA(S ITE,FA(S ISNIL,x)),S FALSE),FA(FA(FA(S ITE,FA(S FINDEQ,x)),S TRUE),FA(FA(r,FA(FA(S CROSSCMB,x),y)),y)))
| FA (FA (FA (S PCPP, r), x), y) -> FA(FA(FA(S ITE, FA(S ISNIL, x)), S FALSE), FA(FA(FA(S ITE, FA(S FINDEQ, x)), S TRUE), FA(FA(r, FA(FA(S CROSSCMB, x), y)), y)))
| FA (S PCP, x) -> FA(FA(FA(S Y, S PCPP),x),x)
| S _ -> term
| V _ -> term
| FA (a,b) ->
let a_nf = _reduce_lo a in
if a_nf = a then FA (a,_reduce_lo b)
......@@ -159,7 +182,7 @@ let reduce_lo term =
_reduce_lo term
let rec nf term =
Printf.printf "%s\n" (trs_term_to_string term);
(* Printf.printf "%s\n" (trs_term_to_string term); *)
let new_term = reduce_lo term in
if new_term = term then term else nf new_term
......
trslib/lexer.mll
View file @ 3ffa20f0
......@@ -5,6 +5,9 @@
exception Eof
}
let letter = ['a'-'z' 'A'-'Z']
let id = letter+
rule token = parse
['\t'] { token lexbuf } (* skip blanks *)
| ['\n' ] { EOF }
......@@ -58,10 +61,12 @@ rule token = parse
| "PCPP" { PCPP }
| "PCP" { PCP }
| "SAAA" { SAAA }
| "SABB" { SABB }
| "SAA" { SAA }
| "SAB" { SAB }
| "SBA" { SBA }
| "SBB" { SBB }
| "SA" { SA }
| "SB" { SB }
| id { V (Lexing.lexeme lexbuf) }
| eof { raise Eof }
trslib/parser.mly
View file @ 3ffa20f0
......@@ -8,10 +8,11 @@
%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 SA SB SAA SAB SBA SBB SAAA SABB
%token LPAREN RPAREN
%token EOF
%token BLANK
%token <string> V
%left BLANK
......@@ -73,6 +74,7 @@ T :
| PCPP { S PCPP }
| PCP { S PCP }
| SAAA { S SAAA }
| SABB { S SABB }
| SBB { S SBB }
| SBA { S SBA }
| SAB { S SAB }
......@@ -81,6 +83,7 @@ T :
| SA { S SA }
| T BLANK T { FA($1, $3) }
| LPAREN T RPAREN { $2 }
| V { V $1 }
;
%%
zmp.txt deleted 100644 → 0
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