| V n ->
(try
lift l (cache_unwind (List.nth e (n - l)))
- with Failure _ -> V (n - l))
+ with Failure _ -> V n)
| L t -> L (aux (l+1) t)
| B -> B in
let t = aux 0 t in
String.concat "," (List.map print_machine s) ^ "]"
;; *)
+ let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
+
+ let rec is_divergent =
+ function
+ t when t = omega -> true
+ | A(t,_) -> is_divergent t
+ | L(t) -> is_divergent t
+ | _ -> false
+
let mwhd m =
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, []
+ m when is_divergent (unwind m) -> [], B, []
| (e,A(t1,t2),s) ->
let t2' = aux g (e,t2,[]) in
let (_,t,_) = t2' in
(try
let e,t,s' = List.nth e n in
aux g (e,t,s'@s)
- with Invalid_argument "List.nth" | Failure _ -> m
+ with Invalid_argument _ | Failure _ -> m
)
| (e, B, _) -> (e, B, [])
| (e, L t, []) ->
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 =