From 18e8638888e5e47d755a6c7c4bff37a1a6ec026b Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 15:27:24 +0200
Subject: [PATCH] Moved env_of_sigma to Pure

---
 ocaml/lambda4.ml | 17 ++---------------
 ocaml/pure.ml    | 13 +++++++++++++
 ocaml/pure.mli   |  1 +
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 311537a..9395daa 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -632,18 +632,6 @@ let optimize_numerals p =
   replace_in_sigma (List.rev perm) p.sigma
 ;;
 
-let env_of_sigma freshno sigma should_explode =
- let rec aux n =
-  if n > freshno then
-   []
-  else
-   let e = aux (n+1) in
-   (try
-    e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
-   with
-    Not_found -> ([], Pure.V n, []) ) :: e
- in aux 0
-;;
 (* ************************************************************************** *)
 
 type result = [
@@ -694,8 +682,7 @@ let solve p =
  let ps = List.map scott_of_nf p.ps in
 
  let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in
- let e' = env_of_sigma freshno sigma' false in
- let e'' = env_of_sigma freshno sigma' true in
+ let e' = Pure.env_of_sigma freshno sigma' in
 
  prerr_endline "--------<REDUCE>---------";
  (function
@@ -707,7 +694,7 @@ let solve p =
    | None -> ()) div;
  List.iter (fun n ->
   verbose ("_::: " ^ (Pure.print n));
-  let t = Pure.mwhd (e'',n,[]) in
+  let t = Pure.mwhd (e',n,[]) in
   verbose ("_:: " ^ (Pure.print t));
   assert (not (Pure.diverged t))
  ) conv ;
diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 7963f87..11cb9af 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -132,6 +132,19 @@ let omega should_explode =
 
 let diverged = (=) B;;
 
+(* Note: maps only variables <= freshno *)
+let env_of_sigma freshno sigma =
+ let rec aux n =
+  if n > freshno then
+   []
+  else
+   let e = aux (n+1) in
+   (try
+    e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
+   with
+    Not_found -> ([], V n, []) ) :: e
+ in aux 0
+
 end
 
 module Scott =
diff --git a/ocaml/pure.mli b/ocaml/pure.mli
index 1b60c09..9b683b3 100644
--- a/ocaml/pure.mli
+++ b/ocaml/pure.mli
@@ -6,6 +6,7 @@ module Pure :
     val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t
     val omega : bool -> t
     val diverged : t -> bool
+    val env_of_sigma : int -> (int * t) list -> (('a * t * ('b list as 'c) as 'b) list as 'a)
   end
 
 module Scott :
-- 
2.39.2