From 93afc8e27cf27754ff73b426e0b1d4df97224dee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 2 Apr 2007 12:20:41 +0000 Subject: [PATCH] Procedural: refactoring --- helm/software/components/acic_procedural/.depend | 14 ++++++-------- .../components/acic_procedural/.depend.opt | 14 ++++++-------- helm/software/components/acic_procedural/Makefile | 2 +- .../acic_procedural/proceduralConversion.ml | 4 ---- ...ceduralPreprocess.ml => proceduralOptimizer.ml} | 2 +- ...duralPreprocess.mli => proceduralOptimizer.mli} | 2 +- helm/software/matita/applyTransformation.ml | 2 +- 7 files changed, 16 insertions(+), 24 deletions(-) rename helm/software/components/acic_procedural/{proceduralPreprocess.ml => proceduralOptimizer.ml} (99%) rename helm/software/components/acic_procedural/{proceduralPreprocess.mli => proceduralOptimizer.mli} (96%) diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 02ce90009..1de52479d 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -2,18 +2,16 @@ proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi -proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ - proceduralPreprocess.cmi -proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ - proceduralPreprocess.cmi +proceduralOptimizer.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ + proceduralOptimizer.cmi +proceduralOptimizer.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ + proceduralOptimizer.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ - proceduralMode.cmi proceduralConversion.cmi -proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ - proceduralMode.cmx proceduralConversion.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ proceduralClassify.cmi acic2Procedural.cmi acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 02ce90009..1de52479d 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -2,18 +2,16 @@ proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi -proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ - proceduralPreprocess.cmi -proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ - proceduralPreprocess.cmi +proceduralOptimizer.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ + proceduralOptimizer.cmi +proceduralOptimizer.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ + proceduralOptimizer.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ - proceduralMode.cmi proceduralConversion.cmi -proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ - proceduralMode.cmx proceduralConversion.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ proceduralClassify.cmi acic2Procedural.cmi acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index 78d3e3b09..df39ba896 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/components/acic_procedural/Makefile @@ -4,7 +4,7 @@ PREDICATES = INTERFACE_FILES = \ proceduralHelpers.mli \ proceduralClassify.mli \ - proceduralPreprocess.mli \ + proceduralOptimizer.mli \ proceduralTypes.mli \ proceduralMode.mli \ proceduralConversion.mli \ diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 5f705053a..538981369 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -31,10 +31,6 @@ module D = Deannotate module UM = UriManager module Rd = CicReduction -module P = ProceduralPreprocess -module T = ProceduralTypes -module M = ProceduralMode - (* helpers ******************************************************************) let cic = D.deannotate_term diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml similarity index 99% rename from helm/software/components/acic_procedural/proceduralPreprocess.ml rename to helm/software/components/acic_procedural/proceduralOptimizer.ml index 2b8e1ea3d..fe06207d3 100644 --- a/helm/software/components/acic_procedural/proceduralPreprocess.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -261,7 +261,7 @@ and opt2_term g c t = (* object preprocessing *****************************************************) -let pp_obj = function +let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> let g bo = Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo); diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.mli b/helm/software/components/acic_procedural/proceduralOptimizer.mli similarity index 96% rename from helm/software/components/acic_procedural/proceduralPreprocess.mli rename to helm/software/components/acic_procedural/proceduralOptimizer.mli index 6d66bf237..45505d72c 100644 --- a/helm/software/components/acic_procedural/proceduralPreprocess.mli +++ b/helm/software/components/acic_procedural/proceduralOptimizer.mli @@ -23,4 +23,4 @@ * http://cs.unibo.it/helm/. *) -val pp_obj: Cic.obj -> Cic.obj +val optimize_obj: Cic.obj -> Cic.obj diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index cff93ace3..de87d5548 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -179,7 +179,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj = (CicNotationPres.mpres_of_box bobj) ) | G.Procedural depth -> - let obj = ProceduralPreprocess.pp_obj obj in + let obj = ProceduralOptimizer.optimize_obj obj in let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in let term_pp = term2pres (n - 8) ids_to_inner_sorts in let lazy_term_pp = term_pp in -- 2.39.2