Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

8 files changed, 214 insertions, 82 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9590c3b765..fb8a6c8a46 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -20,6 +20,7 @@ open Declare
 open Term
 open Termops
 open Rawterm
+open Nametab
 
 (* usage qque peu general: utilise aussi dans record *)
 
@@ -44,8 +45,7 @@ type coe_info_typ = {
   coe_value : unsafe_judgment;
   coe_strength : strength;
   coe_is_identity : bool;
-  coe_param : int;
-  mutable coe_hide : bool }
+  coe_param : int }
 
 type cl_index = int
 type coe_index = int
@@ -137,18 +137,6 @@ let coercion_exists coe =
 
 let coe_of_reference x = x
 
-let hide_coercion coe =
-  let _,coe_info = coercion_info coe in
-  if coe_info.coe_hide then Some coe_info.coe_param else None
-
-let set_coercion_visibility b coe =
-  let _,coe_info = coercion_info coe in
-  coe_info.coe_hide <- not b
-
-let is_coercion_visible coe = 
-  let _,coe_info = coercion_info coe in
-  not coe_info.coe_hide
-
 let coercion_params coe_info = coe_info.coe_param
 
 (* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
@@ -244,9 +232,12 @@ let strength_of_cl = function
 let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
-  | CL_CONST sp -> string_of_id (id_of_global (Global.env()) (ConstRef sp))
-  | CL_IND sp -> string_of_id (id_of_global (Global.env()) (IndRef sp))
-  | CL_SECVAR sp -> string_of_id (id_of_global (Global.env()) (VarRef sp))
+  | CL_CONST sp ->
+      string_of_qualid (shortest_qualid_of_global (Global.env()) (ConstRef sp))
+  | CL_IND sp ->
+      string_of_qualid (shortest_qualid_of_global (Global.env()) (IndRef sp))
+  | CL_SECVAR sp ->
+      string_of_qualid (shortest_qualid_of_global (Global.env()) (VarRef sp))
 
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
@@ -344,8 +335,7 @@ let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps =
 	 { coe_value = v;
 	   coe_strength = stre;
 	   coe_is_identity = isid;
-	   coe_param = ps;
-	   coe_hide = true }),
+	   coe_param = ps }),
 	cls, clt))
 
 let coercion_strength v = v.coe_strength
@@ -357,3 +347,32 @@ let get_coercion_value v = v.coe_value.uj_val
 let classes () = !class_tab
 let coercions () = !coercion_tab
 let inheritance_graph () = !inheritance_graph
+
+let coercion_of_qualid qid =
+  let ref = Nametab.global qid in
+  let coe = coe_of_reference ref in
+  if not (coercion_exists coe) then
+    errorlabstrm "try_add_coercion" 
+      (Nametab.pr_global_env (Global.env()) ref ++ str" is not a coercion");
+  coe
+
+module CoercionPrinting =
+  struct
+    type t = coe_typ
+    let encode = coercion_of_qualid
+    let printer x = pr_global_env (Global.env()) x
+    let key = Goptions.SecondaryTable ("Printing","Coercion")
+    let title = "Explicitly printed coercions: "
+    let member_message x b =
+      str "Explicit printing of coercion " ++ printer x ++
+      str (if b then " is set" else " is unset")
+    let synchronous = true
+  end
+
+module PrintingCoercion  = Goptions.MakeRefTable(CoercionPrinting)
+
+let hide_coercion coe =
+  if not (PrintingCoercion.active coe) then
+    let _,coe_info = coercion_info coe in
+    Some coe_info.coe_param
+  else None
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 3861d8d356..cd5f31db8f 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -15,6 +15,7 @@ open Term
 open Evd
 open Environ
 open Declare
+open Nametab
 (*i*)
 
 (*s This is the type of class kinds *)
@@ -80,15 +81,6 @@ val coercion_info_from_index : coe_index -> coe_typ * coe_info_typ
 
 val coercion_value : coe_index -> (unsafe_judgment * bool)
 
-(*s This is for printing purpose *)
-
-(* [hide_coercion] returns the number of params to skip if the coercion must
-   be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
-val hide_coercion : coe_typ -> int option
-
-val set_coercion_visibility : bool -> coe_typ -> unit
-val is_coercion_visible : coe_typ -> bool
-
 (*s Lookup functions for coercion paths *)
 val lookup_path_between : cl_index * cl_index -> inheritance_path
 val lookup_path_to_fun_from : cl_index -> inheritance_path
@@ -115,9 +107,15 @@ val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
 (*i*)
 
-(* This is for printing purpose *)
+(*s This is for printing purpose *)
 val string_of_class : cl_typ -> string
 val get_coercion_value : coe_info_typ -> constr
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
 val classes : unit -> (int * (cl_typ * cl_info_typ)) list
 val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
+
+(* [hide_coercion] returns the number of params to skip if the coercion must
+   be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
+val hide_coercion : coe_typ -> int option
+
+
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5e718289cc..faa5e9e46b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -28,13 +28,8 @@ open Nametab
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
-let encode_inductive ref =
-  let indsp = match ref with
-    | IndRef indsp -> indsp
-    | _ ->
-        errorlabstrm "indsp_of_id"
-          (pr_global_env (Global.env()) ref ++
-	     str" is not an inductive type") in
+let encode_inductive qid =
+  let indsp = global_inductive qid in
   let constr_lengths = mis_constr_nargs indsp in
   (indsp,constr_lengths)
 
@@ -47,59 +42,64 @@ let isomorphic_to_bool lc =
 
 let isomorphic_to_tuple lc = (Array.length lc = 1)
 
+let encode_bool (loc,_ as locqid) =
+  let (_,lc as x) = encode_inductive locqid in
+  if not (isomorphic_to_bool lc) then
+    user_err_loc (loc,"encode_if",
+      str "This type cannot be seen as a boolean type");
+  x
+
+let encode_tuple (loc,_ as locqid) =
+  let (_,lc as x) = encode_inductive locqid in
+  if not (isomorphic_to_tuple lc) then
+    user_err_loc (loc,"encode_tuple",
+      str "This type cannot be seen as a tuple type");
+  x
+
 module PrintingCasesMake =
   functor (Test : sig 
-     val test : int array -> bool
-     val error_message : string
-     val member_message : global_reference -> bool -> string
+     val encode : qualid located -> inductive * int array
+     val member_message : std_ppcmds -> bool -> std_ppcmds
      val field : string
      val title : string
   end) ->
   struct
     type t = inductive * int array
-    let encode = encode_inductive
-    let check (_,lc) =
-      if not (Test.test lc) then 
-	errorlabstrm "check_encode" (str Test.error_message)
-    let printer (ind,_) =
-      pr_id (basename (path_of_inductive (Global.env()) ind))
+    let encode = Test.encode
+    let printer (ind,_) = pr_global_env (Global.env()) (IndRef ind)
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
-    let member_message = Test.member_message
+    let member_message x = Test.member_message (printer x)
     let synchronous = true
   end
 
 module PrintingCasesIf =
   PrintingCasesMake (struct 
-    let test = isomorphic_to_bool
-    let error_message = "This type cannot be seen as a boolean type"
+    let encode = encode_bool
     let field = "If"
     let title = "Types leading to pretty-printing of Cases using a `if' form: "
-    let member_message ref b =
-      let s = string_of_qualid(shortest_qualid_of_global (Global.env()) ref) in
-      if b then
-        "Cases on elements of " ^ s ^ " are printed using a `if' form"
-      else
-        "Cases on elements of " ^ s ^ " are not printed using `if' form"
+    let member_message s b =
+      str "Cases on elements of " ++ s ++ 
+      str
+	(if b then " are printed using a `if' form"
+         else " are not printed using a `if' form")
   end)
 
 module PrintingCasesLet =
   PrintingCasesMake (struct 
-    let test = isomorphic_to_tuple
-    let error_message = "This type cannot be seen as a tuple type"
+    let encode = encode_tuple
     let field = "Let"
     let title = 
       "Types leading to a pretty-printing of Cases using a `let' form:"
-    let member_message ref b =
-      let s = string_of_qualid(shortest_qualid_of_global (Global.env()) ref) in
-      if b then
-        "Cases on elements of " ^ s ^ " are printed using a `let' form"
-      else
-        "Cases on elements of " ^ s ^ " are not printed using a `let' form"
+    let member_message s b =
+      str "Cases on elements of " ++ s ++
+      str
+	(if b then " are printed using a `let' form"
+         else " are not printed using a `let' form")
   end)
 
-module PrintingIf  = Goptions.MakeIdentTable(PrintingCasesIf)
-module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet)
+module PrintingIf  = Goptions.MakeRefTable(PrintingCasesIf)
+module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
 
 let force_let ci =
   let indsp = ci.ci_ind in
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 14b9cd5e16..65fefb83fd 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -52,3 +52,4 @@ val make_rec_branch_arg :
 val declare_eliminations : mutual_inductive -> unit
 val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
+val make_elimination_ident : identifier -> sorts_family -> identifier
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f69d22dfc8..c7e2b0eb39 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,6 +32,17 @@ type fix_kind = RFix of (int array * int) | RCoFix of int
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
+
+type 'a explicit_substitution = (quantified_hypothesis * 'a) list
+
+type 'a substitution = 
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_substitution
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a substitution
+
 type hole_kind =
   | ImplicitArg of global_reference * int
   | AbstractionType of name
@@ -46,7 +57,6 @@ type 'ctxt reference =
   | RVar of identifier
   | REVar of int * 'ctxt
 
-(*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
   | RRef of loc * global_reference
   | RVar of loc * identifier
@@ -115,3 +125,30 @@ let set_loc_of_rawconstr loc = function
   | RDynamic (_,d)   -> RDynamic (loc,d)
 
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+
+type 'a raw_red_flag = {
+  rBeta : bool;
+  rIota : bool;
+  rZeta : bool;
+  rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
+  rConst : 'a list
+}
+
+type ('a,'b) red_expr_gen =
+  | Red of bool
+  | Hnf
+  | Simpl
+  | Cbv of 'b raw_red_flag
+  | Lazy of 'b raw_red_flag
+  | Unfold of (int list * 'b) list
+  | Fold of 'a list
+  | Pattern of (int list * 'a) list
+  | ExtraRedExpr of string * 'a list
+
+type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
+
+type 'a may_eval =
+  | ConstrTerm of 'a
+  | ConstrEval of ('a, qualid or_metanum) red_expr_gen * 'a
+  | ConstrContext of (loc * identifier) * 'a
+  | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 973bac7192..3a6d681151 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -31,6 +31,17 @@ type fix_kind = RFix of (int array * int) | RCoFix of int
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
+
+type 'a explicit_substitution = (quantified_hypothesis * 'a) list
+
+type 'a substitution = 
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_substitution
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a substitution
+
 type hole_kind =
   | ImplicitArg of global_reference * int
   | AbstractionType of name
@@ -81,3 +92,30 @@ val dummy_loc : loc
 val loc_of_rawconstr : rawconstr -> loc
 val set_loc_of_rawconstr : loc -> rawconstr -> rawconstr
 val join_loc : loc -> loc -> loc
+
+type 'a raw_red_flag = {
+  rBeta : bool;
+  rIota : bool;
+  rZeta : bool;
+  rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
+  rConst : 'a list
+}
+
+type ('a,'b) red_expr_gen =
+  | Red of bool
+  | Hnf
+  | Simpl
+  | Cbv of 'b raw_red_flag
+  | Lazy of 'b raw_red_flag
+  | Unfold of (int list * 'b) list
+  | Fold of 'a list
+  | Pattern of (int list * 'a) list
+  | ExtraRedExpr of string * 'a list
+
+type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
+
+type 'a may_eval =
+  | ConstrTerm of 'a
+  | ConstrEval of ('a, qualid or_metanum) red_expr_gen * 'a
+  | ConstrContext of (loc * identifier) * 'a
+  | ConstrTypeOf of 'a
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ad7e02b775..9bdf5822f8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -21,6 +21,7 @@ open Reductionops
 open Closure
 open Instantiate
 open Cbv
+open Rawterm
 
 exception Elimconst
 exception Redelimination
@@ -743,7 +744,8 @@ let compute = cbv_betadeltaiota
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
  * the specified occurrences. *)
 
-let abstract_scheme env (locc,a,ta) t =
+let abstract_scheme env sigma (locc,a) t =
+  let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
   if occur_meta ta then error "cannot find a type for the generalisation";
   if occur_meta a then 
@@ -752,31 +754,60 @@ let abstract_scheme env (locc,a,ta) t =
     mkLambda (na, ta,subst_term_occ env locc a t)
 
 
-let pattern_occs loccs_trm_typ env sigma c =
-  let abstr_trm = List.fold_right (abstract_scheme env) loccs_trm_typ c in
-  applist(abstr_trm, List.map (fun (_,t,_) -> t) loccs_trm_typ)
+let pattern_occs loccs_trm env sigma c =
+  let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
+  applist(abstr_trm, List.map snd loccs_trm)
 
 (* Generic reduction: reduction functions used in reduction tactics *)
 
-type red_expr =
-  | Red of bool
-  | Hnf
-  | Simpl
-  | Cbv of Closure.RedFlags.reds
-  | Lazy of Closure.RedFlags.reds
-  | Unfold of (int list * evaluable_global_reference) list
-  | Fold of constr list
-  | Pattern of (int list * constr * constr) list
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
+
+open RedFlags
+
+let make_flag_constant = function
+  | EvalVarRef id -> fVAR id
+  | EvalConstRef sp -> fCONST sp
+
+let make_flag f =
+  let red = no_red in
+  let red = if f.rBeta then red_add red fBETA else red in
+  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rZeta then red_add red fZETA else red in
+  let red =
+    if f.rDelta then (* All but rConst *)
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red (Conv_oracle.freeze ()) in
+	List.fold_right
+	  (fun v red -> red_sub red (make_flag_constant v))
+	  f.rConst red
+    else (* Only rConst *)
+        let red = red_add_transparent (red_add red fDELTA) all_opaque in
+	List.fold_right
+	  (fun v red -> red_add red (make_flag_constant v))
+	  f.rConst red
+  in red
+
+let red_expr_tab = ref Stringmap.empty
+
+type generic_reduction_function = constr list -> reduction_function
+
+let declare_red_expr s f =
+  try 
+    let _ = Stringmap.find s in
+    error ("There is already a reduction expression of name "^s)
+  with Not_found ->
+    red_expr_tab := Stringmap.add s f !red_expr_tab
 
 let reduction_of_redexp = function
   | Red internal -> if internal then internal_red_product else red_product
   | Hnf -> hnf_constr
   | Simpl -> nf
-  | Cbv f -> cbv_norm_flags f
-  | Lazy f -> clos_norm_flags f
+  | Cbv f -> cbv_norm_flags (make_flag f)
+  | Lazy f -> clos_norm_flags (make_flag f)
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
   | Pattern lp -> pattern_occs lp
+  | ExtraRedExpr (s,cl) -> Stringmap.find s !red_expr_tab cl
 
 (* Used in several tactics. *)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 4100a31ae3..c03c67c092 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -40,7 +40,7 @@ val unfoldn :
 val fold_commands : constr list ->  reduction_function
 
 (* Pattern *)
-val pattern_occs : (int list * constr * constr) list ->  reduction_function
+val pattern_occs : (int list * constr) list ->  reduction_function
 (* Rem: Lazy strategies are defined in Reduction *)
 
 (* Call by value strategy (uses Closures) *)
@@ -60,6 +60,8 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
    returns [I] and [t'] or fails with a user error *)
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
+open Rawterm
+(*
 type red_expr =
   | Red of bool    (* raise Redelimination if true otherwise UserError *)
   | Hnf
@@ -69,8 +71,14 @@ type red_expr =
   | Unfold of (int list * evaluable_global_reference) list
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
+*)
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
-val reduction_of_redexp : red_expr ->  reduction_function
+val reduction_of_redexp : red_expr -> reduction_function
+
+type generic_reduction_function = constr list -> reduction_function
+
+val declare_red_expr : string -> generic_reduction_function -> unit
 
 (* Opaque and Transparent commands. *)
 val set_opaque_const      : section_path -> unit