Add a few operators in the new version of xlate.ml and make sure

that ast_to_ct is not use anymore in translate_constr


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

4 files changed, 96 insertions, 14 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index a5f620afd..b62339fa5 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -231,10 +231,12 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
+  | CT_if of ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA
   | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
+  | CT_num_encapsulator of ct_NUM_TYPE * ct_FORMULA
   | CT_prodc of ct_BINDER_NE_LIST * ct_FORMULA
 and ct_FORMULA_LIST =
     CT_formula_list of ct_FORMULA list
@@ -348,6 +350,8 @@ and ct_NATURAL_FEATURE =
   | CT_nat_transparent
 and ct_NONE =
     CT_none
+and ct_NUM_TYPE =
+    CT_num_type of string
 and ct_OMEGA_FEATURE =
     CT_coerce_STRING_to_OMEGA_FEATURE of ct_STRING
   | CT_flag_action
@@ -440,6 +444,7 @@ and ct_TACTIC_COM =
     CT_abstract of ct_ID_OPT * ct_TACTIC_COM
   | CT_absurd of ct_FORMULA
   | CT_apply of ct_FORMULA * ct_SPEC_LIST
+  | CT_assert of ct_ID * ct_FORMULA
   | CT_assumption
   | CT_auto of ct_INT_OPT
   | CT_auto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR
@@ -496,6 +501,7 @@ and ct_TACTIC_COM =
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
   | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
+  | CT_pose of ct_ID * ct_FORMULA
   | CT_progress of ct_TACTIC_COM
   | CT_prolog of ct_FORMULA_LIST * ct_INT
   | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
@@ -520,6 +526,7 @@ and ct_TACTIC_COM =
   | CT_transitivity of ct_FORMULA
   | CT_trivial
   | CT_trivial_with of ct_ID_NE_LIST_OR_STAR
+  | CT_truecut of ct_ID_OPT * ct_FORMULA
   | CT_try of ct_TACTIC_COM
   | CT_use of ct_FORMULA
   | CT_use_inversion of ct_ID_OR_INT * ct_FORMULA * ct_ID_LIST
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 9d4d62804..96049aed6 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -7,7 +7,6 @@ open Pp;;
 open Libobject;;
 open Library;;
 open Vernacinterp;;
-(* dead code: open Proof_trees;; *)
 open Termast;;
 open Tacmach;;
 open Pfedit;;
@@ -108,10 +107,8 @@ let rec discard_coercions =
     | it -> it;;
 
 (*translates a formula into a centaur-tree --> FORMULA *)
-let translate_constr at_top assumptions c =
- let com = ast_of_constr at_top assumptions c in
-(* dead code:  let rcom = relativize_cci (discard_coercions com) in *)
- xlate_formula (Ctast.ast_to_ct com) (* dead code: rcom *);;
+let translate_constr at_top env c =
+  xlate_formula (Constrextern.extern_constr at_top env c);;
 
 (*translates a named_context into a centaur-tree --> PREMISES_LIST *)
 (* this code is inspired from printer.ml (function pr_named_context_of) *)
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 24df307c3..1a6bfc4ca 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -599,6 +599,12 @@ and fFORMULA = function
    fID x1;
    fFIX_BINDER_LIST x2;
    fNODE "fixc" 2
+| CT_if(x1, x2, x3, x4) ->
+   fFORMULA_OPT x1;
+   fFORMULA x2;
+   fFORMULA x3;
+   fFORMULA x4;
+   fNODE "if" 4
 | CT_int_encapsulator x -> fATOM "int_encapsulator";
    (f_atom_string x);
    print_string "\n"| CT_lambdac(x1, x2) ->
@@ -613,6 +619,10 @@ and fFORMULA = function
    fSTRING x1;
    fFORMULA_LIST x2;
    fNODE "notation" 2
+| CT_num_encapsulator(x1, x2) ->
+   fNUM_TYPE x1;
+   fFORMULA x2;
+   fNODE "num_encapsulator" 2
 | CT_prodc(x1, x2) ->
    fBINDER_NE_LIST x1;
    fFORMULA x2;
@@ -805,7 +815,10 @@ and fNATURAL_FEATURE = function
 | CT_nat_transparent -> fNODE "nat_transparent" 0
 and fNONE = function
 | CT_none -> fNODE "none" 0
-and fOMEGA_FEATURE = function
+and fNUM_TYPE = function
+| CT_num_type x -> fATOM "num_type";
+   (f_atom_string x);
+   print_string "\n"and fOMEGA_FEATURE = function
 | CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x
 | CT_flag_action -> fNODE "flag_action" 0
 | CT_flag_system -> fNODE "flag_system" 0
@@ -980,6 +993,10 @@ and fTACTIC_COM = function
    fFORMULA x1;
    fSPEC_LIST x2;
    fNODE "apply" 2
+| CT_assert(x1, x2) ->
+   fID x1;
+   fFORMULA x2;
+   fNODE "assert" 2
 | CT_assumption -> fNODE "assumption" 0
 | CT_auto(x1) ->
    fINT_OPT x1;
@@ -1174,6 +1191,10 @@ and fTACTIC_COM = function
    fTACTIC_COM x;
    (List.iter fTACTIC_COM l);
    fNODE "parallel" (1 + (List.length l))
+| CT_pose(x1, x2) ->
+   fID x1;
+   fFORMULA x2;
+   fNODE "pose" 2
 | CT_progress(x1) ->
    fTACTIC_COM x1;
    fNODE "progress" 1
@@ -1258,6 +1279,10 @@ and fTACTIC_COM = function
 | CT_trivial_with(x1) ->
    fID_NE_LIST_OR_STAR x1;
    fNODE "trivial_with" 1
+| CT_truecut(x1, x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "truecut" 2
 | CT_try(x1) ->
    fTACTIC_COM x1;
    fNODE "try" 1
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e52d88f3f..3ac46fa7d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1,4 +1,3 @@
-
 (** Translation from coq abstract syntax trees to centaur vernac
    *)
 open String;;
@@ -16,6 +15,7 @@ open Decl_kinds;;
 open Topconstr;;
 open Libnames;;
 
+
 let in_coq_ref = ref false;;
 
 let xlate_mut_stuff = ref ((fun _ -> 
@@ -268,6 +268,7 @@ let rec nat_to_number =
     | Nvar (_, "O") -> 0
     | _ -> raise Not_natural;;
 
+
 let xlate_sort =
   function
     | RProp Term.Pos -> CT_sortc "Set"
@@ -287,6 +288,22 @@ let notation_to_formula s l = CT_notation(CT_string s, CT_formula_list l);;
 let xlate_reference = function
     Ident(_,i) -> CT_ident (string_of_id i)
   | Qualid(_, q) -> CT_ident (xlate_qualid q);;
+let rec xlate_match_pattern =
+ function
+   | CPatAtom(_, Some s) -> id_to_pattern_var (xlate_reference  s)
+   |CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
+   |  CPatCstr (_, f1 , (arg1 :: args)) ->
+     CT_pattern_app
+      (id_to_pattern_var (xlate_reference  f1),
+      CT_match_pattern_ne_list
+       (xlate_match_pattern arg1, 
+	List.map xlate_match_pattern args))
+    | CPatAlias  (_,  pattern, id) ->
+     CT_pattern_as
+      (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
+    | _ -> xlate_error "Unexpected data while translating a pattern";;
+
+
 
 let xlate_id_opt = function
   | (_,Name id) -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
@@ -296,12 +313,27 @@ let xlate_id_opt_ne_list = function
     [] -> assert false
   | a::l -> CT_id_opt_ne_list(xlate_id_opt a, List.map xlate_id_opt l);;
 
+
+
 let rec xlate_binder = function
     (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+and xlate_formula_opt =
+  function
+    | None -> ctv_FORMULA_OPT_NONE
+    | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e)
+
 and  xlate_binder_l = function
     LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
     |_ -> xlate_error "TODO: Local Def bindings";
 and 
+  xlate_match_pattern_ne_list = function
+    [] -> assert false
+  | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
+                                     List.map xlate_match_pattern l)
+and  translate_one_equation = function
+    (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp,
+	     xlate_formula a)
+and 
   xlate_binder_ne_list = function
     [] -> assert false
   | a::l -> CT_binder_ne_list(xlate_binder a, List.map xlate_binder l)
@@ -309,6 +341,7 @@ and
   xlate_binder_list = function
   l -> CT_binder_list( List.map xlate_binder_l l)
 and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
+
      CRef r -> varc (xlate_reference r)
    | CArrow(_,a,b)-> CT_arrowc (xlate_formula a, xlate_formula b)
    | CProdN(_,ll,b)-> CT_prodc(xlate_binder_ne_list ll, xlate_formula b)
@@ -320,10 +353,27 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	       xlate_formula_ne_list l)
    | CApp(_, f, l) ->
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
+   | CCases (_,po,tml,eqns)-> CT_cases(xlate_formula_opt po, 
+                         xlate_formula_ne_list tml,
+                         CT_eqn_list (List.map 
+         (fun x -> translate_one_equation x)
+			   eqns))
+   | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
+		   CT_if(xlate_formula_opt po,
+                   xlate_formula c,xlate_formula b1,xlate_formula b2)		
+
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
    | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i)
-   | _ -> assert false
+   | CHole _ -> CT_existvarc 
+   | COrderedCase (_,_,_,_,_) -> xlate_error "TODO:COrderedCase"
+   | CDynamic (_, _) -> xlate_error "TODO:CDynamic"
+   | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula  num)
+   | CCast (_, _, _) -> xlate_error "TODO:CCast"
+   | CMeta (_, _) -> xlate_error "TODO:CMeta"
+   | CCoFix (_, _, _) -> xlate_error "TODO:CCoFix"
+   | CFix (_, _, _) -> xlate_error "TODO:CFix"
+
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
   | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a)
@@ -334,10 +384,7 @@ and xlate_formula_ne_list = function
     [] -> assert false
   | a::l -> CT_formula_ne_list(xlate_formula a, List.map xlate_formula l);;
 
-let xlate_formula_opt =
-  function
-    | None -> ctv_FORMULA_OPT_NONE
-    | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e);;
+
 
 let xlate_hyp_location =
  function
@@ -459,7 +506,7 @@ let rec xlate_intro_pattern =
       let insert_conj l = CT_conj_pattern (CT_intro_patt_list
         (List.map xlate_intro_pattern l))
       in CT_disj_pattern(CT_intro_patt_list (List.map insert_conj ll))
-  | IntroWildcard -> xlate_error "TODO: '_' intro pattern"
+  | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
 
 let compute_INV_TYPE_from_string = function
@@ -888,8 +935,13 @@ and xlate_tac =
     | TacNewInduction _ -> xlate_error "TODO: NewInduction"
     | TacInstantiate (_, _) -> xlate_error "TODO: Instantiate"
     | TacLetTac (_, _, _) -> xlate_error "TODO: LetTac"
+    | TacForward (true, Name id, c) -> 
+               CT_pose(CT_ident (string_of_id id), xlate_formula c)
+    | TacForward (false, Name id, c) -> 
+               CT_assert(CT_ident (string_of_id id), xlate_formula c)
     | TacForward (_, _, _) -> xlate_error "TODO: Assert/Pose id:=c"
-    | TacTrueCut (_, _) -> xlate_error "TODO: Assert id:t"
+    | TacTrueCut (idopt, c) -> 
+                             CT_truecut(xlate_ident_opt idopt, xlate_formula c)
     | TacAnyConstructor tacopt -> xlate_error "TODO: Constructor tac"
     | TacExtend(_, "Ring", [arg]) -> 
 	CT_ring
@@ -1537,6 +1589,7 @@ let xlate_vernac =
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
   | VernacLocate(LocateNotation _) -> xlate_error "TODO: Locate Notation"
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
      VernacSetOption (_, _)|VernacUnsetOption _|