Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
alphaLib
Commits
d59e09d9
Commit
d59e09d9
authored
Feb 08, 2017
by
POTTIER Francois
Browse files
Renamed [freshh] to [fresh].
parent
64ecdb42
Changes
5
Hide whitespace changes
Inline
Side-by-side
demos/basic/Main.ml
View file @
d59e09d9
...
...
@@ -243,8 +243,8 @@ let () =
TApp
(
subst1
u
x
t1
,
subst1
u
x
t2
))
end
);
let
x
=
Atom
.
fresh
h
"x"
and
y
=
Atom
.
fresh
h
"y"
in
let
x
=
Atom
.
fresh
"x"
and
y
=
Atom
.
fresh
"y"
in
let
u
=
generate_nominal
atoms
size_of_u
in
assert
(
subst1
u
x
(
TVar
x
)
=
u
);
assert
(
subst1
u
x
(
TVar
y
)
=
TVar
y
);
...
...
@@ -330,10 +330,10 @@ let () =
(* Sample terms. *)
let
x
=
Atom
.
fresh
h
"x"
Atom
.
fresh
"x"
let
y
=
Atom
.
fresh
h
"y"
Atom
.
fresh
"y"
let
id
=
TLambda
(
x
,
TVar
x
)
...
...
demos/basic/TermGenerator.ml
View file @
d59e09d9
...
...
@@ -89,7 +89,7 @@ let rec atoms accu k =
if
k
=
0
then
accu
else
let
a
=
AlphaLib
.
Atom
.
fresh
h
"a"
in
let
a
=
AlphaLib
.
Atom
.
fresh
"a"
in
atoms
(
AtomSet
.
add
a
accu
)
(
k
-
1
)
let
atoms
=
...
...
src/Atom.ml
View file @
d59e09d9
...
...
@@ -72,11 +72,11 @@ let allocate () =
assert
(
number
>=
0
);
number
(* [fresh
h
hint] produces a fresh atom. *)
(* [fresh hint] produces a fresh atom. *)
(* The argument [hint] must not be a string of digits. *)
let
fresh
h
hint
=
let
fresh
hint
=
let
identity
=
allocate
()
and
hint
=
share
(
remove_trailing_digits
hint
)
in
{
identity
;
hint
}
...
...
@@ -84,7 +84,7 @@ let freshh hint =
(* [fresha a] returns a fresh atom modeled after the atom [a]. *)
let
fresha
a
=
fresh
h
a
.
hint
fresh
a
.
hint
(* -------------------------------------------------------------------------- *)
...
...
src/Atom.mli
View file @
d59e09d9
...
...
@@ -14,7 +14,7 @@ val print: out_channel -> atom -> unit
(* Producing fresh atoms. *)
val
fresh
h
:
string
->
atom
val
fresh
:
string
->
atom
val
fresha
:
atom
->
atom
(* Comparison of atoms. *)
...
...
src/KitImport.ml
View file @
d59e09d9
(* This kit serves to construct an [import] function for terms, that is, a
function that transforms strings to atoms. *)
(* We impose the GUH by mapping each binding occurrence to a fresh atom. *)
(* We map every binding occurrence to a fresh atom, so the term that we
produce satisfies global uniqueness. *)
module
StringMap
=
Map
.
Make
(
String
)
...
...
@@ -13,7 +14,7 @@ let empty =
StringMap
.
empty
let
extend
(
x
:
string
)
(
env
:
env
)
:
Atom
.
t
*
env
=
let
a
=
Atom
.
fresh
h
x
in
let
a
=
Atom
.
fresh
x
in
let
env
=
StringMap
.
add
x
a
env
in
a
,
env
...
...
@@ -26,6 +27,6 @@ let lookup (env : env) (x : string) : Atom.t =
raise
(
Unbound
x
)
class
[
'
self
]
map
=
object
(
_
:
'
self
)
method
private
extend
=
extend
method
private
visit_'fn
=
lookup
method
private
extend
x
env
=
extend
x
env
method
private
visit_'fn
env
x
=
lookup
env
x
end
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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