Diverses corrections

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



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

16 files changed, 131 insertions, 63 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index d415cf7d2..ef0ff426d 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -503,8 +503,7 @@ let rec fourier gl=
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-    then (print_string "Tactic Fourier fails.\n";
-		       flush stdout)
+    then Util.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3c1645d47..3b13283e1 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
   type [typ] *)
 
-let coerce_meta_out id = int_of_string (string_of_id id)
-let coerce_meta_in n = id_of_string (string_of_int n)
+let coerce_meta_out id = 
+  let s = string_of_id id in
+  int_of_string (String.sub s 1 (String.length s - 1))
+let coerce_meta_in n =
+  id_of_string ("M" ^ string_of_int n)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index c06738226..dfd813985 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -50,14 +50,16 @@ let ppsp sp = pp(pr_sp sp)
 let ppqualid qid = pp(pr_qualid qid)
 
 (* term printers *)
+let rawdebug = ref false
 let ppconstr x = pp (Termops.print_constr x)
-let ppconstrdb x = pp(Flags.with_option Constrextern.rawdebug Termops.print_constr x)
+let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let pprawconstr = (fun x -> pp(pr_lrawconstr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> pp(pr_ltype x))
+
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
@@ -413,3 +415,48 @@ let _ =
          (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
           ConstrArgType),
          Some "c")]]
+
+(* Setting printer of unbound global reference *)
+open Names
+open Nameops
+open Libnames
+
+let encode_path loc prefix mpdir suffix id =
+  let dir = match mpdir with
+    | None -> []
+    | Some (mp,dir) -> 
+	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
+	repr_dirpath dir) in
+  Qualid (loc, make_qualid 
+    (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
+
+let raw_string_of_ref loc = function
+  | ConstRef cst -> 
+      let (mp,dir,id) = repr_con cst in
+      encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
+  | IndRef (kn,i) ->
+      let (mp,dir,id) = repr_kn kn in
+      encode_path loc "IND" (Some (mp,dir)) [id_of_label id] 
+	(id_of_string ("_"^string_of_int i))
+  | ConstructRef ((kn,i),j) -> 
+      let (mp,dir,id) = repr_kn kn in
+      encode_path loc "CSTR" (Some (mp,dir))
+	[id_of_label id;id_of_string ("_"^string_of_int i)] 
+	(id_of_string ("_"^string_of_int j))
+  | VarRef id -> 
+      encode_path loc "SECVAR" None [] id
+
+let short_string_of_ref loc = function
+  | VarRef id -> Ident (loc,id)
+  | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
+  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn)))
+  | IndRef (kn,i) ->
+      encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
+        (id_of_string ("_"^string_of_int i))
+  | ConstructRef ((kn,i),j) -> 
+      encode_path loc "CSTR" None 
+        [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)]
+        (id_of_string ("_"^string_of_int j))
+
+let _ = Constrextern.set_debug_global_reference_printer
+  (if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1e3587c59..5047d1b98 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -108,35 +108,17 @@ let idopt_of_name = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let rawdebug = ref false
-
-let raw_string_of_ref = function
-  | ConstRef kn -> 
-      "CONST("^(string_of_con kn)^")"
-  | IndRef (kn,i) ->
-      "IND("^(string_of_kn kn)^","^(string_of_int i)^")"
-  | ConstructRef ((kn,i),j) -> 
-      "CONSTRUCT("^
-      (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")"
-  | VarRef id -> 
-      "SECVAR("^(string_of_id id)^")"
-
-let short_string_of_ref = function
-  | VarRef id -> string_of_id id
-  | ConstRef cst -> string_of_label (pi3 (repr_con cst))
-  | IndRef (kn,0) -> string_of_label (pi3 (repr_kn kn))
-  | IndRef (kn,i) -> 
-      "IND("^string_of_label (pi3 (repr_kn kn))^(string_of_int i)^")"
-  | ConstructRef ((kn,i),j) -> 
-      "CONSTRUCT("^
-      string_of_label (pi3 (repr_kn kn))^","^(string_of_int i)^","^(string_of_int j)^")"
+let debug_global_reference_printer =
+  ref (fun _ -> failwith "Cannot print a global reference")
+
+let set_debug_global_reference_printer f =
+  debug_global_reference_printer := f
 
 let extern_reference loc vars r =
   try Qualid (loc,shortest_qualid_of_global vars r)
   with Not_found ->
     (* happens in debugger *)
-    let f = if !rawdebug then raw_string_of_ref else short_string_of_ref in
-    Ident (loc,id_of_string (f r))
+    !debug_global_reference_printer loc r
 
 (************************************************************************)
 (* Equality up to location (useful for translator v8) *)
@@ -922,7 +904,7 @@ let rec raw_of_pat env = function
 	| Name id   -> id
 	| Anonymous ->
 	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
-      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)^"]") in
+      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       RVar (loc,id)
   | PMeta None -> RHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> RPatVar (loc,(false,n))
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 7ae2977f5..a56923fe5 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -56,7 +56,8 @@ val print_no_symbol : bool ref
 val print_projections : bool ref
 
 (* Debug printing options *)
-val rawdebug : bool ref
+val set_debug_global_reference_printer :
+  (loc -> global_reference -> reference) -> unit
 
 (* This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
diff --git a/lib/util.ml b/lib/util.ml
index b317c849c..ccd807a90 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -290,6 +290,7 @@ let check_ident s =
     | _ -> error (s^": an identifier should start with a letter")
   with 
   | End_of_input -> error "The empty string is not an identifier"
+  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence")
   | Invalid_argument _ -> error (s^": invalid utf8 sequence")
 
 (* Lists *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0e7c92a6c..f5ea021d4 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -142,10 +142,7 @@ GEXTEND Gram
     [ [ "_" -> (loc, Anonymous) ] ]
   ;
   global:
-    [ [ r = Prim.reference -> r
-
-      (* This is used in quotations *)
-      | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
+    [ [ r = Prim.reference -> r ] ]
   ;
   constr_pattern:
     [ [ c = constr -> c ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c0fd07c17..c541b5a7e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -95,6 +95,8 @@ GEXTEND Gram
 	  TacArg (TacExternal (loc,com,req,la))
       | st = simple_tactic -> TacAtom (loc,st)
       | a = may_eval_arg -> TacArg(a)
+      | IDENT "constr"; ":"; id = METAIDENT ->
+          TacArg(MetaIdArg (loc,false,id))
       | IDENT "constr"; ":"; c = Constr.constr ->
           TacArg(ConstrMayEval(ConstrTerm c))
       | IDENT "ipattern"; ":"; ipat = simple_intropattern -> 
@@ -125,7 +127,7 @@ GEXTEND Gram
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
       (* Unambigous entries: tolerated w/o "ltac:" modifier *)
-      | id = METAIDENT -> MetaIdArg (loc,id)
+      | id = METAIDENT -> MetaIdArg (loc,true,id)
       | "()" -> TacVoid ] ]
   ;
   may_eval_arg:
@@ -148,7 +150,7 @@ GEXTEND Gram
       | c = Constr.constr -> ConstrTerm c ] ]
   ;
   tactic_atom:
-    [ [ id = METAIDENT -> MetaIdArg (loc,id)
+    [ [ id = METAIDENT -> MetaIdArg (loc,true,id)
       | n = integer -> Integer n
       | "()" -> TacVoid ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5d59a8489..b26f8c77e 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -383,7 +383,8 @@ let parse_after_dot bp c =
 let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
-  | [< ''$'; len = ident_tail (store 0 '$') >] ep -> 
+  | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); 
+      len = ident_tail (store 0 c) >] ep -> 
       comment_stop bp;
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 55c6a4387..2a46388c3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -957,7 +957,8 @@ let rec pr_tac inherited tac =
 and pr_tacarg = function
   | TacDynamic (loc,t) ->
       pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
-  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
+  | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
+  | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
   | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e698a187c..6313a553e 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -470,19 +470,15 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacFun
         ($mlexpr_of_list mlexpr_of_ident_option idol$,
          $mlexpr_of_tactic body$) >>
-(*
-  | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast
-*)
-(*
-  | Tacexpr.TacArg (Tacexpr.AstTacArg (Coqast.Nmeta $dloc$ id)) -> anti loc id
-*)
-  | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,id)) -> anti loc id
+  | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
   | Tacexpr.TacArg t ->
       <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >>
   | _ -> failwith "Quotation of tactic expressions: TODO"
 
 and mlexpr_of_tactic_arg = function
-  | Tacexpr.MetaIdArg (loc,id) -> anti loc id
+  | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
+  | Tacexpr.MetaIdArg (loc,false,id) -> 
+      <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >>
   | Tacexpr.TacCall (loc,t,tl) ->
       <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
   | Tacexpr.Tacexp t ->
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index e5632515d..072d664fc 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -169,8 +169,10 @@ let mentions clenv mv0 =
   let rec menrec mv1 =
     mv0 = mv1 ||
     let mlist =
-      try (fst (meta_fvalue clenv.evd mv1)).freemetas
-      with Anomaly _ | Not_found -> Metaset.empty in
+      try match meta_opt_fvalue clenv.evd mv1 with
+      | Some (b,_) -> b.freemetas
+      | None -> Metaset.empty
+      with Not_found -> Metaset.empty in
     meta_exists menrec mlist
   in menrec
 
@@ -230,6 +232,7 @@ let dependent_metas clenv mvs conclmetas =
 
 let clenv_dependent hyps_only clenv =
   let mvs = collect_metas (clenv_value clenv) in
+  let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
   List.filter
@@ -256,21 +259,47 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
     clenv_unify allow_K CUMUL ~flags:flags
       (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
 
-(* [clenv_pose_dependent_evars clenv]
+(* [clenv_pose_metas_as_evars clenv dep_mvs]
  * For each dependent evar in the clause-env which does not have a value,
  * pose a value for it by constructing a fresh evar.  We do this in
  * left-to-right order, so that every evar's type is always closed w.r.t.
- * metas. *)
+ * metas. 
+
+ * Node added 14/4/08 [HH]: before this date, evars were collected in
+   clenv_dependent by collect_metas in the fold_constr order which is
+   (almost) the left-to-right order of dependencies in term. However,
+   due to K-redexes, collect_metas was sometimes missing some metas.
+   The call to collect_metas has been replaced by a call to
+   undefined_metas, but then the order was the one of definition of
+   the metas (numbers in increasing order) which is _not_ the
+   dependency order when a clenv_fchain occurs (because clenv_fchain
+   plugs a term with a list of consecutive metas in place of a - a priori -
+   arbitrary metavariable belonging to another sequence of consecutive metas:
+   e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of 
+   (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2).
+   To ensure the dependency order, we check that the type of each meta
+   to pose is already meta-free, otherwise we postpone the transformation,
+   hoping that no cycle may happen.
+
+   Another approach could have been to use decimal numbers for metas so that
+   in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2)
+   then making the numeric order match the dependency order.
+*)
 
 let clenv_pose_metas_as_evars clenv dep_mvs =
-  List.fold_left
-    (fun clenv mv ->
+  let rec fold clenv = function
+  | [] -> clenv
+  | mv::mvs -> 
       let ty = clenv_meta_type clenv mv in
-      let (evd,evar) = 
-	new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
-      clenv_assign mv evar {clenv with evd=evd})
-    clenv
-    dep_mvs
+      (* Postpone the evar-ization if dependent on another meta *)
+      (* This assumes no cycle in the dependencies - is it correct ? *)
+      if occur_meta ty then fold clenv (mvs@[mv])
+      else
+	let (evd,evar) = 
+	  new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
+	let clenv = clenv_assign mv evar {clenv with evd=evd} in
+	fold clenv mvs in
+  fold clenv dep_mvs
 
 let evar_clenv_unique_resolver = clenv_unique_resolver
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 91b70e3b0..3adf749f0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -507,6 +507,12 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
 
 let meta_list evd = metamap_to_list evd.metas
 
+let undefined_metas evd =
+  List.sort Pervasives.compare (map_succeed (function
+    | (n,Clval(_,_,typ)) -> failwith ""
+    | (n,Cltyp (_,typ))  -> n)
+    (meta_list evd))
+
 let metas_of evd = 
   List.map (function
     | (n,Clval(_,_,typ)) -> (n,typ.rebus)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ebda685bd..352d3021d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -196,6 +196,7 @@ val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> ev
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
 
+val undefined_metas : evar_defs -> metavariable list
 val metas_of : evar_defs -> metamap
 
 type metabinding = metavariable * constr * instance_status
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 7a90040e5..ca25c722c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -241,7 +241,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
-  | MetaIdArg      of loc * string
+  | MetaIdArg      of loc * bool * string
   | ConstrMayEval  of ('constr,'cst) may_eval
   | IntroPattern   of intro_pattern_expr
   | Reference      of 'ref
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index aba96afb3..3367f89f1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -829,10 +829,12 @@ and intern_tacarg strict ist = function
       IntroPattern (intern_intro_pattern lf ist ipat)
   | Integer n -> Integer n
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
-  | MetaIdArg (loc,s) ->
+  | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
       let id = id_of_string s in
-      if find_ltacvar id ist then Reference (ArgVar (adjust_loc loc,id))
+      if find_ltacvar id ist then
+	if istac then Reference (ArgVar (adjust_loc loc,id))
+	else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
       else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,l) ->
       TacCall (loc,
@@ -1635,7 +1637,7 @@ and interp_tacarg ist gl = function
   | Integer n -> VInteger n
   | IntroPattern ipat -> VIntroPattern (interp_intro_pattern ist gl ipat)
   | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
-  | MetaIdArg (loc,id) -> assert false
+  | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) -> interp_ltac_reference false true ist gl r
   | TacCall (loc,f,l) ->
       let fv = interp_ltac_reference true true ist gl f
@@ -2464,7 +2466,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
-  | MetaIdArg (_loc,_) -> assert false
+  | MetaIdArg (_loc,_,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
   | TacExternal (_loc,com,req,la) ->