X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicReduction.ml;h=7f1ec58359b728857fb4536258e7f33de7b934f1;hb=a957099550619f87a58be467b9b11f2ad6501378;hp=bd8d07b8dd9a516bac801de533b1329864acc58b;hpb=a484672e530900bb3b3aa02f9fff5fedd9fb06a4;p=helm.git diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml index bd8d07b8d..7f1ec5835 100644 --- a/components/cic_proof_checking/cicReduction.ml +++ b/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 = @@ -664,14 +692,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; (k', e', ens', C.MutConstruct (_,_,j,_), []) -> reduce (k, e, ens, (List.nth pl (j-1)), s) | (k', e', ens', C.MutConstruct (_,_,j,_), s') -> - let (arity, r) = + let r = let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (s,ingredients,r,_) -> - let (_,_,arity,_) = List.nth s i in - (arity,r) + C.InductiveDefinition (_,_,r,_) -> r | _ -> raise WrongUriToInductiveDefinition in let ts = @@ -714,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 @@ -740,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 ;; @@ -769,9 +795,11 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) -module R = Reduction(CallByValueByNameForUnwind);; +(*module R = Reduction(CallByValueByNameForUnwind);;*) +module RS = CallByValueByNameForUnwind';; (*module R = Reduction(CallByNameStrategy);;*) (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) +module R = Reduction(RS);; module U = UriManager;; let whd = R.whd @@ -792,7 +820,7 @@ let (===) x y = let are_convertible whd ?(subst=[]) ?(metasenv=[]) = let heuristic = ref true in let rec aux test_equality_only context t1 t2 ugraph = - let aux2 test_equality_only t1 t2 ugraph = + let rec aux2 test_equality_only t1 t2 ugraph = (* this trivial euristic cuts down the total time of about five times ;-) *) (* this because most of the time t1 and t2 are "sintactically" the same *) @@ -858,10 +886,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 *) @@ -971,8 +1003,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 @@ -990,9 +1026,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) -> @@ -1008,7 +1048,8 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); fl1 fl2 (true,ugraph) else false,ugraph - | (C.Cast _, _) | (_, C.Cast _) + | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph + | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false,ugraph end @@ -1027,11 +1068,48 @@ begin (* heuristic := false; *) debug t1 [t2] "PREWHD"; (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) +(* +prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm 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"; +*) +let rec convert_machines ugraph = + function + [] -> true,ugraph + | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl -> + let (b,ugraph) as res = + aux2 test_equality_only + (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph + in + if b then + let problems = + try + Some + (List.combine + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s1) + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s2) + @ tl) + with + Invalid_argument _ -> None + in + match problems with + None -> false,ugraph + | Some problems -> convert_machines ugraph problems + else + res +in + convert_machines ugraph + [R.reduce ~delta:true ~subst context (0,[],[],t1,[]), + R.reduce ~delta:true ~subst context (0,[],[],t2,[])] (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*) +(* aux2 test_equality_only t1' t2' ugraph +*) end in aux false (*c t1 t2 ugraph *) @@ -1117,21 +1195,49 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce = - 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 + (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 - head_beta_reduce he''' - | Cic.Cast (te,_) -> head_beta_reduce te - | t -> t + (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 =