| _ ->
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy ("On the types: " ^
- ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
- ppterm ~metasenv ~subst ~context ty_t));
+ ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context lty));
let metasenv, subst =
unify rdb false metasenv subst context ty_t lty false
in
len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
instantiate rdb test_eq_only metasenv subst context m lc'
(NCicReduction.head_beta_reduce ~subst t1) (not swap)
+ | C.Meta (n,lc), C.Meta (m,lc') when
+ let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+ let _,_,tym = NCicUtils.lookup_meta m metasenv in
+ let tyn = NCicSubstitution.subst_meta lc tyn in
+ let tym = NCicSubstitution.subst_meta lc tym in
+ match tyn,tym with
+ NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+ NCicEnvironment.universe_lt u1 u2
+ | _,_ -> false ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)
| C.Meta (n,lc), t ->
instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) swap
instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) (not swap)
+ (* higher order unification case *)
| NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
- let metasenv, lambda_Mj =
- lambda_intros rdb metasenv subst context (List.length args)
- (NCicTypeChecker.typeof ~metasenv ~subst context meta)
- in
- let metasenv, subst =
- unify rdb test_eq_only metasenv subst context
- (C.Meta (i,l)) lambda_Mj swap
- in
- let metasenv, subst =
- unify rdb test_eq_only metasenv subst context t1 t2 swap
- in
- (try
- let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
- let term = eta_reduce subst term in
- let subst = List.filter (fun (j,_) -> j <> i) subst in
- metasenv, ((i, (name, ctx, term, ty)) :: subst)
- with Not_found -> assert false)
+ (* this easy_case handles "(? ?) =?= (f a)", same number of
+ * args, preferring the instantiation "f" over "\_.f a" for the
+ * metavariable in head position. Since the arguments of the meta
+ * are flexible, delift would ignore them generating a constant
+ * function even in the easy case above *)
+ let easy_case =
+ match t2 with
+ | NCic.Appl (f :: f_args)
+ when
+ List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
+ let mlen = List.length args in
+ let flen = List.length f_args in
+ let min_len = min mlen flen in
+ let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+ let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
+ (try
+ Some (List.fold_left2
+ (fun (m, s) t1 t2 ->
+ unify rdb test_eq_only m s context t1 t2 swap
+ ) (metasenv,subst)
+ ((NCicUntrusted.mk_appl meta mhe)::margs)
+ ((NCicUntrusted.mk_appl f fhe)::fargs))
+ with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
+ None)
+ | _ -> None
+ in
+ (match easy_case with
+ | Some ms -> ms
+ | None ->
+ (* This case handles "(?_f ..ti..) =?= t2", abstracting every
+ * non flexible ti (delift skips local context items that are
+ * flexible) from t2 in two steps:
+ * 1) ?_f := \..xi.. .?
+ * 2) ?_f ..ti.. =?= t2 --unif_machines-->
+ ?_f[..ti..] =?= t2 --instantiate-->
+ delift [..ti..] t2 *)
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj swap
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context t1 t2 swap
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false))
+
| _, NCic.Appl (NCic.Meta (_,_) :: _) ->
unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
ppterm ~metasenv ~subst ~context
(NCicReduction.unwind (k2,e2,t2,s2))));
pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
- let relevance = [] (* TO BE UNDERSTOOD
+ let relevance =
match t1 with
| C.Const r -> NCicEnvironment.get_relevance r
- | _ -> [] *) in
+ | _ -> [] in
let unif_from_stack (metasenv, subst) (t1, t2, b) =
try
let t1 = NCicReduction.from_stack ~delta:max_int t1 in
match l1,l2,r with
| x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
| x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
- | l1, l2, _ ->
+ | l1, l2, _ ->
NCicReduction.unwind (k1,e1,t1,List.rev l1),
NCicReduction.unwind (k2,e2,t2,List.rev l2),
todo
match t1, t2 with
| NCic.Meta _, _ | _, NCic.Meta _ ->
(NCicReduction.unwind (k1,e1,t1,s1)),
- (NCicReduction.unwind (k2,e2,t2,s2)),[]
+ (NCicReduction.unwind (k2,e2,t2,s2)),[]
| _ -> check_stack l1 l2 r []
in
- let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
+ let hh1,hh2,todo =
+ check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
try
fo_unif_heads_and_cont_or_unwind_and_hints
test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
| KeepReducing _ -> assert false
| KeepReducingThis _ ->
assert (not (norm1 && norm2));
- unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+ unif_machines metasenv subst (small_delta_step ~subst m1 m2)
| UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
-> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
| UnificationFailure msg
projects / helm.git / blobdiff