Add a treatement of elaborate Intros tactics, CONJPATTERN and family.

This may not be complete, but it already handles simple cases.


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

1 files changed, 25 insertions, 6 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 22a282a0f..0ce95049a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -42,9 +42,14 @@ Hashtbl.add type_table "Coq.Init.Datatypes.prod"
 Hashtbl.add type_table "Coq.Init.Datatypes.nat"
   [|[|"";"O"; "S"|]|];;
 
+(* //menage a faire....*)
+Hashtbl.add type_table "Coq.Zarith.fast_integer.Z"
+[|[|"";"ZERO";"POS";"NEG"|]|];;
 Hashtbl.add type_table "Coq.ZArith.fast_integer.Z"
 [|[|"";"ZERO";"POS";"NEG"|]|];;
-
+(*//itou *)
+Hashtbl.add type_table "Coq.Zarith.fast_integer.positive"
+[|[|"";"xI";"xO";"XH"|]|];;
 Hashtbl.add type_table "Coq.ZArith.fast_integer.positive"
 [|[|"";"xI";"xO";"XH"|]|];;
 
@@ -243,6 +248,11 @@ let strip_Rform =
     | Rform body -> body
     | _ -> xlate_error "strip_Rform: binder expression as formula";;
 
+let rec flatten_one_level = function
+  [Node(_, _, l)] -> l
+| Node(_, _, l)::tl -> List.append l (flatten_one_level tl)
+| _ -> assert false;;
+
 let make_lambdac dom boundcod =
  let rec gather =
   function
@@ -432,7 +442,11 @@ let xlate_op the_node opn a b =
               let ident = type_desc''.(n) in
               CT_coerce_ID_to_FORMULA(CT_ident ident))
   | _, _ -> xlate_error "xlate_op : MUTCONSTRUCT")
-     
+ |"EXPL" ->(match a, b with
+  | [(Num (_, i))], ((Rform t)::[]) -> 
+             CT_bang (CT_coerce_INT_to_INT_OPT (CT_int i), t)
+  | _, _ -> xlate_error "xlate_op : EXPL ")
+    
  | opn  -> xlate_error ("xlate_op : " ^ opn ^ " doesn't exist (" ^
 			    (string_of_node_loc the_node) ^ ")");;
 
@@ -926,10 +940,12 @@ let rec get_flag_rec =
 
 let rec xlate_intro_pattern =
     function
-    | Node(_,"CONJPATTERN",[Node(_, "LISTPATTERN", l)]) ->
-        CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l))
-    | Node(_, "DISJPATTERN", [Node(_,"LISTPATTERN",l)]) ->
-        CT_disj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l))
+    | Node(_,"CONJPATTERN", l) ->
+        CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern 
+                                               (flatten_one_level l)))
+    | Node(_, "DISJPATTERN", l) ->
+        CT_disj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern 
+                                               (flatten_one_level l)))
     | Node(_, "IDENTIFIER",  [Nvar(_,c)]) ->
         CT_coerce_ID_to_INTRO_PATT(CT_ident c)
     | Node(_, a, _) -> failwith ("xlate_intro_pattern on node " ^ a)
@@ -1784,6 +1800,9 @@ and xlate_vernac =
 	   | [Varg_tactic_arg r] -> ctv_FORMULA_OPT_NONE, Some r
 	   | [Varg_constr b; Varg_tactic_arg r] ->
 	       CT_coerce_FORMULA_to_FORMULA_OPT b, Some r
+	   | [Varg_sorttype b] -> 
+               CT_coerce_FORMULA_to_FORMULA_OPT 
+                    (CT_coerce_SORT_TYPE_to_FORMULA b), None
 	   | _ -> assert false in
          CT_definition
 	   (xlate_defn kind, s,