X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=11fd5123560b1f411bd8a77832c30a6db7150f01;hb=c59d5065faea77ce41431e273a3331f4d152fbfa;hp=576721be3542c1b67a098c05f0fbbadede1e2f85;hpb=38d3574438b4f764ad433915c9733cc73a684b39;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 576721be3..11fd51235 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 = @@ -423,7 +451,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t) | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = @@ -568,19 +597,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function (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 (0,[],[],S.lift (n - k) x,[]) - end - with - Failure _ -> None + if not delta then None + else + 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 (0,[],[],S.lift (n - k) x,[]) + end + with + Failure _ -> None in (match config' with Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s) @@ -615,7 +646,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (_, _, _, 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) -> + | (k, e, ens, C.LetIn (_,m,_,t), s) -> let m' = RS.compute_to_env ~reduce ~unwind k e ens m in reduce (k+1, m'::e, ens, t, s) | (_, _, _, C.Appl [], _) -> assert false @@ -712,12 +743,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 +769,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,9 +798,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 @@ -876,17 +909,21 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + let b',ugraph' = aux true context s1 s2 ugraph in if b' then aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 ugraph' else false,ugraph - | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only - ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' + let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in + if b' then + aux test_equality_only + ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph' + else + false,ugraph else false,ugraph | (C.Appl l1, C.Appl l2) -> @@ -973,8 +1010,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 @@ -992,9 +1033,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) -> @@ -1030,11 +1075,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 *) @@ -1094,7 +1176,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = | C.Lambda (n,s,t) -> let s' = aux ctx s in C.Lambda (n, s', aux ((decl n s')::ctx) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,_,t) -> (* the term is already in weak head normal form *) assert false | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))