modifs pour premiere edition de liens

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

6 files changed, 113 insertions, 26 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index 75fdd346ec..fa0246e327 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -52,11 +52,6 @@ let section_path sl k =
 	make_path pa (id_of_string s) (kind_of_string k)
     | [] -> invalid_arg "section_path"
 
-(* raising located exceptions *)
-let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
-let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
-let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
-
 (* ast destructors *)
 let num_of_ast = function
   | Num(_,n) -> n
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 37823e5adc..7a65850f08 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -9,11 +9,6 @@ open Pcoq
 
 (* Abstract syntax trees. *)
 
-(* raising located exceptions *)
-val anomaly_loc : Coqast.loc * string * std_ppcmds -> 'a
-val user_err_loc : Coqast.loc * string * std_ppcmds -> 'a
-val invalid_arg_loc : Coqast.loc * string -> 'a
-
 val dummy_loc : Coqast.loc
 val loc : Coqast.t -> Coqast.loc
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 0c56d6f0b3..e8eb9c3e4a 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -128,7 +128,7 @@ let ref_from_constr = function
   | _ -> anomaly "Not a reference"
 
 let error_var_not_found str loc s = 
-  Ast.user_err_loc 
+  Util.user_err_loc 
     (loc,str,
      [< 'sTR "The variable"; 'sPC; 'sTR s;
 	'sPC ; 'sTR "was not found"; 
@@ -150,7 +150,7 @@ let dbize_ref k sigma env loc s =
       RRef (loc,ref_from_constr c), il
     with UserError _ ->
       try 
-	RRef (loc,ref_from_constr (Declare.out_syntax_constant id)), []
+	(Syntax_def.search_syntactic_definition id, [])
       with Not_found -> 
 	error_var_not_found "dbize_ref" loc s
 	  
@@ -389,7 +389,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
 	       | _ -> anomaly "Not a reference"
 	   with UserError _ | Not_found ->
 	     try 
-	       let _ = Declare.out_syntax_constant id in 
+	       let _ = Syntax_def.search_syntactic_definition id in 
 	       Node(loc,"SYNCONST",[Nvar(loc,s)])
 	     with Not_found -> 
 	       warning ("Could not globalize "^s); ast)
@@ -526,3 +526,96 @@ let fconstruct_with_univ sigma sign com =
 		(univ_sp, Constraintab.current_constraints(), c) in 
   j
 *)
+
+open Closure
+open Tacred
+
+(* Translation of reduction expression: we need trad because of Fold
+ * Moreover, reduction expressions are used both in tactics and in
+ * vernac. *)
+
+let glob_nvar com =
+  let s = nvar_of_ast com in
+  try 
+    Nametab.sp_of_id CCI (id_of_string s)
+  with Not_found -> 
+    error ("unbound variable "^s)
+
+let cvt_pattern sigma env = function
+  | Node(_,"PATTERN", Node(_,"COMMAND",[com])::nums) ->
+      let occs = List.map num_of_ast nums in
+      let c = constr_of_com sigma env com in
+      let j = Typing.unsafe_machine env sigma c in
+      (occs, j.uj_val, j.uj_type)
+  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
+
+let cvt_unfold = function
+  | Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums, glob_nvar com)
+  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
+
+let cvt_fold sigma sign = function
+  | Node(_,"COMMAND",[c]) -> constr_of_com sigma sign c
+  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
+
+let flag_of_ast lf =
+  let beta = ref false in
+  let delta = ref false in
+  let iota = ref false in
+  let idents = ref (None: (sorts oper -> bool) option) in
+  let set_flag = function
+    | Node(_,"Beta",[]) -> beta := true
+    | Node(_,"Delta",[]) -> delta := true
+    | Node(_,"Iota",[]) -> iota := true
+    | Node(loc,"Unf",l) ->
+        if !delta then
+          if !idents = None then
+            let idl = List.map glob_nvar l in
+            idents := Some
+              (function
+                 | Const sp -> List.mem sp idl
+                 | Abst sp -> List.mem sp idl
+                 | _ -> false)
+          else 
+	    user_err_loc
+	      (loc,"flag_of_ast",
+	       [< 'sTR"Cannot specify identifiers to unfold twice" >])
+        else 
+	  user_err_loc(loc,"flag_of_ast",
+                       [< 'sTR"Delta must be specified before" >])
+    | Node(loc,"UnfBut",l) ->
+        if !delta then
+          if !idents = None then
+            let idl = List.map glob_nvar l in
+            idents := Some
+              (function
+                 | Const sp -> not (List.mem sp idl)
+                 | Abst sp -> not (List.mem sp idl)
+                 | _ -> false)
+          else 
+	    user_err_loc
+	      (loc,"flag_of_ast",
+	       [< 'sTR"Cannot specify identifiers to unfold twice" >])
+        else 
+	  user_err_loc(loc,"flag_of_ast",
+                       [< 'sTR"Delta must be specified before" >])
+    | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
+  in
+  List.iter set_flag lf;
+  { r_beta = !beta;
+    r_iota = !iota;
+    r_delta = match (!delta,!idents) with
+      | (false,_) -> (fun _ -> false)
+      | (true,None) -> (fun _ -> true)
+      | (true,Some p) -> p }
+  
+let redexp_of_ast sigma sign = function
+  | ("Red", []) -> Red
+  | ("Hnf", []) -> Hnf
+  | ("Simpl", []) -> Simpl
+  | ("Unfold", ul) -> Unfold (List.map cvt_unfold ul)
+  | ("Fold", cl) -> Fold (List.map (cvt_fold sigma sign) cl)
+  | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast lf)
+  | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast lf)
+  | ("Pattern",lp) -> Pattern (List.map (cvt_pattern sigma sign) lp)
+  | (s,_) -> invalid_arg ("malformed reduction-expression: "^s)
+
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 5bcbb943d8..04da5c0e6d 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -40,16 +40,16 @@ val globalize_ast     : Coqast.t -> Coqast.t
 
 val type_of_com : env -> Coqast.t -> typed_type
 
-val constr_of_com_casted : unit evar_map -> env -> Coqast.t -> constr ->
+val constr_of_com_casted : 'a evar_map -> env -> Coqast.t -> constr ->
   constr
 
-val constr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr
-val constr_of_com : unit evar_map -> env -> Coqast.t -> constr
-val constr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr
+val constr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
+val constr_of_com : 'a evar_map -> env -> Coqast.t -> constr
+val constr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
 
-val fconstr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com : unit evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
 
 (* Typing with Trad, and re-checking with Mach *)
 (*i
@@ -58,6 +58,9 @@ val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type
 
 (* Typing, re-checking with universes constraints *)
 val fconstruct_with_univ :
-  unit evar_map -> context -> Coqast.t -> unsafe_judgment
+  'a evar_map -> context -> Coqast.t -> unsafe_judgment
 
 i*)
+
+val redexp_of_ast : 
+  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 43ab29db3b..0548788e6e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -312,7 +312,7 @@ GEXTEND Gram
           match (isMeta (nvar_of_ast id), l) with
             | (true, []) -> id
             | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
-            | _ -> user_err_loc
+            | _ -> Util.user_err_loc
                   (loc, "G_tactic.meta_tactic",
                    [< 'sTR"Cannot apply arguments to a meta-tactic." >])
       ] ]
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 61198951d5..20083b8ea9 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -262,7 +262,8 @@ let print_leaf_entry with_values sep (spopt,lobj) =
         [< 'sTR" Syntax Macro " ; 
       	   print_id id ; 'sTR sep;  
            if with_values then 
-             let c = out_syntax_constant id in [< prterm c >]
+             let c = Syntax_def.search_syntactic_definition id in 
+	     [< prrawterm c >]
            else [<>]; 'fNL >]
 	
     | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >]
@@ -428,9 +429,9 @@ let print_name name =
     | Not_found -> 
 	(try 
 	   let (_,typ) = Global.lookup_var name in 
-	   ([< print_var str typ;
-               try print_impl_args (implicits_of_var CCI name)
-               with _ -> [<>] >]) 
+	   [< print_var str typ;
+              try print_impl_args (implicits_of_var CCI name)
+              with _ -> [<>] >]
 	 with Not_found | Invalid_argument _ -> 
 	   error (str ^ " not a defined object"))
     | Invalid_argument _ -> error (str ^ " not a defined object")