aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-05-17 17:24:57 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-29 12:16:29 +0200
commit410b3cc1cc0f677e052cfedcee03e14521264b64 (patch)
treeb092df75c1313b6a149366ff9015134547774283
parent5e979cf6020eea9fa0feaa77c7436a29443e35db (diff)
Program: cleanup in cases, add options
Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
-rw-r--r--doc/refman/Program.tex19
-rw-r--r--pretyping/cases.ml20
-rw-r--r--pretyping/cases.mli1
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/program.ml36
-rw-r--r--pretyping/program.mli2
6 files changed, 56 insertions, 26 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 11dd3a051..e07d64cf9 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -63,10 +63,27 @@ will be first rewritten to:
previous one, an inequality is added in the context of the second
branch. See for example the definition of {\tt div2} below, where the second
branch is typed in a context where $\forall p, \_ <> S (S p)$.
-
+
\item Coercion. If the object being matched is coercible to an inductive
type, the corresponding coercion will be automatically inserted. This also
works with the previous mechanism.
+
+\end{itemize}
+
+There are global options to control the generation of equalities
+and coercions.
+
+\begin{itemize}
+\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates
+ the special treatment of pattern-matching generating equalities and
+ inequalities when using Program (it is on by default). All
+ pattern-matchings and let-patterns are handled using the standard
+ algorithm of Coq (see Section~\ref{Caseexpr}) when this options is
+ deactivated.
+\item {\tt Unset Program Generalized Coercion}\optindex{Program
+ Generalized Coercion} This deactivates the coercion of general
+ inductive types when using Program (the option is on by default).
+ Coercion of subset types and pairs is still active in this case.
\end{itemize}
\subsection{Syntactic control over equalities}
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 205a199f7..78c218a50 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1801,14 +1801,10 @@ let build_inversion_problem loc env sigma tms t =
it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
- (* let sigma, s = Evd.new_sort_variable sigma in *)
-(*FIXME TRY *)
- (* let sigma, s = Evd.new_sort_variable univ_flexible sigma in *)
let s' = Retyping.get_sort_of env sigma t in
let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
let sigma = Evd.set_leq_sort env sigma s' s in
let evdref = ref sigma in
- (* let ty = evd_comb1 (refresh_universes false) evdref ty in *)
let pb =
{ env = pb_env;
evdref = evdref;
@@ -1944,7 +1940,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let preds =
match pred, tycon with
- (* No type annotation *)
+ (* No return clause *)
| None, Some t when not (noccur_with_meta 0 max_int t) ->
(* If the tycon is not closed w.r.t real variables, we try *)
(* two different strategies *)
@@ -1981,12 +1977,6 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let evdref = ref sigma in
let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
let sigma = !evdref in
- (* let sigma = Option.cata (fun tycon -> *)
- (* let na = Name (Id.of_string "x") in *)
- (* let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *)
- (* let predinst = extract_predicate predcclj.uj_val tms in *)
- (* Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *)
- (* !evdref tycon in *)
let predccl = (j_nf_evar sigma predcclj).uj_val in
[sigma, predccl]
in
@@ -2436,7 +2426,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
match tycon' with
| None -> let ev = mkExistential env evdref in ev, ev
| Some t ->
- let pred =
+ let pred =
match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
| Some (evd, pred) -> evdref := evd; pred
| None ->
@@ -2515,11 +2505,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
(* Main entry of the matching compilation *)
let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
- if predopt == None && Flags.is_program_mode () then
- compile_program_cases loc style (typing_fun, evdref)
+ if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
+ compile_program_cases loc style (typing_fun, evdref)
tycon env (predopt, tomatchl, eqns)
else
-
+
(* We build the matrix of patterns and right-hand side *)
let matx = matx_of_eqns env eqns in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d7fff8af4..ba566f374 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -121,4 +121,3 @@ val prepare_predicate : Loc.t ->
Context.Rel.t list ->
Constr.constr option ->
'a option -> (Evd.evar_map * Names.name list * Term.constr) list
-
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index cba28f817..65d79bcc8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -192,7 +192,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let term = co x in
Typing.e_solve_evars env evdref term)
in
- if isEvar c || isEvar c' then
+ if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
(* Second-order unification needed. *)
raise NoSubtacCoercion;
aux [] typ typ' 0 (fun x -> x)
@@ -280,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let c1 = coerce_unify env a a' in
let c2 = coerce_unify env b b' in
match c1, c2 with
- None, None -> None
+ | None, None -> None
| _, _ ->
Some
(fun x ->
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 133f83090..253d85742 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -70,18 +70,40 @@ let mk_coq_and l =
(* true = transparent by default, false = opaque if possible *)
let proofs_transparency = ref true
+let program_cases = ref true
+let program_generalized_coercion = ref true
let set_proofs_transparency = (:=) proofs_transparency
let get_proofs_transparency () = !proofs_transparency
+let is_program_generalized_coercion () = !program_generalized_coercion
+let is_program_cases () = !program_cases
+
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "preferred transparency of Program obligations";
- optkey = ["Transparent";"Obligations"];
- optread = get_proofs_transparency;
- optwrite = set_proofs_transparency; }
-
+ { optsync = true;
+ optdepr = false;
+ optname = "preferred transparency of Program obligations";
+ optkey = ["Transparent";"Obligations"];
+ optread = get_proofs_transparency;
+ optwrite = set_proofs_transparency; }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "program cases";
+ optkey = ["Program";"Cases"];
+ optread = (fun () -> !program_cases);
+ optwrite = (:=) program_cases }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "program generalized coercion";
+ optkey = ["Program";"Generalized";"Coercion"];
+ optread = (fun () -> !program_generalized_coercion);
+ optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 765f35580..023ff8ca5 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -39,3 +39,5 @@ val mk_coq_not : constr -> constr
val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
val get_proofs_transparency : unit -> bool
+val is_program_cases : unit -> bool
+val is_program_generalized_coercion : unit -> bool