X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=af5564d0754c32c39a594bdef0ad2ba6552dd298;hb=ed936515481f5035fde443f4aee55b86e427cef4;hp=b636c2a729aa2ef688d99a8c8a42e0c173b795f5;hpb=bada8520939f45188270ba7ba5e006e55d3a0d15;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index b636c2a72..af5564d07 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -55,8 +55,14 @@ module type Strategy = type env_term type ens_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 to_env : + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> + config -> env_term + val to_ens : + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> + config -> ens_term val from_stack : stack_term -> config val from_stack_list_for_unwind : unwind: (config -> Cic.term) -> @@ -106,6 +112,28 @@ module CallByValueByNameForUnwind = 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 lazy_t * Cic.term lazy_t (* cbv, cbn *) + and env_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *) + and ens_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *) + + let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let to_ens ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let from_stack (c,_) = Lazy.force c + let from_stack_list_for_unwind ~unwind l = List.map (function (_,c) -> Lazy.force c) l + let from_env (c,_) = Lazy.force c + let from_ens (c,_) = Lazy.force c + let from_env_for_unwind ~unwind (_,c) = Lazy.force c + let from_ens_for_unwind ~unwind (_,c) = Lazy.force c + let stack_to_env ~reduce ~unwind config = config + let compute_to_env ~reduce ~unwind k e ens t = + lazy (reduce (k,e,ens,t,[])), lazy (unwind (k,e,ens,t,[])) + let compute_to_stack ~reduce ~unwind config = lazy (reduce config), lazy (unwind config) + end +;; + (* Old Machine module CallByNameStrategy = @@ -712,12 +740,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let leng = List.length fl in let new_env = let counter = ref 0 in - let rec build_env e = - if !counter = leng then e + 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)) + ((RS.to_env ~reduce ~unwind (k,e,ens,C.Fix (!counter -1, fl),[]))::e')) in build_env e in @@ -738,7 +766,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function [] -> ens | (uri,t)::tl -> - push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl + push_exp_named_subst k e ((uri,RS.to_ens ~reduce ~unwind (k,e,ens,t,[]))::ens) tl in reduce ;; @@ -767,7 +795,8 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) -module R = Reduction(CallByValueByNameForUnwind);; +(*module R = Reduction(CallByValueByNameForUnwind);;*) +module R = Reduction(CallByValueByNameForUnwind');; (*module R = Reduction(CallByNameStrategy);;*) (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) module U = UriManager;; @@ -856,10 +885,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); with CicUtil.Subst_not_found _ -> false,ugraph) (* TASSI: CONSTRAINTS *) | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - true,(CicUniv.add_eq t2 t1 ugraph) + (try + true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) (* TASSI: CONSTRAINTS *) | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - true,(CicUniv.add_ge t2 t1 ugraph) + (try + true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) (* TASSI: CONSTRAINTS *) | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph (* TASSI: CONSTRAINTS *) @@ -969,8 +1002,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - let tys = - List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 in if i1 = i2 then List.fold_right2 @@ -988,9 +1025,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - let tys = - List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 - in + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 + in if i1 = i2 then List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> @@ -1116,46 +1157,49 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce ?(delta=false) = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - let he''' = - match he'' with - Cic.Appl l -> Cic.Appl (l@tl') - | _ -> Cic.Appl (he''::tl') +let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = + match upto with + 0 -> t + | n -> + match t with + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce ~delta ~upto:(upto - 1) he''' + | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te + | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition in - head_beta_reduce ~delta he''' - | Cic.Cast (te,_) -> head_beta_reduce ~delta te - | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> - let bo = - match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with - Cic.Constant (_,bo,_,_,_) -> bo - | Cic.Variable _ -> raise ReferenceToVariable - | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - in - (match bo with - None -> t - | Some bo -> - head_beta_reduce - ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) - | Cic.Const (uri,ens) as t when delta=true -> - let bo = - match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with - Cic.Constant (_,bo,_,_,_) -> bo - | Cic.Variable _ -> raise ReferenceToVariable - | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - in - (match bo with - None -> t - | Some bo -> - head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo)) - | t -> t + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~upto + ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) + | Cic.Const (uri,ens) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo)) + | t -> t (* let are_convertible ?subst ?metasenv context t1 t2 ugraph =