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))
- )*)
+ ))*)
;;
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) ->
(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
(* 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
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
(* delifts a term t of n levels strating from k, that is changes (Rel m)
* to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
*)
-let delift_rels_from k n =
- let rec liftaux k =
+let delift_rels_from subst metasenv k n =
+ let rec liftaux subst metasenv k =
let module C = Cic in
function
C.Rel m ->
if m < k then
- C.Rel m
+ C.Rel m, subst, metasenv
else if m < k + n then
raise DeliftingARelWouldCaptureAFreeVariable
else
- C.Rel (m - n)
+ C.Rel (m - n), subst, metasenv
| C.Var (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
in
- C.Var (uri,exp_named_subst')
+ C.Var (uri,exp_named_subst'),subst,metasenv
| C.Meta (i,l) ->
- let l' =
- List.map
- (function
- None -> None
- | Some t -> Some (liftaux k t)
- ) l
- in
- C.Meta(i,l')
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
- | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
- | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
- | C.Appl l -> C.Appl (List.map (liftaux k) l)
+ (try
+ let (_, t,_) = lookup_subst i subst in
+ liftaux subst metasenv k (CicSubstitution.subst_meta l t)
+ with CicUtil.Subst_not_found _ ->
+ let l',to_be_restricted,subst,metasenv =
+ let rec aux con l subst metasenv =
+ match l with
+ [] -> [],[],subst,metasenv
+ | he::tl ->
+ let tl',to_be_restricted,subst,metasenv =
+ aux (con + 1) tl subst metasenv in
+ let he',more_to_be_restricted,subst,metasenv =
+ match he with
+ None -> None,[],subst,metasenv
+ | Some t ->
+ try
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ Some t',[],subst,metasenv
+ with
+ DeliftingARelWouldCaptureAFreeVariable ->
+ None,[i,con],subst,metasenv
+ in
+ he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
+ in
+ aux 1 l subst metasenv in
+ let metasenv,subst = restrict subst to_be_restricted metasenv in
+ C.Meta(i,l'),subst,metasenv)
+ | C.Sort _ as t -> t,subst,metasenv
+ | C.Implicit _ as t -> t,subst,metasenv
+ | C.Cast (te,ty) ->
+ let te',subst,metasenv = liftaux subst metasenv k te in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ C.Cast (te',ty'),subst,metasenv
+ | C.Prod (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Prod (n,s',t'),subst,metasenv
+ | C.Lambda (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Lambda (n,s',t'),subst,metasenv
+ | C.LetIn (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.LetIn (n,s',t'),subst,metasenv
+ | C.Appl l ->
+ let l',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) l ([],subst,metasenv) in
+ C.Appl l',subst,metasenv
| C.Const (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
in
- C.Const (uri,exp_named_subst')
+ C.Const (uri,exp_named_subst'),subst,metasenv
| C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
in
- C.MutInd (uri,tyno,exp_named_subst')
+ C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
| C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
in
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
| C.MutCase (sp,i,outty,t,pl) ->
- C.MutCase (sp, i, liftaux k outty, liftaux k t,
- List.map (liftaux k) pl)
+ let outty',subst,metasenv = liftaux subst metasenv k outty in
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ let pl',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) pl ([],subst,metasenv)
+ in
+ C.MutCase (sp,i,outty',t',pl'),subst,metasenv
| C.Fix (i, fl) ->
let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
- fl
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, i, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,i,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
in
- C.Fix (i, liftedfl)
+ C.Fix (i, liftedfl),subst,metasenv
| C.CoFix (i, fl) ->
let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
- fl
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
in
- C.CoFix (i, liftedfl)
+ C.CoFix (i, liftedfl),subst,metasenv
in
- liftaux k
+ liftaux subst metasenv k
-let delift_rels n t =
- delift_rels_from 1 n t
+let delift_rels subst metasenv n t =
+ delift_rels_from subst metasenv 1 n t
(**** END OF DELIFT ****)
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)
projects / helm.git / blobdiff