* http://cs.unibo.it/helm/.
*)
-module UM = UriManager
module C = Cic
module Pp = CicPp
-module Un = CicUniv
module I = CicInspect
-module E = CicEnvironment
module S = CicSubstitution
-module TC = CicTypeChecker
-module Rf = CicRefine
module DTI = DoubleTypeInference
module HEL = HExtlib
module PEH = ProofEngineHelpers
+module H = ProceduralHelpers
module Cl = ProceduralClassify
-(* helper functions *********************************************************)
-
-let rec list_map_cps g map = function
- | [] -> g []
- | hd :: tl ->
- let h hd =
- let g tl = g (hd :: tl) in
- list_map_cps g map tl
- in
- map h hd
-
-let identity x = x
-
-let comp f g x = f (g x)
-
-let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
- with e ->
- Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
- Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
- Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
- raise e
-
-let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
- with e ->
- Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
- Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
- raise e
-
-let get_tail c t =
- match PEH.split_with_whd (c, t) with
- | (_, hd) :: _, _ -> hd
- | _ -> assert false
-
-let is_proof c t =
- match get_tail c (get_type c (get_type c t)) with
- | C.Sort C.Prop -> true
- | C.Sort _ -> false
- | _ -> assert false
-
-let is_not_atomic = function
- | C.Sort _
- | C.Rel _
- | C.Const _
- | C.Var _
- | C.MutInd _
- | C.MutConstruct _ -> false
- | _ -> true
-
-let get_ind_type uri tyno =
- match E.get_obj Un.empty_ugraph uri with
- | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
- | _ -> assert false
-
-let get_default_eliminator context uri tyno ty =
- let _, (name, _, _, _) = get_ind_type uri tyno in
- let ext = match get_tail context (get_type context ty) with
- | C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.CProp -> "_rec"
- | C.Sort (C.Type _) -> "_rect"
- | t ->
- Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
- assert false
- in
- let buri = UM.buri_of_uri uri in
- let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
- C.Const (uri, [])
-
-let get_ind_parameters c t =
- let ty = get_type c t in
- let ps = match get_tail c ty with
- | C.MutInd _ -> []
- | C.Appl (C.MutInd _ :: args) -> args
- | _ -> assert false
- in
- let disp = match get_tail c (get_type c ty) with
- | C.Sort C.Prop -> 0
- | C.Sort _ -> 1
- | _ -> assert false
- in
- ps, disp
-
(* term preprocessing: optomization 1 ***************************************)
let defined_premise = "DEFINED"
-let define c v =
+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, t) when k > 0 ->
C.Lambda (s, v, aux (pred k) n t)
- | C.Lambda (_, _, t) when n > 0 ->
+ | C.Lambda (_, _, t) when n > 0 ->
aux 0 (pred n) (S.lift (-1) t)
- | t when n > 0 ->
+ | t when n > 0 ->
Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
assert false
| t -> t
| 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
- HLog.warn "Optimizer: remove 1"; g (S.lift (-1) t)
+ 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 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 false c x
+ | 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_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
| 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 false c x
+ 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 false c x
+ 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 false c x
+ 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 false c x else g x
- | v :: vs, (c, b) :: cs ->
- if is_not_atomic v && I.S.mem 0 c && b then begin
+ 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 c v :: rvs) (vs, cs)
+ aux true (define v :: rvs) (vs, cs)
end else
aux d (v :: rvs) (vs, cs)
- | _, [] -> assert false
+ | _, [] -> assert false
in
let h () =
- let classes, conclusion = Cl.classify c (get_type c t) in
+ 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 && csno > 0 then
+ 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 false c x
+ 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 && is_not_atomic rv ->
- let x = C.Appl (t :: List.rev rvs @ [define c rv]) in
- HLog.warn "Optimizer: anticipate 3"; opt1_proof g false c x
+ | 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, _ ->
- if csno > 0 then aux false [] (vs, classes)
- else g (C.Appl (t :: vs))
+ aux false [] (vs, classes)
in
let rec aux h prev = function
| C.LetIn (name, vv, tt) :: vs ->
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 false c x
+ HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
| v :: vs -> aux h (v :: prev) vs
| [] -> h ()
in
in
if es then opt1_proof g es c t else g t
in
- if es then list_map_cps g (fun h -> opt1_term h es c) vs else g vs
+ 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 = get_default_eliminator c uri tyno outty in
- let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
- let ps, sort_disp = get_ind_parameters c arg in
+ 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
in
let lifted_cases = List.map2 map2 cases constructors in
let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
- let x = refine c (C.Appl args) 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 =
| t -> opt1_other g es c t
and opt1_term g es c t =
- if is_proof c t then opt1_proof g es c t else g t
+ if H.is_proof c t then opt1_proof g es c t else g t
(* term preprocessing: optomization 2 ***************************************)
let arg i = C.Rel (succ i) in
let rec aux i f a = function
| [] -> f, a
- | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
+ | (_, 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 identity [] 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)
let g vs =
let x = C.Appl (t :: vs) in
let vsno = List.length vs in
- let _, csno = PEH.split_with_whd (c, get_type c t) 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, get_type c x) in
+ 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
- list_map_cps g (fun h -> opt2_term h c) vs
+ 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, get_type c t) in
+ 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
| t -> opt2_other g c t
and opt2_term g c t =
- if is_proof c t then opt2_proof g c t else g 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 = C.Constant (name, Some bo, ty, pars, attrs) in
+ 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
projects / helm.git / blobdiff