- libraryObjects: new default "natural numbers" with the uri of nat.

[helm.git] / helm / software / components / acic_procedural / proceduralTeX.ml

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index d9d936f6aa622f5e2e01da6a28f90ba4779d9dc6..279ebecb99982bf1cd48b9b19cce54a6a8bdad47 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTeX.ml
+++ b/helm/software/components/acic_procedural/proceduralTeX.ml
@@ -168,9 +168,11 @@ let rec xat frm = function
    | C.AImplicit _                    -> assert false
    | C.AAppl (_, [])                  -> assert false
 
-and xats frm vs =
-   let map v = F.fprintf frm "{%a}" xat v in
-   List.iter map vs
+and xats frm = function
+   | [] -> F.fprintf frm "{}"
+   | vs -> 
+      let map v = F.fprintf frm "{%a}" xat v in
+      List.iter map vs
 
 in
 xat frm t
@@ -179,24 +181,68 @@ let xx frm = function
    | None   -> assert false
    | Some r -> F.fprintf frm "%s" (quote r)
 
+let xh how =
+   if how then "\\dx" else "\\sx"
+
 let tex_of_steps frm sorts l =
 
 let xat frm t = tex_of_annterm frm sorts t in
 
 let rec xl frm = function
-   | []                        -> ()
+   | []                                                    -> ()
    | T.Note _ :: l 
    | T.Statement _ :: l
-   | T.Qed _ :: l              -> xl frm l
-   | T.Intros (_, [r], _) :: l ->
+   | T.Qed _ :: l                                          ->
+      xl frm l
+   | T.Exact (t, _) :: l                                   ->
+      F.fprintf frm "\\Exact{%a}" xat t; xl frm l   
+   | T.Intros (_, [r], _) :: l                             ->
       F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
-   | T.LetIn (r, v, _) :: l    ->
-      F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l   
-   | T.Inductive _ :: _        -> assert false
-   | T.Id _ :: _               -> assert false
-   | T.Clear _ :: _            -> assert false
-   | T.ClearBody _ :: _        -> assert false
-   | T.Branch _ :: _           -> assert false
-   | T.Intros _ :: _           -> assert false
+   | T.LetIn (r, v, _) :: l                                ->
+      F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
+   | T.Change (u, _, None, _, _) :: l                      ->
+      F.fprintf frm "\\Change{%a}{}{%a}" xat u xl l
+   | T.Change (u, _, Some (s, _), _, _) :: l               ->
+      F.fprintf frm "\\Change{%a}{%s}{%a}" xat u (quote s) xl l
+   | T.Rewrite (b, t, None, _, _) :: l                     ->
+      F.fprintf frm "\\Rewrite{%s}{%a}{}{}{%a}" (xh b) xat t xl l
+   | T.Rewrite (b, t, Some (s1, Some s2), _, _) :: l       ->
+      F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
+         (xh b) xat t (quote s1) (quote s2) xl l
+   | T.Rewrite (b, t, Some (s1, None), _, _) :: l          ->
+      F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
+         (xh b) xat t (quote s1) (quote s1) xl l
+   | T.Apply (t, _) :: T.Branch (ls, _) :: l               ->
+      let z = num (List.length ls) in
+      F.fprintf frm "\\%sApply{%a}%a" z xat t xls ls; xl frm l
+   | T.Apply (t, _) :: l                                   ->
+      F.fprintf frm "\\Apply{%a}{%a}" xat t xl l
+   | T.Cases (v, _, _) :: T.Branch (ls, _) :: l            ->
+      let z = num (List.length ls) in
+      F.fprintf frm "\\%sCases{%a}%a" z xat v xls ls; xl frm l
+   | T.Cases (v, _, _) :: l                                ->
+      F.fprintf frm "\\Cases{%a}{%a}" xat v xl l
+   | T.Elim (v, Some t, _, _) :: T.Branch (ls, _) :: l     ->
+      let z = num (List.length ls) in
+      F.fprintf frm "\\%sElim{%a}{%a}{}{}%a" z xat v xat t xls ls; xl frm l
+   | T.Elim (v, Some t, _, _) :: l                         ->
+      F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
+   | T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
+      F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
+   | T.Inductive _ :: _                                    -> assert false
+   | T.Id _ :: _                                           -> assert false
+   | T.Clear _ :: _                                        -> assert false
+   | T.ClearBody _ :: _                                    -> assert false
+   | T.Branch _ :: _                                       -> assert false
+   | T.Intros _ :: _                                       -> assert false
+   | T.Elim _ :: _                                         -> assert false
+   | T.Cut _ :: _                                          -> assert false
+
+and xls frm = function
+   | [] -> F.fprintf frm "{}"
+   | ls -> 
+      let map l = F.fprintf frm "{%a}" xl l in
+      List.iter map (List.rev ls)
+
 in
-xl frm l
+F.fprintf frm "%a@\n" xl l