(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) (* $Id$ *) exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t (* (*** Functions to apply a substitution ***) let apply_subst_gen ~appl_fun subst term = let rec um_aux = let module C = Cic in let module S = CicSubstitution in function C.Rel _ as t -> t | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in C.Var (uri, exp_named_subst') | C.Meta (i, l) -> (try let (_, t,_) = lookup_subst i subst in um_aux (S.subst_meta l t) with CicUtil.Subst_not_found _ -> (* unconstrained variable, i.e. free in subst*) let l' = List.map (function None -> None | Some t -> Some (um_aux t)) l in C.Meta (i,l')) | C.Sort _ | C.Implicit _ as t -> t | 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,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) -> let exp_named_subst' = List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in C.Const (uri, exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in C.MutInd (uri,typeno,exp_named_subst') | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> let exp_named_subst' = List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in C.MutConstruct (uri,typeno,consno,exp_named_subst') | C.MutCase (sp,i,outty,t,pl) -> let pl' = List.map um_aux pl in C.MutCase (sp, i, um_aux outty, um_aux t, pl') | C.Fix (i, fl) -> let fl' = List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl in C.Fix (i, fl') | C.CoFix (i, fl) -> let fl' = List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl in C.CoFix (i, fl') in um_aux term ;; let apply_subst = let appl_fun um_aux he tl = let tl' = List.map um_aux tl in let t' = match um_aux he with Cic.Appl l -> Cic.Appl (l@tl') | he' -> Cic.Appl (he'::tl') in begin match he with Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' | _ -> t' end in fun subst t -> (* incr apply_subst_counter; *) match subst with [] -> t | _ -> apply_subst_gen ~appl_fun subst t ;; let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" let apply_subst s t = profiler.HExtlib.profile (apply_subst s) t let apply_subst_context subst context = match subst with [] -> context | _ -> (* incr apply_subst_context_counter; context_length := !context_length + List.length context; *) List.fold_right (fun item context -> match item with | Some (n, Cic.Decl t) -> let t' = apply_subst subst t in Some (n, Cic.Decl t') :: context | Some (n, Cic.Def (t, ty)) -> let ty' = apply_subst subst ty in let t' = apply_subst subst t in Some (n, Cic.Def (t', ty')) :: context | None -> None :: context) context [] let apply_subst_metasenv subst metasenv = (* 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)) (List.filter (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv) let tempi_type_of_aux_subst = ref 0.0;; let tempi_subst = ref 0.0;; let tempi_type_of_aux = ref 0.0;; *) let newmeta = let maxmeta = ref 0 in fun () -> incr maxmeta; !maxmeta ;; exception NotInTheList;; let position n (shift, lc) = match lc with | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList | NCic.Irl _ -> n - shift | NCic.Ctx tl -> let rec aux k = function | [] -> raise NotInTheList | (NCic.Rel m)::_ when m + shift = n -> k | _::tl -> aux (k+1) tl in aux 1 tl ;; let pack_lc orig = let rec are_contiguous k = function | [] -> true | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl | _ -> false in match orig with | _, NCic.Ctx [] -> 0, NCic.Irl 0 | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl -> shift+k-1, NCic.Irl (List.length l) | _ -> orig ;; let mk_perforated_irl shift len restrictions = let rec aux n = if n = 0 then [] else if List.mem (n+shift) restrictions then aux (n-1) else (NCic.Rel n) :: aux (n-1) in pack_lc (shift, NCic.Ctx (List.rev (aux len))) ;; exception Occur;; let rec force_does_not_occur metasenv subst restrictions t = let rec aux k ms = function | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur | NCic.Rel r as orig -> let amount = List.length (List.filter (fun x -> x < r - k) restrictions) in if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig | NCic.Meta (n, (shift,lc as l)) as orig -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) let (metasenv,subst as ms), restrictions_for_n, l' = let l = NCicUtils.expand_local_context lc in let ms, _, restrictions_for_n, l = List.fold_right (fun t (ms, i, restrictions_for_n, l) -> try let ms, t = aux (k-shift) ms t in ms, i-1, restrictions_for_n, t::l with Occur -> ms, i-1, i::restrictions_for_n, l) l (ms, List.length l, [], []) in ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) in if restrictions_for_n = [] then ms, if l = l' then orig else NCic.Meta (n, l') else let metasenv, subst, newmeta = restrict metasenv subst n restrictions_for_n in (metasenv, subst), NCic.Meta (newmeta, l') | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in aux 0 (metasenv,subst) t and force_does_not_occur_in_context metasenv subst restrictions = function | name, NCic.Decl t as orig -> let (metasenv, subst), t' = force_does_not_occur metasenv subst restrictions t in metasenv, subst, (if t == t' then orig else (name,NCic.Decl t')) | name, NCic.Def (bo, ty) as orig -> let (metasenv, subst), bo' = force_does_not_occur metasenv subst restrictions bo in let (metasenv, subst), ty' = force_does_not_occur metasenv subst restrictions ty in metasenv, subst, (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty'))) and erase_in_context metasenv subst pos restrictions = function | [] -> metasenv, subst, restrictions, [] | hd::tl as orig -> let metasenv, subst, restricted, tl' = erase_in_context metasenv subst (pos+1) restrictions tl in if List.mem pos restricted then metasenv, subst, restricted, tl' else try let metasenv, subst, hd' = let delifted_restricted = List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in force_does_not_occur_in_context metasenv subst delifted_restricted hd in metasenv, subst, restricted, (if hd' == hd && tl' == tl then orig else (hd' :: tl')) with Occur -> metasenv, subst, (pos :: restricted), tl' and restrict metasenv subst i restrictions = assert (restrictions <> []); try let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in try let metasenv, subst, restrictions, newctx = erase_in_context metasenv subst 1 restrictions ctx in let (metasenv, subst), newty = force_does_not_occur metasenv subst restrictions ty in let (metasenv, subst), newbo = force_does_not_occur metasenv subst restrictions bo in let j = newmeta () in let subst_entry_j = j, (name, newctx, newbo, newty) in let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in let new_subst = subst_entry_j :: List.map (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst in (* prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ string_of_int j ^ "\n" ^ NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^ NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^ NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^ NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo ); *) metasenv, new_subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.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") i (String.concat ", " (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo)))) with NCicUtils.Subst_not_found _ -> try let name, ctx, ty = NCicUtils.lookup_meta i metasenv in try let metasenv, subst, restrictions, newctx = erase_in_context metasenv subst 1 restrictions ctx in let (metasenv, subst), newty = force_does_not_occur metasenv subst restrictions ty in let j = newmeta () in let metasenv_entry = j, (name, newctx, newty) in let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in List.map (fun (n,_) as orig -> if i = n then metasenv_entry else orig) metasenv, subst_entry :: subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d "^^ "over the hypotheses %s since metavariable's type depends "^^ "on at least one of them") i (String.concat ", " (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions))))) with | NCicUtils.Meta_not_found _ -> assert false ;; (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), otherwise the occur check does not make sense in case of unification of ?n with ?n *) let delift metasenv subst context n l t = let rec aux k (metasenv, subst as ms) = function | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> (try match List.nth context (n-k-1) with | _,NCic.Def (bo,_) -> (try ms, NCic.Rel ((position (n-k) l) + k) with NotInTheList -> (* CSC: This bit of reduction hurts performances since it is * possible to have an exponential explosion of the size of the * proof. required for nat/nth_prime.ma *) aux k ms (NCicSubstitution.lift n bo)) | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k) with Failure _ -> assert false) (*Unbound variable found in delift*) | NCic.Meta (_,(_,(NCic.Irl 0| NCic.Ctx []))) as orig -> ms, orig | NCic.Meta (i,l1) as orig -> (try let _,_,t,_ = NCicUtils.lookup_subst i subst in aux k ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then raise (MetaSubstFailure (lazy (Printf.sprintf ( "Cannot unify the metavariable ?%d with a term that has "^^ "as subterm %s in which the same metavariable "^^ "occurs (occur check)") i (NCicPp.ppterm ~context ~metasenv ~subst t)))) else let shift1,lc1 = l1 in let shift,lc = l in let shift = shift + k in match lc, lc1 with | NCic.Irl len, NCic.Irl len1 when shift1 + len1 < shift || shift1 > shift + len -> let restrictions = HExtlib.list_seq 1 (len1 + 1) in let metasenv, subst, newmeta = restrict metasenv subst i restrictions in (metasenv, subst), NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1)))) | NCic.Irl len, NCic.Irl len1 -> let low_restrictions, new_shift = if k <= shift1 && shift1 < shift then HExtlib.list_seq 1 (shift - shift1 + 1), k else if shift1 < k (* <= shift *) then let save_below = k - shift1 in HExtlib.list_seq (save_below + 1) (shift - shift1 + 1), shift1 else [], shift1 - shift + k in let high_restrictions = let last = shift + len in let last1 = shift1 + len1 in if last1 > last then let high_gap = last1 - last in HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) else [] in let restrictions = low_restrictions @ high_restrictions in if restrictions = [] then if shift = k then ms, orig else ms, NCic.Meta (i, (new_shift, lc1)) else let metasenv, subst, newmeta = restrict metasenv subst i restrictions in (* {{{ prerr_endline ("RESTRICTIONS FOR: " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta (i,l1))^" that was part of a term unified with " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta (n,l)) ^ " ====> " ^ String.concat "," (List.map string_of_int restrictions) ^ "\nMENV:\n" ^ NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^ NCicPp.ppsubst subst ~metasenv); }}} *) let newlc_len = len1 - List.length restrictions in let meta = NCic.Meta(newmeta,(new_shift, NCic.Irl newlc_len)) in assert ( let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in List.length cctx = newlc_len); (metasenv, subst), meta | _ -> let lc1 = NCicUtils.expand_local_context lc1 in let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in let rec deliftl tbr j ms = function | [] -> ms, tbr, [] | t::tl -> let ms, tbr, tl = deliftl tbr (j+1) ms tl in try let ms, t = aux k ms t in ms, tbr, t::tl with | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl in let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in (* prerr_endline ("TO BE RESTRICTED: " ^ (String.concat "," (List.map string_of_int to_be_r))); *) let l1 = pack_lc (0, NCic.Ctx lc1') in (* prerr_endline ("newmeta:" ^ NCicPp.ppterm ~metasenv ~subst ~context (NCic.Meta (999,l1))); *) if to_be_r = [] then (metasenv, subst), (if lc1' = lc1 then orig else NCic.Meta (i,l1)) else let metasenv, subst, newmeta = restrict metasenv subst i to_be_r in (metasenv, subst), NCic.Meta(newmeta,l1)) | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in try aux 0 (metasenv,subst) t with NotInTheList -> (* This is the case where we fail even first order unification. *) (* 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. *) let msg = (lazy (Printf.sprintf ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^ "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift shift) (NCicUtils.expand_local_context lc)))))) in let shift, lc = l in let lc = NCicUtils.expand_local_context lc in let l = List.map (NCicSubstitution.lift shift) lc in if List.exists (fun t -> NCicUntrusted.metas_of_term subst context t = []) l then raise (Uncertain msg) else raise (MetaSubstFailure msg) ;; let mk_meta ?name metasenv context ty = match ty with | `Typeless -> let n = newmeta () in let ty = NCic.Implicit (`Typeof n) in let menv_entry = (n, (name, context, ty)) in menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty | `Type | `Term -> let context_for_ty = if ty = `Type then [] else context in let n = newmeta () in let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in let m = newmeta () in let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in let menv_entry = (m, (name, context, ty)) in menv_entry :: ty_menv_entry :: metasenv, NCic.Meta (m, (0,NCic.Irl (List.length context))), ty | `WithType ty -> let n = newmeta () in let len = List.length context in let menv_entry = (n, (name, context, ty)) in menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty ;; let saturate ?(delta=0) metasenv context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) -> let metasenv1, arg,_ = mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) in if pno + 1 = goal_arity then ty, metasenv, [], goal_arity+1 else t, metasenv1, arg::args, pno+1 | ty -> match NCicReduction.whd context ty ~delta with | NCic.Prod _ as ty -> aux metasenv ty | ty -> ty, metasenv, [], 0 in let res, newmetasenv, arguments, _ = aux metasenv ty in res, newmetasenv, arguments ;;