The fresh_name generator has been moved to ProofEngineHelpers.

intros_tac now directly uses it ==> no more ~mkname arguments.
The generator has been "improved" so that it does not generate any
more two equal names. The drawback is that every identifier is
augmented with a nonce.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 9076ae70fffce795573bb6733e8140a60e73da04..bb1c2febf583893ed8c81fe387908782c39b0d3f 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1004,8 +1004,7 @@ let assumption_tac ~status:(proof,goal)=
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
                 (*inutile sia questo che quello prima  della chiamata*)
-               ~start:
-                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
+               ~start:PrimitiveTactics.intros_tac
                ~continuation:(Tacticals.then_ 
                        ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1045,11 +1044,11 @@ theoreme,so let's parse our thesis *)
 
    (* now let's change our thesis applying the th and put it with hp *) 
 
-   let proof,gl = Tacticals.then_ 
-       ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:
-          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
-               ~status:(s_proof,s_goal) in
+   let proof,gl =
+    Tacticals.then_ 
+     ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+     ~continuation:PrimitiveTactics.intros_tac
+     ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in
 

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index eba2d571ff8d4fc26ed633f375f3be1fd89872cd..9a037d754d8acc3c37adbc830c41f90c382143fa 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -43,11 +43,7 @@ let lambda_abstract context newmeta ty mknames =
    function
       C.Cast (te,_)   -> collect_context context te
     | C.Prod (n,s,t)  ->
-       let n' =
-        match n with
-           C.Name _ -> n
-         | C.Anonymous -> C.Name (mknames ())
-       in
+       let n' = C.Name (mknames n) in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
         in
@@ -305,13 +301,15 @@ let apply_tac ~term ~status =
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~mknames ~status:(proof, goal) =
+let intros_tac ~status:(proof, goal) =
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta = new_meta ~proof in
-    let (context',ty',bo') = lambda_abstract context newmeta ty mknames in
+    let (context',ty',bo') =
+     lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name)
+    in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
@@ -507,7 +505,7 @@ let elim_simpl_intros_tac ~term =
   ~continuation:
    (Tacticals.then_
      ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
-     ~continuation:(intros_tac ~mknames:(function () -> "FOO")))
+     ~continuation:intros_tac)
 ;;
 
 

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 1fa97805ac50356a407448f5ca206c0a55fecd2b..59a714c78c938e3144f963a12390b54d332451f0 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -28,7 +28,7 @@ val apply_tac:
 val exact_tac:
   term: Cic.term -> ProofEngineTypes.tactic
 val intros_tac:
-  mknames: (unit -> string) -> ProofEngineTypes.tactic
+  ProofEngineTypes.tactic
 val cut_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 val letin_tac:

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 73e2aa177dfa76a0d8280b8f0813bf4f52e3d602..7b4c68ab54a9884e88baeae1acf4d970038348d8 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -136,13 +136,6 @@ let perforate context term ty =
 (*                  Some easy tactics.                      *)
 (************************************************************)
 
-(*CSC: generatore di nomi? Chiedere il nome? *)
-let fresh_name =
- let next_fresh_index = ref 0 in
-  function () ->
-   incr next_fresh_index ;
-   "fresh_name" ^ string_of_int !next_fresh_index
-
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function term ty =
  let metasenv =
@@ -172,8 +165,7 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 
 let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
-let intros () =
-  apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name)
+let intros () = apply_tactic PrimitiveTactics.intros_tac
 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index d191340ea88b8882a290c100bfc51b0d95f07714..74b6fcdaca1f344032da1afc7df9c393f30f9206 100644 (file)
--- a/helm/gTopLevel/proofEngineHelpers.ml
+++ b/helm/gTopLevel/proofEngineHelpers.ml
@@ -23,6 +23,17 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*CSC: generatore di nomi? Chiedere il nome? *)
+let fresh_name =
+ let next_fresh_index = ref 0 in
+  function
+     Cic.Anonymous ->
+      incr next_fresh_index ;
+      "fresh_name" ^ string_of_int !next_fresh_index
+   | Cic.Name name ->
+      incr next_fresh_index ;
+      name ^ string_of_int !next_fresh_index
+
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)

diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli
index c5593235c79b593f7cfa0078f256ada8d1f84849..de0b375960ffa6fe190e40576cb2da849b42b088 100644 (file)
--- a/helm/gTopLevel/proofEngineHelpers.mli
+++ b/helm/gTopLevel/proofEngineHelpers.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+val fresh_name : Cic.name -> string
+
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 95b74ab99c7dde663a5a437cf5ce9da4f5fc1d5c..fc6897bafc9d8afa548a4bd5722705da0c6c0f0e 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -189,7 +189,7 @@ let contradiction_tac ~status =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    T.then_ 
-      ~start: (P.intros_tac ~mknames:(function () -> "FOO")) 
+      ~start:P.intros_tac
       ~continuation:(
         T.then_ 
            ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) 
@@ -495,8 +495,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                                                        (* quale uguaglianza usare, eq o eqT ? *)
               ~continuations:[
                 T.then_ 
-                   ~start:
-                     (P.intros_tac ~mknames:(function () ->"dummy_for_replace"))
+                   ~start:P.intros_tac
                    ~continuation:(T.then_ 
                                      ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
                                      ~continuation:(ProofEngineStructuralRules.clear