Removed the distinction between generic Ltac vars and Let/Intro

bindings, which permits using only one environment for interning
terms.

Ltac semantics was sligthly changed, as it required introducing
a lot of additional coercions from goal variables to other types.
Ltac seemed to be quite non-uniform, as it tried to represent
hypotheses with intropatterns, instead of the dedicated var type.

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

8 files changed, 117 insertions, 64 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 00ea3a71b..12d25c785 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -13,7 +13,7 @@ open Mod_subst
 open Genarg
 
 type glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
   ltacrecvars : (Id.t * Nametab.ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 25050fe7c..9fe553cba 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -11,7 +11,7 @@ open Mod_subst
 open Genarg
 
 type glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
   ltacrecvars : (Id.t * Nametab.ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index c4d6a7a30..04c8c3064 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -44,8 +44,7 @@ let intern_constr_or_thesis globs = function
   | This c -> This (intern_constr globs c)
 
 let add_var id globs=
-  let l1,l2=globs.ltacvars in
-    {globs with ltacvars= (id::l1),(id::l2)}
+    {globs with ltacvars = Id.Set.add id globs.ltacvars}
 
 let add_name nam globs=
  match nam with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 70c7f8d1f..cabbd4755 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1459,7 +1459,7 @@ let do_instr raw_instr pts =
       let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma } in
       let env=  pf_env gl in
-      let ist = {ltacvars = ([],[]); ltacrecvars = [];
+      let ist = {ltacvars = Id.Set.empty; ltacrecvars = [];
 		 gsigma = sigma; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0d1a48f50..9318955df 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -88,6 +88,8 @@ let coerce_to_ident fresh env v =
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroIdentifier id -> id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    out_gen (topwit wit_var) v
   else match Value.to_constr v with
   | None -> fail ()
   | Some c ->
@@ -100,6 +102,9 @@ let coerce_to_intro_pattern env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     snd (out_gen (topwit wit_intro_pattern) v)
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    IntroIdentifier id
   else match Value.to_constr v with
   | Some c when isVar c ->
       (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
@@ -134,6 +139,9 @@ let coerce_to_constr env v =
     ([], c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
 let coerce_to_closed_constr env v =
@@ -146,8 +154,12 @@ let coerce_to_evaluable_ref env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id when List.mem id (Termops.ids_of_context env) -> EvalVarRef id
+    | _, IntroIdentifier id when is_variable env id -> EvalVarRef id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    if List.mem id (Termops.ids_of_context env) then EvalVarRef id
+    else fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (destConst c)
@@ -178,6 +190,9 @@ let coerce_to_hyp env v =
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroIdentifier id when is_variable env id -> id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    if is_variable env id then id else fail ()
   else match Value.to_constr v with
   | Some c when isVar c -> destVar c
   | _ -> fail ()
@@ -215,6 +230,9 @@ let coerce_to_quantified_hypothesis v =
     match v with
     | _, IntroIdentifier id -> NamedHyp id
     | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    NamedHyp id
   else if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else raise (CannotCoerceTo "a quantified hypothesis")
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c449cab8d..6f0d7525d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -54,7 +54,7 @@ let skip_metaid = function
 (** Generic arguments *)
 
 type glob_sign = Genintern.glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   ltacrecvars : (Id.t * ltac_constant) list;
      (* ltac recursive names *)
@@ -62,7 +62,7 @@ type glob_sign = Genintern.glob_sign = {
   genv : Environ.env }
 
 let fully_empty_glob_sign =
-  { ltacvars = ([],[]); ltacrecvars = [];
+  { ltacvars = Id.Set.empty; ltacrecvars = [];
     gsigma = Evd.empty; genv = Environ.empty_env }
 
 let make_empty_glob_sign () =
@@ -124,28 +124,28 @@ let lookup_ltacref r = KNmap.find r !mactab
 (* We have identifier <| global_reference <| constr *)
 
 let find_ident id ist =
-  List.mem id (fst ist.ltacvars) or
+  Id.Set.mem id ist.ltacvars ||
   List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 let find_recvar qid ist = List.assoc qid ist.ltacrecvars
 
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
-let find_var id ist = List.mem id (fst ist.ltacvars)
+let find_var id ist = Id.Set.mem id ist.ltacvars
 
 (* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
-let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
+let find_ctxvar id ist = Id.Set.mem id ist.ltacvars
 
 (* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
-let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
+let find_ltacvar id ist = Id.Set.mem id ist.ltacvars
 
 let find_hyp id ist =
   List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
 (* be fresh in which case it is binding later on *)
-let intern_ident l ist id =
+let intern_ident s ist id =
   (* We use identifier both for variables and new names; thus nothing to do *)
-  if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
+  if not (find_ident id ist) then s := Id.Set.add id !s;
   id
 
 let intern_name l ist = function
@@ -304,7 +304,7 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
-  let ltacvars = (fst lfun, Id.Set.empty) in
+  let ltacvars = (Id.Set.elements lfun, Id.Set.empty) in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
   in
@@ -377,6 +377,7 @@ let intern_flag ist red =
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
+  let ltacvars = Id.Set.elements ltacvars, Id.Set.empty in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.gsigma ist.genv ~as_type ~ltacvars pc
   in
@@ -442,13 +443,11 @@ let intern_hyp_location ist ((occs,id),hl) =
    intern_hyp_or_metaid ist id), hl)
 
 (* Reads a pattern *)
-let intern_pattern ist ?(as_type=false) lfun = function
+let intern_pattern ist ?(as_type=false) ltacvars = function
   | Subterm (b,ido,pc) ->
-      let ltacvars = (lfun, Id.Set.empty) in
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
-      let ltacvars = (lfun, Id.Set.empty) in
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       None, metas, Term pc
 
@@ -459,31 +458,37 @@ let intern_constr_may_eval ist = function
   | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
   | ConstrTerm c -> ConstrTerm (intern_constr ist c)
 
+let name_cons accu = function
+| Anonymous -> accu
+| Name id -> Id.Set.add id accu
+
+let opt_cons accu = function
+| None -> accu
+| Some id -> Id.Set.add id accu
 
 (* Reads the hypotheses of a "match goal" rule *)
 let rec intern_match_goal_hyps ist lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
-      let lfun' = name_cons na (Option.List.cons ido lfun) in
+      let lfun' = name_cons (opt_cons lfun ido) na in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
   | (Def ((_,na) as locna,mv,mp))::tl ->
       let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
       let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
-      let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
+      let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
       lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
 
 (* Utilities *)
 let extract_let_names lrc =
-  List.fold_right
-    (fun ((loc,name),_) l ->
-      if List.mem name l then
-	user_err_loc
-	  (loc, "glob_tactic", str "This variable is bound several times.");
-      name::l)
-    lrc []
+  let fold accu ((loc, name), _) =
+    if Id.Set.mem name accu then user_err_loc
+      (loc, "glob_tactic", str "This variable is bound several times.")
+    else Id.Set.add name accu
+  in
+  List.fold_left fold Id.Set.empty lrc
 
 let clause_app f = function
     { onhyps=None; concl_occs=nl } ->
@@ -641,8 +646,8 @@ and intern_tactic_seq onlytac ist = function
       !lf, TacAtom (adjust_loc loc, t)
   | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
   | TacLetIn (isrec,l,u) ->
-      let (l1,l2) = ist.ltacvars in
-      let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
+      let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in
+      let ist' = { ist with ltacvars } in
       let l = List.map (fun (n,b) ->
 	  (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
       ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
@@ -702,9 +707,8 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist
 and intern_pure_tactic ist = intern_tactic true ist
 
 and intern_tactic_fun ist (var,body) =
-  let (l1,l2) = ist.ltacvars in
-  let lfun' = List.rev_append (Option.List.flatten var) l1 in
-  (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
+  let lfun = List.fold_left opt_cons ist.ltacvars var in
+  (var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body)
 
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
@@ -740,11 +744,13 @@ and intern_match_rule onlytac ist = function
   | (All tc)::tl ->
       All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
   | (Pat (rl,mp,tc))::tl ->
-      let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
+      let {ltacvars=lfun; gsigma=sigma; genv=env} = ist in
       let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
       let ido,metas2,pat = intern_pattern ist lfun mp in
-      let metas = List.uniquize (metas1@metas2) in
-      let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
+      let fold accu x = Id.Set.add x accu in
+      let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
+      let ltacvars = List.fold_left fold ltacvars metas2 in
+      let ist' = { ist with ltacvars } in
       Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
@@ -754,7 +760,7 @@ and intern_genarg ist x =
       in_gen (glbwit wit_int_or_var)
         (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
   | IdentArgType b ->
-      let lf = ref ([],[]) in
+      let lf = ref Id.Set.empty in
       in_gen (glbwit (wit_ident_gen b))
 	(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
   | VarArgType ->
@@ -804,9 +810,11 @@ let glob_tactic x =
     (intern_pure_tactic (make_empty_glob_sign ())) x
 
 let glob_tactic_env l env x =
+  let ltacvars =
+    List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
   (intern_pure_tactic
-    { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
+    { ltacvars; ltacrecvars = []; gsigma = Evd.empty; genv = env })
     x
 
 (***************************************************************************)
@@ -939,7 +947,7 @@ let add_tacdef local isrec tacl =
 
 let () =
   let intern_intro_pattern ist pat =
-    let lf = ref ([], []) in
+    let lf = ref Id.Set.empty in
     let ans = intern_intro_pattern lf ist pat in
     let ist = { ist with ltacvars = !lf } in
     (ist, ans)
@@ -950,7 +958,11 @@ let () =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let f l = Flags.with_option strict_check
-    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])})
+  let f l =
+    let ltacvars =
+      List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
+    in
+    Flags.with_option strict_check
+    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars })
   in
   Hook.set Auto.extern_intern_tac f
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 3fa59ed3b..53a04f700 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -24,7 +24,7 @@ open Nametab
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
 type glob_sign = Genintern.glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
   ltacrecvars : (Id.t * ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 05a62e499..58c64a831 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -363,8 +363,13 @@ let interp_move_location ist gl = function
 
 let interp_reference ist env = function
   | ArgArg (_,r) -> r
-  | ArgVar locid ->
-      interp_ltac_var (coerce_to_reference env) ist (Some env) locid
+  | ArgVar (loc, id) ->
+    try try_interp_ltac_var (coerce_to_reference env) ist (Some env) (loc, id)
+    with Not_found ->
+      try
+        let (v, _, _) = Environ.lookup_named id env in
+        VarRef v
+      with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
 
 let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
 
@@ -372,19 +377,28 @@ let interp_inductive ist = function
   | ArgArg r -> r
   | ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid
 
+let try_interp_evaluable env (loc, id) =
+  let v = Environ.lookup_named id env in
+  match v with
+  | (_, Some _, _) -> EvalVarRef id
+  | _ -> error_not_evaluable (VarRef id)
+
 let interp_evaluable ist env = function
   | ArgArg (r,Some (loc,id)) ->
-      (* Maybe [id] has been introduced by Intro-like tactics *)
-      (try match Environ.lookup_named id env with
-       | (_,Some _,_) -> EvalVarRef id
-       | _ -> error_not_evaluable (VarRef id)
-       with Not_found ->
-       match r with
-       | EvalConstRef _ -> r
-       | _ -> error_global_not_found_loc loc (qualid_of_ident id))
+    (* Maybe [id] has been introduced by Intro-like tactics *)
+    begin
+      try try_interp_evaluable env (loc, id)
+      with Not_found ->
+        match r with
+        | EvalConstRef _ -> r
+        | _ -> error_global_not_found_loc loc (qualid_of_ident id)
+    end
   | ArgArg (r,None) -> r
-  | ArgVar locid ->
-      interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
+  | ArgVar (loc, id) ->
+    try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) (loc, id)
+    with Not_found ->
+      try try_interp_evaluable env (loc, id)
+      with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -794,21 +808,27 @@ let interp_induction_arg ist gl arg =
         strbrk "Cannot coerce " ++ pr_id id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
+      let try_cast_id id' =
+        if Tactics.is_quantified_hypothesis id' gl
+        then ElimOnIdent (loc,id')
+        else
+          (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
+          with Not_found ->
+            user_err_loc (loc,"",
+            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+      in
       try
+        (** FIXME: should be moved to taccoerce *)
         let v = Id.Map.find id ist.lfun in
         let v = Value.normalize v in
         if has_type v (topwit wit_intro_pattern) then
           let v = out_gen (topwit wit_intro_pattern) v in
           match v with
-          | _, IntroIdentifier id' ->
-              if Tactics.is_quantified_hypothesis id' gl
-              then ElimOnIdent (loc,id')
-              else
-                (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
-                with Not_found ->
-                  user_err_loc (loc,"",
-                  pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+          | _, IntroIdentifier id -> try_cast_id id
           | _ -> error ()
+        else if has_type v (topwit wit_var) then
+          let id = out_gen (topwit wit_var) v in
+          try_cast_id id
         else if has_type v (topwit wit_int) then
           ElimOnAnonHyp (out_gen (topwit wit_int) v)
         else match Value.to_constr v with
@@ -1075,7 +1095,10 @@ and force_vrec ist gl v =
 
 and interp_ltac_reference loc' mustbetac ist gl = function
   | ArgVar (loc,id) ->
-      let v = Id.Map.find id ist.lfun in
+      let v =
+        try Id.Map.find id ist.lfun
+        with Not_found -> in_gen (topwit wit_var) id
+      in
       let (sigma,v) = force_vrec ist gl v in
       let v = propagate_trace ist loc id v in
       sigma , if mustbetac then coerce_to_tactic loc id v else v
@@ -1987,7 +2010,8 @@ let interp_tac_gen lfun avoid_ids debug t gl =
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
   let ist = { lfun = lfun; extra = extra } in
-  let ltacvars = List.map fst (Id.Map.bindings lfun), [] in
+  let fold x _ accu = Id.Set.add x accu in
+  let ltacvars = Id.Map.fold fold lfun Id.Set.empty in
   interp_tactic ist
     (intern_pure_tactic {
       ltacvars; ltacrecvars = [];
@@ -2001,7 +2025,7 @@ let eval_ltac_constr gl t =
 
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 let hide_interp t ot gl =
-  let ist = { ltacvars = ([],[]); ltacrecvars = [];
+  let ist = { ltacvars = Id.Set.empty; ltacrecvars = [];
             gsigma = project gl; genv = pf_env gl } in
   let te = intern_pure_tactic ist t in
   let t = eval_tactic te in