From 1410ea677188e9e11d748c69e208d1e90b0a324e Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 23 Feb 2012 09:48:07 +0000 Subject: [PATCH] refiner porting from matita 1. --- matitaB/components/ng_refiner/nCicRefiner.ml | 152 ++-- .../components/ng_refiner/nCicUnification.ml | 812 +++++++++--------- .../components/ng_refiner/nCicUnification.mli | 4 + 3 files changed, 514 insertions(+), 454 deletions(-) diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml index 8deb72797..7cdeb875e 100644 --- a/matitaB/components/ng_refiner/nCicRefiner.ml +++ b/matitaB/components/ng_refiner/nCicRefiner.ml @@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t = ~unify:(fun m s c t1 t2 -> try Some (NCicUnification.unify status m s c t1 t2) with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) - metasenv subst context 0 (0,NCic.Irl 0) typ + metasenv subst context ~-1 (0,NCic.Irl 0) typ with NCicMetaSubst.MetaSubstFailure _ | NCicMetaSubst.Uncertain _ -> @@ -139,6 +139,32 @@ let check_allowed_sort_elimination status localise r orig = aux ;; +(* CSC: temporary thing, waiting for better times *) +let mk_fresh_name context name = +try + let rex = Str.regexp "[0-9']*$" in + let rex2 = Str.regexp "'*$" in + let basename = Str.global_replace rex "" in + let suffix name = + ignore (Str.search_forward rex name 0); + let n = Str.matched_string name in + let n = Str.global_replace rex2 "" n in + if n = "" then 0 else int_of_string n +in + let name' = basename name in + let name' = if name' = "_" then "H" else name' in + let last = + List.fold_left + (fun last (name,_) -> + if basename name = name' then + max last (suffix name) + else + last + ) (-1) context + in + name' ^ (if last = -1 then "" else string_of_int (last + 1)) +with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false + let rec typeof (status:#NCicCoercion.status) ?(localise=fun _ -> Stdpp.dummy_loc) metasenv subst context term expty @@ -166,7 +192,7 @@ let rec typeof (status:#NCicCoercion.status) | NCicUnification.Uncertain _ | NCicUnification.UnificationFailure _ as exc -> try_coercions status ~localise - metasenv subst context t orig infty expty true exc) + metasenv subst context t orig infty (`Type expty) exc) | None -> metasenv, subst, t, infty (*D*)in outside true; rc with exc -> outside false; raise exc in @@ -464,14 +490,17 @@ and check_type status ~localise metasenv subst context (ty as orig_ty) = and try_coercions status ~localise - metasenv subst context t orig_t infty expty perform_unification exc + metasenv subst context t orig_t infty expty exc = let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in try - pp (lazy "WWW: trying coercions -- preliminary unification"); - let metasenv, subst = - NCicUnification.unify status metasenv subst context infty expty - in metasenv, subst, t, expty + (match expty with + `Type expty -> + pp (lazy "WWW: trying coercions -- preliminary unification"); + let metasenv, subst = + NCicUnification.unify status metasenv subst context infty expty + in metasenv, subst, t, expty + | _ -> raise (Failure "Special case Prod or Sort")) with | exn -> (* we try with a coercion *) @@ -482,7 +511,7 @@ and try_coercions status "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (status#ppterm ~metasenv ~subst ~context t) (status#ppterm ~metasenv ~subst ~context infty) - (status#ppterm ~metasenv ~subst ~context expty))) exc) + expty)) exc) | (_,metasenv, newterm, newtype, meta)::tl -> try pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm)); @@ -494,21 +523,28 @@ and try_coercions status status#ppterm ~metasenv ~subst ~context t ^ " === " ^ status#ppterm ~metasenv ~subst ~context meta ^ "\n")); let metasenv, subst = - NCicUnification.unify status metasenv subst context t meta - in - pp (lazy ( "UNIFICATION in CTX:\n"^ - status#ppcontext ~metasenv ~subst context - ^ "\nMENV: " ^ - status#ppmetasenv metasenv ~subst - ^ "\nOF: " ^ - status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^ - status#ppterm ~metasenv ~subst ~context expty ^ "\n")); - let metasenv, subst = - if perform_unification then - NCicUnification.unify status metasenv subst context newtype expty - else metasenv, subst - in - metasenv, subst, newterm, newtype + NCicUnification.unify status metasenv subst context t meta in + match expty with + `Type expty -> + pp (lazy ( "UNIFICATION in CTX:\n"^ + status#ppcontext ~metasenv ~subst context + ^ "\nMENV: " ^ + status#ppmetasenv metasenv ~subst + ^ "\nOF: " ^ + status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^ + status#ppterm ~metasenv ~subst ~context expty ^ "\n")); + let metasenv,subst = + NCicUnification.unify status metasenv subst context newtype expty + in + metasenv, subst, newterm, newtype + | `Sort -> + (match NCicReduction.whd status ~subst context newtype with + NCic.Sort _ -> metasenv,subst,newterm,newtype + | _ -> first exc tl) + | `Prod -> + (match NCicReduction.whd status ~subst context newtype with + NCic.Prod _ -> metasenv,subst,newterm,newtype + | _ -> first exc tl) with | NCicUnification.UnificationFailure _ -> first exc tl | NCicUnification.Uncertain _ as exc -> first exc tl @@ -517,7 +553,8 @@ and try_coercions status try pp (lazy "WWW: trying coercions -- inner check"); match infty, expty, t with - | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> + (* `Sort|`Prod + Match not implemented *) + | _,`Type expty, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> (*{{{*) pp (lazy "CASE"); (* {{{ helper functions *) let get_cl_and_left_p refit outty = @@ -572,6 +609,7 @@ and try_coercions status cl, left_p, leftno, rno | _ -> raise exn in + (*{{{*) pp (lazy "CASE"); let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = match t,n with | _,0 -> @@ -598,8 +636,8 @@ and try_coercions status in (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) - let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in - let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in + let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in + let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in let add_params metasenv subst context cty outty mty m i = @@ -777,7 +815,7 @@ and try_coercions status ~context ~metasenv ~subst pbo)); let metasenv, subst, pbo, _ = try_coercions status ~localise menv s context pbo - orig_t (*??*) infty_pbo expty_pbo perform_unification exc + orig_t (*??*) infty_pbo (`Type expty_pbo) exc in pp (lazy ("CASE: pbo2: " ^ status#ppterm @@ -802,24 +840,29 @@ and try_coercions status let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) in metasenv, subst, t, expty (*}}}*) - | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> - let rec mk_fresh_name ctx firstch n = - let candidate = (String.make 1 firstch) ^ (string_of_int n) in - if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate - else mk_fresh_name ctx firstch (n+1) + | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> + pp (lazy "LETIN"); + let name' = mk_fresh_name context name in + let context_bo = (name', NCic.Def (t,ty)) :: context in + let metasenv, subst, bo2, _ = + try_coercions status ~localise metasenv subst context_bo + bo orig_t (NCicSubstitution.lift status 1 infty) + (`Type (NCicSubstitution.lift status 1 expty)) exc in + let coerced = NCic.LetIn (name',ty,t,bo2) in + pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); + metasenv, subst, coerced, expty + | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ -> (*{{{*) pp (lazy "LAM"); pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t)); - let name_con = mk_fresh_name context 'c' 0 - (*FreshNamesGenerator.mk_fresh_name - ~subst metasenv context ~typ:src2 Cic.Anonymous*) - in + let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in + let name_con = mk_fresh_name context namename in let context_src2 = ((name_con, NCic.Decl src2) :: context) in (* contravariant part: the argument of f:src->ty *) let metasenv, subst, rel1, _ = try_coercions status ~localise metasenv subst context_src2 (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) - (NCicSubstitution.lift status 1 src) perform_unification exc + (`Type (NCicSubstitution.lift status 1 src)) exc in (* covariant part: the result of f(c x); x:src2; (c x):src *) let name_t, bo = @@ -831,13 +874,23 @@ and try_coercions status let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in let metasenv, subst, bo, _ = try_coercions status ~localise metasenv subst context_src2 - bo orig_t ty ty2 perform_unification exc + bo orig_t ty (`Type ty2) exc in let coerced = NCic.Lambda (name_t,src2, bo) in pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); metasenv, subst, coerced, expty (*}}}*) | _ -> raise exc with exc2 -> + let expty = + match expty with + `Type expty -> expty + | `Sort -> + NCic.Sort (NCic.Type + (match NCicEnvironment.get_universes () with + | x::_ -> x + | _ -> assert false)) + | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type) + in pp(lazy("try_coercion " ^ status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^ status#ppterm ~metasenv ~subst ~context expty)); @@ -852,15 +905,19 @@ and force_to_sort status metasenv subst context t orig_t localise ty = metasenv, subst, t, ty with Failure _ -> + let msg = + (lazy (localise orig_t, + "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^ + " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in let ty = NCicReduction.whd status ~subst context ty in + let exn = + if NCicUnification.could_reduce status ~subst context ty then + Uncertain msg + else + RefineFailure msg + in try_coercions status ~localise metasenv subst context - t orig_t ty (NCic.Sort (NCic.Type - (match NCicEnvironment.get_universes status with - | x::_ -> x - | _ -> assert false))) false - (Uncertain (lazy (localise orig_t, - "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^ - " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty))) + t orig_t ty `Sort exn and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) @@ -987,8 +1044,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig let metasenv, subst, newhead, newheadty = try_coercions status ~localise metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty - (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) - false + `Prod (RefineFailure (lazy (localise orig_he, Printf.sprintf ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (status#ppterm ~metasenv ~subst ~context he) @@ -1204,7 +1260,7 @@ let typeof_obj NCicReduction.whd status ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (NCicEnvironment.universe_leq status u1 u2) then + if not (NCicEnvironment.universe_leq u1 u2) then raise (RefineFailure (lazy(localise te, "The type " ^ diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml index cd5c89dd3..d45b14fc9 100644 --- a/matitaB/components/ng_refiner/nCicUnification.ml +++ b/matitaB/components/ng_refiner/nCicUnification.ml @@ -99,6 +99,8 @@ let outside exc_opt = match !times with time1::tl -> times := tl; time1 | [] -> assert false in prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1)); (match exc_opt with + | Some (UnificationFailure msg) -> prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg) + | Some (Uncertain msg) -> prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg) | Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e) | None -> ()); try @@ -132,13 +134,15 @@ let rec mk_irl stop base = ;; (* the argument must be a term in whd *) -let rec could_reduce = +let rec could_reduce status ~subst context = function | C.Meta _ -> true | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args) - when List.length args > recno -> could_reduce (List.nth args recno) - | C.Match (_,_,arg,_) -> could_reduce arg - | C.Appl (he::_) -> could_reduce he + when List.length args > recno -> + let t = NCicReduction.whd status ~subst context (List.nth args recno) in + could_reduce status subst context t + | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg + | C.Appl (he::_) -> could_reduce status ~subst context he | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false ;; @@ -273,6 +277,11 @@ let tipify status exc metasenv subst context t ty = metasenv,subst,t ;; +let put_in_whd status subst context m1 m2 = + NCicReduction.reduce_machine status ~delta:max_int ~subst context m1, + NCicReduction.reduce_machine status ~delta:max_int ~subst context m2 +;; + let rec instantiate status test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t)); @@ -288,14 +297,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap = ppterm status ~metasenv ~subst ~context t)); let (metasenv, subst), t = try - NCicMetaSubst.delift status - ~unify:(fun m s c t1 t2 -> - let ind = !indent in - let res = - try Some (unify status test_eq_only m s c t1 t2 false) - with UnificationFailure _ | Uncertain _ -> None - in - indent := ind; res) + NCicMetaSubst.delift status ~unify:(unify_for_delift status) metasenv subst context n lc t with NCicMetaSubst.Uncertain msg -> pp (lazy ("delift is uncertain: " ^ Lazy.force msg)); @@ -362,13 +364,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap = NCic.Implicit (`Typeof _) -> let (metasenv, subst), ty_t = try - NCicMetaSubst.delift status - ~unify:(fun m s c t1 t2 -> - let ind = !indent in - let res = try Some (unify status test_eq_only m s c t1 t2 false ) - with UnificationFailure _ | Uncertain _ -> None - in - indent := ind; res) + NCicMetaSubst.delift status ~unify:(unify_for_delift status) metasenv subst context n lc ty_t with NCicMetaSubst.Uncertain msg -> pp (lazy ("delift is uncertain: " ^ Lazy.force msg)); @@ -391,22 +387,49 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap = subst) (*D*) in outside None; rc with exn -> outside (Some exn); raise exn -and unify status test_eq_only metasenv subst context t1 t2 swap = - (*D*) inside 'U'; try let rc = - let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) = - (*D*) inside 'F'; try let rc = - pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^ - (if swap then " ==>?== " - else " ==??== " - else " == raise exn + | KeepReducing _ | Uncertain _ as exn -> + let (t1,norm1 as tm1),(t2,norm2 as tm2) = + put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[]) + in + match + try_hints status swap test_eq_only metasenv subst context + (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2) + with + | Some x -> x + | None -> + match exn with + | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2)) + | Uncertain _ as exn -> raise exn + | _ -> assert false + +and unify_for_delift status metasenv subst context t1 t2 = + let ind = !indent in + let res = + try Some + (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst + context (false,t1) (false,t2)) + with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None + in + indent := ind; res + +and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) = + (*D*) inside 'F'; try let rc = + pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^ + (if swap then " ==>?== " + else " ==??== " + else " == - prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant"; - assert false - | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> - let a, b = if swap then b,a else a,b in - if NCicEnvironment.universe_leq status a b then metasenv, subst - else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) - | (C.Sort (C.Type a), C.Sort (C.Type b)) -> - if NCicEnvironment.universe_eq a b then metasenv, subst - else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) - | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> - if (not test_eq_only) then metasenv, subst - else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) - | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> - if (not test_eq_only) then metasenv, subst - else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) - - | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) - | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let metasenv, subst = unify status true metasenv subst context s1 s2 swap in - unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap - | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in - let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in - let context = (name1, C.Def (s1,ty1))::context in - unify status test_eq_only metasenv subst context t1 t2 swap - - | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> - (try - let l1 = NCicUtils.expand_local_context l1 in - let l2 = NCicUtils.expand_local_context l2 in - let metasenv, subst, to_restrict, _ = - List.fold_right2 - (fun t1 t2 (metasenv, subst, to_restrict, i) -> - try - let metasenv, subst = - unify status (*test_eq_only*) true metasenv subst context - (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2) - swap - in - metasenv, subst, to_restrict, i-1 - with UnificationFailure _ | Uncertain _ -> - metasenv, subst, i::to_restrict, i-1) - l1 l2 (metasenv, subst, [], List.length l1) - in - if to_restrict <> [] then - let metasenv, subst, _, _ = - NCicMetaSubst.restrict status metasenv subst n1 to_restrict - in - metasenv, subst - else metasenv, subst - with - | Invalid_argument _ -> assert false - | NCicMetaSubst.MetaSubstFailure msg -> - try - let _,_,term,_ = NCicUtils.lookup_subst n1 subst in - let term1 = NCicSubstitution.subst_meta status lc1 term in - let term2 = NCicSubstitution.subst_meta status lc2 term in - unify status test_eq_only metasenv subst context term1 term2 swap - with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) - - | NCic.Appl (NCic.Meta (i,_)::_ as l1), - NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> - (try - List.fold_left2 - (fun (metasenv, subst) t1 t2 -> - unify status (*test_eq_only*) true metasenv subst context t1 - t2 swap) - (metasenv,subst) l1 l2 - with Invalid_argument _ -> - raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))) - - | _, NCic.Meta (n, _) when is_locked n subst && not swap-> - (let (metasenv, subst), i = - match NCicReduction.whd status ~subst context t1 with - | NCic.Appl (NCic.Meta (i,l) as meta :: args) -> - let metasenv, lambda_Mj = - lambda_intros status metasenv subst context (List.length args) - (NCicTypeChecker.typeof status ~metasenv ~subst context meta) - in - unify status test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj false, - i - | NCic.Meta (i,_) -> (metasenv, subst), i - | _ -> - raise (UnificationFailure (lazy "Locked term vs non - flexible term; probably not saturated enough yet!")) - in - let t1 = NCicReduction.whd status ~subst context t1 in - let j, lj = - match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false - in + else + match (t1,t2) with + | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] + | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> + prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant"; + assert false + | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> + let a, b = if swap then b,a else a,b in + if NCicEnvironment.universe_leq status a b then metasenv, subst + else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) + | (C.Sort (C.Type a), C.Sort (C.Type b)) -> + if NCicEnvironment.universe_eq a b then metasenv, subst + else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) + | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> + if (not test_eq_only) then metasenv, subst + else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) + | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> + if (not test_eq_only) then metasenv, subst + else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) + + | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + let metasenv, subst = unify status true metasenv subst context s1 s2 swap in + unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap + | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> + let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in + let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in + let context = (name1, C.Def (s1,ty1))::context in + unify status test_eq_only metasenv subst context t1 t2 swap + + | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> + (try + let l1 = NCicUtils.expand_local_context l1 in + let l2 = NCicUtils.expand_local_context l2 in + let metasenv, subst, to_restrict, _ = + List.fold_right2 + (fun t1 t2 (metasenv, subst, to_restrict, i) -> + try let metasenv, subst = - instantiate status test_eq_only metasenv subst context j lj t2 true + unify status (*test_eq_only*) true metasenv subst context + (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2) + swap in - (* We need to remove the out_scope_tags to avoid propagation of - them that triggers again the ad-hoc case *) - let subst = - List.map (fun (i,(tag,ctx,bo,ty)) -> - let tag = - List.filter - (function `InScope | `OutScope _ -> false | _ -> true) tag - in - i,(tag,ctx,bo,ty) - ) subst - in - (try - let name, ctx, term, ty = NCicUtils.lookup_subst i subst in - let term = eta_reduce status 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.Meta (n, _), _ when is_locked n subst && swap -> - unify status test_eq_only metasenv subst context t2 t1 false - - | t, C.Meta (n,lc) when List.mem_assoc n subst -> - let _,_,term,_ = NCicUtils.lookup_subst n subst in - let term = NCicSubstitution.subst_meta status lc term in - unify status test_eq_only metasenv subst context t term swap - | C.Meta (n,_), _ when List.mem_assoc n subst -> - unify status test_eq_only metasenv subst context t2 t1 (not swap) - - | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> - let _,_,term,_ = NCicUtils.lookup_subst i subst in - let term = NCicSubstitution.subst_meta status l term in - unify status test_eq_only metasenv subst context t1 - (mk_appl status ~upto:(List.length args) term args) swap - | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst -> - unify status test_eq_only metasenv subst context t2 t1 (not swap) - - | C.Meta (n,_), C.Meta (m,lc') when - let _,cc1,_ = NCicUtils.lookup_meta n metasenv in - let _,cc2,_ = NCicUtils.lookup_meta m metasenv in - (n < m && cc1 = cc2) || - let len1 = List.length cc1 in - let len2 = List.length cc2 in - len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) -> - instantiate status test_eq_only metasenv subst context m lc' - (NCicReduction.head_beta_reduce status ~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 status lc tyn in - let tym = NCicSubstitution.subst_meta status lc tym in - match tyn,tym with - NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> - NCicEnvironment.universe_lt status u1 u2 - | _,_ -> false -> - instantiate status test_eq_only metasenv subst context m lc' - (NCicReduction.head_beta_reduce status ~subst t1) (not swap) - | C.Meta (n,lc), t -> - instantiate status test_eq_only metasenv subst context n lc - (NCicReduction.head_beta_reduce status ~subst t) swap - | t, C.Meta (n,lc) -> - instantiate status test_eq_only metasenv subst context n lc - (NCicReduction.head_beta_reduce status ~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 status 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 status 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 + metasenv, subst, to_restrict, i-1 + with UnificationFailure _ | Uncertain _ -> + metasenv, subst, i::to_restrict, i-1) + l1 l2 (metasenv, subst, [], List.length l1) + in + if to_restrict <> [] then + let metasenv, subst, _, _ = + NCicMetaSubst.restrict status metasenv subst n1 to_restrict + in + metasenv, subst + else metasenv, subst + with + | Invalid_argument _ -> assert false + | NCicMetaSubst.MetaSubstFailure msg -> + try + let _,_,term,_ = NCicUtils.lookup_subst n1 subst in + let term1 = NCicSubstitution.subst_meta status lc1 term in + let term2 = NCicSubstitution.subst_meta status lc2 term in + unify status test_eq_only metasenv subst context term1 term2 swap + with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) + + | NCic.Appl (NCic.Meta (i,_)::_ as l1), + NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> + (try + List.fold_left2 + (fun (metasenv, subst) t1 t2 -> + unify status (*test_eq_only*) true metasenv subst context t1 + t2 swap) + (metasenv,subst) l1 l2 + with Invalid_argument _ -> + raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))) + + | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift -> + (let (metasenv, subst), i = + match NCicReduction.whd status ~subst context t1 with + | NCic.Appl (NCic.Meta (i,l) as meta :: args) -> + let metasenv, lambda_Mj = + lambda_intros status metasenv subst context (List.length args) + (NCicTypeChecker.typeof status ~metasenv ~subst context meta) + in + unify status test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj false, + i + | NCic.Meta (i,_) -> (metasenv, subst), i + | _ -> + raise (UnificationFailure (lazy "Locked term vs non + flexible term; probably not saturated enough yet!")) + in + let t1 = NCicReduction.whd status ~subst context t1 in + let j, lj = + match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false + in + let metasenv, subst = + instantiate status test_eq_only metasenv subst context j lj t2 true + in + (* We need to remove the out_scope_tags to avoid propagation of + them that triggers again the ad-hoc case *) + let subst = + List.map (fun (i,(tag,ctx,bo,ty)) -> + let tag = + List.filter + (function `InScope | `OutScope _ -> false | _ -> true) tag + in + i,(tag,ctx,bo,ty) + ) subst + in + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce status 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.Meta (n, _), _ when is_locked n subst && swap -> + fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1 + + | _, C.Meta (n,lc) when List.mem_assoc n subst -> + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta status lc term in + fo_unif0 during_delift status swap test_eq_only metasenv subst context + m1 (false,term) + | C.Meta (n,_), _ when List.mem_assoc n subst -> + fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1 + + | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> + let _,_,term,_ = NCicUtils.lookup_subst i subst in + let term = NCicSubstitution.subst_meta status l term in + fo_unif0 during_delift status swap test_eq_only metasenv subst context + m1 (false,mk_appl status ~upto:(List.length args) term args) + | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst -> + fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1 + + | C.Meta (n,_), C.Meta (m,lc') when + let _,cc1,_ = NCicUtils.lookup_meta n metasenv in + let _,cc2,_ = NCicUtils.lookup_meta m metasenv in + (n < m && cc1 = cc2) || + let len1 = List.length cc1 in + let len2 = List.length cc2 in + len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) -> + instantiate status test_eq_only metasenv subst context m lc' + (NCicReduction.head_beta_reduce status ~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 status lc tyn in + let tym = NCicSubstitution.subst_meta status lc tym in + match tyn,tym with + NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> + NCicEnvironment.universe_lt u1 u2 + | _,_ -> false -> + instantiate status test_eq_only metasenv subst context m lc' + (NCicReduction.head_beta_reduce status ~subst t1) (not swap) + | C.Meta (n,lc), t -> + instantiate status test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce status ~subst t) swap + | t, C.Meta (n,lc) -> + instantiate status test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce status ~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 status 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 status 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 status metasenv subst context (List.length args) + (NCicTypeChecker.typeof status ~metasenv ~subst context meta) 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 status metasenv subst context (List.length args) - (NCicTypeChecker.typeof status ~metasenv ~subst context meta) - in - let metasenv, subst = - unify status test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj swap - in - let metasenv, subst = - unify status 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 status 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 status test_eq_only metasenv subst context t2 t1 (not swap) - - (* processing this case here we avoid a useless small delta step *) - | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) - when Ref.eq r1 r2 -> - let relevance = NCicEnvironment.get_relevance status r1 in - let metasenv, subst, _ = - try - List.fold_left2 - (fun (metasenv, subst, relevance) t1 t2 -> - let b, relevance = - match relevance with b::tl -> b,tl | _ -> true, [] in - let metasenv, subst = - try unify status test_eq_only metasenv subst context t1 t2 - swap - with UnificationFailure _ | Uncertain _ when not b -> - metasenv, subst - in - metasenv, subst, relevance) - (metasenv, subst, relevance) tl1 tl2 - with - Invalid_argument _ -> - raise (Uncertain (mk_msg status 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 -> - let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in - let _,_,ty,_ = List.nth itl tyno in - let rec remove_prods ~subst context ty = - let ty = NCicReduction.whd status ~subst context ty in - match ty with - | C.Sort _ -> ty - | C.Prod (name,so,ta) -> - remove_prods ~subst ((name,(C.Decl so))::context) ta - | _ -> assert false + let metasenv, subst = + unify status test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj swap in - let is_prop = - match remove_prods ~subst [] ty with - | C.Sort C.Prop -> true - | _ -> false + let metasenv, subst = + unify status test_eq_only metasenv subst context t1 t2 swap in - (* if not (Ref.eq ref1 ref2) then - raise (Uncertain (mk_msg status metasenv subst context t1 t2)) - else*) - let metasenv, subst = - unify status test_eq_only metasenv subst context outtype1 outtype2 swap in - let metasenv, subst = - try unify status test_eq_only metasenv subst context term1 term2 swap - with UnificationFailure _ | Uncertain _ when is_prop -> - metasenv, subst - in - (try - List.fold_left2 - (fun (metasenv,subst) t1 t2 -> - unify status test_eq_only metasenv subst context t1 t2 swap) - (metasenv, subst) pl1 pl2 - with Invalid_argument _ -> assert false) - | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | _ when norm1 && norm2 -> - if (could_reduce t1 || could_reduce t2) then - raise (Uncertain (mk_msg status metasenv subst context t1 t2)) - else - raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) - | _ -> raise (KeepReducing (mk_msg status 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 status metasenv subst context t1 t2)) - in - let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) = - if NCicUntrusted.metas_of_term status subst context t1 = [] && - NCicUntrusted.metas_of_term status subst context t2 = [] - then None - else begin - (*D*) inside 'H'; try let rc = - pp(lazy ("\nProblema:\n" ^ - ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^ - ppterm status ~metasenv ~subst ~context t2)); - let candidates = - NCicUnifHint.look_for_hint status metasenv subst context t1 t2 - in - let rec cand_iter = function - | [] -> None (* raise exc *) - | (metasenv,(c1,c2),premises)::tl -> - pp (lazy ("\nProvo il candidato:\n" ^ - String.concat "\n" - (List.map - (fun (a,b) -> - ppterm status ~metasenv ~subst ~context a ^ " =?= " ^ - ppterm status ~metasenv ~subst ~context b) premises) ^ - "\n-------------------------------------------\n"^ - ppterm status ~metasenv ~subst ~context c1 ^ " = " ^ - ppterm status ~metasenv ~subst ~context c2)); - try - (*D*) inside 'K'; try let rc = - let metasenv,subst = - fo_unif test_eq_only metasenv subst mt1 (false,c1) in - let metasenv,subst = - fo_unif test_eq_only metasenv subst (false,c2) mt2 in - let metasenv,subst = - List.fold_left - (fun (metasenv, subst) (x,y) -> - unify status test_eq_only metasenv subst context x y false) - (metasenv, subst) (List.rev premises) - in - pp(lazy("FUNZIONA!")); - Some (metasenv, subst) - (*D*) in outside None; rc with exn -> outside (Some exn); raise exn - with - KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl - | KeepReducingThis _ -> assert false - 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 status ~delta:max_int ~subst context m1, - NCicReduction.reduce_machine status ~delta:max_int ~subst context m2 - in - let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) = - try fo_unif test_eq_only metasenv subst m1 m2 - with - | UnificationFailure _ as exn -> raise exn - | KeepReducing _ | Uncertain _ as exn -> - let (t1,norm1 as tm1),(t2,norm2 as tm2) = - put_in_whd (0,[],t1,[]) (0,[],t2,[]) - in - match - try_hints metasenv subst - (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2) + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce status 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 (_,_) :: _) -> + fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1 + + | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> + let metasenv,subst = + fo_unif0 during_delift status swap test_eq_only metasenv subst context + (false,hd1) (false,hd2) in + let relevance = + match hd1 with + | C.Const r -> NCicEnvironment.get_relevance status r + | _ -> [] in + let metasenv, subst, _ = + try + List.fold_left2 + (fun (metasenv, subst, relevance) t1 t2 -> + let b, relevance = + match relevance with b::tl -> b,tl | _ -> true, [] in + let metasenv, subst = + try unify status test_eq_only metasenv subst context t1 t2 + swap + with UnificationFailure _ | Uncertain _ when not b -> + metasenv, subst + in + metasenv, subst, relevance) + (metasenv, subst, relevance) tl1 tl2 with - | Some x -> x - | None -> - match exn with - | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2)) - | Uncertain _ as exn -> raise exn - | _ -> assert false - in + Invalid_argument _ -> + raise (Uncertain (mk_msg status 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 -> + let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = + let ty = NCicReduction.whd status ~subst context ty in + match ty with + | C.Sort _ -> ty + | C.Prod (name,so,ta) -> + remove_prods ~subst ((name,(C.Decl so))::context) ta + | _ -> assert false + in + let is_prop = + match remove_prods ~subst [] ty with + | C.Sort C.Prop -> true + | _ -> false + in + (* if not (Ref.eq ref1 ref2) then + raise (Uncertain (mk_msg status metasenv subst context t1 t2)) + else*) + let metasenv, subst = + unify status test_eq_only metasenv subst context outtype1 outtype2 swap in + let metasenv, subst = + try unify status test_eq_only metasenv subst context term1 term2 swap + with UnificationFailure _ | Uncertain _ when is_prop -> + metasenv, subst + in + (try + List.fold_left2 + (fun (metasenv,subst) t1 t2 -> + unify status test_eq_only metasenv subst context t1 t2 swap) + (metasenv, subst) pl1 pl2 + with Invalid_argument _ -> assert false) + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | _ when norm1 && norm2 -> + if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then + raise (Uncertain (mk_msg status metasenv subst context t1 t2)) + else + raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) + | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2)) + (*D*) in outside None; rc with exn -> outside (Some exn); raise exn + +and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) = + if NCicUntrusted.metas_of_term status subst context t1 = [] && + NCicUntrusted.metas_of_term status subst context t2 = [] + then None + else begin +(*D*) inside 'H'; try let rc = + pp(lazy ("\nProblema:\n" ^ + ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^ + ppterm status ~metasenv ~subst ~context t2)); + let candidates = + NCicUnifHint.look_for_hint status metasenv subst context t1 t2 + in + let rec cand_iter = function + | [] -> None (* raise exc *) + | (metasenv,(c1,c2),premises)::tl -> + pp (lazy ("\nProvo il candidato:\n" ^ + String.concat "\n" + (List.map + (fun (a,b) -> + ppterm status ~metasenv ~subst ~context a ^ " =?= " ^ + ppterm status ~metasenv ~subst ~context b) premises) ^ + "\n-------------------------------------------\n"^ + ppterm status ~metasenv ~subst ~context c1 ^ " = " ^ + ppterm status ~metasenv ~subst ~context c2)); + try +(*D*) inside 'K'; try let rc = + let metasenv,subst = + fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in + let metasenv,subst = + fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in + let metasenv,subst = + List.fold_left + (fun (metasenv, subst) (x,y) -> + unify status test_eq_only metasenv subst context x y false) + (metasenv, subst) (List.rev premises) + in + pp(lazy("FUNZIONA!")); + Some (metasenv, subst) + (*D*) in outside None; rc with exn -> outside (Some exn); raise exn + with + KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl + | KeepReducingThis _ -> assert false + in + cand_iter candidates + (*D*) in outside None; rc with exn -> outside (Some exn); raise exn + end + +and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)= + try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2 + with + UnificationFailure _ | Uncertain _ when not norm1 || not norm2 -> + raise (KeepReducing (mk_msg status metasenv subst context t1 t2)) + +and unify status test_eq_only metasenv subst context t1 t2 swap = + (*D*) inside 'U'; try let rc = let fo_unif_heads_and_cont_or_unwind_and_hints test_eq_only metasenv subst m1 m2 cont hm1 hm2 = @@ -787,13 +794,13 @@ and unify status test_eq_only metasenv subst context t1 t2 swap = 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 + try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont with | UnificationFailure _ | KeepReducing _ | Uncertain _ as exn -> let (t1,norm1),(t2,norm2) = hm1, hm2 in match - try_hints metasenv subst + try_hints status swap test_eq_only metasenv subst context (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2) with | Some x -> x, fun x -> x @@ -846,7 +853,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap = try let t1 = NCicReduction.from_stack ~delta:max_int t1 in let t2 = NCicReduction.from_stack ~delta:max_int t2 in - unif_machines metasenv subst (put_in_whd t1 t2) + unif_machines metasenv subst (put_in_whd status subst context t1 t2) with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in @@ -881,12 +888,12 @@ and unify status test_eq_only metasenv subst context t1 t2 swap = | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2)) -> unif_machines metasenv subst (small_delta_step ~subst m1 m2) | UnificationFailure msg - when could_reduce (NCicReduction.unwind status (fst m1)) - || could_reduce (NCicReduction.unwind status (fst m2)) + when could_reduce status ~subst context (NCicReduction.unwind status (fst m1)) + || could_reduce status ~subst context (NCicReduction.unwind status (fst m2)) -> raise (Uncertain msg) (*D*) in outside None; rc with exn -> outside (Some exn); raise exn in - try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2) + try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2) with | KeepReducingThis (msg,tm1,tm2) -> (try @@ -903,15 +910,8 @@ and delift_type_wrt_terms status metasenv subst context t args = let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in let (metasenv, subst), t = try - NCicMetaSubst.delift status - ~unify:(fun m s c t1 t2 -> - let ind = !indent in - let res = - try Some (unify status false m s c t1 t2 false) - with UnificationFailure _ | Uncertain _ -> None - in - indent := ind; res) - metasenv subst context 0 (0,NCic.Ctx lc) t + NCicMetaSubst.delift status ~unify:(unify_for_delift status) + metasenv subst context (-1) (0,NCic.Ctx lc) t with NCicMetaSubst.MetaSubstFailure _ | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t diff --git a/matitaB/components/ng_refiner/nCicUnification.mli b/matitaB/components/ng_refiner/nCicUnification.mli index d0a539c6a..1ce5a95db 100644 --- a/matitaB/components/ng_refiner/nCicUnification.mli +++ b/matitaB/components/ng_refiner/nCicUnification.mli @@ -28,6 +28,10 @@ val fix_sorts: #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.term -> NCic.metasenv * NCic.term +(* this should be moved elsewhere *) +(* The term must be in whd *) +val could_reduce: #NCicCoercion.status -> subst:NCic.substitution -> NCic.context -> NCic.term -> bool + (* delift_type_wrt_terms st m s c t args * lift t (length args) * [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ] -- 2.39.2