From ff3bd23d19abd7c9e981fd754f54d536fc563ec3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Feb 2009 20:54:13 +0000 Subject: [PATCH] ProceduralTeX completed and tested on the terms given as examples in the paper about the procedural reconstruction --- .../components/acic_procedural/.depend | 10 +-- .../components/acic_procedural/.depend.opt | 10 +-- .../components/acic_procedural/Makefile | 2 +- .../acic_procedural/acic2Procedural.ml | 17 ++++- .../acic_procedural/acic2Procedural.mli | 2 + .../acic_procedural/proceduralTeX.ml | 64 +++++++++++++++---- 6 files changed, 81 insertions(+), 24 deletions(-) diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index d79de5566..4a57a7a11 100644 --- 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 d79de5566..4a57a7a11 100644 --- 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 06538c53e..2ed14382a 100644 --- 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 ae64d1f19..0edb5c8b0 100644 --- 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 230e74f46..8cbcb1c7e 100644 --- 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 d9d936f6a..7d1e20a4d 100644 --- 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 -- 2.39.2