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) ->
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 =
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
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
;;
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
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
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) ->
(* 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 *)
(* performs an head beta/cast reduction *)
-let rec head_beta_reduce ?(delta=false) =
- 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 ~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
+ (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 =
projects / helm.git / blobdiff