Commit 9bbc2d35 authored by POTTIER Francois's avatar POTTIER Francois

Repository creation.

parents
# Editing:
*~
# Compilation:
*.native
_build
*.processed.ml
# MacOS:
.DS_Store
If TVar is a constructor of some type other than term
(e.g. value: one substitues values for variables in terms)
then Toolbox must be adapted.
Check that every module has an .mli file, except where that would be too heavy.
The type (_, _) abstraction could be transparent, private, or opaque.
Benchmark fa versus fa' and decide which one to keep.
Possibly cut Toolbox.Make down into several smaller functors.
At least [subst] should be a separate functor.
Operations on terms:
simultaneous opening? (nominal)
conversion from debruijn back to nominal
a printer for debruijn terms?
-- test for global uniqueness everywhere an environment is extended?
Operations on each kind of environment:
Entering a binder (and testing for global uniqueness).
Add printers for Atom.Map
and possibly the various kinds of environments that we use.
Document the precondition and postcondition of every function
in terms of ownership of atoms.
Deal with more complex forms of binding.
Try dealing with binding and hash-consing at the same time.
Try dealing with suspended substitutions.
(As a distinct construct. Not necessarily at abstractions.)
Look at the visitors in Why3.
------------------------------------------------------------------------------
TODO (POSSIBLY):
Can we treat 'bn specially so that we do not need to implement visit_'bn?
Or should we just mark 'bn as [@opaque] so as to get visit_'bn for free? Ugly.
Operations in nominal style, without the GUH.
Capture-avoiding substitution with freshening of bound names.
B _build
PKG pprint
PKG visitors.ppx
PKG visitors.runtime
PKG alphaLib
open Printf
open AlphaLib
open Term
module T = Toolbox.Make(Term)
open T
(* Sample terms. *)
let x =
Atom.freshh "x"
let y =
Atom.freshh "y"
let id =
TLambda (x, TVar x)
let delta_body =
TApp (TVar x, TVar x)
let delta =
TLambda (x, delta_body)
let omega =
TApp (delta, copy delta)
let samples = [
TVar y;
id;
TApp (id, TVar y);
TApp (id, TVar x);
TApp (id, copy id);
delta;
omega;
import KitImport.empty (TLambda ("x", TVar "x"));
import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
]
let closed_samples = [
id;
TApp (id, copy id);
delta;
omega;
import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z")));
]
let evaluate f =
List.iter f samples
(* A non-hygienic term printer. This printer shows the real (internal) identity
of atoms, using [Atom.show]. *)
let nhprint oc t =
Print.term oc (show t)
(* A hygienic term printer. This printer uses [export]. *)
let hprint oc t =
(* works for closed terms only, as of now *)
Print.term oc (export KitExport.empty t)
let () =
printf "Testing size...\n";
[
TVar y, 1;
id, 2;
TApp (id, TVar y), 4;
TApp (id, copy id), 5;
delta, 4;
omega, 9;
] |> List.iter (fun (t, i) ->
assert (size t = i)
)
let print_copy t =
printf "copy(%a) = %a\n%!"
nhprint t
nhprint (copy t)
let () =
evaluate print_copy
let print_export t =
printf "export(%a) = %a\n%!"
nhprint t
hprint t
let () =
List.iter print_export closed_samples
let print_fa t =
printf "fa(%a) = %a\n%!"
nhprint t
Atom.Set.print (fa t)
let () =
evaluate print_fa
let print_fa' t =
printf "fa'(%a) = %a\n%!"
nhprint t
Atom.Set.print (fa' t)
let () =
evaluate print_fa'
let print_subst1 u x t =
let t' = subst1 u x t in
printf "substituting %a for %a in %a = ...\n %a\n%s\n%!"
nhprint u
Atom.print x
nhprint t
nhprint t'
(if t == t' then "(physically equal)" else "(physically distinct)")
let () =
print_subst1 (TVar y) x (TVar x);
print_subst1 (TVar y) x (TVar y);
print_subst1 delta x delta_body;
print_subst1 (copy delta) x (copy delta);
()
let print_equiv t1 t2 =
printf "equiv: %a ~ %a = %b\n%!"
nhprint t1
nhprint t2
(equiv t1 t2)
let () =
print_equiv id id;
print_equiv id (TVar x);
print_equiv (TVar x) (TVar y);
print_equiv delta (copy delta);
print_equiv omega (copy omega);
print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar y));
print_equiv (TLambda (x, TVar x)) (TLambda (y, TVar x));
print_equiv
(import KitImport.empty (TLambda ("z", TLambda ("z", TVar "z"))))
(import KitImport.empty (TLambda ("z", TLambda ("y", TVar "z"))))
;
()
let print_wf t =
printf "wf(%a) = %b\n%!"
nhprint t
(try wf t; true with IllFormed _ -> false)
let () =
evaluate print_wf
TARGET := \
Main.native
OCAMLBUILD := \
ocamlbuild \
-use-ocamlfind \
-classic-display \
-cflags "-g" -lflags "-g" \
MLI := \
$(patsubst %.ml,%.inferred.mli,$(wildcard *.ml))
.PHONY: all test mli processed clean
all:
@ $(OCAMLBUILD) $(TARGET)
test: all
@ ./$(TARGET)
mli:
@ $(OCAMLBUILD) $(MLI)
include Makefile.preprocess
processed: Term.processed.ml
clean:
@ rm -f *~
@ rm -f *.processed.ml
@ $(OCAMLBUILD) -clean
# This Makefile allows running visitors as a preprocessor,
# so as to inspect the generated code and possibly include
# it in a TeX document.
# This assumes the visitors package is installed.
# The rewriting command.
PPX := `ocamlfind query ppx_deriving`/ppx_deriving \
`ocamlfind query visitors`/ppx_deriving_visitors.cma
REWRITE := ocamlfind ppx_tools/rewriter -ppx '$(PPX)'
# Use GNU sed to extract the generated code.
# This requires GNU sed 3.95 or above, I am told.
SED := $(shell if command -v gsed >/dev/null ; then echo gsed ; else echo sed ; fi)
EXTRACT := $(SED) -e '/VISITORS.BEGIN/,/VISITORS.END/!d;//d'
# Use sed to fix some deficiencies of OCaml's code printer.
# 0. Force a space after a comma.
# 1. Replace multiple consecutive spaces with a single space.
# This will destroy indentation; we restore it afterwards.
# 2. Force a line break after [in].
# 3. Force a line break after [->].
# 4. (Ad hoc.) Force a line break between [= let],
# presumably at the beginning of a method definition.
# 5. Remove the line break between [=] and [object].
BEAUTIFY := \
| $(SED) -e 's/,/, /g' \
| $(SED) -e 's/ / /g' \
| $(SED) -e 's/ in / in\n/g' \
| $(SED) -e 's/ -> / ->\n/g' \
| $(SED) -e 's/= let /=\nlet /g' \
| perl -0777 -pe 's/=\n *object/= object/gs' \
# Use ocp-indent to beautify the generated code.
INDENT := ocp-indent --config=JaneStreet,match_clause=4
%.processed.ml: %.ml
$(REWRITE) $< | $(EXTRACT) $(BEAUTIFY) | $(INDENT) > $@
open PPrint
(* -------------------------------------------------------------------------- *)
(* A block with indentation. *)
let indentation = 2
let block opening contents closing =
group (opening ^^ nest indentation (contents) ^^ closing)
(* -------------------------------------------------------------------------- *)
(* Parentheses with indentation. *)
(* We allow breaking a parenthesized thing into several lines by leaving the
opening and closing parentheses alone on a line and indenting the content. *)
let parens d =
block
lparen
(break 0 ^^ d)
(break 0 ^^ rparen)
(* -------------------------------------------------------------------------- *)
(* Lambda-calculus application. *)
let app d1 d2 =
(* The following definition would reject a large argument on a line of
its own, indented: *)
(* group (d1 ^^ nest indentation (break 1 ^^ d2)) *)
(* However, that would be redundant with the fact that large arguments
are usually parenthesized, and we already break lines and indent
within the parentheses. So, the following suffices: *)
group (d1 ^^ space ^^ d2)
(* -------------------------------------------------------------------------- *)
(* Running a buffer printer in a fresh buffer, and sending the result to an
output channel. *)
let run (oc : out_channel) (print : Buffer.t -> 'a -> unit) (x : 'a) =
let b = Buffer.create 1024 in
print b x;
Buffer.output_buffer oc b
(* -------------------------------------------------------------------------- *)
(* Printing a document into an output channel, with fixed parameters. *)
let output (oc : out_channel) (d : document) =
run oc (PPrintEngine.ToBuffer.pretty 0.9 80) d
open PPrint
open PPrintAux
open Term
let rec term0 t =
match t with
| TVar x ->
string x
| TLambda _
| TApp (_, _) ->
parens (term t)
and term1 t =
match t with
| TApp (t1, t2) ->
app (term1 t1) (term0 t2)
| _ ->
term0 t
and term2 t =
match t with
| TLambda (x, t) ->
block
(backslash ^^ string x ^^ dot)
(term2 t)
empty
| _ ->
term1 t
and term t =
term2 t
let term (oc : out_channel) (t : raw_term) : unit =
output oc (term t)
open AlphaLib
open Abstraction
type ('fn, 'bn) term =
| TVar of 'fn
| TLambda of ('bn, ('fn, 'bn) term) abstraction
| TApp of ('fn, 'bn) term * ('fn, 'bn) term
[@@deriving
visitors { variety = "iter"; public = ["visit_term"];
ancestors = ["Bn.iter"; "Abstraction.iter"] }
,
visitors { variety = "map"; public = ["visit_term"];
ancestors = ["Bn.map"; "Abstraction.map"] }
,
visitors { variety = "endo"; public = ["visit_term"];
ancestors = ["Bn.endo"; "Abstraction.endo"] }
,
visitors { variety = "reduce"; public = ["visit_term"];
ancestors = ["Bn.reduce"; "Abstraction.reduce"] }
,
visitors { variety = "iter2"; public = ["visit_term"];
ancestors = ["Bn.iter2"; "Abstraction.iter2"] }
]
type raw_term =
(string, string) term
type nominal_term =
(Atom.t, Atom.t) term
type db_term =
(int, unit) term
true: \
safe_string, \
warn(A-4-44), \
package(pprint), \
package(visitors.ppx), \
package(visitors.runtime), \
package(alphaLib)
B _build
PKG visitors.runtime
(* -------------------------------------------------------------------------- *)
(* A universal, concrete type of single-name abstractions. *)
(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
in de Bruijn style, etc. -- so we parameterize the abstraction over the
type ['bn] of the bound name and over the type ['term] of the body. This
makes this type definition almost trivial -- it is just a pair -- but it
still serves as a syntactic marker of where abstractions are located. *)
type ('bn, 'term) abstraction =
'bn * 'term
(* -------------------------------------------------------------------------- *)
(* The main effect of an abstraction is to cause the environment to be
enriched when the abstraction is traversed. The following classes define
where the environment is enriched. *)
(* These classes do not know the type of the environment, and do not know how
it is enriched; the latter task is delegated to virtual methods, such as
[extend] and [restrict]. The implementation of these methods is provided
by separate ``kits''. *)
(* We need one class per variety of visitor, which is a bit painful. *)
(* The method [visit_abstraction] is polymorphic in the type of terms. This is
important, as it means that one can use several instances of [abstraction]
in a single type definition and still be able to construct well-typed
visitors. *)
(* The virtual methods [extend] and [restrict] are not polymorphic in the
types of bound names and environments. On the contrary, each kit comes
with certain specific types of bound names and environments. *)
(* Because [iter] and [iter2] are special cases of [reduce] and [reduce2],
respectively, we define them that way, so as to save effort. *)
class virtual ['self] map = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private visit_abstraction: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction
= fun _ f env (x, body) ->
let x', env' = self#extend x env in
x', f env' body
end
class virtual ['self] endo = object (self : 'self)
method private virtual extend: 'bn -> 'env -> 'bn * 'env
method private visit_abstraction: 'term .
_ ->
('env -> 'term -> 'term) ->
'env -> ('bn, 'term) abstraction -> ('bn, 'term) abstraction
= fun _ f env ((x, body) as this) ->
let x', env' = self#extend x env in
let body' = f env' body in
if x == x' && body == body' then
this
else
x', body'
end
class virtual ['self] reduce = object (self : 'self)
method private virtual extend: 'bn -> 'env -> 'env
method private virtual restrict: 'bn -> 'z -> 'z
method private visit_abstraction: 'term .
_ ->
('env -> 'term -> 'z) ->
'env -> ('bn, 'term) abstraction -> 'z
= fun _ f env (x, body) ->
let env' = self#extend x env in
self#restrict x (f env' body)
end
class virtual ['self] iter = object (_ : 'self)
inherit ['self] reduce
method private restrict _ () = ()
end
class virtual ['self] map2 = object (self : 'self)
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'bn3 * 'env
method private visit_abstraction: 'term1 'term2 'term3 .
_ ->
('env -> 'term1 -> 'term2 -> 'term3) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction -> ('bn3, 'term3) abstraction
= fun _ f env (x1, body1) (x2, body2) ->
let x3, env' = self#extend x1 x2 env in
x3, f env' body1 body2
end
class virtual ['self] reduce2 = object (self : 'self)
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual restrict: 'bn1 -> 'bn2 -> 'z -> 'z
method private visit_abstraction: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2 -> 'z) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction -> 'z
= fun _ f env (x1, body1) (x2, body2) ->
let env' = self#extend x1 x2 env in
self#restrict x1 x2 (f env' body1 body2)
end
class virtual ['self] iter2 = object (_ : 'self)
inherit ['self] reduce2
method private restrict _ _ () = ()
end
(* -------------------------------------------------------------------------- *)
(* We impose maximal sharing on strings so as to reduce the total amount of
space that they occupy. This is done using a weak hash set. *)
module StringStorage =
Weak.Make(struct
type t = string
let equal (s1 : string) (s2 : string) = (s1 = s2)
let hash = Hashtbl.hash
end)
let share : string -> string =
StringStorage.merge (StringStorage.create 128)
(* -------------------------------------------------------------------------- *)
(* Removing any trailing digits in a string. *)
let is_digit c =
Char.code '0' <= Char.code c && Char.code c <= Char.code '9'
let remove_trailing_digits (s : string) : string =
let n = ref (String.length s) in
while !n > 0 && is_digit s.[!n-1] do n := !n-1 done;
(* We assume that there is at least one non-digit character in the string. *)
assert (!n > 0);
String.sub s 0 !n
(* -------------------------------------------------------------------------- *)
(* An atom is implemented as a pair of an integer identity and a string that
serves as a printing hint. *)
(* We maintain the invariant that a hint is nonempty and does not end in a
digit. This allows us to later produce unique identifiers, without risk of
collisions, by concatenating a hint and a unique number. *)
(* To preserve space, hints are maximally shared. This is not essential for
correctness, though. *)
type atom = { identity: int; hint: string }
type t = atom
let identity a =
a.identity
let hint a =
a.hint
(* These printing functions should be used for debugging purposes only. One
must understand, here, that only the identity of the atom matters, and
the hint is just an indication of where and why this atom was created. *)
let show a =
Printf.sprintf "%s/%d" a.hint a.identity
let print oc a =
output_string oc (show a)
(* -------------------------------------------------------------------------- *)
(* A global integer counter holds the next available identity. *)
let counter =
ref 0
let allocate () =
let number = !counter in
counter := number + 1;
assert (number >= 0);
number
(* [freshh hint] produces a fresh atom. *)
(* The argument [hint] must not be a string of digits. *)
let freshh hint =
let identity = allocate()
and hint = share (remove_trailing_digits hint) in
{ identity; hint }
(* [fresha a] returns a fresh atom modeled after the atom [a]. *)
let fresha a =
freshh a.hint
(* -------------------------------------------------------------------------- *)
(* Comparison of atoms. *)
let equal a b =
a.identity = b.identity
let compare a b =
(* Identities are always positive numbers (see [allocate] above)
so I believe overflow is impossible here. *)
a.identity - b.identity
let hash a =
Hashtbl.hash a.identity
(* -------------------------------------------------------------------------- *)
(* A scratch buffer for printing. *)
let scratch =
Buffer.create 1024
(* [print_separated_sequence] prints a sequence of elements into the [scratch]
buffer. The sequence is given by the higher-order iterator [iter], applied
to the collection [xs]. The separator is the string [sep]. Each element is
transformed to a string by the function [show]. *)
let print_separated_sequence show sep iter xs : unit =
let first = ref true in
iter (fun x ->
if !first then begin
Buffer.add_string scratch (show x);
first := false
end
else begin
Buffer.add_string scratch sep;
Buffer.add_string scratch (show x)
end
) xs
(* -------------------------------------------------------------------------- *)
(* Sets and maps. *)
module Order = struct
type t = atom
let compare = compare
end
module Set = struct
include Set.Make(Order)
(* Sets of atoms form a monoid under union. *)
class ['z] monoid = object
method zero: 'z = empty
method plus: 'z -> 'z -> 'z = union
end
(* These printing functions should be used for debugging purposes only. *)
let print_to_scratch xs =
Buffer.clear scratch;
Buffer.add_string scratch "{";
print_separated_sequence show ", " iter xs;
Buffer.add_string scratch "}"
let show xs =
print_to_scratch xs;
let result = Buffer.contents scratch in
Buffer.reset scratch;
result
let print oc xs =
print_to_scratch xs;
Buffer.output_buffer oc scratch;
Buffer.reset scratch
end
module Map =
Map.Make(Order)
(* TEMPORARY document *)
(* Atoms. *)
type atom
type t =
atom
val identity: atom -> int
val hint: atom -> string