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
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.Meta (n, l) as orig ->
(* we ignore the subst since restrict will take care of already
restrict metasenv subst n restrictions_for_n
in
(metasenv, subst), NCic.Meta (newmeta, l')
- | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
+ | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
in
aux 0 (metasenv,subst) t
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 "^^
let reloc_irl = mk_restricted_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
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 ->
+ | 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, []
let metasenv, subst, newmeta =
restrict metasenv subst i to_be_r in
(metasenv, subst), NCic.Meta(newmeta,l1))
- | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
+ | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
in
- aux 0 (metasenv,subst) t
-;;
-
-(*
- in
- let res =
- try
- deliftaux 0 t
- with
- NotInTheList ->
+ 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. *)
-(* 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
- )))); *)
- let msg = (lazy (sprintf
- "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
- (ppterm ~metasenv subst t)
- (String.concat "; "
- (List.map
- (function Some t -> ppterm ~metasenv subst t | None -> "_")
- l))))
+ 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
- (function
- Some t -> CicUtil.is_meta_closed (apply_subst subst t)
- | None -> true) l
+ (fun t -> NCicUntrusted.metas_of_term subst context t = [])
+ l
then
raise (Uncertain msg)
else
raise (MetaSubstFailure msg)
- in
- let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
- res, metasenv, subst
;;
-*)
(*
(* delifts a term t of n levels strating from k, that is changes (Rel m)
delift_rels_from subst metasenv 1 n t
*)
+let mk_meta ?name metasenv context 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))
+;;
+
+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 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