X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=56e98775f31caf7276303a091dbeb22612128046;hb=0c8963a0f3aef05cf4866e8bcd3fdbebddac8b87;hp=7ba2cffbcfaa76298770ed8c19c5a5c369badadc;hpb=afa05d30f20de12e031c3e5c3e5c33c19c42a7d8;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 7ba2cffbc..56e98775f 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -23,9 +23,10 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* TODO unify exceptions *) -exception CicReductionInternalError;; exception WrongUriToInductiveDefinition;; exception Impossible of int;; exception ReferenceToConstant;; @@ -53,64 +54,73 @@ module type Strategy = type stack_term type env_term type ens_term - val to_stack : Cic.term -> stack_term - val to_stack_list : Cic.term list -> stack_term list - val to_env : Cic.term -> env_term - val to_ens : Cic.term -> ens_term - val from_stack : - unwind: - (int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> Cic.term) -> - stack_term -> Cic.term - val from_stack_list : - unwind: - (int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> Cic.term) -> + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + val to_env : config -> env_term + val to_ens : config -> ens_term + val from_stack : stack_term -> config + val from_stack_list_for_unwind : + unwind: (config -> Cic.term) -> stack_term list -> Cic.term list - val from_env : env_term -> Cic.term - val from_ens : ens_term -> Cic.term + val from_env : env_term -> config + val from_env_for_unwind : + unwind: (config -> Cic.term) -> + env_term -> Cic.term + val from_ens : ens_term -> config + val from_ens_for_unwind : + unwind: (config -> Cic.term) -> + ens_term -> Cic.term val stack_to_env : - reduce: - (int * env_term list * ens_term Cic.explicit_named_substitution * - Cic.term * stack_term list -> Cic.term) -> - unwind: - (int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> Cic.term) -> + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> stack_term -> env_term val compute_to_env : - reduce: - (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * - stack_term list -> Cic.term) -> - unwind: - (int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> Cic.term) -> + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> int -> env_term list -> ens_term Cic.explicit_named_substitution -> Cic.term -> env_term val compute_to_stack : - reduce: - (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * - stack_term list -> Cic.term) -> - unwind: - (int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> Cic.term) -> - int -> env_term list -> ens_term Cic.explicit_named_substitution -> - Cic.term -> stack_term + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> + config -> stack_term end ;; +module CallByValueByNameForUnwind = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config * config (* cbv, cbn *) + and ens_term = config * config (* cbv, cbn *) + + let to_env c = c,c + let to_ens c = c,c + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l + let from_env (c,_) = c + let from_ens (c,_) = c + let from_env_for_unwind ~unwind (_,c) = unwind c + let from_ens_for_unwind ~unwind (_,c) = unwind c + let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[]) + let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[]) + let compute_to_stack ~reduce ~unwind config = config + end +;; + + module CallByNameStrategy = struct type stack_term = Cic.term type env_term = Cic.term type ens_term = Cic.term - let to_stack v = v - let to_stack_list l = l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = v let to_ens v = v let from_stack ~unwind v = v let from_stack_list ~unwind l = l let from_env v = v let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t @@ -122,14 +132,15 @@ module CallByValueStrategy = type stack_term = Cic.term type env_term = Cic.term type ens_term = Cic.term - let to_stack v = v - let to_stack_list l = l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = v let to_ens v = v let from_stack ~unwind v = v let from_stack_list ~unwind l = l let from_env v = v let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[]) let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[]) @@ -141,14 +152,15 @@ module CallByValueStrategyByNameOnConstants = type stack_term = Cic.term type env_term = Cic.term type ens_term = Cic.term - let to_stack v = v - let to_stack_list l = l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = v let to_ens v = v let from_stack ~unwind v = v let from_stack_list ~unwind l = l let from_env v = v let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens = function @@ -166,14 +178,15 @@ module LazyCallByValueStrategy = type stack_term = Cic.term lazy_t type env_term = Cic.term lazy_t type ens_term = Cic.term lazy_t - let to_stack v = lazy v - let to_stack_list l = List.map to_stack l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = lazy v let to_ens v = lazy v let from_stack ~unwind v = Lazy.force v let from_stack_list ~unwind l = List.map (from_stack ~unwind) l let from_env v = Lazy.force v let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[])) let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[])) @@ -185,14 +198,15 @@ module LazyCallByValueStrategyByNameOnConstants = type stack_term = Cic.term lazy_t type env_term = Cic.term lazy_t type ens_term = Cic.term lazy_t - let to_stack v = lazy v - let to_stack_list l = List.map to_stack l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = lazy v let to_ens v = lazy v let from_stack ~unwind v = Lazy.force v let from_stack_list ~unwind l = List.map (from_stack ~unwind) l let from_env v = Lazy.force v let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = lazy ( @@ -212,14 +226,15 @@ module LazyCallByNameStrategy = type stack_term = Cic.term lazy_t type env_term = Cic.term lazy_t type ens_term = Cic.term lazy_t - let to_stack v = lazy v - let to_stack_list l = List.map to_stack l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = lazy v let to_ens v = lazy v let from_stack ~unwind v = Lazy.force v let from_stack_list ~unwind l = List.map (from_stack ~unwind) l let from_env v = Lazy.force v let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t) let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t) @@ -233,10 +248,7 @@ module type stack_term = reduce:bool -> Cic.term type env_term = reduce:bool -> Cic.term type ens_term = reduce:bool -> Cic.term - let to_stack v = - let value = lazy v in - fun ~reduce -> Lazy.force value - let to_stack_list l = List.map to_stack l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = let value = lazy v in fun ~reduce -> Lazy.force value @@ -247,6 +259,8 @@ module let from_stack_list ~unwind l = List.map (from_stack ~unwind) l let from_env v = (v ~reduce:true) let from_ens v = (v ~reduce:true) + let from_env_for_unwind ~unwind v = (v ~reduce:true) + let from_ens_for_unwind ~unwind v = (v ~reduce:true) let stack_to_env ~reduce ~unwind v = v let compute_to_stack ~reduce ~unwind k e ens t = let svalue = @@ -277,22 +291,22 @@ module module ClosuresOnStackByValueFromEnvOrEnsStrategy = struct - type stack_term = - int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term - type env_term = Cic.term - type ens_term = Cic.term - let to_stack v = (0,[],[],v) - let to_stack_list l = List.map to_stack l - let to_env v = v - let to_ens v = v - let from_stack ~unwind (k,e,ens,t) = unwind k e ens t - let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config + and ens_term = config + + let to_env config = config + let to_ens config = config + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l let from_env v = v let from_ens v = v - let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[]) - let compute_to_env ~reduce ~unwind k e ens t = - unwind k e ens t - let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t) + let from_env_for_unwind ~unwind config = unwind config + let from_ens_for_unwind ~unwind config = unwind config + let stack_to_env ~reduce ~unwind config = reduce config + let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]) + let compute_to_stack ~reduce ~unwind config = config end ;; @@ -302,14 +316,15 @@ module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy = int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term type env_term = Cic.term type ens_term = Cic.term - let to_stack v = (0,[],[],v) - let to_stack_list l = List.map to_stack l + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list let to_env v = v let to_ens v = v let from_stack ~unwind (k,e,ens,t) = unwind k e ens t let from_stack_list ~unwind l = List.map (from_stack ~unwind) l let from_env v = v let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v let stack_to_env ~reduce ~unwind (k,e,ens,t) = match t with Cic.Const _ as t -> unwind k e ens t @@ -329,7 +344,7 @@ module Reduction(RS : Strategy) = (* k is the length of the environment e *) (* m is the current depth inside the term *) - let unwind' m k e ens t = + let rec unwind' m k e ens t = let module C = Cic in let module S = CicSubstitution in if k = 0 && ens = [] then @@ -341,7 +356,7 @@ module Reduction(RS : Strategy) = if n <= m then t else let d = try - Some (RS.from_env (List.nth e (n-m-1))) + Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1))) with _ -> None in (match d with @@ -354,7 +369,7 @@ module Reduction(RS : Strategy) = debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ; *) if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then - CicSubstitution.lift m (RS.from_ens (List.assq uri ens)) + CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind (List.assq uri ens)) else let params = let o,_ = @@ -492,7 +507,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, && List.mem uri params -> - (uri,CicSubstitution.lift m (RS.from_ens t)) :: + (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) :: (filter_and_lift (uri::already_instantiated) tl) | _::tl -> filter_and_lift already_instantiated tl (* @@ -509,9 +524,11 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; (filter_and_lift [] (List.rev ens)) in unwind_aux m t - ;; - let unwind = unwind' 0;; + and unwind (k,e,ens,t,s) = + let t' = unwind' 0 k e ens t in + if s = [] then t' else Cic.Appl (t'::(RS.from_stack_list_for_unwind ~unwind s)) + ;; (* let unwind = @@ -521,37 +538,34 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; ;; *) - let reduce ~delta ?(subst = []) context : config -> Cic.term = + let reduce ~delta ?(subst = []) context : config -> config = let module C = Cic in let module S = CicSubstitution in let rec reduce = function - (k, e, _, C.Rel n, s) -> - let d = + (k, e, _, C.Rel n, s) as config -> + let config' = try Some (RS.from_env (List.nth e (n-1))) with - _ -> + Failure _ -> try begin match List.nth context (n - 1 - k) with None -> assert false | Some (_,C.Decl _) -> None - | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x) + | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) end with - _ -> None + Failure _ -> None in - (match d with - Some t' -> reduce (0,[],[],t',s) - | None -> - if s = [] then - C.Rel (n-k) - else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s)) - ) - | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> + (match config' with + Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s) + | None -> config) + | (k, e, ens, C.Var (uri,exp_named_subst), s) as config -> if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then - reduce (0, [], [], RS.from_ens (List.assq uri ens), s) + let (k',e',ens',t',s') = RS.from_ens (List.assq uri ens) in + reduce (k',e',ens',t',s'@s) else ( let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri @@ -560,28 +574,22 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_,_) -> - let t' = unwind k e ens t in - if s = [] then t' else - C.Appl (t'::(RS.from_stack_list ~unwind s)) + | C.Variable (_,None,_,_,_) -> config | C.Variable (_,Some body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in reduce (0, [], ens', body, s) ) - | (k, e, ens, (C.Meta (n,l) as t), s) -> + | (k, e, ens, C.Meta (n,l), s) as config -> (try let (_, term,_) = CicUtil.lookup_subst n subst in reduce (k, e, ens,CicSubstitution.subst_meta l term,s) - with CicUtil.Subst_not_found _ -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) - | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) - | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *) + with CicUtil.Subst_not_found _ -> config) + | (_, _, _, C.Sort _, _) + | (_, _, _, C.Implicit _, _) as config -> config | (k, e, ens, C.Cast (te,ty), s) -> - reduce (k, e, ens, te, s) (* s should be empty *) - | (k, e, ens, (C.Prod _ as t), s) -> - unwind k e ens t (* s should be empty *) - | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' + reduce (k, e, ens, te, s) + | (_, _, _, C.Prod _, _) as config -> config + | (_, _, _, C.Lambda _, []) as config -> config | (k, e, ens, C.Lambda (_,_,t), p::s) -> reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s) | (k, e, ens, C.LetIn (_,m,t), s) -> @@ -591,29 +599,11 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (k, e, ens, C.Appl (he::tl), s) -> let tl' = List.map - (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl + (function t -> RS.compute_to_stack ~reduce ~unwind (k,e,ens,t,[])) tl in reduce (k, e, ens, he, (List.append tl') s) - (* CSC: Old Dead Code - | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) - | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s) - | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) - | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) -> - (* strict evaluation, but constants are NOT unfolded *) - let red = - function - C.Const _ as t -> unwind k e ens t - | t -> reduce (k,e,ens,t,[]) - in - let tl' = List.map red tl in - reduce (k, e, ens, he , List.append tl' s) - | (k, e, ens, C.Appl l, s) -> - C.Appl (List.append (List.map (unwind k e ens) l) s) - *) - | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false-> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) - | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> + | (_, _, _, C.Const _, _) as config when delta=false-> config + | (k, e, ens, C.Const (uri,exp_named_subst), s) as config -> (let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in @@ -622,9 +612,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) reduce (0, [], ens', body, s) - | C.Constant (_,None,_,_,_) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) + | C.Constant (_,None,_,_,_) -> config | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in @@ -632,16 +620,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; reduce (0, [], ens', body, s) | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) - | (k, e, ens, (C.MutInd _ as t),s) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) - | (k, e, ens, (C.MutConstruct _ as t),s) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) - | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) -> + | (_, _, _, C.MutInd _, _) + | (_, _, _, C.MutConstruct _, _) as config -> config + | (k, e, ens, C.MutCase (mutind,i,outty,term,pl),s) as config -> let decofix = function - C.CoFix (i,fl) -> + (k, e, ens, C.CoFix (i,fl), s) -> let (_,_,body) = List.nth fl i in let body' = let counter = ref (List.length fl) in @@ -650,34 +634,20 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; fl body in - (* the term is the result of a reduction; *) - (* so it is already unwinded. *) - reduce (0,[],[],body',[]) - | C.Appl (C.CoFix (i,fl) :: tl) -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - (* the term is the result of a reduction; *) - (* so it is already unwinded. *) - reduce (0,[],[],body',RS.to_stack_list tl) - | t -> t + reduce (k,e,ens,body',s) + | config -> config in (match decofix (reduce (k,e,ens,term,[])) with - C.MutConstruct (_,_,j,_) -> - reduce (k, e, ens, (List.nth pl (j-1)), s) - | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> + (k', e', ens', C.MutConstruct (_,_,j,_), []) -> + reduce (k, e, ens, (List.nth pl (j-1)), []) + | (k', e', ens', C.MutConstruct (_,_,j,_), s') -> let (arity, r) = let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (tl,ingredients,r,_) -> - let (_,_,arity,_) = List.nth tl i in + C.InductiveDefinition (s,ingredients,r,_) -> + let (_,_,arity,_) = List.nth s i in (arity,r) | _ -> raise WrongUriToInductiveDefinition in @@ -686,98 +656,76 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let rec eat_first = function (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | (n,he::s) when n > 0 -> eat_first (n - 1, s) | _ -> raise (Impossible 5) in - eat_first (num_to_eat,tl) + eat_first (num_to_eat,s') in - (* ts are already unwinded because they are a sublist of tl *) - reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s) - | C.Cast _ | C.Implicit _ -> + reduce (k, e, ens, (List.nth pl (j-1)), ts@s) + | (_, _, _, C.Cast _, _) + | (_, _, _, C.Implicit _, _) -> raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) - ) - | (k, e, ens, (C.Fix (i,fl) as t), s) -> + | config' -> + (*CSC: here I am unwinding the configuration and for sure I + will do it twice; to avoid this unwinding I should push the + "match [] with _" continuation on the stack; + another possibility is to just return the original configuration, + partially undoing the weak-head computation *) + (*this code is uncorrect since term' lives in e' <> e + let term' = unwind config' in + (k, e, ens, C.MutCase (mutind,i,outty,term',pl),s) + *) + config) + | (k, e, ens, C.Fix (i,fl), s) as config -> let (_,recindex,_,body) = List.nth fl i in let recparam = try - Some (RS.from_stack ~unwind (List.nth s recindex)) + Some (RS.from_stack (List.nth s recindex)) with _ -> None in (match recparam with Some recparam -> - (match reduce (0,[],[],recparam,[]) with - (* match recparam with *) - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - (* OLD - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - reduce (k, e, ens, body', s) *) - (* NEW *) + (match reduce recparam with + (_,_,_,C.MutConstruct _,_) as config -> let leng = List.length fl in - let fl' = - let unwind_fl (name,recindex,typ,body) = - (name,recindex,unwind k e ens typ, - unwind' leng k e ens body) + let new_env = + let counter = ref 0 in + let rec build_env e = + if !counter = leng then e + else + (incr counter ; + build_env + ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e)) in - List.map unwind_fl fl + build_env e in - let new_env = - let counter = ref 0 in - let rec build_env e = - if !counter = leng then e - else - (incr counter ; - build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e)) - in - build_env e - in - reduce (k+leng, new_env, ens, body, s) - | _ -> - let t' = unwind k e ens t in - if s = [] then t' else - C.Appl (t'::(RS.from_stack_list ~unwind s)) - ) - | None -> - let t' = unwind k e ens t in - if s = [] then t' else - C.Appl (t'::(RS.from_stack_list ~unwind s)) + let rec replace i s t = + match i,s with + 0,_::tl -> t::tl + | n,he::tl -> he::(replace (n - 1) tl t) + | _,_ -> assert false in + let new_s = + replace recindex s (RS.compute_to_stack ~reduce ~unwind config) + in + reduce (k+leng, new_env, ens, body, new_s) + | _ -> config) + | None -> config ) - | (k, e, ens, (C.CoFix (i,fl) as t),s) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) + | (_,_,_,C.CoFix _,_) as config -> config and push_exp_named_subst k e ens = function [] -> ens | (uri,t)::tl -> - push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl + push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl in - reduce - ;; - (* - let rec whd context t = - try - reduce context (0, [], [], t, []) - with Not_found -> - debug_print (lazy (CicPp.ppterm t)) ; - raise Not_found + reduce ;; - *) - let rec whd ?(delta=true) ?(subst=[]) context t = - reduce ~delta ~subst context (0, [], [], t, []) + let whd ?(delta=true) ?(subst=[]) context t = + unwind (reduce ~delta ~subst context (0, [], [], t, [])) ;; - end ;; @@ -798,7 +746,8 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) -module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; +module R = Reduction(CallByValueByNameForUnwind);; +(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) module U = UriManager;; let whd = R.whd @@ -1019,21 +968,11 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = | (_,_) -> false,ugraph end in - begin - debug t1 [t2] "PREWHD"; - (* - (match t1 with - Cic.Meta _ -> - debug_print (lazy (CicPp.ppterm t1)); - debug_print (lazy (CicPp.ppterm (whd ~subst context t1))); - debug_print (lazy (CicPp.ppterm t2)); - debug_print (lazy (CicPp.ppterm (whd ~subst context t2))) - | _ -> ()); *) - let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in - let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in - debug t1' [t2'] "POSTWHD"; - aux2 test_equality_only t1' t2' ugraph - end + debug t1 [t2] "PREWHD"; + let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in + let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in + debug t1' [t2'] "POSTWHD"; + aux2 test_equality_only t1' t2' ugraph in aux false (*c t1 t2 ugraph *) ;; @@ -1077,7 +1016,6 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = let t = whd ~delta ~subst ctx term in let aux = normalize ~delta ~subst in let decl name t = Some (name, C.Decl t) in - let def name t = Some (name, C.Def (t,None)) in match t with | C.Rel n -> t | C.Var (uri,exp_named_subst) ->