let rec aux g =
function
(* mmm -> print_endline (print_machine mmm); match mmm with *)
+ m when unwind m = let d = L(A(V 0, V 0)) in A(d,d) -> [], B, []
| (e,A(t1,t2),s) ->
let t2' = aux g (e,t2,[]) in
let (_,t,_) = t2' in
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 =