nDiscriminationTree.cmx: nDiscriminationTree.cmi
nCicMetaSubst.cmo: nCicMetaSubst.cmi
nCicMetaSubst.cmx: nCicMetaSubst.cmi
-nCicUnification.cmo: nCicUnification.cmi
-nCicUnification.cmx: nCicUnification.cmi
+nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi
+nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi
nCicRefiner.cmo: nCicRefiner.cmi
nCicRefiner.cmx: nCicRefiner.cmi
let rec perforate ctx menv = function
| NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+ let menv, ty = perforate ctx menv ty in
NCicMetaSubst.mk_meta menv ctx ty
| t ->
NCicUntrusted.map_term_fold_a
(fun e ctx -> e::ctx) ctx perforate menv t
in
- let ctx, ity = intros ty in
- let menv, pty = perforate [] [] ty in
+ let ctx, pty = intros ty in
+ let menv, pty = perforate ctx [] pty in
(*
let sty, menv, _ =
NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
in
*)
(* let ctx, ty = intros ty in *)
+ let left, right =
+ match NCicReduction.whd ~delta:max_int ctx pty with
+ | NCic.Appl [eq;t;a;b] -> a, b
+ | _-> assert false
+ in
+
+
+(*
let whd ty =
match ty with
| NCic.Appl [eq;t;a;b] ->
NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
| t -> NCicReduction.whd ~delta:0 ctx t
in
+*)
(*
prerr_endline
(Printf.sprintf "%s == %s"
let metasenv, subst =
try
(* prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
- NCicUnification.unify menv [] ctx ity pty
+ NCicUnification.unify menv [] ctx left right
with
| NCicUnification.Uncertain msg
| NCicUnification.UnificationFailure msg
| NCicMetaSubst.MetaSubstFailure msg ->
prerr_endline (Lazy.force msg);
- prerr_endline
- (Printf.sprintf "RESULT OF UNIF\n%s\n%s == %s\n"
- (NCicPp.ppcontext ~metasenv:menv ~subst:[] ctx)
- (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
- (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx pty));
[], []
| Sys.Break -> [],[]
in
- if (NCicReduction.are_convertible ~subst ctx ity pty)
+ if (NCicReduction.are_convertible ~subst ctx left right)
then
prerr_endline ("OK: " ^ NUri.string_of_uri u)
else
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+ (prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+ prerr_endline
+ (Printf.sprintf
+ ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmenv:\n%s\n" ^^
+ "context:\n%s\n%s == %s\n%s == %s\n")
+ (NCicPp.ppsubst ~metasenv subst)
+ (NCicPp.ppmetasenv ~subst metasenv)
+ (NCicPp.ppcontext ~metasenv ~subst ctx)
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
+ (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
+ (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
(*let inferred_ty =
NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
in*)
definition hole : ∀A:Type.A → A ≝ λA.λx.x.
+axiom foo:
+ ∀P:Type.∀f:P→P→Prop.∀x:P.
+ (λw. ((∀e:P.f x (w x)) = (∀y:P. f x (hole ? y))))
+ (λw:P.hole ? w). (* OK *)
+
+axiom foo:
+ ∀P:Type.∀f:P→P→P.∀x,y:P.
+ (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w). (* OK, restringe Rel1 *)
+
+axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *)
axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *)
-axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *)
+
axiom foo: (λx,y.(λz. z x + z y) (λw:nat.hole ? w)) = λx,y.x. (* OK *)
| _ -> 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)))
;;
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, 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
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
+ prerr_endline ("restricting ?" ^ string_of_int i ^ " to ?" ^
+ string_of_int j ^ " : " ^ NCicPp.ppterm ~metasenv ~context:newctx
+ ~subst newty ^" in a shorter context:\n" ^
+ NCicPp.ppcontext ~metasenv ~subst newctx);
+ 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)
restrict metasenv subst i restrictions
in
(metasenv, subst),
- NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
+ NCic.Meta(newmeta, mk_perforated_irl shift1 len1 restrictions)
| NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
| NCic.Irl _, NCic.Irl _ ->
ms, NCic.Meta (i, (shift1 - shift, lc1))
| 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),
* we could ? := Type_j with j <= i... *)
let subst = (n, (name, ctx, t, ty)) :: subst in
pp ("?"^string_of_int n^" := "^NCicPp.ppterm
- ~metasenv ~subst ~context:ctx t);
+ ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t));
let metasenv =
List.filter (fun (m,_) -> not (n = m)) metasenv
in
projects / helm.git / commitdiff