X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=576721be3542c1b67a098c05f0fbbadede1e2f85;hb=38d3574438b4f764ad433915c9733cc73a684b39;hp=046ab908ab1b66a20f2291ddb5837ba1b3ae9900;hpb=eca6985fb1ddae45b0600b5e44fd5c8f404d2842;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 046ab908a..576721be3 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 @@ -357,7 +380,7 @@ module Reduction(RS : Strategy) = let d = try Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1))) - with _ -> None + with Failure _ -> None in (match d with Some t' -> @@ -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 = @@ -682,7 +703,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; try Some (RS.from_stack (List.nth s recindex)) with - _ -> None + Failure _ -> None in (match recparam with Some recparam -> @@ -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,18 +1120,61 @@ 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 - head_beta_reduce he''' - | Cic.Cast (te,_) -> head_beta_reduce te - | 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 = + let before = Unix.gettimeofday () in + let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in + let after = Unix.gettimeofday () in + let diff = after -. before in + if diff > 0.1 then + begin + let nc = List.map (function None -> None | Some (n,_) -> Some n) context in + prerr_endline + ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc); + end; + res +*)