prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_transformations / sequent2pres.ml

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 2b159e1c898736b759af10bf4bbc3affc9f10060..ad2724134f47562b6c0c58633a3941a26b7a8967 100644 (file)
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -85,20 +85,32 @@ let sequent2pres term2pres (_,_,context,ty) =
       []
       (context2pres context)) in
  let pres_goal = term2pres ty in 
- (Box.b_v
-    []
-    [pres_context;
-     b_ink [None,"width","4cm"; None,"height","1px"];
-     pres_goal])
+ (Box.b_h [] [
+   Box.b_space; 
+   (Box.b_v []
+      [Box.b_space;
+       pres_context;
+       b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+       Box.b_space; 
+       pres_goal])
+ ])
 ;;
 
+(*
 let sequent2pres ~ids_to_inner_sorts =
  sequent2pres 
   (function p -> 
    (Cexpr2pres.cexpr2pres_charcount 
     (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
 ;;
+*)
 
-
-
+let sequent2pres ~ids_to_inner_sorts =
+  sequent2pres
+    (fun annterm ->
+      let (ast, ids_to_uris) as arg =
+        Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+      in
+      let astbox = Ast2pres.ast2astBox arg in
+      Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astbox)