From: Wilmer Ricciotti Date: Mon, 15 Dec 2008 19:16:46 +0000 (+0000) Subject: First attempt to implement unification hints. X-Git-Tag: make_still_working~4392 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2e2d1f6cccad2cc1ce70ef7fa2841cf0a457953;p=helm.git First attempt to implement unification hints. --- diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 63ab446c7..28551550d 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -570,7 +570,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in -(* let time = Unix.gettimeofday () in *) + let time = Unix.gettimeofday () in let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj @@ -581,7 +581,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri (text,prefix_len,obj)) in - (* + let time = Unix.gettimeofday () -. time in prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time); (NCicLibrary.clear_cache (); @@ -650,7 +650,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ) | _ -> ()) ); - *) + let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status, metasenv, cic diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 0efb49bff..9f14c503f 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -40,7 +40,8 @@ let refine_term assert false in let metasenv, subst, term, _ = - NCicRefiner.typeof + NCicRefiner.typeof + (NCicUnifHint.db ()) ~look_for_coercion:( if use_coercions then NCicCoercion.look_for_coercion coercion_db diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index c8ccb5d0c..89e6fd7e9 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,10 +1,11 @@ -nCicCoercion.cmi: nDiscriminationTree.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi -nCicCoercion.cmo: nDiscriminationTree.cmi nCicCoercion.cmi -nCicCoercion.cmx: nDiscriminationTree.cmx nCicCoercion.cmi +nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi +nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi +nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi +nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index f3a7fba40..1b2c293bc 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -5,8 +5,9 @@ INTERFACE_FILES = \ nDiscriminationTree.mli \ nCicMetaSubst.mli \ nCicCoercion.mli \ + nCicUnifHint.mli \ nCicUnification.mli \ - nCicRefiner.mli \ + nCicRefiner.mli IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index c8f6bdb59..d47767528 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -49,7 +49,7 @@ let exp_implicit metasenv context expty = ;; -let check_allowed_sort_elimination localise r orig = +let check_allowed_sort_elimination hdb localise r orig = let mkapp he arg = match he with | C.Appl l -> C.Appl (l @ [arg]) @@ -67,7 +67,7 @@ let check_allowed_sort_elimination localise r orig = NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type in let metasenv, subst = - try NCicUnification.unify metasenv subst context + try NCicUnification.unify hdb metasenv subst context arity2 (C.Prod (name, so1, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) @@ -79,7 +79,7 @@ let check_allowed_sort_elimination localise r orig = | C.Sort _ (* , t ==?== C.Prod _ *) -> let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in let metasenv, subst = - try NCicUnification.unify metasenv subst context + try NCicUnification.unify hdb metasenv subst context arity2 (C.Prod ("_", ind, meta)) with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf "expected %s, found %s" (* XXX localizzare meglio *) @@ -97,7 +97,7 @@ let check_allowed_sort_elimination localise r orig = aux ;; -let rec typeof +let rec typeof hdb ?(localise=fun _ -> Stdpp.dummy_loc) ~look_for_coercion metasenv subst context term expty = @@ -114,11 +114,11 @@ let rec typeof (NCicPp.ppterm ~metasenv ~subst ~context expty))); try let metasenv, subst = - NCicUnification.unify metasenv subst context infty expty + NCicUnification.unify hdb metasenv subst context infty expty in metasenv, subst, t, expty with exc -> - try_coercions ~look_for_coercion ~localise + try_coercions hdb ~look_for_coercion ~localise metasenv subst context t orig infty expty true exc) | None -> metasenv, subst, t, infty (*D*)in outside(); rc with exc -> outside (); raise exc @@ -165,12 +165,12 @@ let rec typeof | C.Prod (name,(s as orig_s),(t as orig_t)) -> let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in let metasenv, subst, s, s1 = - force_to_sort ~look_for_coercion + force_to_sort hdb ~look_for_coercion metasenv subst context s orig_s localise s1 in let context1 = (name,(C.Decl s))::context in let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in let metasenv, subst, t, s2 = - force_to_sort ~look_for_coercion + force_to_sort hdb ~look_for_coercion metasenv subst context1 t orig_t localise s2 in let metasenv, subst, s, t, ty = sort_of_prod localise metasenv subst @@ -189,12 +189,12 @@ let rec typeof let metasenv, subst, s, ty_s = typeof_aux metasenv subst context None s in let metasenv, subst, s, _ = - force_to_sort ~look_for_coercion + force_to_sort hdb ~look_for_coercion metasenv subst context s orig_s localise ty_s in let (metasenv,subst), exp_ty_t = match exp_s with | Some exp_s -> - (try NCicUnification.unify metasenv subst context s exp_s,exp_ty_t + (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context @@ -210,7 +210,7 @@ let rec typeof let metasenv, subst, ty, ty_ty = typeof_aux metasenv subst context None ty in let metasenv, subst, ty, _ = - force_to_sort ~look_for_coercion + force_to_sort hdb ~look_for_coercion metasenv subst context ty orig_ty localise ty_ty in let metasenv, subst, t, _ = typeof_aux metasenv subst context (Some ty) t in @@ -223,7 +223,7 @@ let rec typeof | C.Appl ((he as orig_he)::(_::_ as args)) -> let metasenv, subst, he, ty_he = typeof_aux metasenv subst context None he in - eat_prods ~localise ~look_for_coercion + eat_prods hdb ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r, @@ -246,7 +246,7 @@ let rec typeof let metasenv, subst, ind, ind_ty = typeof_aux metasenv subst context None ind in let metasenv, subst = - check_allowed_sort_elimination localise r orig_term metasenv subst + check_allowed_sort_elimination hdb localise r orig_term metasenv subst context ind ind_ty outsort in (* let's check if the type of branches are right *) @@ -288,7 +288,7 @@ let rec typeof in typeof_aux metasenv subst context expty term -and try_coercions +and try_coercions hdb ~localise ~look_for_coercion metasenv subst context t orig_t infty expty perform_unification exc = @@ -310,7 +310,7 @@ and try_coercions NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n")); let metasenv, subst = - NCicUnification.unify metasenv subst context meta t + NCicUnification.unify hdb metasenv subst context meta t in pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context @@ -321,7 +321,7 @@ and try_coercions NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n")); let metasenv, subst = if perform_unification then - NCicUnification.unify metasenv subst context newtype expty + NCicUnification.unify hdb metasenv subst context newtype expty else metasenv, subst in metasenv, subst, newterm, newtype @@ -332,7 +332,7 @@ and try_coercions first exc (look_for_coercion metasenv subst context infty expty) -and force_to_sort +and force_to_sort hdb ~look_for_coercion metasenv subst context t orig_t localise ty = match NCicReduction.whd ~subst context ty with @@ -350,7 +350,7 @@ and force_to_sort metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0)) | C.Sort _ as ty -> metasenv, subst, t, ty | ty -> - try_coercions ~localise ~look_for_coercion metasenv subst context + try_coercions hdb ~localise ~look_for_coercion metasenv subst context t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false (Uncertain (lazy (localise orig_t, "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t @@ -378,7 +378,7 @@ and sort_of_prod (NCicPp.ppterm ~subst ~metasenv ~context y) (NCicPp.ppterm ~subst ~metasenv ~context x)))) -and eat_prods +and eat_prods hdb ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args = (*D*)inside 'E'; try let rc = @@ -388,14 +388,14 @@ and eat_prods match NCicReduction.whd ~subst context ty_he with | C.Prod (_,s,t) -> let metasenv, subst, arg, _ = - typeof ~look_for_coercion ~localise + typeof hdb ~look_for_coercion ~localise metasenv subst context arg (Some s) in let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in aux metasenv subst (arg :: args_so_far) he t tl | C.Meta _ | C.Appl (C.Meta _ :: _) as t -> let metasenv, subst, arg, ty_arg = - typeof ~look_for_coercion ~localise + typeof hdb ~look_for_coercion ~localise metasenv subst context arg None in let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv @@ -404,7 +404,7 @@ and eat_prods let flex_prod = C.Prod ("_", ty_arg, meta) in (* next line grants that ty_args is a type *) let metasenv,subst, flex_prod, _ = - typeof ~look_for_coercion ~localise metasenv subst + typeof hdb ~look_for_coercion ~localise metasenv subst context flex_prod None in pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context @@ -412,7 +412,7 @@ and eat_prods NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); let metasenv, subst = - try NCicUnification.unify metasenv subst context t flex_prod + try NCicUnification.unify hdb metasenv subst context t flex_prod with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf ("The term %s has an inferred type %s, but is applied to the" ^^ " argument %s of type %s") @@ -433,7 +433,7 @@ and eat_prods (List.length args) (List.length args_so_far)))) | ty -> let metasenv, subst, newhead, newheadty = - try_coercions ~localise ~look_for_coercion metasenv subst context + try_coercions hdb ~localise ~look_for_coercion metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) false diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index 741477080..2df108697 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -16,6 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; val typeof : + NCicUnifHint.db -> ?localise:(NCic.term -> Stdpp.location) -> look_for_coercion:( NCic.metasenv -> NCic.substitution -> NCic.context -> diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index c324b0ec6..abbafc458 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,200 +245,223 @@ 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 = - let fo_unif test_eq_only metasenv subst t1 t2 = +and unify hdb test_eq_only metasenv subst context t1 t2 = + (*D*) inside 'U'; try let rc = + let rec fo_unif test_eq_only metasenv subst t1 t2 = + let try_hints metasenv subst context 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 + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1); + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c1); + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2); + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c2); + 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 (fo_unif test_eq_only metasenv subst t1 t2) + with + UnificationFailure _ | Uncertain _ -> cand_iter tl + in + cand_iter candidates + in + (*D*) inside 'F'; try let rc = pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); if t1 === t2 then metasenv, subst else - match (t1,t2) with - | (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) - | (C.Sort (C.Type a), C.Sort (C.Type b)) -> - if NCicEnvironment.universe_eq a b then metasenv, subst - else raise (fail_exc metasenv subst context t1 t2) - | (C.Sort C.Prop,C.Sort (C.Type _)) -> - if (not test_eq_only) then metasenv, subst - else raise (fail_exc 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 - | (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 context = (name1, C.Def (s1,ty1))::context in - unify 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 - 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 test_eq_only metasenv subst context - (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) - 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 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 lc1 term in - let term2 = NCicSubstitution.subst_meta lc2 term in - unify 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 - with NCicUtils.Subst_not_found _-> - instantiate 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 - with NCicUtils.Subst_not_found _-> - instantiate 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 - - | _, 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) - - | 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) - (metasenv,subst) l1 l2 - with Invalid_argument _ -> - raise (fail_exc metasenv subst context t1 t2)) - - | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) -> - (* 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 - test_eq_only false - metasenv subst context t2 args - in - unify 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 - test_eq_only true - metasenv subst context t1 args - in - unify test_eq_only metasenv subst context - beta_expanded (C.Meta (i,l)) - - (* 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 r1 in - let relevance = match r1 with - | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth lno relevance in - HExtlib.mk_list false lno @ relevance - | _ -> relevance - 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 + match (try_hints metasenv subst context t1 t2) with + | Some x -> x + | None -> + match (t1,t2) with + | (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) + | (C.Sort (C.Type a), C.Sort (C.Type b)) -> + if NCicEnvironment.universe_eq a b then metasenv, subst + else raise (fail_exc metasenv subst context t1 t2) + | (C.Sort C.Prop,C.Sort (C.Type _)) -> + if (not test_eq_only) then metasenv, subst + else raise (fail_exc 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 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 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 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 + 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 = - try unify test_eq_only metasenv subst context t1 t2 - with UnificationFailure _ | Uncertain _ when not b -> - metasenv, subst + unify hdb test_eq_only metasenv subst context + (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) in - metasenv, subst, relevance) - (metasenv, subst, relevance) tl1 tl2 - with Invalid_argument _ -> - raise (uncert_exc metasenv subst context t1 t2) - in - metasenv, subst - - | (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 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 - let is_prop = - match remove_prods ~subst [] ty with - | 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 - let metasenv, subst = - try unify test_eq_only metasenv subst context term1 term2 - with UnificationFailure _ | Uncertain _ when is_prop -> + 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 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 lc1 term in + let term2 = NCicSubstitution.subst_meta lc2 term in + 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 hdb test_eq_only metasenv subst context term t + with NCicUtils.Subst_not_found _-> + 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 hdb test_eq_only metasenv subst context t term + with NCicUtils.Subst_not_found _-> + 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 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 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 hdb test_eq_only metasenv subst context t1 t2) + (metasenv,subst) l1 l2 + with Invalid_argument _ -> + raise (fail_exc metasenv subst context t1 t2)) + + | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) -> + (* 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 hdb + test_eq_only false + metasenv subst context t2 args + in + 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 hdb + test_eq_only true + metasenv subst context t1 args + in + 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 *) + | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) + when Ref.eq r1 r2 -> + let relevance = NCicEnvironment.get_relevance r1 in + let relevance = match r1 with + | Ref.Ref (_,Ref.Con (_,_,lno)) -> + let _,relevance = HExtlib.split_nth lno relevance in + HExtlib.mk_list false lno @ relevance + | _ -> relevance + 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 hdb test_eq_only metasenv subst context t1 t2 + with UnificationFailure _ | Uncertain _ when not b -> + metasenv, subst + in + metasenv, subst, relevance) + (metasenv, subst, relevance) tl1 tl2 + with Invalid_argument _ -> + raise (uncert_exc metasenv subst context t1 t2) + in + metasenv, subst + + | (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 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 + let is_prop = + match remove_prods ~subst [] ty with + | 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 - (try - List.fold_left2 - (fun (metasenv,subst) -> - unify 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) + if not (Ref.eq ref1 ref2) then + raise (uncert_exc metasenv subst context t1 t2) + else + let metasenv, subst = + unify hdb test_eq_only metasenv subst context outtype1 outtype2 in + let metasenv, subst = + 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 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 height_of = function @@ -520,8 +543,8 @@ and unify test_eq_only metasenv subst context t1 t2 = (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify = +let unify hdb = indent := ""; - unify false;; + unify hdb false;; diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 97976b7a3..54ccf2143 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -16,6 +16,7 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; val unify : + NCicUnifHint.db -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> NCic.metasenv * NCic.substitution