Commit ab16a1c3 authored by POTTIER Francois's avatar POTTIER Francois

Rename [abstraction] to [abs]. Use macros to make the type definitions more readable.

parent 65a0eb0c
......@@ -3,7 +3,7 @@ open BindingForms
type ('fn, 'bn) term =
| TVar of 'fn
| TLambda of ('bn, ('fn, 'bn) term) abstraction
| TLambda of ('bn, ('fn, 'bn) term) abs
| TApp of ('fn, 'bn) term * ('fn, 'bn) term
[@@deriving
......
......@@ -11,12 +11,14 @@ type tyvar =
(* Types. *)
type ('fn, 'bn) typ =
#define TYP ('fn, 'bn) typ
type TYP =
| TyVar of 'fn
| TyArrow of ('fn, 'bn) typ * ('fn, 'bn) typ
| TyProduct of ('fn, 'bn) typ * ('fn, 'bn) typ
| TyForall of ('bn, ('fn, 'bn) typ) abstraction
| TyMu of ('bn, ('fn, 'bn) typ) abstraction
| TyArrow of TYP * TYP
| TyProduct of TYP * TYP
| TyForall of ('bn, TYP) abs
| TyMu of ('bn, TYP) abs
(* Term variables. *)
......@@ -24,15 +26,17 @@ and tevar = (string[@opaque])
(* Terms. *)
and ('fn, 'bn) term =
#define TERM ('fn, 'bn) term
and TERM =
| TeVar of tevar
| TeAbs of tevar * ('fn, 'bn) typ * ('fn, 'bn) term
| TeApp of ('fn, 'bn) term * ('fn, 'bn) term
| TeLet of tevar * ('fn, 'bn) term * ('fn, 'bn) term
| TeTyAbs of ('bn, ('fn, 'bn) term) abstraction
| TeTyApp of ('fn, 'bn) term * ('fn, 'bn) typ
| TePair of ('fn, 'bn) term * ('fn, 'bn) term
| TeProj of int * ('fn, 'bn) term
| TeAbs of tevar * TYP * TERM
| TeApp of TERM * TERM
| TeLet of tevar * TERM * TERM
| TeTyAbs of ('bn, TERM) abs
| TeTyApp of TERM * TYP
| TePair of TERM * TERM
| TeProj of int * TERM
(* Visitor generation. *)
......
......@@ -10,7 +10,7 @@ type void
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 =
type ('bn, 'term) abs =
'bn * 'term
(* -------------------------------------------------------------------------- *)
......@@ -45,10 +45,10 @@ class virtual ['self] map = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private visit_abstraction: 'term1 'term2 .
method private visit_abs: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs
= fun _ f env (x, body) ->
let x', env' = self#extend x env in
x', f env' body
......@@ -62,10 +62,10 @@ class virtual ['self] endo = object (self : 'self)
method private virtual extend: 'bn -> 'env -> 'bn * 'env
method private visit_abstraction: 'term .
method private visit_abs: 'term .
_ ->
('env -> 'term -> 'term) ->
'env -> ('bn, 'term) abstraction -> ('bn, 'term) abstraction
'env -> ('bn, 'term) abs -> ('bn, 'term) abs
= fun _ f env ((x, body) as this) ->
let x', env' = self#extend x env in
let body' = f env' body in
......@@ -85,10 +85,10 @@ class virtual ['self] reduce = object (self : 'self)
method private virtual restrict: 'bn -> 'z -> 'z
method private visit_abstraction: 'term .
method private visit_abs: 'term .
_ ->
('env -> 'term -> 'z) ->
'env -> ('bn, 'term) abstraction -> 'z
'env -> ('bn, 'term) abs -> 'z
= fun _ f env (x, body) ->
let env' = self#extend x env in
self#restrict x (f env' body)
......@@ -110,10 +110,10 @@ class virtual ['self] map2 = object (self : 'self)
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'bn3 * 'env
method private visit_abstraction: 'term1 'term2 'term3 .
method private visit_abs: 'term1 'term2 'term3 .
_ ->
('env -> 'term1 -> 'term2 -> 'term3) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction -> ('bn3, 'term3) abstraction
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> ('bn3, 'term3) abs
= fun _ f env (x1, body1) (x2, body2) ->
let x3, env' = self#extend x1 x2 env in
x3, f env' body1 body2
......@@ -129,10 +129,10 @@ class virtual ['self] reduce2 = object (self : 'self)
method private virtual restrict: 'bn1 -> 'bn2 -> 'z -> 'z
method private visit_abstraction: 'term1 'term2 .
method private visit_abs: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2 -> 'z) ->
'env -> ('bn1, 'term1) abstraction -> ('bn2, 'term2) abstraction -> 'z
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
= fun _ f env (x1, body1) (x2, body2) ->
let env' = self#extend x1 x2 env in
self#restrict x1 x2 (f env' body1 body2)
......
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