From bf7d2a3ad2535e7d57db79c17c81aaf67d956965 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 1 Jun 2014 10:26:41 +0200
Subject: Use of "H"-based names for propositional hypotheses obtained by
 destruction of schemes in Type such as sumbool.

Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).

This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.

Examples:

*** Non dependent case ***

Goal {True}+{False}-> True.
intros [|].

Before:

  t : True
  ============================
   True

and

  f : False
  ============================
   True

After:

  H : True
  ============================
   True

  H : False
  ============================
   True

*** Dependent case ***

Goal forall x:{True}+{False}, x=x.
intros [|].

Before:

  t : True
  ============================
   left t = left t

  f : False
  ============================
   right f = right f

After:

  HTrue : True
  ============================
   left HTrue = left HTrue

  HFalse : False
  ============================
   right HFalse = right HFalse
---
 pretyping/namegen.ml | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

(limited to 'pretyping/namegen.ml')

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index c6c21f025..0581f7283 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -61,6 +61,20 @@ let is_constructor id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
+let head_name c = (* Find the head constant of a constr if any *)
+  let rec hdrec c =
+    match kind_of_term c with
+    | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
+    | Cast (c,_,_) | App (c,_) -> hdrec c
+    | Proj (kn,_) -> Some (Label.to_id (con_label kn))
+    | Const _ | Ind _ | Construct _ | Var _ ->
+	Some (basename_of_global (global_of_constr c))
+    | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
+	Some (match lna.(i) with Name id -> id | _ -> assert false)
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+  in
+  hdrec c
+
 let lowercase_first_char id = (* First character of a constr *)
   Unicode.lowercase_first_char (Id.to_string id)
 
@@ -71,11 +85,8 @@ let sort_hdchar = function
 let hdchar env c =
   let rec hdrec k c =
     match kind_of_term c with
-    | Prod (_,_,c)    -> hdrec (k+1) c
-    | Lambda (_,_,c)  -> hdrec (k+1) c
-    | LetIn (_,_,_,c) -> hdrec (k+1) c
-    | Cast (c,_,_)    -> hdrec k c
-    | App (f,l)       -> hdrec k f
+    | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
+    | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_)
     | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
     | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
@@ -89,13 +100,10 @@ let hdchar env c =
 	     | (Name id,_,_)   -> lowercase_first_char id
 	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
-    | Fix ((_,i),(lna,_,_)) ->
-	let id = match lna.(i) with Name id -> id | _ -> assert false in
-	lowercase_first_char id
-    | CoFix (i,(lna,_,_)) ->
+    | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	let id = match lna.(i) with Name id -> id | _ -> assert false in
 	lowercase_first_char id
-    | Meta _|Evar _|Case (_, _, _, _) -> "y"
+    | Meta _ | Evar _ | Case (_, _, _, _) -> "y"
   in
   hdrec 0 c
 
-- 
cgit v1.2.3