ProceduralTeX completed and tested on the terms given as examples in the paper about...

diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend
index d79de5566183d0428037432ea79e73face4b5449..4a57a7a117faa3668fab8b16c6fc1f9758c60c14 100644 (file)
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -13,11 +13,13 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
 proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralTeX.cmi 
 proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
     proceduralTeX.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \
+    proceduralHelpers.cmi proceduralConversion.cmi proceduralClassify.cmi \
+    acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \
+    proceduralHelpers.cmx proceduralConversion.cmx proceduralClassify.cmx \
+    acic2Procedural.cmi 

diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index d79de5566183d0428037432ea79e73face4b5449..4a57a7a117faa3668fab8b16c6fc1f9758c60c14 100644 (file)
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -13,11 +13,13 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
 proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralTeX.cmi 
 proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
     proceduralTeX.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \
+    proceduralHelpers.cmi proceduralConversion.cmi proceduralClassify.cmi \
+    acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \
+    proceduralHelpers.cmx proceduralConversion.cmx proceduralClassify.cmx \
+    acic2Procedural.cmi 

diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile
index 06538c53e3aadc3cd73a9f4d8db975c28ea03e07..2ed14382a78f6085369a241b9c1a8d1258e42aa0 100644 (file)
--- a/helm/software/components/acic_procedural/Makefile
+++ b/helm/software/components/acic_procedural/Makefile
@@ -8,8 +8,8 @@ INTERFACE_FILES =                \
        proceduralTypes.mli      \
        proceduralMode.mli       \
        proceduralConversion.mli \
-       acic2Procedural.mli      \
        proceduralTeX.mli        \
+       acic2Procedural.mli      \
        $(NULL)
 IMPLEMENTATION_FILES =          \
        $(INTERFACE_FILES:%.mli=%.ml)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index ae64d1f19af4c904e804cd3dd3fd48001c525d9b..0edb5c8b041c9e2c5415790bd3a1badfca2ead20 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -45,6 +45,7 @@ module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
+module X    = ProceduralTeX
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -55,6 +56,8 @@ type status = {
    case: int list
 }
 
+let tex_formatter = ref None
+
 let debug = ref false
 
 (* helpers ******************************************************************)
@@ -515,9 +518,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
       context     = [];
       case        = []
    } in
-   L.time_stamp "P : LEVEL 2  ";
-   HLog.debug "Procedural: level 2 transformation";
+   L.time_stamp "P : LEVEL 1  ";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_obj st ?flavour ?info anobj in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in
@@ -533,7 +540,11 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       context     = context;
       case        = []
    } in
-   HLog.debug "Procedural: level 2 transformation";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_proof st annterm in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli
index 230e74f46e54121183a2e5fb90191029b298b9de..8cbcb1c7e3f9457a578053e7fdcf41ac762fbe8e 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.mli
+++ b/helm/software/components/acic_procedural/acic2Procedural.mli
@@ -39,4 +39,6 @@ val procedural_of_acic_term:
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list
 
+val tex_formatter: Format.formatter option ref
+
 val debug: bool ref

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index d9d936f6aa622f5e2e01da6a28f90ba4779d9dc6..7d1e20a4d65cb67ba656b07c83e133204dd7c53d 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTeX.ml
+++ b/helm/software/components/acic_procedural/proceduralTeX.ml
@@ -179,24 +179,64 @@ 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.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 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