Commit 08c457e3 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

pcp trs

parent 806a28dc
......@@ -783,18 +783,19 @@ let rec _reduce_lo subst term =
let reduce_lo subst term = _reduce_lo subst term
let rec _reduce_ri subst term =
let rec _reduce_ne subst term =
match term with
| AVar (s, t) -> term
| ALam ((xs, e), t) -> ALam ((xs, _reduce_ri subst e), t)
| ALam ((xs, e), t) -> ALam ((xs, _reduce_ne subst e), t)
| AApp (e1, e2, t) -> (
let right = _reduce_ri subst e2 in
let left = _reduce_ri subst e1 in
let right = _reduce_ne subst e2 in
match e1 with
| ALam _ -> beta subst (AApp (left, right, t))
| _ -> (AApp (left, right, t)))
| ALam _ -> beta subst (AApp (e1, right, t))
| _ ->
let left = _reduce_ne subst e1 in
AApp (left, right, t))
let reduce_ri subst term = _reduce_ri subst term
let reduce_ne subst term = _reduce_ne subst term
let rec _extract_first_redex_pos path =
match path with
......@@ -868,6 +869,53 @@ let rec nf subst term =
let new_term = reduce_lo subst term in
if new_term = term then term else nf subst new_term
let rec _reduce_lo_memo subst term cache =
match Hashtbl.mem cache term with
| true ->
Printf.printf "Cache hit _reduce_lo_memo.\n";
Hashtbl.find cache term
| false -> (
Printf.printf "NO Cache hit %s.\n\n" (a_term_to_string term);
match term with
| AVar (s, t) -> term
| ALam ((xs, e), t) -> ALam ((xs, _reduce_lo_memo subst e cache), t)
| AApp (e1, e2, t) -> (
match e1 with
| ALam _ -> beta subst term
| _ ->
let left = _reduce_lo_memo subst e1 cache in
Hashtbl.add cache e1 left;
(* Printf.printf "Cache add %s.\n" (a_term_to_string e1); *)
if left = e1 then
let arg = _reduce_lo_memo subst e2 cache in
(* Printf.printf "Cache add %s.\n" (a_term_to_string e2); *)
Hashtbl.add cache e2 arg;
AApp (e1, arg, t)
else AApp (left, e2, t) ))
let reduce_lo_memo subst term =
let h = Hashtbl.create 100 in
_reduce_lo_memo subst term h
let rec _nf_memo subst term cache =
(
match Hashtbl.mem cache term with
| true -> (
let tc = Hashtbl.find cache term in
Printf.printf "Cache hit.\n";
if tc = term then tc else _nf_memo subst tc cache)
| false -> (
Printf.printf "NO Cache hit %s.\n\n" (a_term_to_string term);
let result = reduce_lo_memo subst term in
Hashtbl.add cache term result;
if result = term then result else _nf_memo subst result cache)
)
let nf_memo subst term =
let cache = Hashtbl.create 1000 in
_nf_memo subst term cache
let is_linear term =
let be = b_edges term in
not (Util.duplicates (List.map (fun x -> List.hd (List.rev x)) be))
......@@ -8,4 +8,4 @@
(menhir
(modules grammar))
(documentation)
(documentation (package alpha))
......@@ -103,7 +103,9 @@ let s_b = "(/x a b.b x)"
let s_ab = "(/x a b.a (b x))"
let s_aa = "(/x a b.a (a x))"
let s_ba = "(/x a b.b (a x))"
let t_ba = tree_of_string s_ba
let s_baba = "(/x a b.b (a (b (a x))))"
let t_baba = tree_of_string s_baba
(* LIST OF TILES *)
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.a (b x)) (/x a b.a x))"
......@@ -114,6 +116,15 @@ let t_tile2 = tree_of_string s_tile2
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))" *)
let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.a (b (b x))))"
let t_tile1 = tree_of_string s_tile1
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.b (b x)) (/x a b.b x))"
let t_tile2 = tree_of_string s_tile2
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))"
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (b (a x))) (/x a b.b x))"
let t_tile1 = tree_of_string s_tile1
......@@ -124,14 +135,14 @@ let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (b x)))"
let t_tile3 = tree_of_string s_tile3 *)
(* SOLUTION 2113 *)
let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.b (b (b x))))"
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.b (b (b x))))"
let t_tile1 = tree_of_string s_tile1
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.b (a (b (b (b x))))) (/x a b.b (a x)))"
let t_tile2 = tree_of_string s_tile2
let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b (a x)) (/x a b.a x))"
let t_tile3 = tree_of_string s_tile3
let t_tile3 = tree_of_string s_tile3 *)
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (a (a x))) (/x a b.b x))"
......@@ -143,7 +154,7 @@ let t_tile2 = tree_of_string s_tile2
let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (a x)))"
let t_tile3 = tree_of_string s_tile3 *)
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile3 ^ " (" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")))"
(* let s_tiles = "(" ^ s_cons ^ " " ^ s_tile3 ^ " (" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")))" *)
let t_tiles = tree_of_string s_tiles
......@@ -187,15 +198,16 @@ let ls = tree_of_string ("(/c.(c (/x./y.y)) (/c.(c (/c.(c (/x./a./b.b x)) (/x./a
UnT), t_tiles, UnT) *)
let tilestiles = Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT)
let tmp = Core.AApp(Core.AApp(t_cross_append, tilestiles, UnT), t_tiles, UnT)
(* let tmp = Core.AApp(Core.AApp(t_cross_append, tilestiles, UnT), t_tiles, UnT) *)
let tmp = Core.AApp(Core.AApp(eq_str, t_baba, UnT), t_baba, UnT)
(* let tmp = tilestiles *)
let pcpp = tree_of_string (s_pcp ^" "^s_tiles^" y")
let () =
Printf.printf "PCP\n";
Printf.printf "-----------------------------\n%s\n-----------------------------\n" (Core.a_term_to_string tmp);
Printf.printf "tiles: %s\n" (s_tiles);
Printf.printf "res_tmp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst tmp));
(* Printf.printf "tiles: %s\n" (s_tiles); *)
Printf.printf "res_tmp: %s\n" (Core.a_term_to_string (Core.nf_memo Core.casubst tmp));
(* Printf.printf "pcpp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst pcpp)); *)
Printf.printf "Alpha conversions: %d\n" (!Core.counter);
Printf.printf "Beta conversions: %d\n" (!Core.beta_counter);
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.1"
maintainer: ["samuel.frontull@student.uibk.ac.at"]
authors: ["Samuel Frontull"]
license: "Apache-2.0"
homepage: "https://github.com/schtailmuel/trs"
bug-reports: "https://github.com/schtailmuel/trs/issues"
depends: [
"dune" {>= "2.0"}
]
build: [
["dune" "subst"] {pinned}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git+https://github.com/schtailmuel/trs.git"
(executables
(names main)
(libraries trs))
open Trs
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"))); *)
Printf.printf "%s\n" (Core.trs_term_to_string (Core.nf
(tree_of_string "PCP NIL\n")))
(* Printf.printf "%s\n" (Core.a_term_to_string (List.hd (List.rev reduction))); *)
(** Type definition of the a term.
Each abstraction, application and variable has additional information
about the type and the position in the term.
*)
type trs_symbol =
ITE | TRUE | FALSE | AND | OR | AT | AF |
PAIR | FST | SND | MKPAIR | Y | EMPTY | ISEMPTY |
CONCAT | PREPA | PREPB | NEXTA | NEXTB | TLSTR |
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
type trs_term =
S of trs_symbol | FA of trs_term * trs_term
let trs_symbol_to_string symbol =
match symbol with
| ITE -> "ITE"
| TRUE -> "TRUE"
| FALSE -> "FALSE"
| AND -> "AND"
| OR -> "OR"
| AT -> "AT"
| AF -> "AF"
| PAIR -> "PAIR"
| FST -> "FST"
| SND -> "SND"
| MKPAIR -> "MKPAIR"
| Y -> "Y"
| EMPTY -> "EMPTY"
| ISEMPTY -> "ISEMPTY"
| CONCAT -> "CONCAT"
| PREPA -> "PREPA"
| PREPB -> "PREPB"
| NEXTA -> "NEXTA"
| NEXTB -> "NEXTB"
| TLSTR -> "TLSTR"
| HDA -> "HDA"
| HDB -> "HDB"
| HDEQ -> "HDEQ"
| EQP -> "EQP"
| EQ -> "EQ"
| PREFIXP -> "PREFIXP"
| PREFIX -> "PREFIX"
| NIL -> "NIL"
| CONS -> "CONS"
| HDL -> "HDL"
| TLL -> "TLL"
| ISNIL -> "ISNIL"
| APPENDP -> "APPENDP"
| APPEND -> "APPEND"
| SIMPP -> "SIMPP"
| SIMP -> "SIMP"
| PVALID -> "PVALID"
| FINDEQP -> "FINDEQP"
| FINDEQ -> "FINDEQ"
| CMB -> "CMB"
| MAPCMBP -> "MAPCMBP"
| MAPCMB -> "MAPCMB"
| CROSSCMBP -> "CROSSCMBP"
| CROSSCMB -> "CROSSCMB"
| PCPP -> "PCPP"
| PCP -> "PCP"
let rec _trs_term_to_string term =
match term with
| FA (a,b) ->
(
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)
| _, _ -> (_trs_term_to_string a) ^ " " ^ (_trs_term_to_string b)
)
| S a -> trs_symbol_to_string a
(** Convert a {e a_term} to string *)
let trs_term_to_string term = _trs_term_to_string term
(* let tree_of_string s = Grammar.input Lexer.token (Lexing.from_string s) *)
let itetruefalse = FA (FA (S ITE, S FALSE), S TRUE)
let rec _reduce_lo term =
match term with
| 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) )
| FA (S FST, a) -> ( FA (a, S TRUE) )
| FA (S SND, a) -> ( FA (a, S FALSE) )
| 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 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 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 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 (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) )
| 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 (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)
| 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 (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 (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 (S PCP, x) -> FA(FA(FA(S Y, S PCPP),x),x)
| S _ -> term
| FA (a,b) ->
let a_nf = _reduce_lo a in
if a_nf = a then FA (a,_reduce_lo b)
else FA (a_nf, b)
(* | _ -> failwith("NOT COVERED " ^ (trs_term_to_string term)) *)
let reduce_lo term =
_reduce_lo term
let rec nf 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
(* let () =
Printf.printf "%s\n" (trs_term_to_string (tree_of_string "ITE TRUE")) *)
(library
(flags (-w))
(name trs)
(public_name trs))
(ocamllex lexer)
(menhir
(modules parser))
(* File lexer.mll *)
{
open Parser (* The type token is defined in parser.mli *)
open Lexing
exception Eof
}
rule token = parse
['\t'] { token lexbuf } (* skip blanks *)
| ['\n' ] { EOF }
| ' ' { BLANK }
| '(' { LPAREN }
| ')' { RPAREN }
| "ITE" { ITE }
| "TRUE" { TRUE }
| "FALSE" { FALSE }
| "AND" { AND }
| "OR" { OR }
| "AT" { AT }
| "AF" { AF }
| "PAIR" { PAIR }
| "FST" { FST }
| "SND" { SND }
| "MKPAIR" { MKPAIR }
| "Y" { Y }
| "EMPTY" { EMPTY }
| "ISEMPTY" { ISEMPTY }
| "CONCAT" { CONCAT }
| "PREPA" { PREPA }
| "PREPB" { PREPB }
| "NEXTA" { NEXTA }
| "NEXTB" { NEXTB }
| "TLSTR" { TLSTR }
| "HDA" { HDA }
| "HDB" { HDB }
| "HDEQ" { HDEQ }
| "EQP" { EQP }
| "EQ" { EQ }
| "PREFIXP" { PREFIXP }
| "PREFIX" { PREFIX }
| "NIL" { NIL }
| "CONS" { CONS }
| "HDL" { HDL }
| "TLL" { TLL }
| "ISNIL" { ISNIL }
| "APPENDP" { APPENDP }
| "APPEND" { APPEND }
| "SIMPP" { SIMPP }
| "SIMP" { SIMP }
| "PVALID" { PVALID }
| "FINDEQP" { FINDEQP }
| "FINDEQ" { FINDEQ }
| "CMB" { CMB }
| "MAPCMBP" { MAPCMBP }
| "MAPCMB" { MAPCMB }
| "CROSSCMBP" { CROSSCMBP }
| "CROSSCMB" { CROSSCMB }
| "PCPP" { PCPP }
| "PCP" { PCP }
| eof { raise Eof }
%{
open Core
%}
%token ITE TRUE FALSE AND OR AT AF
%token PAIR FST SND MKPAIR
%token Y
%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 LPAREN RPAREN
%token EOF
%token BLANK
%left BLANK
%start input
%type <Core.trs_term> input
%type <Core.trs_term> T
/* Grammar follows */
%%
input:
T EOF { $1 }
;
T :
ITE { S ITE }
| TRUE { S TRUE }
| FALSE { S FALSE }
| AND { S AND }
| OR { S OR }
| AT { S AT }
| AF { S AF }
| PAIR { S PAIR }
| FST { S FST }
| SND { S SND }
| MKPAIR { S MKPAIR }
| Y { S Y }
| EMPTY { S EMPTY }
| ISEMPTY { S ISEMPTY }
| CONCAT { S CONCAT }
| PREPA { S PREPA }
| PREPB { S PREPB }
| NEXTA { S NEXTA }
| NEXTB { S NEXTB }
| TLSTR { S TLSTR }
| HDA { S HDA }
| HDB { S HDB }
| HDEQ { S HDEQ }
| EQP { S EQP }
| EQ { S EQ }
| PREFIXP { S PREFIXP }
| PREFIX { S PREFIX }
| NIL { S NIL }
| CONS { S CONS }
| HDL { S HDL }
| TLL { S TLL }
| ISNIL { S ISNIL }
| APPENDP { S APPENDP }
| APPEND { S APPEND }
| SIMPP { S SIMPP }
| SIMP { S SIMP }
| PVALID { S PVALID }
| FINDEQP { S FINDEQP }
| FINDEQ { S FINDEQ }
| CMB { S CMB }
| MAPCMBP { S MAPCMBP }
| MAPCMB { S MAPCMB }
| CROSSCMBP { S CROSSCMBP }
| CROSSCMB { S CROSSCMB }
| PCPP { S PCPP }
| PCP { S PCP }
| T BLANK T { FA($1, $3) }
| LPAREN T RPAREN { $2 }
;
%%
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