path: root/proofs/logic.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *)

open Pp
open Util
open Names
open Nameops
open Evd
open Term
open Termops
open Sign
open Environ
open Reductionops
open Inductive
open Inductiveops
open Typing
open Proof_trees
open Proof_type
open Typeops
open Type_errors
open Coqast
open Retyping
open Evarutil
 
type refiner_error =

  (* Errors raised by the refiner *)
  | BadType of constr * constr * constr
  | OccurMeta of constr
  | OccurMetaGoal of constr
  | CannotApply of constr * constr
  | NotWellTyped of constr
  | NonLinearProof of constr

  (* Errors raised by the tactics *)
  | CannotUnify of constr * constr
  | CannotUnifyBindingType of constr * constr
  | CannotGeneralize of constr
  | IntroNeedsProduct
  | DoesNotOccurIn of constr * identifier
  | NoOccurrenceFound of constr

exception RefinerError of refiner_error

open Pretype_errors

let catchable_exception = function
  | Util.UserError _ | TypeError _ | RefinerError _
  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
    Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) | 
    Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true
  | _ -> false

let error_cannot_unify (m,n) =
  raise (RefinerError (CannotUnify (m,n)))

(* Tells if the refiner should check that the submitted rules do not
   produce invalid subgoals *)
let check = ref false

let without_check tac gl =
  let c = !check in
  check := false;
  try let r = tac gl in check := c; r with e -> check := c; raise e

let with_check = Options.with_option check
   
(************************************************************************)
(************************************************************************)
(* Implementation of the structural rules (moving and deleting
   hypotheses around) *)

let check_clear_forward cleared_ids used_ids whatfor =
  if !check && cleared_ids<>[] then
    Idset.iter
      (fun id' ->
        if List.mem id' cleared_ids then
          error (string_of_id id'^" is used in "^whatfor))
      used_ids

(* The Clear tactic: it scans the context for hypotheses to be removed
   (instead of iterating on the list of identifier to be removed, which
   forces the user to give them in order). *)
let clear_hyps ids gl =
  let env = Global.env() in
  let (nhyps,rmv) =
    Sign.fold_named_context
      (fun (id,c,ty as d) (hyps,rmv) ->
        if List.mem id ids then
          (hyps,id::rmv)
        else begin
          check_clear_forward rmv (global_vars_set_of_decl env d)
            ("hypothesis "^string_of_id id);
          (add_named_decl d hyps, rmv)
        end)
      gl.evar_hyps
      ~init:(empty_named_context,[]) in
  let ncl = gl.evar_concl in
  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
  mk_goal nhyps ncl

(* The ClearBody tactic *)

(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
   returns [tail::(f head (id,_,_) tail)] *)
let apply_to_hyp sign id f =
  let found = ref false in
  let sign' =
    fold_named_context_both_sides
      (fun head (idc,c,ct as d) tail ->
	 if idc = id then begin
	   found := true; f head d tail
	 end else 
	   add_named_decl d head)
      sign ~init:empty_named_context
  in
  if (not !check) || !found then sign' else error "No such assumption"

(* Same but with whole environment *)
let apply_to_hyp2 env id f =
  let found = ref false in
  let env' =
    fold_named_context_both_sides
      (fun env (idc,c,ct as d) tail ->
	 if idc = id then begin
	   found := true; f env d tail
	 end else 
	   push_named d env)
      (named_context env) ~init:(reset_context env)
  in
  if (not !check) || !found then env' else error "No such assumption"

let apply_to_hyp_and_dependent_on sign id f g =
  let found = ref false in
  let sign =
    Sign.fold_named_context
      (fun (idc,_,_ as d) oldest ->
         if idc = id then (found := true; add_named_decl (f d) oldest)
         else if !found then add_named_decl (g d) oldest
         else add_named_decl d oldest)
      sign ~init:empty_named_context
  in
  if (not !check) || !found then sign else error "No such assumption"

let check_typability env sigma c =
  if !check then let _ = type_of env sigma c in () 

let recheck_typability (what,id) env sigma t =
  try check_typability env sigma t
  with _ ->
    let s = match what with
      | None -> "the conclusion"
      | Some id -> "hypothesis "^(string_of_id id) in
    error
      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
  
let remove_hyp_body env sigma id =
  apply_to_hyp2 env id
    (fun env (_,c,t) tail ->
       match c with
         | None -> error ((string_of_id id)^" is not a local definition")
         | Some c ->
             let env' = push_named (id,None,t) env in
             if !check then 
               ignore
                 (Sign.fold_named_context 
                    (fun (id',c,t as d) env'' ->
                       (match c with
                          | None -> 
                              recheck_typability (Some id',id) env'' sigma t
                          | Some b ->
                              let b' = mkCast (b,t) in
                              recheck_typability (Some id',id) env'' sigma b');
                       push_named d env'')
                    (List.rev tail) ~init:env');
             env')


(* Auxiliary functions for primitive MOVE tactic
 *
 * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
 * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
 * left side [left] of the full signature if [toleft=true] or to the hyps 
 * on the right side [right] if [toleft=false].
 * If [with_dep] then dependent hypotheses are moved accordingly. *)

let split_sign hfrom hto l =
  let rec splitrec left toleft = function
    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
    | (hyp,c,typ) as d :: right ->
      	if hyp = hfrom then 
	  (left,right,d,toleft) 
      	else 
	  splitrec (d::left) (toleft or (hyp = hto)) right
  in 
  splitrec [] false l

let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
  let env = Global.env() in
  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
    if toleft
    then occur_var_in_decl env hyp2 d
    else occur_var_in_decl env hyp d2
  in
  let rec moverec first middle = function
    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
    | (hyp,_,_) as d :: right ->
	let (first',middle') =
      	  if List.exists (test_dep d) middle then 
	    if with_dep & (hyp <> hto) then 
	      (first, d::middle)
            else 
	      error 
		("Cannot move "^(string_of_id idfrom)^" after "
		 ^(string_of_id hto)
		 ^(if toleft then ": it occurs in " else ": it depends on ")
		 ^(string_of_id hyp))
          else 
	    (d::first, middle)
	in
      	if hyp = hto then 
	  (List.rev first')@(List.rev middle')@right
      	else 
	  moverec first' middle' right
  in
  if toleft then 
    List.rev_append (moverec [] [declfrom] left) right
  else 
    List.rev_append left (moverec [] [declfrom] right)

let check_backward_dependencies sign d =
  if not (Idset.for_all
	    (fun id -> mem_named_context id sign)
	    (global_vars_set_of_decl (Global.env()) d))
  then
    error "Can't introduce at that location: free variable conflict"


let check_forward_dependencies id tail =
  let env = Global.env() in
  List.iter
    (function (id',_,_ as decl) ->
       if occur_var_in_decl env id decl then
	 error ((string_of_id id) ^ " is used in hypothesis " 
		^ (string_of_id id')))
    tail


let rename_hyp id1 id2 sign =
  apply_to_hyp_and_dependent_on sign id1
    (fun (_,b,t) -> (id2,b,t))
    (map_named_declaration (replace_vars [id1,mkVar id2]))

let replace_hyp sign id d =
  apply_to_hyp sign id
    (fun sign _ tail ->
       if !check then
	 (check_backward_dependencies sign d;
	  check_forward_dependencies id tail);
       add_named_decl d sign)

let insert_after_hyp sign id d =
  apply_to_hyp sign id
    (fun sign d' _ ->
       if !check then check_backward_dependencies sign d;
       add_named_decl d (add_named_decl d' sign))

(************************************************************************)
(************************************************************************)
(* Implementation of the logical rules *)

(* Will only be used on terms given to the Refine rule which have meta 
variables only in Application and Case *)

let collect_meta_variables c = 
  let rec collrec acc c = match kind_of_term c with
    | Meta mv -> mv::acc
    | Cast(c,_) -> collrec acc c
    | (App _| Case _) -> fold_constr collrec acc c
    | _ -> acc
  in 
  List.rev(collrec [] c)

let check_conv_leq_goal env sigma arg ty conclty =
  if !check & not (is_conv_leq env sigma ty conclty) then 
    raise (RefinerError (BadType (arg,ty,conclty)))

let goal_type_of env sigma c =
  (if !check then type_of else Retyping.get_type_of) env sigma c

let rec mk_refgoals sigma goal goalacc conclty trm =
  let env = evar_env goal in
  let hyps = goal.evar_hyps in
(*
   if  not (occur_meta trm) then
    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
    let _ = conv_leq_goal env sigma trm t'ty conclty in
      (goalacc,t'ty)
  else
*)
  match kind_of_term trm with
    | Meta _ ->
	if occur_meta conclty then
          raise (RefinerError (OccurMetaGoal conclty));
	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty

    | Cast (t,ty) ->
	check_typability env sigma ty;
	check_conv_leq_goal env sigma trm ty conclty;
	mk_refgoals sigma goal goalacc ty t

    | App (f,l) ->
	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
	let (acc'',conclty') =
	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
	check_conv_leq_goal env sigma trm conclty' conclty;
        (acc'',conclty')

    | Case (_,p,c,lf) ->
	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
	check_conv_leq_goal env sigma trm conclty' conclty;
	let acc'' = 
	  array_fold_left2
            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
            acc' lbrty lf 
	in
	(acc'',conclty')

    | _ -> 
	if occur_meta trm then raise (RefinerError (OccurMeta trm));
      	let t'ty = goal_type_of env sigma trm in
	check_conv_leq_goal env sigma trm t'ty conclty;
        (goalacc,t'ty)

(* Same as mkREFGOALS but without knowing te type of the term. Therefore,
 * Metas should be casted. *)

and mk_hdgoals sigma goal goalacc trm =
  let env = evar_env goal in
  let hyps = goal.evar_hyps in
  match kind_of_term trm with
    | Cast (c,ty) when isMeta c ->
	check_typability env sigma ty;
	(mk_goal hyps (nf_betaiota ty))::goalacc,ty

    | App (f,l) ->
	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
	mk_arggoals sigma goal acc' hdty (Array.to_list l)

    | Case (_,p,c,lf) ->
	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
	let acc'' = 
	  array_fold_left2
            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
            acc' lbrty lf 
	in
	(acc'',conclty')

    | _ -> goalacc, goal_type_of env sigma trm

and mk_arggoals sigma goal goalacc funty = function
  | [] -> goalacc,funty
  | harg::tlargs as allargs ->
      let t = whd_betadeltaiota (evar_env goal) sigma funty in
      match kind_of_term t with
	| Prod (_,c1,b) ->
	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
	| LetIn (_,c1,_,b) ->
	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
	| _ -> raise (RefinerError (CannotApply (t,harg)))

and mk_casegoals sigma goal goalacc p c =
  let env = evar_env goal in
  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
  let pj = {uj_val=p; uj_type=pt} in 
  let indspec =
    try find_mrectype env sigma ct
    with Not_found -> anomaly "mk_casegoals" in
  let (lbrty,conclty) =
    type_case_branches_with_names env indspec pj c in
  (acc'',lbrty,conclty)


let error_use_instantiate () =
  errorlabstrm "Logic.prim_refiner"
    (str"cannot intro when there are open metavars in the domain type" ++
       spc () ++ str"- use Instantiate")

let convert_hyp sign sigma (id,b,bt as d) =
  apply_to_hyp sign id
    (fun sign (_,c,ct) _ ->
       let env = Global.env_of_context sign in
       if !check && not (is_conv env sigma bt ct) then
	 (* Just a warning in V8.0bugfix for compatibility *)
	 msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ 
	       str " (not well-typed in current signature)");
       if !check && not (option_compare (is_conv env sigma) b c) then
	 msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++
	       str " (not well-typed in current signature)");
       add_named_decl d sign)


(************************************************************************)
(************************************************************************)
(* Primitive tactics are handled here *)

let prim_refiner r sigma goal =
  let env = evar_env goal in
  let sign = goal.evar_hyps in
  let cl = goal.evar_concl in
  match r with
    (* Logical rules *)
    | Intro id ->
    	if !check && mem_named_context id sign then
	  error "New variable is already declared";
        (match kind_of_term (strip_outer_cast cl) with
	   | Prod (_,c1,b) ->
	       if occur_meta c1 then error_use_instantiate();
	       let sg = mk_goal (add_named_decl (id,None,c1) sign)
			  (subst1 (mkVar id) b) in
	       [sg]
	   | LetIn (_,c1,t1,b) ->
	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
	       let sg =
		 mk_goal (add_named_decl (id,Some c1,t1) sign)
		   (subst1 (mkVar id) b) in
	       [sg]
	   | _ ->
	       raise (RefinerError IntroNeedsProduct))
	
    | Intro_replacing id ->
	(match kind_of_term (strip_outer_cast cl) with
           | Prod (_,c1,b) ->
	       if occur_meta c1 then error_use_instantiate();
	       let sign' = replace_hyp sign id (id,None,c1) in
	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
	       [sg]
           | LetIn (_,c1,t1,b) ->
	       if occur_meta c1 then error_use_instantiate();
	       let sign' = replace_hyp sign id (id,Some c1,t1) in
	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
	       [sg]
	   | _ ->
	       raise (RefinerError IntroNeedsProduct))
	
    | Cut (b,id,t) ->
    	if !check && mem_named_context id sign then
	  error "New variable is already declared";
        if occur_meta t then error_use_instantiate();
        let sg1 = mk_goal sign (nf_betaiota t) in
        let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
        if b then [sg1;sg2] else [sg2;sg1]  

    | FixRule (f,n,rest) ->
     	let rec check_ind env k cl = 
          match kind_of_term (strip_outer_cast cl) with 
            | Prod (na,c1,b) -> 
            	if k = 1 then 
		  try 
		    fst (find_inductive env sigma c1)
		  with Not_found -> 
		    error "cannot do a fixpoint on a non inductive type"
            	else 
		  check_ind (push_rel (na,None,c1) env) (k-1) b
            | _ -> error "not enough products"
	in
	let (sp,_) = check_ind env n cl in
	let all = (f,n,cl)::rest in
     	let rec mk_sign sign = function 
	  | (f,n,ar)::oth ->
	      let (sp',_)  = check_ind env n ar in 
	      if not (sp=sp') then 
		error ("fixpoints should be on the same " ^ 
		       "mutual inductive declaration");
	      if !check && mem_named_context f sign then 
		error "name already used in the environment";
	      mk_sign (add_named_decl (f,None,ar) sign) oth
	  | [] -> 
	      List.map (fun (_,_,c) -> mk_goal sign c) all
	in 
	mk_sign sign all
	
    | Cofix (f,others) ->
     	let rec check_is_coind env cl = 
	  let b = whd_betadeltaiota env sigma cl in
          match kind_of_term b with
            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
            | _ -> 
		try 
		  let _ = find_coinductive env sigma b in ()
                with Not_found -> 
		  error ("All methods must construct elements " ^
			  "in coinductive types")
	in
	let all = (f,cl)::others in
     	List.iter (fun (_,c) -> check_is_coind env c) all;
        let rec mk_sign sign = function 
          | (f,ar)::oth ->
	      (try
                (let _ = Sign.lookup_named f sign in
                error "name already used in the environment")
              with
              |	Not_found ->
                  mk_sign (add_named_decl (f,None,ar) sign) oth)
	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
     	in 
	mk_sign sign all

    | Refine c ->
        if not (list_distinct (collect_meta_variables c)) then
          raise (RefinerError (NonLinearProof c));
	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
	let sgl = List.rev sgl in
	sgl

    (* Conversion rules *)
    | Convert_concl cl' ->
	check_typability env sigma cl';
	if (not !check) || is_conv_leq env sigma cl' cl then
          let sg = mk_goal sign cl' in
          [sg]
	else 
	  error "convert-concl rule passed non-converting term"

    | Convert_hyp (id,copt,ty) ->
	[mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]

    (* And now the structural rules *)
    | Thin ids -> 
	[clear_hyps ids goal]

    | ThinBody ids ->
	let clear_aux env id =
          let env' = remove_hyp_body env sigma id in
          if !check then recheck_typability (None,id) env' sigma cl;
          env'
	in
	let sign' = named_context (List.fold_left clear_aux env ids) in
     	let sg = mk_goal sign' cl in
     	[sg]

    | Move (withdep, hfrom, hto) ->
  	let (left,right,declfrom,toleft) = split_sign hfrom hto sign in
  	let hyps' = 
	  move_after withdep toleft (left,declfrom,right) hto in
  	[mk_goal hyps' cl]

    | Rename (id1,id2) ->
        if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
          error ((string_of_id id2)^" is already used");
        let sign' = rename_hyp id1 id2 sign in
        let cl' = replace_vars [id1,mkVar id2] cl in
        [mk_goal sign' cl']

(************************************************************************)
(************************************************************************)
(* Extracting a proof term from the proof tree *)

(* Util *)
let rec rebind id1 id2 = function
  | [] -> []
  | id::l -> 
      if id = id1 then id2::l else
        let l' = rebind id1 id2 l in
        if id = id2 then
          (* TODO: find a more elegant way to hide a variable *)
          (id_of_string "_@")::l'
        else id::l'

let prim_extractor subfun vl pft =
  let cl = pft.goal.evar_concl in
  match pft.ref with
    | Some (Prim (Intro id), [spf]) ->
	(match kind_of_term (strip_outer_cast cl) with
	   | Prod (_,ty,_) ->
	       let cty = subst_vars vl ty in
	       mkLambda (Name id, cty, subfun (id::vl) spf)
	   | LetIn (_,b,ty,_) ->
	       let cb = subst_vars vl b in
	       let cty = subst_vars vl ty in
	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
	   | _ -> error "incomplete proof!")
	
    | Some (Prim (Intro_replacing id),[spf]) ->
	(match kind_of_term (strip_outer_cast cl) with
	   | Prod (_,ty,_) ->
	       let cty = subst_vars vl ty in
	       mkLambda (Name id, cty, subfun (id::vl) spf)
	   | LetIn (_,b,ty,_) ->
	       let cb = subst_vars vl b in
	       let cty = subst_vars vl ty in
	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
	   | _ -> error "incomplete proof!")

    | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)

    | Some (Prim (FixRule (f,n,others)),spfl) ->
	let all = Array.of_list ((f,n,cl)::others) in
	let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in
	let names = Array.map (fun (f,_,_) -> Name f) all in
	let vn = Array.map (fun (_,n,_) -> n-1) all in
	let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in
	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
	mkFix ((vn,0),(names,lcty,lfix))	

    | Some (Prim (Cofix (f,others)),spfl) ->
	let all = Array.of_list ((f,cl)::others) in
	let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in
	let names  = Array.map (fun (f,_) -> Name f) all in
	let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in 
	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
	mkCoFix (0,(names,lcty,lfix))
	  
    | Some (Prim (Refine c),spfl) ->
	let mvl = collect_meta_variables c in
	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
	let cc = subst_vars vl c in 
	plain_instance metamap cc

    (* Structural and conversion rules do not produce any proof *)
    | Some (Prim (Convert_concl _),[pf]) ->
	subfun vl pf
	
    | Some (Prim (Convert_hyp _),[pf]) ->
	subfun vl pf

    | Some (Prim (Thin _),[pf]) ->
     (* No need to make ids Anonymous in vl: subst_vars take the more recent *)
	subfun vl pf
	
    | Some (Prim (ThinBody _),[pf]) ->
	subfun vl pf
	
    | Some (Prim (Move _),[pf]) ->
	subfun vl pf

    | Some (Prim (Rename (id1,id2)),[pf]) ->
	subfun (rebind id1 id2 vl) pf

    | Some _ -> anomaly "prim_extractor"

    | None-> error "prim_extractor handed incomplete proof"
	  
(* Pretty-printer *)

open Printer

let prterm x = prterm_env (Global.env()) x

let pr_prim_rule_v7 = function
  | Intro id -> 
      str"Intro " ++ pr_id id
	
  | Intro_replacing id -> 
      (str"intro replacing "  ++ pr_id id)
	
  | Cut (b,id,t) ->
      if b then
        (str"Assert " ++ prterm t)
      else
        (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
	
  | FixRule (f,n,[]) ->
      (str"Fix " ++ pr_id f ++ str"/" ++ int n)
      
  | FixRule (f,n,others) -> 
      let rec print_mut = function
	| (f,n,ar)::oth -> 
           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
        | [] -> mt () in
      (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
         str" with " ++ print_mut others)

  | Cofix (f,[]) ->
      (str"Cofix " ++ pr_id f)

  | Cofix (f,others) ->
      let rec print_mut = function
	| (f,ar)::oth ->
	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
        | [] -> mt () in
      (str"Cofix " ++ pr_id f ++  str" with " ++ print_mut others)

  | Refine c -> 
      str(if occur_meta c then "Refine " else "Exact ") ++
      Constrextern.with_meta_as_hole prterm c
      
  | Convert_concl c ->
      (str"Change "  ++ prterm c)
      
  | Convert_hyp (id,None,t) ->
      (str"Change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)

  | Convert_hyp (id,Some c,t) ->
      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "
       ++ pr_id id ++ str" (Type of "  ++ pr_id id ++ str ")")
      
  | Thin ids ->
      (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
      
  | ThinBody ids ->
      (str"ClearBody "  ++ prlist_with_sep pr_spc pr_id ids)
      
  | Move (withdep,id1,id2) ->
      (str (if withdep then "Dependent " else "") ++
	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)

  | Rename (id1,id2) ->
      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)

let pr_prim_rule_v8 = function
  | Intro id -> 
      str"intro " ++ pr_id id
	
  | Intro_replacing id -> 
      (str"intro replacing "  ++ pr_id id)
	
  | Cut (b,id,t) ->
      if b then
        (str"assert " ++ prterm t)
      else
        (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
	
  | FixRule (f,n,[]) ->
      (str"fix " ++ pr_id f ++ str"/" ++ int n)
      
  | FixRule (f,n,others) -> 
      let rec print_mut = function
	| (f,n,ar)::oth -> 
           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
        | [] -> mt () in
      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
         str" with " ++ print_mut others)

  | Cofix (f,[]) ->
      (str"cofix " ++ pr_id f)

  | Cofix (f,others) ->
      let rec print_mut = function
	| (f,ar)::oth ->
	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
        | [] -> mt () in
      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)

  | Refine c -> 
      str(if occur_meta c then "refine " else "exact ") ++
      Constrextern.with_meta_as_hole prterm c
      
  | Convert_concl c ->
      (str"change "  ++ prterm c)
      
  | Convert_hyp (id,None,t) ->
      (str"change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)

  | Convert_hyp (id,Some c,t) ->
      (str"change "  ++ prterm c  ++ spc ()  ++ str"in "
       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
      
  | Thin ids ->
      (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
      
  | ThinBody ids ->
      (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
      
  | Move (withdep,id1,id2) ->
      (str (if withdep then "dependent " else "") ++
	 str"move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)

  | Rename (id1,id2) ->
      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)

let pr_prim_rule t =
  if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t