From df3e9efe1690fb5d93061b657e6ddcc3c11745db Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 11 Mar 2009 13:20:57 +0000 Subject: [PATCH] the level 1 reconstruction procedure is now in Procedural1 Procedural2 coming soon .... --- .../components/acic_procedural/.depend | 11 ++++--- .../components/acic_procedural/.depend.opt | 11 ++++--- .../components/acic_procedural/Makefile | 1 + .../acic_procedural/acic2Procedural.ml | 29 ++++++------------- .../acic_procedural/acic2Procedural.mli | 2 -- .../{procedural-1.ml => procedural1.ml} | 0 .../{procedural-1.mli => procedural1.mli} | 23 +++++++-------- 7 files changed, 34 insertions(+), 43 deletions(-) rename helm/software/components/acic_procedural/{procedural-1.ml => procedural1.ml} (100%) rename helm/software/components/acic_procedural/{procedural-1.mli => procedural1.mli} (63%) diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 4a57a7a11..96306b2e6 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,3 +1,4 @@ +procedural1.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi @@ -13,13 +14,15 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi +procedural1.cmo: proceduralTypes.cmi proceduralTeX.cmi proceduralHelpers.cmi \ + proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi +procedural1.cmx: proceduralTypes.cmx proceduralTeX.cmx proceduralHelpers.cmx \ + proceduralConversion.cmx proceduralClassify.cmx procedural1.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.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural1.cmi \ acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \ - proceduralHelpers.cmx proceduralConversion.cmx proceduralClassify.cmx \ +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural1.cmx \ acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 4a57a7a11..96306b2e6 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,3 +1,4 @@ +procedural1.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi @@ -13,13 +14,15 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi +procedural1.cmo: proceduralTypes.cmi proceduralTeX.cmi proceduralHelpers.cmi \ + proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi +procedural1.cmx: proceduralTypes.cmx proceduralTeX.cmx proceduralHelpers.cmx \ + proceduralConversion.cmx proceduralClassify.cmx procedural1.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.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural1.cmi \ acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \ - proceduralHelpers.cmx proceduralConversion.cmx proceduralClassify.cmx \ +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural1.cmx \ acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index 2ed14382a..d0304111f 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/components/acic_procedural/Makefile @@ -8,6 +8,7 @@ INTERFACE_FILES = \ proceduralTypes.mli \ proceduralMode.mli \ proceduralConversion.mli \ + procedural1.mli \ proceduralTeX.mli \ acic2Procedural.mli \ $(NULL) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 043bd6e3a..f749ce8d2 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +module L = Librarian + +module T = ProceduralTypes module P1 = Procedural1 module X = ProceduralTeX @@ -32,20 +35,13 @@ let tex_formatter = ref None let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?info ?depth ?flavour prefix anobj = - let st = { - sorts = ids_to_inner_sorts; - types = ids_to_inner_types; - max_depth = depth; - depth = 0; - context = []; - case = [] - } in + let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in L.time_stamp "P : LEVEL 1 "; HLog.debug "Procedural: level 1 transformation"; - let steps = proc_obj st ?flavour ?info anobj in + let steps = P1.proc_obj st ?flavour ?info anobj in let _ = match !tex_formatter with | None -> () - | Some frm -> X.tex_of_steps frm st.sorts steps + | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps in L.time_stamp "P : RENDERING"; HLog.debug "Procedural: grafite rendering"; @@ -54,19 +50,12 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix context annterm = - let st = { - sorts = ids_to_inner_sorts; - types = ids_to_inner_types; - max_depth = depth; - depth = 0; - context = context; - case = [] - } in + let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in HLog.debug "Procedural: level 1 transformation"; - let steps = proc_proof st annterm in + let steps = P1.proc_proof st annterm in let _ = match !tex_formatter with | None -> () - | Some frm -> X.tex_of_steps frm st.sorts steps + | Some frm -> X.tex_of_steps frm ids_to_inner_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 8cbcb1c7e..082bb071b 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -40,5 +40,3 @@ val procedural_of_acic_term: GrafiteAst.statement list val tex_formatter: Format.formatter option ref - -val debug: bool ref diff --git a/helm/software/components/acic_procedural/procedural-1.ml b/helm/software/components/acic_procedural/procedural1.ml similarity index 100% rename from helm/software/components/acic_procedural/procedural-1.ml rename to helm/software/components/acic_procedural/procedural1.ml diff --git a/helm/software/components/acic_procedural/procedural-1.mli b/helm/software/components/acic_procedural/procedural1.mli similarity index 63% rename from helm/software/components/acic_procedural/procedural-1.mli rename to helm/software/components/acic_procedural/procedural1.mli index 8cbcb1c7e..708e698df 100644 --- a/helm/software/components/acic_procedural/procedural-1.mli +++ b/helm/software/components/acic_procedural/procedural1.mli @@ -23,22 +23,19 @@ * http://cs.unibo.it/helm/. *) -val procedural_of_acic_object: - ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> - ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> ?info:string -> - ?depth:int -> ?flavour:Cic.object_flavour -> string -> Cic.annobj -> - (Cic.annterm, Cic.annterm, - Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) - GrafiteAst.statement list +type status -val procedural_of_acic_term: +val init: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> string -> Cic.context -> Cic.annterm -> - (Cic.annterm, Cic.annterm, - Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) - GrafiteAst.statement list + ?depth:int -> Cic.context -> status + +val proc_proof: + status -> Cic.annterm -> + ProceduralTypes.step list -val tex_formatter: Format.formatter option ref +val proc_obj: + ?flavour:Cic.object_flavour -> ?info:string -> status -> Cic.annobj -> + ProceduralTypes.step list val debug: bool ref -- 2.39.2