From a031240cd6e2e0dcd6936eca6e535f3c55d0b91a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Jan 2006 16:18:10 +0000 Subject: [PATCH] (Partial commit) Improved version of cicReduction. Configurations can now be preserved as much as possible (without need to go back to terms by means of unwind). This allows the implementation of new strategies and removes a few sources of inefficiences. The commit is partial since not every strategy has been ported yet. --- helm/ocaml/cic_proof_checking/Makefile | 3 + helm/ocaml/cic_proof_checking/cicReduction.ml | 366 ++++++++---------- 2 files changed, 174 insertions(+), 195 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 3fbe90ddb..28462e58e 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -25,6 +25,9 @@ EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common +cicReduction.cmo: OCAMLOPTIONS+=-rectypes +cicReduction.cmx: OCAMLOPTIONS+=-rectypes + all: all_utilities opt: opt_utilities diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index b7592f0fa..dd1e57f91 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -27,7 +27,6 @@ (* TODO unify exceptions *) -exception CicReductionInternalError;; exception WrongUriToInductiveDefinition;; exception Impossible of int;; exception ReferenceToConstant;; @@ -55,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 @@ -124,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,[]) @@ -143,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 @@ -168,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,[])) @@ -187,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 ( @@ -214,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) @@ -235,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 @@ -249,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 = @@ -279,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 ;; @@ -304,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 @@ -331,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 @@ -343,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 @@ -356,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,_ = @@ -494,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 (* @@ -511,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 = @@ -523,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 @@ -562,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) -> @@ -593,7 +599,7 @@ 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 @@ -612,10 +618,8 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (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 @@ -624,9 +628,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 @@ -634,16 +636,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 @@ -652,34 +650,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 @@ -688,33 +672,39 @@ 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 reduce recparam with (* match recparam with *) - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> + (_,_,_,C.MutConstruct _,_) as config -> (* OLD let body' = let counter = ref (List.length fl) in @@ -726,44 +716,37 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; reduce (k, e, ens, body', s) *) (* NEW *) 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 + reduce ;; (* let rec whd context t = @@ -775,8 +758,8 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; ;; *) - 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, [])) ;; @@ -800,6 +783,7 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) +(*module R = Reduction(CallByValueByNameForUnwind);; *) module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; module U = UriManager;; @@ -1021,16 +1005,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = | (_,_) -> false,ugraph end in - begin + 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"; -- 2.39.2