let position n (shift, lc) =
match lc with
| NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
- | NCic.Irl len -> n - shift
+ | NCic.Irl _ -> n - shift
| NCic.Ctx tl ->
let rec aux k = function
| [] -> raise NotInTheList
| _ -> orig
;;
+
let mk_restricted_irl shift len restrictions =
+ let rec aux n =
+ if n = 0 then 0 else
+ if List.mem (n+shift) restrictions then aux (n-1)
+ else 1+aux (n-1)
+ in
+ pack_lc (shift, NCic.Irl (aux len))
+;;
+
+
+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)
+ 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 (metasenv, subst as ms) = function
+ 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, l) as orig ->
(* we ignore the subst since restrict will take care of already
* instantiated/restricted metavariabels *)
force_does_not_occur metasenv subst restrictions bo in
let j = newmeta () in
let subst_entry_j = j, (name, newctx, newty, newbo) in
- let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions 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
metasenv,
subst_entry_j :: List.map
- (fun (n,x) as orig -> if i = n then subst_entry_i else orig) subst,
+ (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst,
j
with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
("Cannot restrict the context of the metavariable ?%d over "^^
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_restricted_irl 0 (List.length ctx) restrictions 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,x) as orig -> if i = n then metasenv_entry else orig)
+ (fun (n,_) as orig -> if i = n then metasenv_entry else orig)
metasenv,
subst_entry :: subst, j
with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
let shift,lc = l in
match lc, lc1 with
| NCic.Irl len, NCic.Irl len1
- when shift1 < shift || len1 + shift1 > len + shift ->
+ when shift1 - k < shift || len1 + shift1 - k > len + shift ->
+ let low_gap = max 0 (shift - (shift1 - k)) in
+ let high_gap = max 0 (shift1 + len1 - k - (shift + len)) in
let restrictions =
- HExtlib.list_seq 1 (shift - shift1) @
- HExtlib.list_seq (shift+len+1) (shift1+len1)
+ HExtlib.list_seq 1 (low_gap+1) @
+ HExtlib.list_seq (len1-high_gap) len1
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));
+*)
let metasenv, subst, newmeta =
restrict metasenv subst i restrictions
in
- (metasenv, subst),
- NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
- | NCic.Irl len, NCic.Irl len1 when shift = 0 -> ms, orig
- | NCic.Irl len, NCic.Irl len1 ->
+ let meta =
+ NCic.Meta(newmeta,(k,NCic.Irl (len - low_gap - high_gap)))
+ in
+ (metasenv, subst), meta
+
+ | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
+ | NCic.Irl _, NCic.Irl _ ->
ms, NCic.Meta (i, (shift1 - shift, lc1))
| _ ->
- let to_be_restricted = ref [] in
let lc1 = NCicUtils.expand_local_context lc1 in
let rec deliftl tbr j ms = function
| [] -> ms, tbr, []
| 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 (shift, NCic.Ctx lc1') in
if to_be_r = [] then
(metasenv, subst),
delift_rels_from subst metasenv 1 n t
*)
+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
+;;
projects / helm.git / blobdiff