Commit 161d3f5f authored by POTTIER Francois's avatar POTTIER Francois

Move [show] after [export].

parent cf64e180
......@@ -93,10 +93,6 @@ __AVOID
AVOID(typ)
AVOID(term)
__SHOW
SHOW(typ)
SHOW(term)
__IMPORT
IMPORT(typ)
IMPORT(term)
......@@ -105,6 +101,10 @@ __EXPORT
EXPORT(typ)
EXPORT(term)
__SHOW
SHOW(typ)
SHOW(term)
__SIZE
SIZE(typ)
SIZE(term)
......
......@@ -131,21 +131,6 @@
(* -------------------------------------------------------------------------- *)
#define SHOW_CLASS __show
#define SHOW_FUN(term) CONCAT(show_, term)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* TEMPORARY use string * loc so as to be able to give a location *)
#define IMPORT_FUN(term) CONCAT(import_, term)
......@@ -177,6 +162,21 @@
(* -------------------------------------------------------------------------- *)
#define SHOW_CLASS __show
#define SHOW_FUN(term) CONCAT(show_, term)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
#define SIZE_CLASS __size
#define SIZE_FUN(term) CONCAT(size_, term)
......
......@@ -55,15 +55,15 @@ module Make (Term : INPUT) = struct
__AVOID
AVOID(term)
__SHOW
SHOW(term)
__IMPORT
IMPORT(term)
__EXPORT
EXPORT(term)
__SHOW
SHOW(term)
__SIZE
SIZE(term)
......
......@@ -74,14 +74,6 @@ module type OUTPUT = sig
val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
(* [show_term] converts its argument to a raw term using [Atom.show] both at
free name occurrences and bound name occurrences. It is in principle a
debugging tool only, as the strings produced by [Atom.show] do not make
sense (at free atoms) and are not beautiful. It is nevertheless a correct
printer IF the term is closed. *)
val show_term: nominal_term -> raw_term
(* [import_term] converts a raw term to a nominal term that satisfies the
Global Uniqueness Hypothesis, that is, a nominal term where every binding
name occurrence is represented by a unique atom. [import] expects every
......@@ -97,6 +89,14 @@ module type OUTPUT = sig
val export_term: KitExport.env -> nominal_term -> raw_term
(* [show_term] converts its argument to a raw term using [Atom.show] both at
free name occurrences and bound name occurrences. It is in principle a
debugging tool only, as the strings produced by [Atom.show] do not make
sense (at free atoms) and are not beautiful. It is nevertheless a correct
printer IF the term is closed. *)
val show_term: nominal_term -> raw_term
(* [size_term] computes the size of its argument. Beware: this counts the
nodes whose type is [term], but does not count the nodes of other types. *)
......
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