(* ||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 let newmeta = let maxmeta = ref 0 in fun () -> incr maxmeta; !maxmeta ;; exception NotInTheList;; let position to_skip n (shift, lc) = match lc with | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *) | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList | NCic.Irl _ -> n - shift | NCic.Ctx tl -> let rec aux to_skip k = function | [] -> raise NotInTheList | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl | (NCic.Rel m)::_ when m + shift = n -> k | _::tl -> aux to_skip (k+1) tl in aux to_skip 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 ;; let rec flexible_arg subst = function | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> (try let _,_,t,_ = List.assoc i subst in flexible_arg subst t with Not_found -> true) | _ -> false ;; let flexible subst l = List.exists (flexible_arg subst) l;; let in_scope_tag = "tag:in_scope" ;; let out_scope_tag_prefix = "tag:out_scope:" let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;; let is_out_scope_tag tag = String.length tag > String.length out_scope_tag_prefix && String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix ;; let int_of_out_scope_tag tag = int_of_string (String.sub tag (String.length out_scope_tag_prefix) (String.length tag - (String.length out_scope_tag_prefix))) ;; (* 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 ~unify metasenv subst context n l t = let unify_list in_scope = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> if flexible_arg subst t then None else let lb = List.map (fun t -> t, flexible_arg subst t) l in HExtlib.list_findopt (fun (li,flexible) i -> if flexible || i < in_scope then None else let li = NCicSubstitution.lift (k+shift) li in match unify metasenv subst context li t with | Some (metasenv,subst) -> Some ((metasenv, subst), NCic.Rel (i+1+k)) | None -> None) lb in let rec aux (context,k,in_scope) (metasenv, subst as ms) t = match unify_list in_scope metasenv subst context k t with | Some x -> x | None -> match t with | 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 in_scope (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 (context,k,in_scope) ms (NCicSubstitution.lift n bo)) | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k) with Failure _ -> assert false) (*Unbound variable found in delift*) | NCic.Meta (i,_) when i=n -> 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)))) | NCic.Meta (i,l1) as orig -> (try let tag,c,t,ty = NCicUtils.lookup_subst i subst in let in_scope, clear = match tag with | Some tag when tag = in_scope_tag -> 0, true | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true | _ -> in_scope, false in let ms = if not clear then ms else metasenv, (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst in aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig 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 (context,k,in_scope) 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 e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t in try aux (context,0,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 = let tyof = function Some s -> Some ("typeof_"^s) | None -> None in let rec mk_meta name n metasenv context = function | `WithType ty -> let len = List.length context in let menv_entry = (n, (name, context, ty)) in menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty | `Sort -> let ty = NCic.Implicit (`Typeof n) in mk_meta (tyof name) n metasenv [] (`WithType ty) | `Type -> let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Sort in mk_meta name n metasenv context (`WithType ty) | `Term -> let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Type in mk_meta name n metasenv context (`WithType ty) in mk_meta name (newmeta ()) metasenv context ty ;; let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) as ty -> 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 ~subst 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 ;;