From 46b671c7473385ec7747a796e85b3cf704d000c6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 27 Jul 2017 16:10:49 +0200 Subject: Evd/evarsolve: add an abstraction field to evars for unification Named evar_abstract_arguments, this field indicates if the evar arguments corresponding to certain hypothesis can be immitated during inversion or not. If the argument comes from an abstraction (the evar was of arrow type), then imitation is disallowed as it gives unnatural solutions, and lambda abstraction is preferred. --- engine/evarutil.ml | 16 ++++++++++------ engine/evarutil.mli | 7 ++++--- engine/evd.ml | 11 +++++++++++ engine/evd.mli | 12 ++++++++++++ 4 files changed, 37 insertions(+), 9 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index d70c009c6d..840c14b241 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -424,8 +424,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate - ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) + ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -441,6 +441,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_concl = typ; evar_body = Evar_empty; evar_filter = filter; + evar_abstract_arguments = abstract_arguments; evar_source = src; evar_candidates = candidates } in @@ -452,11 +453,12 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = @@ -469,7 +471,8 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -477,7 +480,8 @@ let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?h match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming + ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 23b240f1a0..bb0da44103 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -42,7 +42,7 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> @@ -50,7 +50,7 @@ val new_evar : val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> @@ -80,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..2d28892e6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -126,6 +126,15 @@ struct end +module Abstraction = struct + + type t = bool list + + let identity = [] + + let abstract_last l = true :: l +end + (* The kinds of existential variables are now defined in [Evar_kinds] *) (* The type of mappings for existential variables *) @@ -143,6 +152,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : Filter.t; + evar_abstract_arguments : Abstraction.t; evar_source : Evar_kinds.t Loc.located; evar_candidates : constr list option; (* if not None, list of allowed instances *)} @@ -151,6 +161,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; + evar_abstract_arguments = Abstraction.identity; evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; } diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..1c852971f5 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -77,6 +77,14 @@ sig end +module Abstraction : sig + type t = bool list + + val identity : t + + val abstract_last : t -> t +end + (** {6 Evar infos} *) type evar_body = @@ -94,6 +102,10 @@ type evar_info = { (** Boolean mask over {!evar_hyps}. Should have the same length. When filtered out, the corresponding variable is not allowed to occur in the solution *) + evar_abstract_arguments : Abstraction.t; + (** Boolean information over {!evar_hyps}, telling if an hypothesis instance + can be immitated or should stay abstract in HO unification problems + and inversion (see [second_order_matching_with_args] for its use). *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : econstr list option; -- cgit v1.2.3 From 1c9e1a39652b401805029519055aa62adacde339 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jul 2018 17:07:49 +0200 Subject: evarconv/evarsolve: HO matching algorithm with occurrence selection Also extend evarconv to handle frozen evars and flags for delta and betaiota reduction. - Make evar_conv unification take a record of flags - Adds an imitate_defs option to evarsolve, deactivated in first-order unification - Add a way to call back conv_algo differently on types - We distinguish comparison of terms and types which might be different w.r.t. delta reductions allowed (everything for types, controlled for terms). We keep the with_cs flag even for types, to avoid incompatibilities (in HoTT's theories/Spaces/No.v, the refine in No_encode_le_lt would diverge due to trying a default canonical structure during type verification). - In evarsolve, do_project_effects checks evar instances now - Solve evar-evar unification using miller patterns if possible. - FO heuristic in evarconv - Do not catch critical exceptions in evarconv - Force HO matching to abstract toplevel evar args, This disallows K on them, more compatible with w_unify_to_subterm. - occur_rigidly improvement, better approx of occur-check. - K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into account in apply_on_subterm and evar_conv_x. This allow implementing a unification without reduction, e.g. for the fast path of rewrite subterm selection. - second_order_matching works up-to cumulativity - pretyping/coercion: now take unification flags as argument - pretyping/unification: default_occurrence_test takes a frozen_evars set export elim_flags_evars to compute frozen evars before elim - evarsolve: fix evar_define doing check in the wrong order, as conv_algo can trigger the definition of the evar itself, define it first in the evd. - w_unify: disallow HO in consider_remaining. Only used in rewrite now - use evar_abstraction info - catch second_order_matching NoOccurrence exception in second_order_matching_with_args - unify_with_heuristics in API - second_order_matching: thin evars after abstraction to put in the right env or fail. --- engine/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evd.mli b/engine/evd.mli index 1c852971f5..1f6a0da882 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -104,7 +104,7 @@ type evar_info = { in the solution *) evar_abstract_arguments : Abstraction.t; (** Boolean information over {!evar_hyps}, telling if an hypothesis instance - can be immitated or should stay abstract in HO unification problems + can be imitated or should stay abstract in HO unification problems and inversion (see [second_order_matching_with_args] for its use). *) evar_source : Evar_kinds.t located; (** Information about the evar. *) -- cgit v1.2.3 From 781f050bcfabe02e225f3c1d29ee649610d6d680 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 12:42:04 +0200 Subject: Abstraction naming --- engine/evd.ml | 8 ++++++-- engine/evd.mli | 6 +++++- 2 files changed, 11 insertions(+), 3 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 2d28892e6e..a89a67c287 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -128,11 +128,15 @@ end module Abstraction = struct - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list let identity = [] - let abstract_last l = true :: l + let abstract_last l = Abstract :: l end (* The kinds of existential variables are now defined in [Evar_kinds] *) diff --git a/engine/evd.mli b/engine/evd.mli index 1f6a0da882..fcccb1be5a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -78,7 +78,11 @@ sig end module Abstraction : sig - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list val identity : t -- cgit v1.2.3