open Terms;; open Subst;; open Mterms;; (********** Lazy **********) (* An abstract machine based on the closure calculus of Coq V6.2 *) (* Zipper to map a value of type 'a into a value of type 'b *) type ('a, 'b) stk = Ztop | Zappl of 'a * ('a, 'b) stk | Zappr of 'b * ('a, 'b) stk | Zlam of mterm subs * lambda * ('a, 'b) stk | Zshift of int * ('a, 'b) stk | Zupdate of mterm * ('a, 'b) stk ;; (* Invariants of the stacks: - Zshift are collapsed - no redex in the stack (e.g. no Zlam(_,_,Zappl(_,_)) ) *) (* Build a lambda from a mterm, assuming there is no uncomputed closure in it. It mainly consists in flushing the shifts. *) let to_lambda t = let rec lbda_rec lfts m stk = match m.term with Frel i -> zip_lbda (Rel (reloc_rel lfts i)) stk | Fapp(a,b) -> lbda_rec lfts a (Zappl ((lfts,b), stk)) | Flam(u,e,f) -> lbda_rec (llift lfts) u (Zlam (e,f,stk)) | Flift (k,m) -> lbda_rec (lshift k lfts) m stk | Fclos _ -> failwith "lbda_rec: found a closure" and zip_lbda t = function Ztop -> t | Zappr(u,s) -> zip_lbda (App(u,t)) s | Zlam(_,_,s) -> zip_lbda (Lam t) s | Zappl((lfts,b),s) -> lbda_rec lfts b (Zappr(t,s)) | Zshift _ | Zupdate _ -> assert false (* cannot happen *) in lbda_rec lid t Ztop ;; (* Do not generate update marks when it is obviously useless *) let zup m s = if m.norm = Red then Zupdate(m,s) else s ;; (* Collapse the shifts in the stack *) let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k,s)) -> Zshift(n+k,s) | _ -> Zshift(n,s) ;; (* Tries to rebuild the term until it reaches the top, or find an uncomputed closure. Preconditions: - m must be normal and neutral - the argument of Zappr is normal and neutral (untrue in an implementation of a call-by-value strategy) *) let rec zip m stk = match stk with Ztop -> (m, Ztop) | Zappr(a,s) -> zip {norm=Norm; term=Fapp(a,m)} s | Zlam (e,f,s) -> zip {norm=Norm; term=Flam(m,e,f)} s | Zshift(k,s) -> zip {norm=Norm; term=Flift(k,m)} s | Zupdate(m',s) -> zip (update m' (Norm, m.term)) s | Zappl(a,s) -> let s' = Zappr(m,s) in if is_val a then zip a s' else (a, s') ;; (* This "machine" strips the term from applications, lifts and closure. Thus, it returns either a value (with tag Norm), or a lambda. The result is always a subterm or a reduct of the input. *) let rec knh m stk = if is_val m then (m,stk) else match m.term with | Fapp(a,b) -> knh a (Zappl (b, zup m stk)) | Flift(k,a) -> knh a (zshift k stk) | Frel i -> (set_norm m; (m, stk)) | Flam (bd,e,f) -> (set_whnf m; (m, stk)) | Fclos(e,f) -> knht e f (Zupdate(m,stk)) (* The same for pure terms *) and knht e t stk = match t with App(a,b) -> knht e a (Zappl (mk_clos e b, stk)) | Lam f -> ({norm=Whnf; term=Flam(mk_clos (subs_lift e) f, e, f)}, stk) | Rel i -> knh (clos_rel e i) stk ;; (* This "machine" looks for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) let get_arg h stk = let rec get_arg_rec depth = function Zappl(arg,s) -> (Some(depth,arg), s) | Zshift(k,s) -> get_arg_rec (k+depth) s | Zupdate(m,s) -> update m (lift_fterm depth h); get_arg_rec depth s | s -> (None, zshift depth s) in get_arg_rec 0 stk ;; (* Computes a normal form from the result of knh. *) let rec knr m stk = match m.term with | Flam(bd,e,f) -> (match get_arg m stk with (Some (depth,arg),s) -> knit (subs_shift_cons(depth,e,arg)) f s | (None,s) -> if is_val m then (m,s) else kni bd (Zlam (e,f,s))) | _ -> (m,stk) (* Computes the normal form of a term *) and kni m stk = let (hm,s) = knh m stk in knr hm s and knit e t stk = let (ht,s) = knht e t stk in knr ht s ;; (* Computes the full normal form of a term. 1- Calls kni 2- tries to rebuild the term. If a closure still has to be computed, calls itself recursively. *) let rec walk m stk = let (nm,s) = kni m stk in match zip nm s with (rm,Ztop) -> rm | (rm,s') -> walk rm s' ;; (* Initialization and then normalization *) let kl t = let (m,s) = knit subs_id t Ztop in walk m s ;; let nkni t = to_lambda (kl t) ;;