Notation concise pour la valeur par défaut des cas reconnus comme

impossibles dans un filtrage dépendant.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 39 insertions, 11 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index de1599ab0..761c44b71 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -673,6 +673,7 @@ Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and
 Julien Forest acted as maintainers of features they implemented in
 previous versions of Coq.
 
+Julien Narboux contributed to CoqIDE.
 Nicolas Tabareau made the adaptation of the interface of the old
 ``setoid rewrite'' tactic to the new version. Lionel Mamane worked on
 the interaction between Coq and its external interfaces. With Samuel
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ca3347dbb..73614797a 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -109,6 +109,14 @@ let arith_module = make_dir ["Coq";"Arith";"Arith"]
 
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_kn dir id
+let make_con dir id = Libnames.encode_con dir id
+
+(** Identity *)
+
+let id = make_con datatypes_module (id_of_string "id")
+let type_of_id = make_con datatypes_module (id_of_string "ID")
+
+let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
 
 (** Natural numbers *)
 let nat_kn = make_kn datatypes_module (id_of_string "nat")
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2f2cb64be..9d65e5978 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,6 +63,27 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 =
 let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
+(**********************************************************************)
+(* Functions to deal with impossible cases *)
+
+let impossible_default_case = ref None
+
+let set_impossible_default_clause c = impossible_default_case := Some c
+
+let coq_unit_judge =
+  let na1 = Name (id_of_string "A") in
+  let na2 = Name (id_of_string "H") in
+  fun () -> 
+    match !impossible_default_case with
+    | Some (id,type_of_id) ->
+	make_judge id type_of_id
+    | None -> 
+	(* In case the constants id/ID are not defined *)
+	make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+                 (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)))
+
+(**********************************************************************)
+
 module type S = sig
   val compile_cases :
     loc -> case_style ->
@@ -520,15 +541,6 @@ let extract_rhs pb =
         eqn.rhs
 
 (**********************************************************************)
-(* Functions to deal with impossible cases *)
-
-let coq_unit_judge =
-  let na1 = Name (id_of_string "A") in
-  let na2 = Name (id_of_string "H") in
-  { uj_val = mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1));
-    uj_type =  mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)) }
-
-(**********************************************************************)
 (* Functions to deal with matrix factorization *)
 
 let occur_in_rhs na rhs =
@@ -909,7 +921,8 @@ let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
     match kind_of_term (whd_evar (evars_of !(pb.evdref)) pred) with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase ->
-	pb.evdref := Evd.evar_define evk coq_unit_judge.uj_type !(pb.evdref);
+	let default = (coq_unit_judge ()).uj_type in
+	pb.evdref := Evd.evar_define evk default !(pb.evdref);
       (* we add an "assert false" case *)
       let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in
       let aliasnames =
@@ -1816,7 +1829,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     (* A typing function that provides with a canonical term for absurd cases*)
     let typing_fun tycon env evdref = function
     | Some t ->	typing_fun tycon env evdref t
-    | None -> coq_unit_judge in
+    | None -> coq_unit_judge () in
 
     let pb =
       { env       = env;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ee01d2e71..4b203586a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -46,6 +46,7 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -
 
 val error_needs_inversion : env -> constr -> types -> 'a
 
+val set_impossible_default_clause : constr * types -> unit
 (*s Compilation of pattern-matching. *)
 
 type alias_constr =
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 3525908ab..eb12be1a0 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -182,6 +182,11 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
+(** Identity *)
+
+Definition ID := forall A:Type, A -> A.
+Definition id : ID := fun A x => x.
+
 (* begin hide *)
 
 (* Compatibility *)