* http://cs.unibo.it/helm/.
*)
+module UM = UriManager
module C = Cic
module Pp = CicPp
module I = CicInspect
+module E = CicEnvironment
module S = CicSubstitution
module DTI = DoubleTypeInference
module HEL = HExtlib
module PEH = ProofEngineHelpers
+module TC = CicTypeChecker
+module Un = CicUniv
+module L = Librarian
+module Ut = CicUtil
module H = ProceduralHelpers
module Cl = ProceduralClassify
-(* term preprocessing: optomization 1 ***************************************)
+(* debugging ****************************************************************)
-let defined_premise = "DEFINED"
+let debug = ref false
-let define v =
+(* term optimization ********************************************************)
+
+let critical = ref true
+
+type status = {
+ dummy: unit;
+ info: string
+}
+
+let info st str = {st with info = st.info ^ str ^ "\n"}
+
+let defined_premise = "LOCAL"
+
+let define c v =
let name = C.Name defined_premise in
- C.LetIn (name, v, C.Rel 1)
+ let ty = H.get_type "define" c v in
+ C.LetIn (name, v, ty, C.Rel 1)
let clear_absts m =
let rec aux k n = function
| 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
+ Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
+ assert false
+ | t -> t
in
aux m
| 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 rec opt_letin g st es c name v w t =
+ let name = H.mk_fresh_name true c name in
+ let entry = Some (name, C.Def (v, w)) in
+ 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
- | 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))
+ 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 "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
+ 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
+ opt_proof g (info st "Optimizer: remove 5") true c x
+(* | v when t = C.Rel 1 ->
+ g (info st "Optimizer: remove 6") v
+*) | 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 =
- let name = H.mk_fresh_name c name in
+and opt_lambda g st es c name w t =
+ let name = H.mk_fresh_name true 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
+ 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
- | C.LetIn (mame, vv, tt) ->
+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, C.Appl (tt :: vs)) in
- HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
+ let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in
+ 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 x = C.Appl (C.LetIn (name, v, tt) :: vs) in
- HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
+ let w = H.get_type "opt_appl 1" c v in
+ let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in
+ 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 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 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.Appl (t :: vvs)) :: vs) in
- HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x
+ let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
+ 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 rv]) in
- HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
+ let x = C.Appl (t :: List.rev rvs @ [define c rv]) in
+ 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
- | C.LetIn (name, vv, tt) :: vs ->
+ 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 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 ()
+ let ww = H.get_type "opt_appl 2" c vv in
+ let x = C.LetIn (name, vv, ww, y) in
+ 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
+ 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_map_cps g (fun h -> opt1_term h es c) vs else g vs
+ 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_critical 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
let lps, rps = HEL.split_nth lpsno ps in
let rpsno = List.length rps in
+ if rpsno = 0 && sort_disp = 0 then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ opt_mutcase_plain g st es c uri tyno outty arg cases
+ else
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)
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
+ opt_proof g (info st "Optimizer: remove 3") es c x
-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)
+and opt_mutcase_plain g st es c uri tyno outty arg cases =
+ let g st v =
+ let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ let map h v (st, vs) =
+ let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+ in
+ if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
in
- g (absts t)
+ if es then opt_proof g st es c arg else g st arg
-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 opt_mutcase g =
+ if !critical then opt_mutcase_critical g else opt_mutcase_plain g
-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 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 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 opt_other g st es c t = g st t
-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 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
-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 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
-and opt2_term g c t =
- if H.is_proof c t then opt2_proof g c t else g t
+(* object optimization ******************************************************)
-(* 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 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)
+ let count_nodes = I.count_nodes ~meta:false 0 in
+ let st, c = {info = ""; dummy = ()}, [] in
+ L.time_stamp ("PO: OPTIMIZING " ^ name);
+ let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
+ if !debug then begin
+ Printf.eprintf "BEGIN: %s\n" name;
+ Printf.eprintf "Initial : %s\n" (Pp.ppterm bo);
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
+ end;
+ 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 "Ut.pp_term : ";
+ Ut.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" (count_nodes bo) in
+ let st = info st nodes in
+ L.time_stamp ("PO: DONE " ^ name);
+ C.Constant (name, Some bo, ty, pars, attrs), st.info
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
+ 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
projects / helm.git / blobdiff