X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=f4880e426de66ffd74b78808eea763cb4b761a71;hb=87e3427435d3e120cc0292764a93a68b6daddd4a;hp=0bc05674bced1f7ccf563c06532ab5cedb272b3a;hpb=4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 0bc05674b..f4880e426 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -107,6 +107,7 @@ module CallByValueByNameForUnwind = ;; +(* Old Machine module CallByNameStrategy = struct type stack_term = Cic.term @@ -126,6 +127,28 @@ module CallByNameStrategy = let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t end ;; +*) + +module CallByNameStrategy = + 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 + and ens_term = config + + let to_env c = c + let to_ens 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 = 0,[],[],unwind config,[] + let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[] + let compute_to_stack ~reduce ~unwind config = config + end +;; module CallByValueStrategy = struct @@ -641,14 +664,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 = @@ -747,6 +768,7 @@ module R = Reduction module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) module R = Reduction(CallByValueByNameForUnwind);; +(*module R = Reduction(CallByNameStrategy);;*) (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) module U = UriManager;; @@ -766,8 +788,9 @@ let (===) x y = (* t1, t2 must be well-typed *) 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 *) @@ -811,12 +834,36 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = if b2 then true,ugraph1 else false,ugraph else false,ugraph + | C.Meta (n1,l1), _ -> + (try + let _,term,_ = CicUtil.lookup_subst n1 subst in + let term' = CicSubstitution.subst_meta l1 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2); +*) + aux test_equality_only context term' t2 ugraph + with CicUtil.Subst_not_found _ -> false,ugraph) + | _, C.Meta (n2,l2) -> + (try + let _,term,_ = CicUtil.lookup_subst n2 subst in + let term' = CicSubstitution.subst_meta l2 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +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 -> - 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 *) @@ -963,16 +1010,32 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = 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 in + let res = + if !heuristic then + aux2 test_equality_only t1 t2 ugraph + else + false,ugraph + in + if fst res = true then + res + else +begin +(*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) + (* heuristic := false; *) debug t1 [t2] "PREWHD"; +(*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"; +(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*) aux2 test_equality_only t1' t2' ugraph +end in aux false (*c t1 t2 ugraph *) ;; @@ -1057,7 +1120,7 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce = +let rec head_beta_reduce ?(delta=false) = function (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> let he'' = CicSubstitution.subst he' t in @@ -1069,11 +1132,36 @@ let rec head_beta_reduce = Cic.Appl l -> Cic.Appl (l@tl') | _ -> Cic.Appl (he''::tl') in - head_beta_reduce he''' - | Cic.Cast (te,_) -> head_beta_reduce te + 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 -(*Debugging code +(* let are_convertible ?subst ?metasenv context t1 t2 ugraph = let before = Unix.gettimeofday () in let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in