From: Ferruccio Guidi Date: Mon, 2 Apr 2007 12:20:41 +0000 (+0000) Subject: Procedural: refactoring X-Git-Tag: make_still_working~6412 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93afc8e27cf27754ff73b426e0b1d4df97224dee;p=helm.git Procedural: refactoring --- 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/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml new file mode 100644 index 000000000..fe06207d3 --- /dev/null +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -0,0 +1,274 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module Pp = CicPp +module I = CicInspect +module S = CicSubstitution +module DTI = DoubleTypeInference +module HEL = HExtlib +module PEH = ProofEngineHelpers + +module H = ProceduralHelpers +module Cl = ProceduralClassify + +(* term preprocessing: optomization 1 ***************************************) + +let defined_premise = "DEFINED" + +let define v = + let name = C.Name defined_premise in + C.LetIn (name, v, C.Rel 1) + +let clear_absts m = + let rec aux k n = function + | C.Lambda (s, v, t) when k > 0 -> + C.Lambda (s, v, aux (pred k) n t) + | C.Lambda (_, _, t) when n > 0 -> + aux 0 (pred n) (S.lift (-1) t) + | t when n > 0 -> + Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t); + assert false + | t -> t + in + aux m + +let rec add_abst k = function + | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t) + | t when k > 0 -> assert false + | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t) + +let rec opt1_letin g es c name v t = + let name = H.mk_fresh_name c name in + let entry = Some (name, C.Def (v, None)) in + let g t = + if DTI.does_not_occur 1 t then begin + let x = S.lift (-1) t in + HLog.warn "Optimizer: remove 1"; opt1_proof g true c x + end else + let g = function + | C.LetIn (nname, vv, tt) when H.is_proof c v -> + let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in + HLog.warn "Optimizer: swap 1"; opt1_proof g true c x + | v -> + g (C.LetIn (name, v, t)) + in + if es then opt1_term g es c v else g v + in + if es then opt1_proof g es (entry :: c) t else g t + +and opt1_lambda g es c name w t = + let name = H.mk_fresh_name c name in + let entry = Some (name, C.Decl w) in + let g t = + let name = if DTI.does_not_occur 1 t then C.Anonymous else name in + g (C.Lambda (name, w, t)) + in + if es then opt1_proof g es (entry :: c) t else g t + +and opt1_appl g es c t vs = + let g vs = + let g = function + | C.LetIn (mame, vv, tt) -> + let vs = List.map (S.lift 1) vs in + let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in + HLog.warn "Optimizer: swap 2"; opt1_proof g true c x + | C.Lambda (name, ww, tt) -> + let v, vs = List.hd vs, List.tl vs in + let x = C.Appl (C.LetIn (name, v, tt) :: vs) in + HLog.warn "Optimizer: remove 2"; opt1_proof g true c x + | C.Appl vvs -> + let x = C.Appl (vvs @ vs) in + HLog.warn "Optimizer: nested application"; opt1_proof g true c x + | t -> + let rec aux d rvs = function + | [], _ -> + let x = C.Appl (t :: List.rev rvs) in + if d then opt1_proof g true c x else g x + | v :: vs, (cc, bb) :: cs -> + if H.is_not_atomic v && I.S.mem 0 cc && bb then begin + HLog.warn "Optimizer: anticipate 1"; + aux true (define v :: rvs) (vs, cs) + end else + aux d (v :: rvs) (vs, cs) + | _, [] -> assert false + in + let h () = + let classes, conclusion = Cl.classify c (H.get_type c t) in + let csno, vsno = List.length classes, List.length vs in + if csno < vsno then + let vvs, vs = HEL.split_nth csno vs in + let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in + HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x + else match conclusion, List.rev vs with + | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv -> + let x = C.Appl (t :: List.rev rvs @ [define rv]) in + HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x + | Some _, _ -> + g (C.Appl (t :: vs)) + | None, _ -> + aux false [] (vs, classes) + in + let rec aux h prev = function + | C.LetIn (name, vv, tt) :: vs -> + let t = S.lift 1 t in + let prev = List.map (S.lift 1) prev in + let vs = List.map (S.lift 1) vs in + let y = C.Appl (t :: List.rev prev @ tt :: vs) in + let x = C.LetIn (name, vv, y) in + HLog.warn "Optimizer: swap 3"; opt1_proof g true c x + | v :: vs -> aux h (v :: prev) vs + | [] -> h () + in + aux h [] vs + in + if es then opt1_proof g es c t else g t + in + if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs + +and opt1_mutcase g es c uri tyno outty arg cases = + let eliminator = H.get_default_eliminator c uri tyno outty in + let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in + let ps, sort_disp = H.get_ind_parameters c arg in + let lps, rps = HEL.split_nth lpsno ps in + let rpsno = List.length rps in + let predicate = clear_absts rpsno (1 - sort_disp) outty in + let is_recursive t = + I.S.mem tyno (I.get_mutinds_of_uri uri t) + in + let map2 case (_, cty) = + let map (h, case, k) (_, premise) = + if h > 0 then pred h, case, k else + if is_recursive premise then + 0, add_abst k case, k + 2 + else + 0, case, succ k + in + let premises, _ = PEH.split_with_whd (c, cty) in + let _, lifted_case, _ = + List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises)) + in + lifted_case + in + let lifted_cases = List.map2 map2 cases constructors in + let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in + let x = H.refine c (C.Appl args) in + HLog.warn "Optimizer: remove 3"; opt1_proof g es c x + +and opt1_cast g es c t w = + let g t = HLog.warn "Optimizer: remove 4"; g t in + if es then opt1_proof g es c t else g t + +and opt1_other g es c t = g t + +and opt1_proof g es c = function + | C.LetIn (name, v, t) -> opt1_letin g es c name v t + | C.Lambda (name, w, t) -> opt1_lambda g es c name w t + | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs) + | C.Appl [t] -> opt1_proof g es c t + | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws + | C.Cast (t, w) -> opt1_cast g es c t w + | t -> opt1_other g es c t + +and opt1_term g es c t = + if H.is_proof c t then opt1_proof g es c t else g t + +(* term preprocessing: optomization 2 ***************************************) + +let expanded_premise = "EXPANDED" + +let eta_expand g tys t = + assert (tys <> []); + let name i = Printf.sprintf "%s%u" expanded_premise i in + let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in + let arg i = C.Rel (succ i) in + let rec aux i f a = function + | [] -> f, a + | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl + in + let n = List.length tys in + let absts, args = aux 0 H.identity [] tys in + let t = match S.lift n t with + | C.Appl ts -> C.Appl (ts @ args) + | t -> C.Appl (t :: args) + in + g (absts t) + +let rec opt2_letin g c name v t = + let entry = Some (name, C.Def (v, None)) in + let g t = + let g v = g (C.LetIn (name, v, t)) in + opt2_term g c v + in + opt2_proof g (entry :: c) t + +and opt2_lambda g c name w t = + let entry = Some (name, C.Decl w) in + let g t = g (C.Lambda (name, w, t)) in + opt2_proof g (entry :: c) t + +and opt2_appl g c t vs = + let g vs = + let x = C.Appl (t :: vs) in + let vsno = List.length vs in + let _, csno = PEH.split_with_whd (c, H.get_type c t) in + if vsno < csno then + let tys, _ = PEH.split_with_whd (c, H.get_type c x) in + let tys = List.rev (List.tl tys) in + let tys, _ = HEL.split_nth (csno - vsno) tys in + HLog.warn "Optimizer: eta 1"; eta_expand g tys x + else g x + in + H.list_map_cps g (fun h -> opt2_term h c) vs + +and opt2_other g c t = + let tys, csno = PEH.split_with_whd (c, H.get_type c t) in + if csno > 0 then begin + let tys = List.rev (List.tl tys) in + HLog.warn "Optimizer: eta 2"; eta_expand g tys t + end else g t + +and opt2_proof g c = function + | C.LetIn (name, v, t) -> opt2_letin g c name v t + | C.Lambda (name, w, t) -> opt2_lambda g c name w t + | C.Appl (t :: vs) -> opt2_appl g c t vs + | t -> opt2_other g c t + +and opt2_term g c t = + if H.is_proof c t then opt2_proof g c t else g t + +(* object preprocessing *****************************************************) + +let optimize_obj = function + | C.Constant (name, Some bo, ty, pars, attrs) -> + let g bo = + Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo); + let _ = H.get_type [] (C.Cast (bo, ty)) in + C.Constant (name, Some bo, ty, pars, attrs) + in + Printf.eprintf "BEGIN: %s\n" name; + begin try opt1_term (opt2_term g []) true [] bo + with e -> failwith ("PPP: " ^ Printexc.to_string e) end + | obj -> obj diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.mli b/helm/software/components/acic_procedural/proceduralOptimizer.mli new file mode 100644 index 000000000..45505d72c --- /dev/null +++ b/helm/software/components/acic_procedural/proceduralOptimizer.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val optimize_obj: Cic.obj -> Cic.obj diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.ml b/helm/software/components/acic_procedural/proceduralPreprocess.ml deleted file mode 100644 index 2b8e1ea3d..000000000 --- a/helm/software/components/acic_procedural/proceduralPreprocess.ml +++ /dev/null @@ -1,274 +0,0 @@ -(* Copyright (C) 2003-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -module C = Cic -module Pp = CicPp -module I = CicInspect -module S = CicSubstitution -module DTI = DoubleTypeInference -module HEL = HExtlib -module PEH = ProofEngineHelpers - -module H = ProceduralHelpers -module Cl = ProceduralClassify - -(* term preprocessing: optomization 1 ***************************************) - -let defined_premise = "DEFINED" - -let define v = - let name = C.Name defined_premise in - C.LetIn (name, v, C.Rel 1) - -let clear_absts m = - let rec aux k n = function - | C.Lambda (s, v, t) when k > 0 -> - C.Lambda (s, v, aux (pred k) n t) - | C.Lambda (_, _, t) when n > 0 -> - aux 0 (pred n) (S.lift (-1) t) - | t when n > 0 -> - Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t); - assert false - | t -> t - in - aux m - -let rec add_abst k = function - | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t) - | t when k > 0 -> assert false - | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t) - -let rec opt1_letin g es c name v t = - let name = H.mk_fresh_name c name in - let entry = Some (name, C.Def (v, None)) in - let g t = - if DTI.does_not_occur 1 t then begin - let x = S.lift (-1) t in - HLog.warn "Optimizer: remove 1"; opt1_proof g true c x - end else - let g = function - | C.LetIn (nname, vv, tt) when H.is_proof c v -> - let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in - HLog.warn "Optimizer: swap 1"; opt1_proof g true c x - | v -> - g (C.LetIn (name, v, t)) - in - if es then opt1_term g es c v else g v - in - if es then opt1_proof g es (entry :: c) t else g t - -and opt1_lambda g es c name w t = - let name = H.mk_fresh_name c name in - let entry = Some (name, C.Decl w) in - let g t = - let name = if DTI.does_not_occur 1 t then C.Anonymous else name in - g (C.Lambda (name, w, t)) - in - if es then opt1_proof g es (entry :: c) t else g t - -and opt1_appl g es c t vs = - let g vs = - let g = function - | C.LetIn (mame, vv, tt) -> - let vs = List.map (S.lift 1) vs in - let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in - HLog.warn "Optimizer: swap 2"; opt1_proof g true c x - | C.Lambda (name, ww, tt) -> - let v, vs = List.hd vs, List.tl vs in - let x = C.Appl (C.LetIn (name, v, tt) :: vs) in - HLog.warn "Optimizer: remove 2"; opt1_proof g true c x - | C.Appl vvs -> - let x = C.Appl (vvs @ vs) in - HLog.warn "Optimizer: nested application"; opt1_proof g true c x - | t -> - let rec aux d rvs = function - | [], _ -> - let x = C.Appl (t :: List.rev rvs) in - if d then opt1_proof g true c x else g x - | v :: vs, (cc, bb) :: cs -> - if H.is_not_atomic v && I.S.mem 0 cc && bb then begin - HLog.warn "Optimizer: anticipate 1"; - aux true (define v :: rvs) (vs, cs) - end else - aux d (v :: rvs) (vs, cs) - | _, [] -> assert false - in - let h () = - let classes, conclusion = Cl.classify c (H.get_type c t) in - let csno, vsno = List.length classes, List.length vs in - if csno < vsno then - let vvs, vs = HEL.split_nth csno vs in - let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in - HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x - else match conclusion, List.rev vs with - | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv -> - let x = C.Appl (t :: List.rev rvs @ [define rv]) in - HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x - | Some _, _ -> - g (C.Appl (t :: vs)) - | None, _ -> - aux false [] (vs, classes) - in - let rec aux h prev = function - | C.LetIn (name, vv, tt) :: vs -> - let t = S.lift 1 t in - let prev = List.map (S.lift 1) prev in - let vs = List.map (S.lift 1) vs in - let y = C.Appl (t :: List.rev prev @ tt :: vs) in - let x = C.LetIn (name, vv, y) in - HLog.warn "Optimizer: swap 3"; opt1_proof g true c x - | v :: vs -> aux h (v :: prev) vs - | [] -> h () - in - aux h [] vs - in - if es then opt1_proof g es c t else g t - in - if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs - -and opt1_mutcase g es c uri tyno outty arg cases = - let eliminator = H.get_default_eliminator c uri tyno outty in - let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in - let ps, sort_disp = H.get_ind_parameters c arg in - let lps, rps = HEL.split_nth lpsno ps in - let rpsno = List.length rps in - let predicate = clear_absts rpsno (1 - sort_disp) outty in - let is_recursive t = - I.S.mem tyno (I.get_mutinds_of_uri uri t) - in - let map2 case (_, cty) = - let map (h, case, k) (_, premise) = - if h > 0 then pred h, case, k else - if is_recursive premise then - 0, add_abst k case, k + 2 - else - 0, case, succ k - in - let premises, _ = PEH.split_with_whd (c, cty) in - let _, lifted_case, _ = - List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises)) - in - lifted_case - in - let lifted_cases = List.map2 map2 cases constructors in - let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in - let x = H.refine c (C.Appl args) in - HLog.warn "Optimizer: remove 3"; opt1_proof g es c x - -and opt1_cast g es c t w = - let g t = HLog.warn "Optimizer: remove 4"; g t in - if es then opt1_proof g es c t else g t - -and opt1_other g es c t = g t - -and opt1_proof g es c = function - | C.LetIn (name, v, t) -> opt1_letin g es c name v t - | C.Lambda (name, w, t) -> opt1_lambda g es c name w t - | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs) - | C.Appl [t] -> opt1_proof g es c t - | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws - | C.Cast (t, w) -> opt1_cast g es c t w - | t -> opt1_other g es c t - -and opt1_term g es c t = - if H.is_proof c t then opt1_proof g es c t else g t - -(* term preprocessing: optomization 2 ***************************************) - -let expanded_premise = "EXPANDED" - -let eta_expand g tys t = - assert (tys <> []); - let name i = Printf.sprintf "%s%u" expanded_premise i in - let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in - let arg i = C.Rel (succ i) in - let rec aux i f a = function - | [] -> f, a - | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl - in - let n = List.length tys in - let absts, args = aux 0 H.identity [] tys in - let t = match S.lift n t with - | C.Appl ts -> C.Appl (ts @ args) - | t -> C.Appl (t :: args) - in - g (absts t) - -let rec opt2_letin g c name v t = - let entry = Some (name, C.Def (v, None)) in - let g t = - let g v = g (C.LetIn (name, v, t)) in - opt2_term g c v - in - opt2_proof g (entry :: c) t - -and opt2_lambda g c name w t = - let entry = Some (name, C.Decl w) in - let g t = g (C.Lambda (name, w, t)) in - opt2_proof g (entry :: c) t - -and opt2_appl g c t vs = - let g vs = - let x = C.Appl (t :: vs) in - let vsno = List.length vs in - let _, csno = PEH.split_with_whd (c, H.get_type c t) in - if vsno < csno then - let tys, _ = PEH.split_with_whd (c, H.get_type c x) in - let tys = List.rev (List.tl tys) in - let tys, _ = HEL.split_nth (csno - vsno) tys in - HLog.warn "Optimizer: eta 1"; eta_expand g tys x - else g x - in - H.list_map_cps g (fun h -> opt2_term h c) vs - -and opt2_other g c t = - let tys, csno = PEH.split_with_whd (c, H.get_type c t) in - if csno > 0 then begin - let tys = List.rev (List.tl tys) in - HLog.warn "Optimizer: eta 2"; eta_expand g tys t - end else g t - -and opt2_proof g c = function - | C.LetIn (name, v, t) -> opt2_letin g c name v t - | C.Lambda (name, w, t) -> opt2_lambda g c name w t - | C.Appl (t :: vs) -> opt2_appl g c t vs - | t -> opt2_other g c t - -and opt2_term g c t = - if H.is_proof c t then opt2_proof g c t else g t - -(* object preprocessing *****************************************************) - -let pp_obj = function - | C.Constant (name, Some bo, ty, pars, attrs) -> - let g bo = - Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo); - let _ = H.get_type [] (C.Cast (bo, ty)) in - C.Constant (name, Some bo, ty, pars, attrs) - in - Printf.eprintf "BEGIN: %s\n" name; - begin try opt1_term (opt2_term g []) true [] bo - with e -> failwith ("PPP: " ^ Printexc.to_string e) end - | obj -> obj diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.mli b/helm/software/components/acic_procedural/proceduralPreprocess.mli deleted file mode 100644 index 6d66bf237..000000000 --- a/helm/software/components/acic_procedural/proceduralPreprocess.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* Copyright (C) 2003-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val pp_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