diff options
| -rw-r--r-- | proofs/clenv.ml | 125 | ||||
| -rw-r--r-- | proofs/clenv.mli | 31 |
2 files changed, 156 insertions, 0 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 3ef346634..946e67b0e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -544,3 +544,128 @@ let pr_clenv clenv = (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) + +(****************************************************************) +(** Evar version of mk_clenv *) + +type hole = { + hole_evar : constr; + hole_type : types; + hole_deps : bool * bool; + hole_name : Name.t; +} + +type clause = { + cl_holes : hole list; + cl_concl : types; +} + +let make_evar_clause env sigma bound t = + (** FIXME: do the renaming online *) + let t = rename_bound_vars_as_displayed [] [] t in + let rec clrec (sigma, holes) n t = match n, kind_of_term t with + | (Some 0, _) -> (sigma, holes, t) + | (n, Cast (t, _, _)) -> clrec (sigma, holes) n t + | (n, Prod (na, t1, t2)) -> + let store = Typeclasses.set_resolvable Evd.Store.empty false in + let sigma, ev = new_evar ~store env sigma t1 in + let dep = dependent (mkRel 1) t2 in + let hole = { + hole_evar = ev; + hole_type = t1; + hole_deps = (dep, dep); + (* We fix it later *) + hole_name = na; + } in + let t2 = if dep then subst1 ev t2 else t2 in + clrec (sigma, hole :: holes) (Option.map ((+) (-1)) n) t2 + | (n, LetIn (na, b, _, t)) -> clrec (sigma, holes) n (subst1 b t) + | (n, _) -> (sigma, holes, t) + in + let (sigma, holes, t) = clrec (sigma, []) bound t in + let fold holes h = + if fst h.hole_deps then + (** Some subsequent term uses the hole *) + let (ev, _) = destEvar h.hole_evar in + let is_dep hole = occur_evar ev hole.hole_type in + let in_hyp = List.exists is_dep holes in + let in_ccl = occur_evar ev t in + let h = { h with hole_deps = (in_hyp, in_ccl) } in + h :: holes + else + (** The hole does not occur anywhere *) + h :: holes + in + let holes = List.fold_left fold [] holes in + let clause = { cl_concl = t; cl_holes = holes } in + (sigma, clause) + +let explain_no_such_bound_variable holes id = + let fold h accu = match h.hole_name with + | Anonymous -> accu + | Name id -> id :: accu + in + let mvl = List.fold_right fold holes [] in + let expl = match mvl with + | [] -> str " (no bound variables at all in the expression)." + | [id] -> str "(possible name is: " ++ pr_id id ++ str ")." + | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")." + in + errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl) + +let evar_with_name holes id = + let map h = match h.hole_name with + | Anonymous -> None + | Name id' -> if Id.equal id id' then Some h else None + in + let hole = List.map_filter map holes in + match hole with + | [] -> explain_no_such_bound_variable holes id + | [h] -> h.hole_evar + | _ -> + errorlabstrm "" + (str "Binder name \"" ++ pr_id id ++ + str "\" occurs more than once in clause.") + +let evar_of_binder holes = function +| NamedHyp s -> evar_with_name holes s +| AnonHyp n -> + try + let h = List.nth holes (pred n) in + h.hole_evar + with e when Errors.noncritical e -> + errorlabstrm "" (str "No such binder.") + +let define_with_type sigma env ev c = + let t = Retyping.get_type_of env sigma ev in + let ty = Retyping.get_type_of env sigma c in + let j = Environ.make_judge c ty in + let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in + let (ev, _) = destEvar ev in + let sigma = Evd.define ev j.Environ.uj_val sigma in + sigma + +let solve_evar_clause env sigma hyp_only clause = function +| NoBindings -> sigma +| ImplicitBindings largs -> + let map h = + let (in_hyp, in_ccl) = h.hole_deps in + let depends = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in + if depends then Some h.hole_evar else None + in + let evs = List.map_filter map clause.cl_holes in + let len = List.length evs in + if Int.equal len (List.length largs) then + let fold sigma ev arg = define_with_type sigma env ev arg in + let sigma = List.fold_left2 fold sigma evs largs in + sigma + else + error_not_right_number_missing_arguments len +| ExplicitBindings lbind -> + let () = check_bindings lbind in + let fold sigma (_, binder, c) = + let ev = evar_of_binder clause.cl_holes binder in + define_with_type sigma env ev c + in + let sigma = List.fold_left fold sigma lbind in + sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 35bed8f40..b57178cd4 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Environ open Evd @@ -105,3 +106,33 @@ val clenv_push_prod : clausenv -> clausenv (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.std_ppcmds +(** {6 Evar version} *) + +type hole = { + hole_evar : constr; + hole_type : types; + hole_deps : bool * bool; + (** Dependent in hypotheses then in conclusion *) + hole_name : Name.t; +} + +type clause = { + cl_holes : hole list; + cl_concl : types; +} + +val make_evar_clause : env -> evar_map -> int option -> types -> + (evar_map * clause) +(** An evar version of {!make_clenv_binding}. Given a type [t], + [evar_environments env sigma n t bl] tries to eliminate at most [n] products + of the type [t] by filling it with evars. It returns the resulting type + together with the list of holes generated. Assumes that [t] is well-typed + in the environment. *) + +val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings -> + evar_map +(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained + in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in + the environment. The boolean [hyps] is a compatibility flag that allows to + consider arguments to be dependent only when they appear in hypotheses and + not in the conclusion. *) |