let _,_,t,_ = NCicUtils.lookup_subst i subst in
let t = NCicSubstitution.subst_meta lc t in
eat_lambdas ctx t
- with NCicUtils.Subst_not_found _ -> ctx, t)
+ with Not_found -> ctx, t)
| t -> ctx, t
in
let context_body = eat_lambdas [] t in
let time2 = Unix.gettimeofday () in
let time1 =
match !times with time1::tl -> times := tl; time1 | [] -> assert false in
- prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
+ prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
(match exc_opt with
| Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e)
| None -> ());
| _ ->
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy ("On the types: " ^
- ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
- ppterm ~metasenv ~subst ~context lty));
+ ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context ty_t));
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), _ ->
- (* 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))
-
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+ in
+ let metasenv, subst =
+ try
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj swap
+ with UnificationFailure msg | Uncertain msg when not norm2->
+ (* failure: let's try again argument vs argument *)
+ raise (KeepReducing msg)
+ 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)
with
Invalid_argument _ ->
raise (Uncertain (mk_msg metasenv subst context t1 t2))
+ | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+ raise (KeepReducing (mk_msg metasenv subst context t1 t2))
| KeepReducing _ | KeepReducingThis _ -> assert false
in
metasenv, subst
| (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
- C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
+ C.Match (ref2,outtype2,term2,pl2)) ->
let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
| C.Sort C.Prop -> true
| _ -> false
in
- (* if not (Ref.eq ref1 ref2) then
+ if not (Ref.eq ref1 ref2) then
raise (Uncertain (mk_msg metasenv subst context t1 t2))
- else*)
+ else
let metasenv, subst =
unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
let metasenv, subst =
| _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
(*D*) in outside None; rc with exn -> outside (Some exn); raise exn
in
- let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
- try fo_unif test_eq_only metasenv subst nt1 nt2
- with
- UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
- raise (KeepReducing (mk_msg metasenv subst context t1 t2))
- in
let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
- if NCicUntrusted.metas_of_term subst context t1 = [] &&
- NCicUntrusted.metas_of_term subst context t2 = []
- then None
- else begin
(*D*) inside 'H'; try let rc =
pp(lazy ("\nProblema:\n" ^
ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
List.fold_left
(fun (metasenv, subst) (x,y) ->
unify rdb test_eq_only metasenv subst context x y false)
- (metasenv, subst) (List.rev premises)
+ (metasenv, subst) premises
in
pp(lazy("FUNZIONA!"));
Some (metasenv, subst)
in
cand_iter candidates
(*D*) in outside None; rc with exn -> outside (Some exn); raise exn
- end
in
let put_in_whd m1 m2 =
NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
| Uncertain _ as exn -> raise exn
| _ -> assert false
in
- let fo_unif_heads_and_cont_or_unwind_and_hints
- test_eq_only metasenv subst m1 m2 cont hm1 hm2
- =
- let ms, continuation =
- (* calling the continuation inside the outermost try is an option
- and makes unification stronger, but looks not frequent to me
- that heads unify but not the arguments and that an hints can fix
- that *)
- try fo_unif test_eq_only metasenv subst m1 m2, cont
- with
- | UnificationFailure _
- | KeepReducing _ | Uncertain _ as exn ->
- let (t1,norm1),(t2,norm2) = hm1, hm2 in
- match
- try_hints metasenv subst
- (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
- with
- | Some x -> x, fun x -> x
- | None ->
- match exn with
- | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
- | UnificationFailure _ | Uncertain _ as exn -> raise exn
- | _ -> assert false
- in
- continuation ms
- in
let height_of = function
| NCic.Const (Ref.Ref (_,Ref.Def h))
| NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
match t1 with
| C.Const r -> NCicEnvironment.get_relevance r
| _ -> [] *) in
- let unif_from_stack (metasenv, subst) (t1, t2, b) =
+ let unif_from_stack t1 t2 b metasenv subst =
try
let t1 = NCicReduction.from_stack ~delta:max_int t1 in
let t2 = NCicReduction.from_stack ~delta:max_int t2 in
NCicReduction.unwind (k2,e2,t2,List.rev l2),
todo
in
- let check_stack l1 l2 r =
- match t1, t2 with
- | NCic.Meta _, _ | _, NCic.Meta _ ->
- (NCicReduction.unwind (k1,e1,t1,s1)),
- (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) relevance [] in
try
- fo_unif_heads_and_cont_or_unwind_and_hints
- test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
- (fun ms -> List.fold_left unif_from_stack ms todo)
- m1 m2
+ let metasenv,subst =
+ fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
+ List.fold_left
+ (fun (metasenv,subst) (x1,x2,r) ->
+ unif_from_stack x1 x2 r metasenv subst
+ ) (metasenv,subst) todo
with
| 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