Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Experiment: adding an [nb_occurs] function. #32

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions examples/lambda.expected
Original file line number Diff line number Diff line change
Expand Up @@ -43,3 +43,8 @@ Same as above with the custom renaming:
→ λy.(y) y
(λy.λx.(y) (y) x) λy.λx.(y) (y) x
→ λx.λx'.(x) (x) (x) (x) x'
Number of x in x1: 1
Number of x in x2: 2
Number of x in x3: 3
Number of x in xy: 3
Number of y in xy: 1
14 changes: 14 additions & 0 deletions examples/lambda.ml
Original file line number Diff line number Diff line change
Expand Up @@ -225,3 +225,17 @@ let _ =
Printf.printf " %a\n\t→ %a\n%!" print2 fst_yx print2 (seval fst_yx);
Printf.printf " %a\n\t→ %a\n%!" print2 swap_y print2 (seval swap_y);
Printf.printf " %a\n\t→ %a\n%!" print2 four print2 (seval four)

(* Testing number of occurences. *)
let _ =
let vx = fresh_var "x" in
let vy = fresh_var "y" in
let x1 = var vx in
let x2 = app x1 x1 in
let x3 = app x1 x2 in
let xy = app x3 (var vy) in
Printf.printf "Number of x in x1: %i\n" (Bindlib.nb_occurs vx x1);
Printf.printf "Number of x in x2: %i\n" (Bindlib.nb_occurs vx x2);
Printf.printf "Number of x in x3: %i\n" (Bindlib.nb_occurs vx x3);
Printf.printf "Number of x in xy: %i\n" (Bindlib.nb_occurs vx xy);
Printf.printf "Number of y in xy: %i\n" (Bindlib.nb_occurs vy xy)
43 changes: 24 additions & 19 deletions lib/bindlib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -123,11 +123,8 @@ and 'a var = {
var_box : 'a box; (* Variable as a boxed object. *)
}

(* Variable of any type (using an existential). In principle, this constructor
can be unboxed since it has a single constructor. However, this only works
starting from OCaml 4.11.0. The annotation is erased for prior versions. *)
and any_var = V : 'a var -> any_var
[@@unboxed]
(* Variable of any type (using an existential). *)
and any_var = V : 'a var * int -> any_var

let name_of x = x.var_name
let hash_var x = Hashtbl.hash (`HVar, x.var_key)
Expand All @@ -148,19 +145,19 @@ let uids_of xs = Array.map uid_of xs
let merge_uniq : any_var list -> any_var list -> any_var list =
let rec merge_uniq acc l1 l2 =
match (l1, l2) with
| ([] , _ ) -> List.rev_append acc l2
| (_ , [] ) -> List.rev_append acc l1
| ((V(x) as vx)::xs, (V(y) as vy)::ys) ->
if x.var_key = y.var_key then merge_uniq (vx::acc) xs ys else
| ([] , _ ) -> List.rev_append acc l2
| (_ , [] ) -> List.rev_append acc l1
| ((V(x,n) as vx) :: xs, (V(y,m) as vy) :: ys) ->
if x.var_key = y.var_key then merge_uniq (V(x, n+m) :: acc) xs ys else
if x.var_key < y.var_key then merge_uniq (vx::acc) xs l2 else
(* x.var_key > y.var_key*) merge_uniq (vy::acc) l1 ys
in merge_uniq []

let remove : 'a var -> any_var list -> any_var list = fun {var_key ; _} ->
let rec remove acc = function
| (V(x) as v)::l when x.var_key < var_key -> remove (v::acc) l
| (V(x) )::l when x.var_key = var_key -> List.rev_append acc l
| _ -> raise Not_found
| (V(x,_) as v)::l when x.var_key < var_key -> remove (v::acc) l
| (V(x,_) )::l when x.var_key = var_key -> List.rev_append acc l
| _ -> raise Not_found
in remove []

(* Function [minimize vs n cl] constructs a minimal closure equivalent to [cl]
Expand All @@ -181,7 +178,7 @@ let minimize : any_var list -> int -> 'a closure -> 'a closure = fun vs n t ->
let size = List.length vs in
let tab = Array.make size 0 in
let prefix = ref true in
let f (new_vp, i) (V(var)) =
let f (new_vp, i) (V(var,_)) =
let j = IMap.find var.var_key vp in
if i <> j then prefix := false;
tab.(i) <- j;
Expand All @@ -204,7 +201,15 @@ let apply_box : ('a -> 'b) box -> 'a box -> 'b box = fun f a ->
let occur : 'a var -> 'b box -> bool = fun v b ->
match b with
| Box(_) -> false
| Env(vs,_,_) -> List.exists (fun (V(x)) -> x.var_key = v.var_key) vs
| Env(vs,_,_) -> List.exists (fun (V(x,_)) -> x.var_key = v.var_key) vs

let nb_occurs : 'a var -> 'b box -> int = fun v b ->
match b with
| Box(_) -> 0
| Env(vs,_,_) ->
match List.find (fun (V(x,_)) -> x.var_key = v.var_key) vs with
| V(_,n) -> n
| exception Not_found -> 0

let is_closed : 'a box -> bool = fun b ->
match b with Box(_) -> true | Env(_,_,_) -> false
Expand Down Expand Up @@ -235,7 +240,7 @@ let unbox b =
let nbvs = List.length vs in
let env = Env.create nbvs (nbvs + nb) in
let cur = ref 0 in
let fn vp (V(x)) =
let fn vp (V(x,_)) =
let i = !cur in incr cur;
Env.set env i (x.var_mkfree x);
IMap.add x.var_key i vp
Expand Down Expand Up @@ -384,7 +389,7 @@ let mbind_apply b args = box_apply2 msubst b args
let build_var_aux key vp = Env.get (IMap.find key vp)
let build_var var_key var_mkfree name =
let rec x =
let var_box = Env([V(x)], 0, build_var_aux var_key) in
let var_box = Env([V(x,1)], 0, build_var_aux var_key) in
{var_key; var_name = name; var_mkfree; var_box}
in x

Expand Down Expand Up @@ -455,14 +460,14 @@ let bind_var : 'a var -> 'b box -> ('a, 'b) binder box = fun x b ->
| Env(vs,n,t) ->
try
match vs with
| [V(y)] ->
| [V(y,_)] ->
if x.var_key <> y.var_key then raise Not_found;
(* The variable to bind is the last one. *)
let r = 0 in
let t = t (IMap.singleton x.var_key r) in
let value = bind_var_aux1 n t in
Box(build_binder x 0 true value)
| _ ->
| _ ->
let vs = remove x vs in
(* General case. *)
let cl vp =
Expand Down Expand Up @@ -634,7 +639,7 @@ module Ctxt(R:Renaming) = struct
match b with
| Box(_) -> empty_ctxt
| Env(vs,_,_) ->
let add ctxt (V(x)) = reserve_name (name_of x) ctxt in
let add ctxt (V(x,_)) = reserve_name (name_of x) ctxt in
List.fold_left add empty_ctxt vs

let new_var_in ctxt mkfree name =
Expand Down
3 changes: 3 additions & 0 deletions lib/bindlib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -479,6 +479,9 @@ val is_closed : 'a box -> bool
linear time with respect to the number of free variables in [b]. *)
val occur : 'a var -> 'b box -> bool

(** [nb_occurs x b] indicates how many times variable [x] occurs in [b]. *)
val nb_occurs : 'a var -> 'b box -> int

(** [bind_apply bb barg] is the same as [box_apply2 subst bb barg]. *)
val bind_apply : ('a, 'b) binder box -> 'a box -> 'b box

Expand Down
4 changes: 0 additions & 4 deletions lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,5 @@
(name bindlib)
(public_name bindlib)
(synopsis "An efficient representation of binders")
(preprocess
(action
(run ocaml %{project_root}/lib/pp.ml %{ocaml_version} %{input-file})))
(preprocessor_deps pp.ml)
(modules bindlib)
(wrapped false))
27 changes: 0 additions & 27 deletions lib/pp.ml

This file was deleted.