1 files changed, 165 insertions, 0 deletions
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
new file mode 100644
index 00000000..e63baecf
--- /dev/null
+++ b/contrib/interface/translate.ml
@@ -0,0 +1,165 @@
+open Names;;
+open Sign;;
+open Util;;
+open Ast;;
+open Term;;
+open Pp;;
+open Libobject;;
+open Library;;
+open Vernacinterp;;
+open Termast;;
+open Tacmach;;
+open Pfedit;;
+open Parsing;;
+open Evd;;
+open Evarutil;;
+
+open Xlate;;
+open Ctast;;
+open Vtp;;
+open Ascent;;
+open Environ;;
+open Proof_type;;
+
+(* dead code: let rel_reference gt k oper = 
+ if is_existential_oper oper then ope("XTRA", [str "ISEVAR"])
+ else begin
+  let id = id_of_global oper in
+  let oper', _ = global_operator (Nametab.sp_of_id k id) id in
+  if oper = oper' then nvar (string_of_id id)
+  else failwith "xlate"
+end;;
+*)
+
+(* dead code: 
+let relativize relfun =
+ let rec relrec =
+  function
+     | Nvar (_, id) -> nvar id
+     | Slam (l, na, ast) -> Slam (l, na, relrec ast)
+     | Node (loc, nna, l) as ast -> begin
+       try relfun ast
+       with
+       | Failure _ -> Node (loc, nna, List.map relrec l)
+     end
+     | a -> a in
+ relrec;;
+*)
+
+(* dead code:
+let dbize_sp =
+ function
+    | Path (loc, sl, s) -> begin
+      try section_path sl s
+      with
+      | Invalid_argument _ | Failure _ ->
+      anomaly_loc
+       (loc, "Translate.dbize_sp (taken from Astterm)",
+       [< str "malformed section-path" >])
+    end
+    | ast ->
+     anomaly_loc
+      (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
+      [< str "not a section-path" >]);;
+*)
+
+(* dead code:
+let relativize_cci gt = relativize (function
+    | Node (_, "CONST", (p :: _)) as gt ->
+     rel_reference gt CCI (Const (dbize_sp p))
+    | Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt ->
+     rel_reference gt CCI (MutInd (dbize_sp p, tyi))
+    | Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt ->
+     rel_reference gt CCI (MutConstruct (
+      (dbize_sp p, tyi), i))
+    | _ -> failwith "caught") gt;;
+*)
+
+let coercion_description_holder = ref (function _ -> None : t -> int option);;
+
+let coercion_description t = !coercion_description_holder t;;
+
+let set_coercion_description f =
+ coercion_description_holder:=f; ();;
+
+let rec nth_tl l n = if n = 0 then l
+ else (match l with
+ | a :: b -> nth_tl b (n - 1)
+ | [] -> failwith "list too short for nth_tl");;
+
+let rec discard_coercions =
+ function
+    | Slam (l, na, ast) -> Slam (l, na, discard_coercions ast)
+    | Node (l, ("APPLIST" as nna), (f :: args as all_sons)) ->
+     (match coercion_description f with
+     | Some n ->
+      let new_args =
+       try nth_tl args n
+       with
+       | Failure "list too short for nth_tl" -> [] in
+      (match new_args with
+       | a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args)
+       | a :: [] -> discard_coercions a
+       | [] -> Node (l, nna, List.map discard_coercions all_sons))
+     | None -> Node (l, nna, List.map discard_coercions all_sons))
+    | Node (l, nna, all_sons) ->
+     Node (l, nna, List.map discard_coercions all_sons)
+    | it -> it;;
+
+(*translates a formula into a centaur-tree --> FORMULA *)
+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) *)
+let translate_sign env =
+  let l = 
+    Environ.fold_named_context
+      (fun env (id,v,c) l -> 
+	 (match v with
+	      None ->
+	       	CT_premise(CT_ident(string_of_id id), translate_constr false env c)
+	    | Some v1 ->
+		CT_eval_result
+		  (CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)),
+		   translate_constr false env v1,
+		   translate_constr false env c))::l)
+      env ~init:[] 
+  in
+  CT_premises_list l;;
+       
+(* the function rev_and_compact performs two operations:
+   1- it reverses the list of integers given as argument
+   2- it replaces sequences of "1" by a negative number that is
+      the length of the sequence. *)
+let rec rev_and_compact l = function
+    [] -> l
+  | 1::tl -> 
+      (match l with
+              n::tl' -> 
+        if n < 0 then
+          rev_and_compact ((n - 1)::tl') tl
+        else
+          rev_and_compact ((-1)::l) tl
+      |       [] -> rev_and_compact [-1] tl)
+  | a::tl ->
+      if a < 0 then
+      (match l with
+        n::tl' ->
+          if n < 0 then
+            rev_and_compact ((n + a)::tl') tl
+          else
+            rev_and_compact (a::l) tl
+      | [] -> rev_and_compact (a::l) tl)
+      else
+      rev_and_compact (a::l) tl;;
+
+(*translates an int list into a centaur-tree --> SIGNED_INT_LIST *)
+let translate_path l =
+ CT_signed_int_list
+ (List.map (function n -> CT_coerce_INT_to_SIGNED_INT (CT_int n))
+    (rev_and_compact [] l));;
+
+(*translates a path and a goal into a centaur-tree --> RULE *)
+let translate_goal (g:goal) =
+ CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;