The Coq mailing list

[Pierre Letouzey <letouzey AT lri.fr>]

You may have noticed that Coq V6.x and V7 have slightly different
naming conventions when doing Intro. and Intros. That is quite annoying
when porting codes like the Coq contribs, so I wrote yesterday a small
tool that can help:

In the script, it expands "Intros." into "Intros foo bar."
where "foo bar" are the name Coq would use when doing the "Intros".

So I can expand all the "Intros." with a Coq V6, and then my script is
made of explicit intros that Coq V7 understands (hopefully).

The tool is made of two patches for coq-6.3.1, and some proof-general
macros.

In src/parsing/g_vernac.ml4, after line 454, insert
=======================================================================
      | LIDENT "Show"; LIDENT "Intro";"."-> <:ast< (SHOWINTRO) >>
      | LIDENT "Show"; LIDENT "Intros";"."-> <:ast< (SHOWINTROS) >>
=======================================================================

In src/env/vernacentries.ml, at the end, add
======================================================================
(* Simulate the Intro(s) tactic *)

let next_global_ident_from id avoid =
  let rec next_rec id =
    let id = next_ident_away_from id avoid in
    if (not((Declare.is_global id))) then id
    else  next_rec (lift_ident id)
  in next_rec id;;

let next_global_ident_away id avoid =
  let id  = next_ident_away id avoid in
  if (not((Declare.is_global id))) then id
  else  next_global_ident_from (lift_ident id) avoid;;

let fresh_id avoid id gl =
  next_global_ident_away id (avoid@(ids_of_sign (pf_untyped_hyps gl)));;

let id_of_name = function
    Anonymous -> id_of_string "H"
  | Name id   -> id;;

let rec do_renum avoid gl = function
    [] -> ""
  | [n] -> (string_of_id (fresh_id avoid (id_of_name n) gl))
  | n :: l -> let id = fresh_id avoid (id_of_name n) gl in
        (string_of_id id)^" "^(do_renum (id :: avoid) gl l);;

add("SHOWINTRO", function [] -> (fun () ->
  let pf = get_pftreestate() in
  let gl = nth_goal_of_pftreestate 1 pf in
  let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
  let n = List.hd (List.rev_map fst l) in
  message (string_of_id (fresh_id [] (id_of_name n) gl))));;

add("SHOWINTROS", function [] -> (fun () ->
  let pf = get_pftreestate() in
  let gl = nth_goal_of_pftreestate 1 pf in
  let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
  let l = List.rev_map fst l in
  message (do_renum [] gl l)));;
=====================================================================

After recompiling, this provides two new commands:

Show Intro.
Show Intros.

that show what names coq will use when doing Intro(s).


The following macros can then be used in proof-general:
==================================================================
(defun coq-ShowIntro () ""
  (interactive)
  (proof-shell-invisible-command "Show Intro."))

(defun coq-ShowIntros () ""
  (interactive)
  (proof-shell-invisible-command "Show Intros."))

(defun getline (buf n) "" (interactive)
   (let ((buforig (current-buffer)))
     (progn
        (switch-to-buffer buf)
        (goto-line n)
        (let ((debut (point)))
           (progn
             (end-of-line)
             (let ((chaine (buffer-substring debut (point))))
                (progn
                  (switch-to-buffer buforig)
                  (eval chaine))))))))

(defun coq-ExpandI ()
  "Expand both Intro or Intros"
  (interactive)
  (re-search-forward "Intros? *\\.")
  (re-search-backward "Intros? *\\.")
  (let ((s (looking-at "Intros")))
    (progn
      (proof-assert-until-point)
      (proof-shell-wait)
      (if s
        (coq-ShowIntros)
        (coq-ShowIntro))
      (proof-shell-wait)
      (re-search-forward "Intros?")
      (insert " ")
      (insert (getline "*coq-response*" 2)))))

(defun coq-ExpandIAll ()
  "Expand both Intro or Intros"
  (interactive)
  (while (re-search-forward "Intros? *\\." nil t)
    (progn
      (re-search-backward "Intros? *\\.")
      (let ((s (looking-at "Intros")))
        (progn
          (proof-assert-until-point)
          (proof-shell-wait)
          (if s
            (coq-ShowIntros)
            (coq-ShowIntro))
          (proof-shell-wait)
          (re-search-forward "Intros?")
          (insert " ")
          (insert (getline "*coq-response*" 2)))))))
=============================================================

The coq-ExpandI function plays the script until the next Intro(s).
and then expand it. The coq-ExpandAll do the same thing for all Intro(s).

REMARKS:
* This is higly experimental, but I found it useful.
* No hope for expanding Intro(s) inside a sequence of tactics. Personnaly
I looked at them by hand.
* The patch is for Coq-6.3.1, because it is the source langage of the
translation I was doing yesterday. I will soon make a patch for Coq-7
* Questions/Remarks welcome...



-- 
Pierre Letouzey
---------------
letouzey AT lri.fr
            Tel:01 69 15 42 35 (France)
http://www.eleves.ens.fr:8080/home/letouzey