From 9e010764b6de0d8a268a6ecb83e8e90246bee129 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 18 Oct 2008 19:04:17 +0000 Subject: [PATCH] Acic2Procedural: now we accept an optional string argument "info" intended as a comment for the rendered proof (appears afer qed) ProceduralOptimizer: - we generate some comments for acic2Procedural.ml info (see above) - optimize_term is now available ApplyTransformation: we fixed a bug in the procedural rendering of auto proofs: the proof term must be optimized before rendering! (it is written on the paper about the procedural rendering for PLMMS 2007) --- .../acic_procedural/acic2Procedural.ml | 12 +- .../acic_procedural/acic2Procedural.mli | 2 +- .../acic_procedural/proceduralHelpers.ml | 21 +- .../acic_procedural/proceduralHelpers.mli | 6 +- .../acic_procedural/proceduralOptimizer.ml | 251 ++++++++---------- .../acic_procedural/proceduralOptimizer.mli | 4 +- helm/software/matita/applyTransformation.ml | 8 +- 7 files changed, 144 insertions(+), 160 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 253162009..c9a323248 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -447,13 +447,15 @@ let get_flavour ?flavour attrs = | Some fl -> fl | None -> aux attrs -let proc_obj ?flavour st = function +let proc_obj ?flavour ?(info="") st = function | C.AConstant (_, _, s, Some v, t, [], attrs) -> begin match get_flavour ?flavour attrs with | flavour when List.mem flavour th_flavours -> let ast = proc_proof st v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in - let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in + let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n" + "COMMENTS" info "tactics" steps "nodes" nodes + in T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text] | flavour when List.mem flavour def_flavours -> [T.Statement (flavour, Some s, t, Some v, "")] @@ -469,8 +471,8 @@ let proc_obj ?flavour st = function (* interface functions ******************************************************) -let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth - ?flavour prefix anobj = +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; @@ -481,7 +483,7 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth } in L.time_stamp "P : LEVEL 2 "; HLog.debug "Procedural: level 2 transformation"; - let steps = proc_obj st ?flavour anobj in + let steps = proc_obj st ?flavour ?info anobj in L.time_stamp "P : RENDERING"; HLog.debug "Procedural: grafite rendering"; let r = List.rev (T.render_steps [] steps) in diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index 852bc05a5..230e74f46 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -25,7 +25,7 @@ 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 -> + 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) diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 91f7016cd..7d95d8677 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -50,10 +50,10 @@ let abst s w = Some (s, C.Decl w) let abbr s v w = Some (s, C.Def (v, w)) let pp_sort out = function - | C.Type _ -> out "\Type" - | C.Prop -> out "\Prop" - | C.CProp _ -> out "\CProp" - | C.Set -> out "\Set" + | C.Type _ -> out "*Type" + | C.Prop -> out "*Prop" + | C.CProp _ -> out "*CProp" + | C.Set -> out "*Set" let pp_name out = function | C.Name s -> out s @@ -163,6 +163,19 @@ let mk_fresh_name context = function (* helper functions *********************************************************) +let rec list_fold_right_cps g map l a = + match l with + | [] -> g a + | hd :: tl -> + let h a = map g hd a in + list_fold_right_cps h map tl a + +let rec list_fold_left_cps g map a = function + | [] -> g a + | hd :: tl -> + let h a = list_fold_left_cps g map a tl in + map h a hd + let rec list_map_cps g map = function | [] -> g [] | hd :: tl -> diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 6b90e815c..1e0717efa 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -27,8 +27,12 @@ val pp_term: (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit val mk_fresh_name: Cic.context -> Cic.name -> Cic.name +val list_fold_right_cps: + ('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c +val list_fold_left_cps: + ('b -> 'c) -> (('b -> 'c) -> 'b -> 'a -> 'c) -> 'b -> 'a list -> 'c val list_map_cps: - ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b + ('b list -> 'c) -> (('b -> 'c) -> 'a -> 'c) -> 'a list -> 'c val identity: 'a -> 'a val compose: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 3ac567095..8d1108abe 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -43,7 +43,14 @@ module Cl = ProceduralClassify let debug = ref false -(* term preprocessing: optomization 1 ***************************************) +(* term optimization ********************************************************) + +type status = { + dummy: unit; + info: string +} + +let info st str = {st with info = st.info ^ str ^ "\n"} let defined_premise = "DEFINED" @@ -70,100 +77,106 @@ let rec add_abst k = function | 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 w t = +let rec opt_letin g st es c name v w t = let name = H.mk_fresh_name c name in let entry = Some (name, C.Def (v, w)) in - let g t = - if DTI.does_not_occur 1 t then begin + let g st t = + if DTI.does_not_occur 1 t then let x = S.lift (-1) t in - HLog.warn "Optimizer: remove 1"; opt1_proof g true c x - end else - let g = function + opt_proof g (info st "Optimizer: remove 1") true c x + else + let g st = function | C.LetIn (nname, vv, ww, tt) when H.is_proof c v -> let eentry = Some (nname, C.Def (vv, ww)) in - let ttw = H.get_type "opt1_letin 1" (eentry :: c) tt in + let ttw = H.get_type "opt_letin 1" (eentry :: c) tt in let x = C.LetIn (nname, vv, ww, - C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in - HLog.warn "Optimizer: swap 1"; opt1_proof g true c x - | v when H.is_proof c v && H.is_atomic v -> + C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) + in + opt_proof g (info st "Optimizer: swap 1") true c x + | v when H.is_proof c v && H.is_atomic v -> let x = S.subst v t in - HLog.warn "Optimizer: remove 5"; opt1_proof g true c x - | v -> - g (C.LetIn (name, v, w, t)) + opt_proof g (info st "Optimizer: remove 5") true c x + | v -> + g st (C.LetIn (name, v, w, t)) in - if es then opt1_term g es c v else g v + if es then opt_term g st es c v else g st v in - if es then opt1_proof g es (entry :: c) t else g t + if es then opt_proof g st es (entry :: c) t else g st t -and opt1_lambda g es c name w t = +and opt_lambda g st 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 = g (C.Lambda (name, w, t)) in - if es then opt1_proof g es (entry :: c) t else g t + let g st t = g st (C.Lambda (name, w, t)) in + if es then opt_proof g st es (entry :: c) t else g st t -and opt1_appl g es c t vs = - let g vs = - let g = function +and opt_appl g st es c t vs = + let g (st, vs) = + let g st = function | C.LetIn (mame, vv, tyty, tt) -> let vs = List.map (S.lift 1) vs in let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in - HLog.warn "Optimizer: swap 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: swap 2") true c x | C.Lambda (name, ww, tt) -> let v, vs = List.hd vs, List.tl vs in - let w = H.get_type "opt1_appl 1" c v in + let w = H.get_type "opt_appl 1" c v in let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in - HLog.warn "Optimizer: remove 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: remove 2") true c x | C.Appl vvs -> let x = C.Appl (vvs @ vs) in - HLog.warn "Optimizer: nested application"; opt1_proof g true c x + opt_proof g (info st "Optimizer: nested application") true c x | t -> - let rec aux d rvs = function +(* + let rec aux st d rvs = function | [], _ -> let x = C.Appl (t :: List.rev rvs) in - if d then opt1_proof g true c x else g x + if d then opt_proof g st true c x else g st 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 c v :: rvs) (vs, cs) - end else - aux d (v :: rvs) (vs, cs) + if H.is_not_atomic v && I.S.mem 0 cc && bb then + aux (st info "Optimizer: anticipate 1") true + (define c v :: rvs) (vs, cs) + else + aux st d (v :: rvs) (vs, cs) | _, [] -> assert false in - let h () = - let classes, conclusion = Cl.classify c (H.get_type "opt1_appl 3" c t) in +*) + let h st = + let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" 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 (C.Appl (t :: vvs)) :: vs) in - HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: anticipate 2") 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 c rv]) in - HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x + opt_proof g (info st "Optimizer: anticipate 3";) true c x | _ (* Some _, _ *) -> - g (C.Appl (t :: vs)) + g st (C.Appl (t :: vs)) (* | None, _ -> aux false [] (vs, classes) *) in - let rec aux h prev = function + let rec aux h st prev = function | C.LetIn (name, vv, tyty, 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 ww = H.get_type "opt1_appl 2" c vv in + let ww = H.get_type "opt_appl 2" c vv in let x = C.LetIn (name, vv, ww, y) in - HLog.warn "Optimizer: swap 3"; opt1_proof g true c x - | v :: vs -> aux h (v :: prev) vs - | [] -> h () + opt_proof g (info st "Optimizer: swap 3") true c x + | v :: vs -> aux h st (v :: prev) vs + | [] -> h st in - aux h [] vs + aux h st [] vs in - if es then opt1_proof g es c t else g t + if es then opt_proof g st es c t else g st t in - if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs + let map h v (st, vs) = + let h st vv = h (st, vv :: vs) in opt_term h st es c v + in + if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs) -and opt1_mutcase g es c uri tyno outty arg cases = +and opt_mutcase g st 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 @@ -190,116 +203,62 @@ and opt1_mutcase g es c uri tyno outty arg cases = 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 + opt_proof g (info st "Optimizer: remove 3") es c x -and opt1_other g es c t = g t +and opt_cast g st es c t w = + let g st t = g (info st "Optimizer: remove 4") t in + if es then opt_proof g st es c t else g st t -and opt1_proof g es c = function - | C.LetIn (name, v, ty, t) -> opt1_letin g es c name v ty 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 opt_other g st es c t = g st t -and opt1_term g es c t = - if H.is_proof c t then opt1_proof g es c t else g t +and opt_proof g st es c = function + | C.LetIn (name, v, ty, t) -> opt_letin g st es c name v ty t + | C.Lambda (name, w, t) -> opt_lambda g st es c name w t + | C.Appl (t :: v :: vs) -> opt_appl g st es c t (v :: vs) + | C.Appl [t] -> opt_proof g st es c t + | C.MutCase (u, n, t, v, ws) -> opt_mutcase g st es c u n t v ws + | C.Cast (t, w) -> opt_cast g st es c t w + | t -> opt_other g st es c t -(* term preprocessing: optomization 2 ***************************************) +and opt_term g st es c t = + if H.is_proof c t then opt_proof g st es c t else g st t -let expanded_premise = "EXPANDED" +(* object optimization ******************************************************) -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 w t = - let entry = Some (name, C.Def (v, w)) in - let g t = - let g v = g (C.LetIn (name, v, w, 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 "opt2_appl 1" c t) in - if vsno < csno then - let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" 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 "opt2_other" 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, w, t) -> opt2_letin g c name v w 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 wrap g st c bo = + try opt_term g st true c bo + with + | E.Object_not_found uri -> + let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in + failwith msg + | e -> + let msg = "optimize_obj: " ^ Printexc.to_string e in + failwith msg let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> - let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in - let g bo = - if !debug then begin - Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" - (Pp.ppterm bo) (I.count_nodes 0 bo); + let st, c = {info = ""; dummy = ()}, [] in + let bo, ty = H.cic_bc c bo, H.cic_bc c ty in + let g st bo = + if !debug then begin + Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo); prerr_string "H.pp_term : "; - H.pp_term prerr_string [] [] bo; prerr_newline () + H.pp_term prerr_string [] c bo; prerr_newline () end; (* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *) + let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in + let st = info st nodes in L.time_stamp ("PO: DONE " ^ name); - C.Constant (name, Some bo, ty, pars, attrs) + C.Constant (name, Some bo, ty, pars, attrs), st.info in - L.time_stamp ("PO: OPTIMIZING " ^ name); - if !debug then - Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" - name (I.count_nodes 0 bo); - begin try opt1_term g (* (opt2_term g []) *) true [] bo with - | E.Object_not_found uri -> - let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in - failwith msg - | e -> - let msg = "optimize_obj: " ^ Printexc.to_string e in - failwith msg - end - | obj -> obj + L.time_stamp ("PO: OPTIMIZING " ^ name); + if !debug then Printf.eprintf "BEGIN: %s\n" name; + let nodes = Printf.sprintf "Initial nodes: %u" (I.count_nodes 0 bo) in + wrap g (info st nodes) c bo + | obj -> obj, "" + +let optimize_term c bo = + let st = {info = ""; dummy = ()} in + let bo = H.cic_bc c bo in + let g st bo = bo, st.info in + wrap g st c bo diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.mli b/helm/software/components/acic_procedural/proceduralOptimizer.mli index 3e2eebf00..1e7bdada2 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.mli +++ b/helm/software/components/acic_procedural/proceduralOptimizer.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) -val optimize_obj: Cic.obj -> Cic.obj +val optimize_obj: Cic.obj -> Cic.obj * string + +val optimize_term: Cic.context -> Cic.term -> Cic.term * string val debug: bool ref diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index e1821ed88..ac044cefe 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -44,6 +44,7 @@ module G = GrafiteAst module GE = GrafiteEngine module LS = LibrarySync module Ds = CicDischarge +module PO = ProceduralOptimizer let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) @@ -203,7 +204,7 @@ let txt_of_cic_object (CicNotationPres.mpres_of_box bobj) ) | G.Procedural depth -> - let obj = ProceduralOptimizer.optimize_obj obj in + let obj, info = PO.optimize_obj obj in let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in let lazy_term_pp = term_pp in @@ -212,7 +213,7 @@ let txt_of_cic_object ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = Acic2Procedural.procedural_of_acic_object - ~ids_to_inner_sorts ~ids_to_inner_types + ~ids_to_inner_sorts ~ids_to_inner_types ~info ?depth ?flavour prefix aobj in "\n\n" ^ String.concat "" (List.map aux script) @@ -309,6 +310,7 @@ let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name = (* procedural_txt_of_cic_term *) let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = + let term, _info = PO.optimize_term context term in let annterm, ids_to_inner_sorts, ids_to_inner_types = try Cic2acic.acic_term_of_cic_term context term with e -> @@ -327,6 +329,8 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = String.concat "" (List.map aux script) ;; +(****************************************************************************) + let txt_of_macro ~map_unicode_to_tex metasenv context m = GrafiteAstPp.pp_macro ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context) -- 2.39.2