Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
Samuel Frontull
wltrs
Commits
117665ac
Commit
117665ac
authored
Jun 05, 2022
by
Frontull Samuel
Browse files
maximal free subterms only one function
parent
d98c5076
Changes
2
Hide whitespace changes
Inline
Side-by-side
lib/core.ml
View file @
117665ac
...
...
@@ -10,9 +10,6 @@ let _LAM = "1"
type
term
=
Var
of
string
|
Lam
of
string
*
term
|
App
of
term
*
term
let
remove
l1
f
x
=
L
.
fold_left
(
fun
acc
hd
->
if
f
hd
=
x
then
acc
else
hd
::
acc
)
[]
l1
let
label
=
ref
0
let
next_label
()
=
...
...
@@ -32,9 +29,7 @@ type l_term =
(** lambda term to labeled lambda term *)
let
rec
term_to_l_term
=
function
|
Var
x
->
LVar
x
|
Lam
(
x
,
e
)
->
let
l
=
next_label
()
in
LLam
(
l
,
x
,
term_to_l_term
e
)
|
Lam
(
x
,
e
)
->
LLam
(
next_label
()
,
x
,
term_to_l_term
e
)
|
App
(
e1
,
e2
)
->
LApp
(
term_to_l_term
e1
,
term_to_l_term
e2
)
(** labeled lambda term to lambda term *)
...
...
@@ -43,7 +38,7 @@ let rec l_term_to_term = function
|
LLam
(
_
,
v
,
t
)
->
Lam
(
v
,
l_term_to_term
t
)
|
LApp
(
e1
,
e2
)
->
App
(
l_term_to_term
e1
,
l_term_to_term
e2
)
(** rename
every
occurrence of variable {e x} in {e term} to {e y} *)
(** rename
the free
occurrence
s
of variable {e x} in {e term} to {e y} *)
let
rec
rename
term
x
y
=
match
term
with
|
LVar
s
->
if
s
=
x
then
LVar
y
else
term
...
...
@@ -61,13 +56,14 @@ let rec default_names_r pos = function
let
default_names
term
=
default_names_r
_ROOT
term
(** Extract the name of a variable from a {e a_term} *)
let
lvname
=
function
LVar
n
->
n
|
_
->
""
(** remove element {e x} from list {e l1} *)
let
remove
l1
x
=
L
.
fold_left
(
fun
acc
hd
->
if
hd
=
x
then
acc
else
hd
::
acc
)
[]
l1
(** Extract the free variables in a {e a_term} *)
let
rec
free_variables
=
function
|
LVar
x
->
[
LVar
x
]
|
LLam
(
_
,
x
,
e
)
->
remove
(
free_variables
e
)
lvname
x
|
LLam
(
_
,
x
,
e
)
->
remove
(
free_variables
e
)
(
LVar
x
)
|
LApp
(
e1
,
e2
)
->
free_variables
e1
@
free_variables
e2
let
counter
=
ref
0
...
...
@@ -86,22 +82,17 @@ let rec subst m x y =
|
LApp
(
e1
,
e2
)
->
LApp
(
subst
e1
x
y
,
subst
e2
x
y
)
(** capture-avoiding substitution *)
let
rec
_
casubst
m
x
n
fvn
=
let
rec
casubst
m
x
n
=
match
m
with
|
LVar
y
->
if
x
=
y
then
n
else
m
|
LApp
(
e1
,
e2
)
->
LApp
(
_
casubst
e1
x
n
fvn
,
_
casubst
e2
x
n
fvn
)
|
LLam
(
l
,
y
,
e
)
->
(
|
LApp
(
e1
,
e2
)
->
LApp
(
casubst
e1
x
n
,
casubst
e2
x
n
)
|
LLam
(
l
,
y
,
e
)
->
if
y
=
x
then
m
else
let
inters
=
List
.
filter
(
fun
x
->
x
=
y
)
fvn
in
match
inters
with
|
[]
->
LLam
(
l
,
y
,
_casubst
e
x
n
fvn
)
|
hd
::
_
->
let
f
=
next_fresh
()
in
let
m'
=
subst
m
hd
f
in
_casubst
m'
x
n
fvn
)
let
casubst
m
x
n
=
_casubst
m
x
n
(
L
.
map
lvname
(
free_variables
n
))
else
if
L
.
mem
(
LVar
y
)
(
free_variables
n
)
then
let
f
=
next_fresh
()
in
let
m'
=
subst
m
y
f
in
casubst
m'
x
n
else
LLam
(
l
,
y
,
casubst
e
x
n
)
(** apply a beta step *)
let
beta
=
function
...
...
@@ -149,9 +140,7 @@ let rec _weak_step term pos p =
|
LLam
(
l
,
x
,
e
)
->
LLam
(
l
,
x
,
_weak_step
e
pos
(
p
^
_LAM
))
|
_
->
term
let
weak_step
term
=
_weak_step
term
(
weak_redexpos
term
)
_ROOT
let
weak_step_pos
term
pos
=
_weak_step
term
pos
_ROOT
let
weak_step
term
pos
=
_weak_step
term
pos
_ROOT
(** TRS term *)
type
trs_term
=
...
...
@@ -168,7 +157,7 @@ let rec fvar_trsterm = function
|
TDes
(
e1
,
e2
)
->
fvar_trsterm
e1
@
fvar_trsterm
e2
|
TCon
(
_
,
fvs
)
->
L
.
flatten
(
L
.
map
(
fun
x
->
fvar_trsterm
(
fst
x
))
fvs
)
let
rec
_components_l
term
xs
pos
lterm
=
let
rec
maximal_free_sub
term
s
xs
pos
lterm
=
if
free_variables
lterm
=
[]
then
[
(
lterm
,
pos
)
]
else
match
lterm
with
...
...
@@ -180,40 +169,35 @@ let rec _components_lterm xs pos lterm =
match
(
e1_fvs
,
e2_fvs
)
with
|
[]
,
[]
->
[
(
lterm
,
pos
)
]
|
[]
,
_
->
[
(
e1
,
pos
^
_APP_L
)
]
@
_components_l
term
xs
(
pos
^
_APP_R
)
e2
[
(
e1
,
pos
^
_APP_L
)
]
@
maximal_free_sub
term
s
xs
(
pos
^
_APP_R
)
e2
|
_
,
[]
->
_components_l
term
xs
(
pos
^
_APP_L
)
e1
@
[
(
e2
,
pos
^
_APP_R
)
]
maximal_free_sub
term
s
xs
(
pos
^
_APP_L
)
e1
@
[
(
e2
,
pos
^
_APP_R
)
]
|
_
,
_
->
_components_l
term
xs
(
pos
^
_APP_L
)
e1
@
_components_l
term
xs
(
pos
^
_APP_R
)
e2
)
|
LLam
(
_
,
y
,
e
)
->
_components_l
term
(
LVar
y
::
xs
)
(
pos
^
_LAM
)
e
maximal_free_sub
term
s
xs
(
pos
^
_APP_L
)
e1
@
maximal_free_sub
term
s
xs
(
pos
^
_APP_R
)
e2
)
|
LLam
(
_
,
y
,
e
)
->
maximal_free_sub
term
s
(
LVar
y
::
xs
)
(
pos
^
_LAM
)
e
let
rec
l_term_to_trsterm
=
function
|
LVar
x
->
TVar
x
|
LApp
(
e1
,
e2
)
->
TDes
(
l_term_to_trsterm
e1
,
l_term_to_trsterm
e2
)
|
LLam
(
l
,
x
,
e
)
->
let
cmps
=
_components_l
term
[
LVar
x
]
_LAM
e
in
let
cmps
=
maximal_free_sub
term
s
[
LVar
x
]
_LAM
e
in
TCon
(
l
,
L
.
map
(
fun
(
t
,
p
)
->
(
l_term_to_trsterm
t
,
p
))
cmps
)
let
rec
_cs_to_var
xs
pos
lterm
=
if
free_variables
lterm
=
[]
then
LVar
(
"v_"
^
pos
)
else
match
lterm
with
|
LVar
_
->
if
L
.
mem
lterm
xs
then
lterm
else
LVar
(
"v_"
^
pos
)
|
LApp
(
e1
,
e2
)
->
(
let
e1_fvs
=
intersect
xs
(
free_variables
e1
)
in
let
e2_fvs
=
intersect
xs
(
free_variables
e2
)
in
match
(
e1_fvs
,
e2_fvs
)
with
|
[]
,
[]
->
LVar
(
"v_"
^
pos
)
|
_
,
_
->
let
e1'
=
_cs_to_var
xs
(
pos
^
_APP_L
)
e1
in
let
e2'
=
_cs_to_var
xs
(
pos
^
_APP_R
)
e2
in
LApp
(
e1'
,
e2'
)
)
|
LLam
(
l
,
y
,
e
)
->
let
e'
=
_cs_to_var
(
LVar
y
::
xs
)
(
pos
^
_LAM
)
e
in
LLam
(
l
,
y
,
e'
)
let
rec
_term_to_pattern
lterm
ps
p
=
if
L
.
mem
p
ps
then
LVar
(
"v_"
^
p
)
else
match
lterm
with
|
LVar
_
->
lterm
|
LApp
(
e1
,
e2
)
->
LApp
(
_term_to_pattern
e1
ps
(
p
^
_APP_L
)
,
_term_to_pattern
e2
ps
(
p
^
_APP_R
))
|
LLam
(
l
,
x
,
e
)
->
LLam
(
l
,
x
,
_term_to_pattern
e
ps
(
p
^
_LAM
))
let
cs_to_var
lterm
xs
=
_cs_to_var
xs
_ROOT
lterm
let
term_to_pattern
lterm
xs
=
let
fs
=
maximal_free_subterms
xs
_ROOT
lterm
in
let
ps
=
L
.
map
snd
fs
in
_term_to_pattern
lterm
ps
_ROOT
type
trs_rule
=
RR
of
trs_term
*
trs_term
...
...
@@ -221,10 +205,10 @@ let rec rules = function
|
LVar
_
->
[]
|
LApp
(
e1
,
e2
)
->
rules
e1
@
rules
e2
|
LLam
(
l
,
x
,
e
)
->
let
e'
=
cs_to_var
e
[
LVar
x
]
in
let
e_t
=
l_term_to_trsterm
e'
in
let
trsterm_t
=
l_term_to_trsterm
(
LLam
(
l
,
x
,
e'
))
in
RR
(
TDes
(
trsterm_t
,
TVar
x
)
,
e_t
)
::
rules
e
let
p
=
term_to_pattern
e
[
LVar
x
]
in
let
rhs
=
l_term_to_trsterm
p
in
let
lhs
=
l_term_to_trsterm
(
LLam
(
l
,
x
,
p
))
in
RR
(
TDes
(
lhs
,
TVar
x
)
,
rhs
)
::
rules
e
let
rec
_redexpos
pos
=
function
|
TDes
(
TCon
(
_
,
_
)
,
_
)
->
pos
...
...
@@ -294,11 +278,7 @@ let rec _rewrite_step tterm rules pos p =
fvs
)
|
_
->
tterm
let
rewrite_step
xs
t
=
_rewrite_step
t
xs
(
redexpos
t
)
_ROOT
let
rewrite_step_at_pos
xs
t
pos
=
_rewrite_step
t
xs
pos
_ROOT
let
rewrite_step
xs
t
pos
=
_rewrite_step
t
xs
pos
_ROOT
let
rec
find_rule
rules
label
=
match
rules
with
...
...
@@ -314,23 +294,18 @@ let next_fresh_2 () =
"v"
^
string_of_int
!
counter_projection
let
rec
trsterm_to_lterm
xs
=
function
|
TVar
x
->
LVar
x
|
TDes
(
e1
,
e2
)
->
LApp
(
trsterm_to_lterm
xs
e1
,
trsterm_to_lterm
xs
e2
)
|
TCon
(
l
,
tcs
)
->
(
let
rule
=
find_rule
xs
l
in
match
rule
with
|
RR
(
TDes
(
TCon
(
_
,
rcs
)
,
var
)
,
r
)
->
if
L
.
mem
var
(
L
.
flatten
(
L
.
map
(
fun
f
->
fvar_trsterm
(
fst
f
))
tcs
))
then
let
f
=
next_fresh_2
()
in
let
r'
=
subst
r
[
(
var
,
TVar
f
)
]
in
LLam
(
l
,
f
,
trsterm_to_lterm
xs
(
subst
r'
(
zip_cs
rcs
tcs
)))
else
LLam
(
l
,
vtname
var
,
trsterm_to_lterm
xs
(
subst
r
(
zip_cs
rcs
tcs
)))
|
_
->
failwith
"Not a RR found."
)
|
TVar
x
->
LVar
x
|
TDes
(
e1
,
e2
)
->
LApp
(
trsterm_to_lterm
xs
e1
,
trsterm_to_lterm
xs
e2
)
|
TCon
(
l
,
tcs
)
->
(
let
rule
=
find_rule
xs
l
in
match
rule
with
|
RR
(
TDes
(
TCon
(
_
,
rcs
)
,
var
)
,
rhs
)
->
if
L
.
mem
var
(
L
.
flatten
(
L
.
map
(
fun
f
->
fvar_trsterm
(
fst
f
))
tcs
))
then
let
f
=
next_fresh_2
()
in
let
r'
=
subst
rhs
[
(
var
,
TVar
f
)
]
in
LLam
(
l
,
f
,
trsterm_to_lterm
xs
(
subst
r'
(
zip_cs
rcs
tcs
)))
else
LLam
(
l
,
vtname
var
,
trsterm_to_lterm
xs
(
subst
rhs
(
zip_cs
rcs
tcs
)))
|
_
->
failwith
"No rule with such label."
)
lib/io.ml
View file @
117665ac
...
...
@@ -55,14 +55,14 @@ let trs_rule_to_string term =
let
rules_to_string
xs
=
String
.
concat
".
\n
"
(
L
.
map
trs_rule_to_string
xs
)
let
trs_to_string
xs
t
=
"TRS:
\n
"
^
rules_to_string
xs
^
".
\n
----
\n
"
^
trs_term_to_string_nopos
t
"TRS:
\n
"
^
rules_to_string
xs
^
".
\n
----
\n
"
^
trs_term_to_string_nopos
t
let
rec
_simulate_lterm_in_trs
lterm
rules
tterm
alltrue
=
let
pos
=
weak_redexpos
lterm
in
if
pos
<>
""
then
let
lterm'
=
weak_step
_pos
lterm
pos
in
let
trsterm'
=
rewrite_step
_at_pos
rules
tterm
pos
in
let
trsterm'_lterm
=
trsterm_to_lterm
rules
trsterm'
in
let
lterm'
=
weak_step
lterm
pos
in
let
trsterm'
=
rewrite_step
rules
tterm
pos
in
let
trsterm'_lterm
=
trsterm_to_lterm
rules
trsterm'
in
let
alpha_eq
=
default_names
trsterm'_lterm
=
default_names
lterm'
in
let
alltrue
=
alltrue
&&
alpha_eq
in
let
str
=
...
...
@@ -78,7 +78,8 @@ let rec _simulate_lterm_in_trs lterm rules tterm alltrue =
in
str
::
(
if
lterm
=
lterm'
then
[]
else
_simulate_lterm_in_trs
lterm'
rules
trsterm'
alltrue
)
(
if
lterm
=
lterm'
then
[]
else
_simulate_lterm_in_trs
lterm'
rules
trsterm'
alltrue
)
else
[]
let
simulate_lterm_in_trs
lterm
=
...
...
@@ -91,4 +92,4 @@ let simulate_lterm_in_trs lterm =
let
print_simulation
lterm
=
let
sim
=
simulate_lterm_in_trs
lterm
in
Printf
.
printf
"
\n
%s
\n
"
sim
Printf
.
printf
"
%s
"
sim
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment