diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 263 |
1 files changed, 132 insertions, 131 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b590f743..82cc1b7d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 8708 2006-04-14 08:13:02Z jforest $ *) +(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -23,6 +23,91 @@ open Reduction exception Elimconst + +(**********************************************************************) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) + +type 'a stack_member = + | Zapp of 'a list + | Zcase of case_info * 'a * 'a array + | Zfix of 'a * 'a stack + | Zshift of int + | Zupdate of 'a + +and 'a stack = 'a stack_member list + +let empty_stack = [] +let append_stack_list = function + | ([],s) -> s + | (l1, Zapp l :: s) -> Zapp (l1@l) :: s + | (l1, s) -> Zapp l1 :: s +let append_stack v s = append_stack_list (Array.to_list v, 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 + +let rec stack_args_size = function + | Zapp l::s -> List.length l + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + +(* When used as an argument stack (only Zapp can appear) *) +let rec decomp_stack = function + | Zapp[v]::s -> Some (v, s) + | Zapp(v::l)::s -> Some (v, (Zapp l :: s)) + | Zapp [] :: s -> decomp_stack s + | _ -> None +let rec decomp_stackn = function + | Zapp [] :: s -> decomp_stackn s + | Zapp l :: s -> (Array.of_list l, s) + | _ -> assert false +let array_of_stack s = + let rec stackrec = function + | [] -> [] + | Zapp args :: s -> args :: (stackrec s) + | _ -> assert false + in Array.of_list (List.concat (stackrec s)) +let rec list_of_stack = function + | [] -> [] + | Zapp args :: s -> args @ (list_of_stack s) + | _ -> assert false +let rec app_stack = function + | f, [] -> f + | f, (Zapp [] :: s) -> app_stack (f, s) + | f, (Zapp args :: s) -> + app_stack (applist (f, args), s) + | _ -> assert false +let rec stack_assign s p c = match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then + Zapp args :: stack_assign s (p-q) c + else + (match list_chop p args with + (bef, _::aft) -> Zapp (bef@c::aft) :: s + | _ -> assert false) + | _ -> s +let rec stack_tail p s = + if p = 0 then s else + match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then stack_tail (p-q) s + else Zapp (list_skipn p args) :: s + | _ -> failwith "stack_tail" +let rec stack_nth s p = match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then stack_nth s (p-q) + else List.nth args p + | _ -> raise Not_found + +(**************************************************************) (* The type of (machine) states (= lambda-bar-calculus' cuts) *) type state = constr * constr stack @@ -428,13 +513,13 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) - when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + when Evd.mem sigma ev & Evd.is_defined sigma ev -> whd_evar sigma (Evd.existential_value sigma (ev,args)) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar evd = - local_strong (whd_evar evd) +let nf_evar sigma = + local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) let clos_norm_flags flgs env sigma t = @@ -451,113 +536,49 @@ let nf_betadeltaiota env sigma = du type checking : (fun x => x + x) M *) -let nf_betaiotaevar_preserving_vm_cast env sigma t = - let push decl (env,subst) = - (Environ.push_rel decl env, Esubst.subs_lift subst) in - let cons decl v (env, subst) = (push_rel decl env, Esubst.subs_cons (v,subst)) in - - let app_stack t (f, stack) = - let t' = app_stack (f,stack) in - match kind_of_term t, kind_of_term t' with - | App(f,args), App(f',args') when f == f' && array_for_all2 (==) args args' -> t - | _ -> t' - in - let rec whrec (env, subst as es) (t, stack as s) = - match kind_of_term t with - | Rel i -> - let t' = - match Esubst.expand_rel i subst with - | Inl (k,e) -> lift k e - | Inr (k,None) -> mkRel k - | Inr (k, Some p) -> lift (k-p) (mkRel p) (*??????? == mkRel k ! Julien *) - (* Est correct ??? *) - in - if t = t' then s else t', stack - | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> s - | Evar (e,al) -> - let al' = Array.map (norm es) al in - begin match existential_opt_value sigma (e,al') with - | Some body -> whrec (env,Esubst.ESID 0) (body, stack) (**** ????? ****) - | None -> - if array_for_all2 (==) al al' then s else (mkEvar (e, al'), stack) - end - | Cast (c,VMcast,t) -> - let c' = norm es c in - let t' = norm es t in - if c == c' && t == t' then s - else (mkCast(c',VMcast,t'),stack) - | Cast (c,DEFAULTcast,_) -> - whrec es (c, stack) - - | Prod (na,t,c) -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t==t' && c==c' then s else (mkProd (na, t', c'), stack) - - | Lambda (na,t,c) -> - begin match decomp_stack stack with - | Some (a,m) -> - begin match kind_of_term a with - | Rel i when not (evaluable_rel i env) -> - whrec (cons (na,None,t) a es) (c, m) - | Var id when not (evaluable_named id env)-> - whrec (cons (na,None,t) a es) (c, m) - | _ -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t == t' && c == c' then s - else mkLambda (na, t', c'), stack - end - | _ -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t == t' && c == c' then s - else mkLambda(na,t',c'),stack - - end - | LetIn (na,b,t,c) -> - let b' = norm es b in - let t' = norm es t in - let c' = norm (push (na, Some b', t') es) c in - if b==b' && t==t' && c==c' then s - else mkLetIn (na, b', t', c'), stack - - | App (f,cl) -> - let cl' = Array.map (norm es) cl in - whrec es (f, append_stack cl' stack) - - | Case (ci,p,d,lf) -> - let (c,cargs) = whrec es (d, empty_stack) in - if reducible_mind_case c then - whrec es (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - let p' = norm es p in - let d' = app_stack d (c,cargs) in - let lf' = Array.map (norm es) lf in - if p==p' && d==d' && array_for_all2 (==) lf lf' then s - else (mkCase (ci, p', d', lf'), stack) - | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.map (norm es) tl in - let es' = - array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl' in - let bl' = Array.map (norm es') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' - then s - else (mkFix (ln,(lna,tl',bl')), stack) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.map (norm es) tl in - let es' = - array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl in - let bl' = Array.map (norm es') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' - then s - else (mkCoFix (ln,(lna,tl',bl')), stack) - - and norm es t = app_stack t (whrec es (t,empty_stack)) in - norm (env, Esubst.ESID 0) t - +let rec whd_betaiotaevar_preserving_vm_cast env sigma t = + let rec stacklam_var subst t stack = + match (decomp_stack stack,kind_of_term t) with + | Some (h,stacktl), Lambda (_,_,c) -> + begin match kind_of_term h with + | Rel i when not (evaluable_rel i env) -> + stacklam_var (h::subst) c stacktl + | Var id when not (evaluable_named id env)-> + stacklam_var (h::subst) c stacktl + | _ -> whrec (substl subst t, stack) + end + | _ -> whrec (substl subst t, stack) + and whrec (x, stack as s) = + match kind_of_term x with + | Evar ev -> + (match existential_opt_value sigma ev with + | Some body -> whrec (body, stack) + | None -> s) + | Cast (c,VMcast,t) -> + let c = app_stack (whrec (c,empty_stack)) in + let t = app_stack (whrec (t,empty_stack)) in + (mkCast(c,VMcast,t),stack) + | Cast (c,DEFAULTcast,_) -> + whrec (c, stack) + | App (f,cl) -> whrec (f, append_stack cl stack) + | Lambda (na,t,c) -> + (match decomp_stack stack with + | Some (a,m) -> stacklam_var [a] c m + | _ -> s) + | Case (ci,p,d,lf) -> + let (c,cargs) = whrec (d, empty_stack) in + if reducible_mind_case c then + whrec (reduce_mind_case + {mP=p; mconstr=c; mcargs=list_of_stack cargs; + mci=ci; mlf=lf}, stack) + else + (mkCase (ci, p, app_stack (c,cargs), lf), stack) + | x -> s + in + app_stack (whrec (t,empty_stack)) + +let nf_betaiotaevar_preserving_vm_cast = + strong whd_betaiotaevar_preserving_vm_cast (* lazy weak head reduction functions *) let whd_flags flgs env sigma t = @@ -825,26 +846,6 @@ let is_arity env sigma c = match find_conclusion env sigma c with | Sort _ -> true | _ -> false - -let info_arity env sigma c = - match find_conclusion env sigma c with - | Sort (Prop Null) -> false - | Sort (Prop Pos) -> true - | _ -> raise IsType - -let is_info_arity env sigma c = - try (info_arity env sigma c) with IsType -> true - -let is_type_arity env sigma c = - match find_conclusion env sigma c with - | Sort (Type _) -> true - | _ -> false - -let is_info_type env sigma t = - let s = t.utj_type in - (s = Prop Pos) || - (s <> Prop Null && - try info_arity env sigma t.utj_val with IsType -> true) (*************************************) (* Metas *) |