;;
+(* Old Machine
module CallByNameStrategy =
struct
type stack_term = Cic.term
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
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' ->
(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 =
try
Some (RS.from_stack (List.nth s recindex))
with
- _ -> None
+ Failure _ -> None
in
(match recparam with
Some recparam ->
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
*)
module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(CallByNameStrategy);;*)
(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
module U = UriManager;;
(* 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 *)
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 *)
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 *)
;;
(* 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
+*)
projects / helm.git / blobdiff