X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=838fad9dedfb4288d2d4dac99326da6f693bd1d5;hb=d45787d8c1bd22f27b64f214a9fb8f54e69c9533;hp=c4940e08989c259b403aff5e24d74034509ec93a;hpb=e7759b1c1f40380748ac052bce5b677bc8fd71cb;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index c4940e089..838fad9de 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -99,14 +99,14 @@ let fix_sorts swap metasenv subst context meta t = aux () t ;; -let rec beta_expand num test_eq_only swap metasenv subst context t arg = +let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg = let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = try let metasenv, subst = if swap then - unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) + unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) else - unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' + unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' in (metasenv, subst), NCic.Rel (1 + n) with Uncertain _ | UnificationFailure _ -> @@ -141,7 +141,7 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg = with NCicTypeChecker.TypeCheckerFailure _ -> metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) -and beta_expand_many test_equality_only swap metasenv subst context t args = +and beta_expand_many hdb test_equality_only swap metasenv subst context t args = (* (*D*) inside 'B'; try let rc = *) pp (lazy (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) @@ -150,7 +150,7 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = List.fold_right (fun arg (num,subst,metasenv,t) -> let metasenv, subst, t = - beta_expand num test_equality_only swap metasenv subst context t arg + beta_expand hdb num test_equality_only swap metasenv subst context t arg in num+1,subst,metasenv,t) args (1,subst,metasenv,t) @@ -160,13 +160,13 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = metasenv, subst, hd (* (*D*) in outside (); rc with exn -> outside (); raise exn *) -and instantiate test_eq_only metasenv subst context n lc t swap = +and instantiate hdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = pp (lazy(string_of_int n ^ " :=?= "^ NCicPp.ppterm ~metasenv ~subst ~context t)); let unify test_eq_only m s c t1 t2 = - if swap then unify test_eq_only m s c t2 t1 - else unify test_eq_only m s c t1 t2 + if swap then unify hdb test_eq_only m s c t2 t1 + else unify hdb test_eq_only m s c t1 t2 in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let metasenv, subst, t = @@ -245,16 +245,21 @@ and instantiate test_eq_only metasenv subst context n lc t swap = metasenv, subst (*D*) in outside(); rc with exn -> outside (); raise exn -and unify test_eq_only metasenv subst context t1 t2 = - (*D*) inside 'U'; try let rc = +and unify hdb test_eq_only metasenv subst context t1 t2 = + (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = (*D*) inside 'F'; try let rc = - pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2)); + pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv + ~subst metasenv)); if t1 === t2 then metasenv, subst 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 -> if NCicEnvironment.universe_leq a b then metasenv, subst else raise (fail_exc metasenv subst context t1 t2) @@ -267,13 +272,13 @@ and unify test_eq_only 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 true metasenv subst context s1 s2 in - unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 + let metasenv, subst = unify hdb true metasenv subst context s1 s2 in + unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in - let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in + let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in + let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in let context = (name1, C.Def (s1,ty1))::context in - unify test_eq_only metasenv subst context t1 t2 + unify hdb test_eq_only metasenv subst context t1 t2 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> (try @@ -284,7 +289,7 @@ and unify test_eq_only metasenv subst context t1 t2 = (fun t1 t2 (metasenv, subst, to_restrict, i) -> try let metasenv, subst = - unify test_eq_only metasenv subst context + unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) in metasenv, subst, to_restrict, i-1 @@ -305,41 +310,41 @@ and unify test_eq_only metasenv subst context t1 t2 = let _,_,term,_ = NCicUtils.lookup_subst n1 subst in let term1 = NCicSubstitution.subst_meta lc1 term in let term2 = NCicSubstitution.subst_meta lc2 term in - unify test_eq_only metasenv subst context term1 term2 + unify hdb test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) | C.Meta (n,lc), t -> (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify test_eq_only metasenv subst context term t + unify hdb test_eq_only metasenv subst context term t with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t false) + instantiate hdb test_eq_only metasenv subst context n lc t false) | t, C.Meta (n,lc) -> (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify test_eq_only metasenv subst context t term + unify hdb test_eq_only metasenv subst context t term with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t true) + instantiate hdb test_eq_only metasenv subst context n lc t true) | 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 l term in - unify test_eq_only metasenv subst context (mk_appl term args) t2 + unify hdb test_eq_only metasenv subst context (mk_appl term args) t2 | _, 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 l term in - unify test_eq_only metasenv subst context t1 (mk_appl term args) + unify hdb test_eq_only metasenv subst context t1 (mk_appl term args) | 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 test_eq_only metasenv subst context t1 t2) + unify hdb test_eq_only metasenv subst context t1 t2) (metasenv,subst) l1 l2 with Invalid_argument _ -> raise (fail_exc metasenv subst context t1 t2)) @@ -348,20 +353,20 @@ and unify test_eq_only metasenv subst context t1 t2 = (* we verify that none of the args is a Meta, since beta expanding w.r.t a metavariable makes no sense *) let metasenv, subst, beta_expanded = - beta_expand_many + beta_expand_many hdb test_eq_only false metasenv subst context t2 args in - unify test_eq_only metasenv subst context + unify hdb test_eq_only metasenv subst context (C.Meta (i,l)) beta_expanded | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) -> let metasenv, subst, beta_expanded = - beta_expand_many + beta_expand_many hdb test_eq_only true metasenv subst context t1 args in - unify test_eq_only metasenv subst context + unify hdb test_eq_only metasenv subst context beta_expanded (C.Meta (i,l)) (* processing this case here we avoid a useless small delta step *) @@ -381,7 +386,7 @@ and unify test_eq_only metasenv subst context t1 t2 = let b, relevance = match relevance with b::tl -> b,tl | _ -> true, [] in let metasenv, subst = - try unify test_eq_only metasenv subst context t1 t2 + try unify hdb test_eq_only metasenv subst context t1 t2 with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in @@ -394,13 +399,13 @@ and unify test_eq_only metasenv subst context t1 t2 = | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), 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 = + let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = let ty = NCicReduction.whd ~subst context ty in match ty with | C.Sort _ -> ty - | C.Prod (name,so,ta) -> + | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta | _ -> assert false in @@ -409,35 +414,46 @@ and unify test_eq_only metasenv subst context t1 t2 = | C.Sort C.Prop -> true | _ -> false in - let rec remove_prods ~subst context ty = - let ty = NCicReduction.whd ~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 if not (Ref.eq ref1 ref2) then raise (uncert_exc metasenv subst context t1 t2) else let metasenv, subst = - unify test_eq_only metasenv subst context outtype1 outtype2 in + unify hdb test_eq_only metasenv subst context outtype1 outtype2 in let metasenv, subst = - try unify test_eq_only metasenv subst context term1 term2 + try unify hdb test_eq_only metasenv subst context term1 term2 with UnificationFailure _ | Uncertain _ when is_prop -> metasenv, subst in (try List.fold_left2 (fun (metasenv,subst) -> - unify test_eq_only metasenv subst context) + unify hdb test_eq_only metasenv subst context) (metasenv, subst) pl1 pl2 with Invalid_argument _ -> raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | _ when NCicUntrusted.metas_of_term subst context t1 = [] && + NCicUntrusted.metas_of_term subst context t2 = [] -> + raise (fail_exc metasenv subst context t1 t2) | _ -> raise (uncert_exc metasenv subst context t1 t2) (*D*) in outside(); rc with exn -> outside (); raise exn in + let try_hints metasenv subst t1 t2 (* exc*) = + let candidates = + NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 + in + let rec cand_iter = function + | [] -> None (* raise exc *) + | (metasenv,c1,c2)::tl -> + try + let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in + let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in + Some (metasenv, subst) + with + UnificationFailure _ | Uncertain _ -> cand_iter tl + in + cand_iter candidates + in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) @@ -449,7 +465,7 @@ and unify test_eq_only metasenv subst context t1 t2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step + let small_delta_step ~subst ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) = assert (not (norm1 && norm2)); @@ -468,12 +484,13 @@ and unify test_eq_only metasenv subst context t1 t2 = function | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> (*D*) inside 'M'; try let rc = -(* - pp (lazy((if are_normal then "*" else " ") ^ " " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ + pp (lazy("UM: " ^ + NCicPp.ppterm ~metasenv ~subst ~context + (NCicReduction.unwind (k1,e1,t1,s1)) ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); -*) + NCicPp.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 match t1 with | C.Const r -> NCicEnvironment.get_relevance r @@ -486,37 +503,42 @@ and unify test_eq_only metasenv subst context t1 t2 = with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in - let rec check_stack l1 l2 r (metasenv, subst) = + let rec check_stack l1 l2 r todo = match l1,l2,r with - | x1::tl1, x2::tl2, r::tr -> - check_stack tl1 tl2 tr - (unif_from_stack x1 x2 r metasenv subst) - | x1::tl1, x2::tl2, [] -> - check_stack tl1 tl2 [] - (unif_from_stack x1 x2 true metasenv subst) + | 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, _ -> - fo_unif test_eq_only metasenv subst - (NCicReduction.unwind (k1,e1,t1,List.rev l1)) - (NCicReduction.unwind (k2,e2,t2,List.rev l2)) + NCicReduction.unwind (k1,e1,t1,List.rev l1), + NCicReduction.unwind (k2,e2,t2,List.rev l2), + todo in - try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) + let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in + try + let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in + List.fold_left + (fun (metasenv,subst) (x1,x2,r) -> + unif_from_stack x1 x2 r metasenv subst + ) (metasenv,subst) todo with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> - unif_machines metasenv subst (small_delta_step m1 m2) + unif_machines metasenv subst (small_delta_step ~subst m1 m2) (*D*) in outside(); rc with exn -> outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 with UnificationFailure msg | Uncertain msg as exn -> - try - unif_machines metasenv subst - (put_in_whd (0,[],t1,[]) (0,[],t2,[])) - with - | UnificationFailure _ -> raise (UnificationFailure msg) - | Uncertain _ -> raise exn + match try_hints metasenv subst t1 t2 with + | Some x -> x + | None -> + try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify = +let unify hdb = indent := ""; - unify false;; + unify hdb false;;