Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 736a8791 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added [BindingFormsSimplified], currently unused.

parent 6ba01709
(* This is a simplified version of [BindingFormsUnbound] which supports neither
[recursive] nor [repeat]. As a result, the code is very much simplified; the
environments have two components instead of four, and the [lookup] method is
not needed. *)
(* -------------------------------------------------------------------------- *)
(* This module defines a little language that allows the user to describe
complex binding constructs, in the style of Weirich et al.'s "Binders
unbound" (ICFP 2011). *)
(* Following alphaCaml and "Binders unbound", we distinguish "terms" versus
"patterns". The syntax of these categories is as follows:
t ::= ... (* products, sums, etc. *)
| abstraction(p)
p ::= ... (* products, sums, etc. *)
| binder
| inner(t)
| outer(t)
| rebind(p)
The combinator [inner(p)] can be viewed as sugar for [rebind(outer(p))].
Our [rebind(p)] takes just one argument. Weirich et al.'s [rebind],
which takes two arguments, is emulated by writing [p1 * rebind(p2)].
This encoding relies on the fact that pairs are traversed left-to-right. *)
(* -------------------------------------------------------------------------- *)
(* Type definitions. *)
type 'p abstraction =
type 'bn binder =
type 't inner =
type 't outer =
type 'p rebind =
(* Weirich et al.'s [bind] combinator, which takes a pattern and a term and
constructs a term, can be defined in terms of the above combinators, as
follows. *)
(* In natural syntax, this is [abstraction (p * inner(t))]. *)
type ('p, 't) bind =
('p * 't inner) abstraction
(* -------------------------------------------------------------------------- *)
(* When traversing a pattern, our visitors maintain a richer environment than
when traversing a term. If a normal term-traversal environment has type
['env], then an enriched pattern-traversal environment has type ['env penv]
as defined below. *)
(* The meaning of the above combinators is defined by the manner in which they
extend or use this enriched environment. *)
(* The [current] component is a mutable reference to an environment. This
environment is extended when a [binder] combinator is visited. This
mutable state is implicitly threaded from left to right. *)
(* The [outer] component is an immutable environment. It is transmitted in
a top-down manner. *)
type 'env penv = {
current: 'env ref; (* do NOT replace this with a mutable field! *)
outer: 'env;
(* -------------------------------------------------------------------------- *)
(* A few auxiliary functions. *)
(* [abstraction] initializes an enriched environment. [current] and [outer]
are initialized with the environment that exists outside the abstraction. *)
let abstraction (env : 'env) : 'env penv =
{ current = ref env; outer = env }
(* [rebind] copies the [current] component of the environment into the [outer]
component. In other words, it locally changes the meaning of [outer]. *)
let rebind (penv : 'env penv) : 'env penv =
{ penv with outer = !(penv.current) }
(* -------------------------------------------------------------------------- *)
(* [map] *)
class virtual ['self] map = object (self : 'self)
method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
(* [visit_abstraction] initializes an enriched environment using the
auxiliary function [abstraction]. *)
method private visit_abstraction: 'env 'p1 'p2 .
('env penv -> 'p1 -> 'p2) ->
'env -> 'p1 abstraction -> 'p2 abstraction
= fun visit_p env p1 ->
visit_p (abstraction env) p1
(* [binder] extends the environment via a call to the virtual method
[extend]. *)
method private visit_binder:
_ ->
'env penv -> 'bn1 binder -> 'bn2 binder
= fun _ penv x1 ->
let env = !(penv.current) in
let env, x2 = self#extend env x1 in
penv.current := env;
(* [inner(p)] can be viewed as sugar for [rebind(outer(p))]. Therefore, this
code should ideally be generated. *)
method private visit_inner: 'env 't1 't2 .
('env -> 't1 -> 't2) ->
'env penv -> 't1 inner -> 't2 inner
= fun visit_t penv t1 ->
self#visit_rebind (self#visit_outer visit_t) penv t1
(* An [outer] subterm is visited using the [outer] component of the enriched
environment. *)
method private visit_outer: 'env 't1 't2 .
('env -> 't1 -> 't2) ->
'env penv -> 't1 outer -> 't2 outer
= fun visit_t penv t1 ->
visit_t penv.outer t1
(* [visit_rebind] updates the enriched environment using the auxiliary
function [rebind]. *)
method private visit_rebind: 'env 'p1 'p2 .
('env penv -> 'p1 -> 'p2) ->
'env penv -> 'p1 rebind -> 'p2 rebind
= fun visit_p penv p1 ->
visit_p (rebind penv) p1
(* [bind(p, t)] is sugar for [abstraction (p * rebind(outer(t)))].
Therefore, the following code should ideally be generated. We write it by
hand in a slightly simpler form, where [visit_abstraction] is inlined. *)
method private visit_bind: 'env 'p1 'p2 't1 't2 .
('env penv -> 'p1 -> 'p2) ->
('env -> 't1 -> 't2) ->
'env -> ('p1, 't1) bind -> ('p2, 't2) bind
= fun visit_p visit_t env (p1, t1) ->
let penv = abstraction env in
let p2 = visit_p penv p1 in
let t2 = self#visit_inner visit_t penv t1 in
p2, t2
(* -------------------------------------------------------------------------- *)
(* [iter] *)
class virtual ['self] iter = object (self : 'self)
method private virtual extend: 'env -> 'bn -> 'env
method private visit_abstraction: 'env 'p .
('env penv -> 'p -> unit) ->
'env -> 'p abstraction -> unit
= fun visit_p env p ->
visit_p (abstraction env) p
method private visit_binder:
_ ->
'env penv -> 'bn binder -> unit
= fun _ penv x ->
let env = !(penv.current) in
let env = self#extend env x in
penv.current := env
method private visit_inner: 'env 't .
('env -> 't -> unit) ->
'env penv -> 't inner -> unit
= fun visit_t penv t ->
self#visit_rebind (self#visit_outer visit_t) penv t
method private visit_outer: 'env 't .
('env -> 't -> unit) ->
'env penv -> 't outer -> unit
= fun visit_t penv t ->
visit_t penv.outer t
method private visit_rebind: 'env 'p .
('env penv -> 'p -> unit) ->
'env penv -> 'p rebind -> unit
= fun visit_p penv p ->
visit_p (rebind penv) p
method private visit_bind: 'env 'p 't .
('env penv -> 'p -> unit) ->
('env -> 't -> unit) ->
'env -> ('p, 't) bind -> unit
= fun visit_p visit_t env (p, t) ->
let penv = abstraction env in
visit_p penv p;
self#visit_inner visit_t penv t
......@@ -2,6 +2,7 @@ Atom
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