metasenv_length := 0;
context_length := 0
let print_counters () =
- debug_print (Printf.sprintf
+ debug_print (lazy (Printf.sprintf
"apply_subst: %d
apply_subst_context: %d
apply_subst_metasenv: %d
((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
!context_length
((float !context_length) /. (float !apply_subst_context_counter))
- )*)
+ ))*)
-exception MetaSubstFailure of string
-exception Uncertain of string
-exception AssertFailure of string
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
exception DeliftingARelWouldCaptureAFreeVariable;;
let debug_print = fun _ -> ()
;;
let apply_subst =
-(* CSC: old code that never performs beta reduction
- let appl_fun um_aux he tl =
- let tl' = List.map um_aux tl in
- begin
- match um_aux he with
- Cic.Appl l -> Cic.Appl (l@tl')
- | he' -> Cic.Appl (he'::tl')
- end
- in
- apply_subst_gen ~appl_fun
-*)
let appl_fun um_aux he tl =
let tl' = List.map um_aux tl in
let t' =
in
begin
match he with
- Cic.Meta (m,_) ->
- let rec beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- beta_reduce (Cic.Appl(he''::tl'))
- | t -> t
- in
- beta_reduce t'
+ Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
| _ -> t'
end
in
let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
-let ppmetasenv ?(sep = "\n") metasenv subst =
+let ppmetasenv ?(sep = "\n") subst metasenv =
String.concat sep
(List.map
(fun (i, c, t) ->
(more @ more_to_be_restricted @ more_to_be_restricted',
metasenv')
with Occur ->
- raise (MetaSubstFailure (sprintf
+ raise (MetaSubstFailure (lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
- n (names_of_context_indexes context to_be_restricted))))
- metasenv ([], [])
+ n (names_of_context_indexes context to_be_restricted)))))
+ metasenv ([], [])
in
let (more_to_be_restricted', subst) = (* restrict subst *)
List.fold_right
@ more_to_be_restricted'@more_to_be_restricted'' in
(more, subst')
with Occur ->
- let error_msg = sprintf
+ let error_msg = lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
- (ppterm subst term)
+ (ppterm subst term))
in
(* DEBUG
- debug_print error_msg;
- debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
- debug_print ("subst = \n" ^ (ppsubst subst));
- debug_print ("context = \n" ^ (ppcontext subst context)); *)
+ debug_print (lazy error_msg);
+ debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
+ debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
+ debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
raise (MetaSubstFailure error_msg)))
subst ([], [])
in
otherwise the occur check does not make sense *)
(*
- debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
- al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))));
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
*)
let module S = CicSubstitution in
deliftaux k (S.lift m t)
| Some (_,C.Decl t) ->
C.Rel ((position (m-k) l) + k)
- | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+ | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
with
Failure _ ->
- raise (MetaSubstFailure "Unbound variable found in deliftaux")
+ raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
with CicUtil.Subst_not_found _ ->
(* see the top level invariant *)
if (i = n) then
- raise (MetaSubstFailure (sprintf
+ raise (MetaSubstFailure (lazy (sprintf
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
- i (ppterm subst t)))
+ i (ppterm subst t))))
else
begin
(* I do not consider the term associated to ?i in subst since *)
(* The reason is that our delift function is weaker than first *)
(* order (in the sense of alpha-conversion). See comment above *)
(* related to the delift function. *)
-(* debug_print "First Order UnificationFailure during delift" ;
-debug_print(sprintf
+(* debug_print (lazy "First Order UnificationFailure during delift") ;
+debug_print(lazy (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
(String.concat "; "
(List.map
(function Some t -> ppterm subst t | None -> "_") l
- ))); *)
- raise (Uncertain (sprintf
+ )))); *)
+ raise (Uncertain (lazy (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
(String.concat "; "
(List.map
(function Some t -> ppterm subst t | None -> "_")
- l))))
+ l)))))
in
let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
res, metasenv, subst
let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
-let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)