X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=5c5db75b4bb88f93ef54640b0952e77067338567;hb=440dece50deaf24f3e5216cf14cac5eca00fda85;hp=213aa2356bd1e3d9940efccdc4420f1e7dd05b2b;hpb=ed1ee239fa5380b061453d8d2e8a75ceba024b52;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 213aa2356..5c5db75b4 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -34,6 +34,37 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let ndebug = ref false;; +let indent = ref "";; +let times = ref [];; +let pp s = + if !ndebug then + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; +let inside c = + if !ndebug then + begin + let time1 = Unix.gettimeofday () in + indent := !indent ^ String.make 1 c; + times := time1 :: !times; + prerr_endline ("{{{" ^ !indent ^ " ") + end +;; +let outside ok = + if !ndebug then + begin + let time2 = Unix.gettimeofday () in + let time1 = + match !times with time1::tl -> times := tl; time1 | [] -> assert false in + prerr_endline ("}}} " ^ string_of_float (time2 -. time1)); + if not ok then prerr_endline "exception raised!"; + try + indent := String.sub !indent 0 (String.length !indent -1) + with + Invalid_argument _ -> indent := "??"; () + end +;; + let debug = false let profile = false let debug_print s = if debug then prerr_endline (Lazy.force s) @@ -55,8 +86,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 +143,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 +482,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 = @@ -494,31 +554,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst params exp_named_subst' m = - (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params - let ens' = - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) - List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens - in - let rec filter_and_lift = - function - [] -> [] - | uri::tl -> - let r = filter_and_lift tl in - (try - (uri,(List.assq uri ens'))::r - with - Not_found -> r - ) - in - filter_and_lift params - *) - - (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) - (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) - - (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) - (*CSC: codice altamente inefficiente *) + (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) let rec filter_and_lift already_instantiated = function [] -> [] @@ -533,18 +569,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, (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 -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (filter_and_lift [] (List.rev ens)) + let res = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in unwind_aux m t @@ -568,19 +610,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 +659,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 @@ -717,7 +761,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; 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 +782,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 +811,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 @@ -790,6 +836,8 @@ let (===) x y = let are_convertible whd ?(subst=[]) ?(metasenv=[]) = let heuristic = ref true in let rec aux test_equality_only context t1 t2 ugraph = + (*D*)inside 'B'; try let rc = + pp (lazy (CicPp.ppterm t1 ^ " vs " ^ CicPp.ppterm t2)); let rec aux2 test_equality_only t1 t2 ugraph = (* this trivial euristic cuts down the total time of about five times ;-) *) @@ -854,19 +902,16 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); *) aux test_equality_only context t1 term' ugraph with CicUtil.Subst_not_found _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - (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)) -> - (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 *) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when test_equality_only -> + (try true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when not test_equality_only -> + (try true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) + | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> let b',ugraph' = aux true context s1 s2 ugraph in @@ -876,27 +921,36 @@ 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) -> + let b, ugraph = + aux test_equality_only context (List.hd l1) (List.hd l2) ugraph + in + if not b then false, ugraph + else (try List.fold_right2 (fun x y (b,ugraph) -> if b then - aux test_equality_only context x y ugraph + aux true context x y ugraph else - false,ugraph) l1 l2 (true,ugraph) + false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph) with Invalid_argument _ -> false,ugraph ) @@ -959,7 +1013,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); let b'',ugraph''=aux test_equality_only context outtype1 outtype2 ugraph in if b'' then - let b''',ugraph'''= aux test_equality_only context + let b''',ugraph'''= aux true context term1 term2 ugraph'' in List.fold_right2 (fun x y (b,ugraph) -> @@ -1038,12 +1092,50 @@ 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 test_equality_only 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 true ugraph problems + else + res +in + convert_machines test_equality_only 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 + (*D*)in outside true; rc with exc -> outside false; raise exc in aux false (*c t1 t2 ugraph *) ;; @@ -1102,7 +1194,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))