| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
| C.Appl (hd :: tl) -> appl_fun um_aux hd tl
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
| _ -> t'
end
in
- fun s t ->
+ fun subst t ->
(* incr apply_subst_counter; *)
- apply_subst_gen ~appl_fun s t
+match subst with
+ [] -> t
+ | _ -> apply_subst_gen ~appl_fun subst t
;;
let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
profiler.HExtlib.profile (apply_subst s) t
-let rec apply_subst_context subst context =
+let apply_subst_context subst context =
+ match subst with
+ [] -> context
+ | _ ->
(*
incr apply_subst_context_counter;
context_length := !context_length + List.length context;
let t' = apply_subst subst t in
Some (n, Cic.Decl t') :: context
| Some (n, Cic.Def (t, ty)) ->
- let ty' =
- match ty with
- | None -> None
- | Some ty -> Some (apply_subst subst ty)
- in
+ let ty' = apply_subst subst ty in
let t' = apply_subst subst t in
Some (n, Cic.Def (t', ty')) :: context
| None -> None :: context)
incr apply_subst_metasenv_counter;
metasenv_length := !metasenv_length + List.length metasenv;
*)
+match subst with
+ [] -> metasenv
+ | _ ->
List.map
(fun (n, context, ty) ->
(n, apply_subst_context subst context, apply_subst subst ty))
(***** Pretty printing functions ******)
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-
-let ppterm_in_name_context subst term name_context =
- CicPp.pp (apply_subst subst term) name_context
+let ppterm ~metasenv subst term =
+ CicPp.ppterm ~metasenv (apply_subst subst term)
-let ppterm_in_context subst term context =
+let ppterm_in_context ~metasenv subst term context =
let name_context =
List.map (function None -> None | Some (n,_) -> Some n) context
in
- ppterm_in_name_context subst term name_context
+ CicPp.pp ~metasenv (apply_subst subst term) name_context
+
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
-let ppcontext' ?(sep = "\n") subst context =
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+ ppterm_in_context ~metasenv subst term context
+ else
+ !ppterm_in_context_ref ~metasenv subst term context
+
+let ppcontext' ~metasenv ?(sep = "\n") subst context =
let separate s = if s = "" then "" else s ^ sep in
List.fold_right
- (fun context_entry (i,name_context) ->
+ (fun context_entry (i,context) ->
match context_entry with
Some (n,Cic.Decl t) ->
sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
- (ppterm_in_name_context subst t name_context), (Some n)::name_context
+ (ppterm_in_context ~metasenv subst t context),
+ context_entry::context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
- (match ty with
- None -> "_"
- | Some ty -> ppterm_in_name_context subst ty name_context)
- (ppterm_in_name_context subst bo name_context), (Some n)::name_context
+ (ppterm_in_context ~metasenv subst ty context)
+ (ppterm_in_context ~metasenv subst bo context),
+ context_entry::context
| None ->
- sprintf "%s_ :? _" (separate i), None::name_context
+ sprintf "%s_ :? _" (separate i), context_entry::context
) context ("",[])
-let ppsubst_unfolded subst =
+let ppsubst_unfolded ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t,_)) ->
- let context,name_context = ppcontext' ~sep:"; " subst c in
- sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_name_context subst t name_context))
+ (fun (idx, (c, t,ty)) ->
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+ (ppterm_in_context ~metasenv subst t context))
subst)
(*
Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
subst) *)
;;
-let ppsubst subst =
+let ppsubst ~metasenv subst =
String.concat "\n"
(List.map
- (fun (idx, (c, t, _)) ->
- let context,name_context = ppcontext' ~sep:"; " [] c in
- sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_name_context [] t name_context))
+ (fun (idx, (c, t, ty)) ->
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in
+ sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context)
+ (ppterm_in_context ~metasenv [] t context))
subst)
;;
-let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
+let ppcontext ~metasenv ?sep subst context =
+ fst (ppcontext' ~metasenv ?sep subst context)
let ppmetasenv ?(sep = "\n") subst metasenv =
String.concat sep
(List.map
(fun (i, c, t) ->
- let context,name_context = ppcontext' ~sep:"; " subst c in
- sprintf "%s |- ?%d: %s" context i
- (ppterm_in_name_context subst t name_context))
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d: %s" scontext i
+ (ppterm_in_context ~metasenv subst t context))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
- | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+ | C.LetIn (name,so,ty,dest) ->
+ C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
(!more_to_be_restricted, res)
let rec restrict subst to_be_restricted metasenv =
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
let names_of_context_indexes context indexes =
String.concat ", "
(List.map
force_does_not_occur subst to_be_restricted bo
in
let more_to_be_restricted, ty' =
- match ty with
- | None -> more_to_be_restricted, None
- | Some ty ->
- let more_to_be_restricted', ty' =
- force_does_not_occur subst to_be_restricted ty
- in
- more_to_be_restricted @ more_to_be_restricted',
- Some ty'
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ ty'
in
more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
in
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 ~metasenv subst term))
in
(* DEBUG
debug_print (lazy error_msg);
raise (MetaSubstFailure error_msg)))
subst ([], [])
in
- match more_to_be_restricted @ more_to_be_restricted' with
- | [] -> (metasenv, subst)
- | l -> restrict subst l metasenv
+ restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
;;
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
let module S = CicSubstitution in
let l =
- let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+ let (_, canonical_context, _) =
+ try
+ CicUtil.lookup_meta n metasenv
+ with CicUtil.Meta_not_found _ ->
+ raise (MetaSubstFailure (lazy
+ ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+ "declared in the metasenv")))
+ in
List.map2 (fun ct lt ->
match (ct, lt) with
| None, _ -> None
let rec deliftaux k =
let module C = Cic in
function
- C.Rel m ->
+ | C.Rel m as t->
if m <=k then
- C.Rel m
+ t
else
- (try
+ (try
match List.nth context (m-k-1) with
Some (_,C.Def (t,_)) ->
+ (try
+ C.Rel ((position (m-k) l) + k)
+ with
+ NotInTheList ->
(*CSC: Hmmm. This bit of reduction is not in the spirit of *)
(*CSC: first order unification. Does it help or does it harm? *)
(*CSC: ANSWER: it hurts performances since it is possible to *)
(*CSC: have an exponential explosion of the size of the proof.*)
(*CSC: However, without this bit of reduction some "apply" in *)
(*CSC: the library fail (e.g. nat/nth_prime.ma). *)
- deliftaux k (S.lift m t)
+ deliftaux k (S.lift m t))
| Some (_,C.Decl t) ->
C.Rel ((position (m-k) l) + k)
| None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
with
- Failure _ ->
+ Failure _ ->
raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
)
| C.Var (uri,exp_named_subst) ->
if (i = n) then
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 ~metasenv subst t))))
else
begin
(* I do not consider the term associated to ?i in subst since *)
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (deliftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
)))); *)
let msg = (lazy (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
- (ppterm subst t)
+ (ppterm ~metasenv subst t)
(String.concat "; "
(List.map
- (function Some t -> ppterm subst t | None -> "_")
+ (function Some t -> ppterm ~metasenv subst t | None -> "_")
l))))
in
if
let rec liftaux subst metasenv k =
let module C = Cic in
function
- C.Rel m ->
+ C.Rel m as t ->
if m < k then
- C.Rel m, subst, metasenv
+ t, subst, metasenv
else if m < k + n then
raise DeliftingARelWouldCaptureAFreeVariable
else
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) ->
+ | C.LetIn (n,s,ty,t) ->
let s',subst,metasenv = liftaux subst metasenv k s in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
- C.LetIn (n,s',t'),subst,metasenv
+ C.LetIn (n,s',ty',t'),subst,metasenv
| C.Appl l ->
let l',subst,metasenv =
List.fold_right
Format.pp_print_newline ppf ();
Format.pp_print_flush ppf ()
-let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst)
let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
projects / helm.git / blobdiff