-proceduralClassify.cmo: proceduralClassify.cmi
-proceduralClassify.cmx: proceduralClassify.cmi
-proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi
-proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi
+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
proceduralTypes.cmo: proceduralTypes.cmi
proceduralTypes.cmx: proceduralTypes.cmi
proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
proceduralMode.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
proceduralMode.cmx proceduralConversion.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
- proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
- proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+ proceduralClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+ proceduralClassify.cmx acic2Procedural.cmi
-proceduralClassify.cmo: proceduralClassify.cmi
-proceduralClassify.cmx: proceduralClassify.cmi
-proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi
-proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi
+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
proceduralTypes.cmo: proceduralTypes.cmi
proceduralTypes.cmx: proceduralTypes.cmi
proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
proceduralMode.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
proceduralMode.cmx proceduralConversion.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
- proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
- proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+ proceduralClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+ proceduralClassify.cmx acic2Procedural.cmi
PREDICATES =
INTERFACE_FILES = \
+ proceduralHelpers.mli \
proceduralClassify.mli \
proceduralPreprocess.mli \
proceduralTypes.mli \
module C = Cic
module I = CicInspect
module D = Deannotate
-module DTI = DoubleTypeInference
module TC = CicTypeChecker
module Un = CicUniv
module UM = UriManager
module PER = ProofEngineReduction
module Pp = CicPp
-module P = ProceduralPreprocess
module Cl = ProceduralClassify
module T = ProceduralTypes
module Cn = ProceduralConversion
| {A.annsynthesized = st; A.annexpected = None} -> Some (st, st)
with Not_found -> None
with Invalid_argument _ -> failwith "A2P.get_inner_types"
-
+(*
let get_inner_sort st v =
try
let id = Ut.id_of_annterm v in
try Hashtbl.find st.sorts id
with Not_found -> `Type (CicUniv.fresh())
with Invalid_argument _ -> failwith "A2P.get_sort"
-
+*)
let get_type msg st bo =
try
let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
| C.Name s -> s
let mk_intros st script =
-try
if st.intros = [] then script else
let count = List.length st.intros in
T.Intros (Some count, List.rev st.intros, "") :: script
-with Invalid_argument _ -> failwith "A2P.mk_intros"
-let rec mk_arg st = function
- | C.ARel (_, _, _, name) as what -> convert st ~name what, what
- | what -> [], what
+let mk_arg st = function
+ | C.ARel (_, _, _, name) as what -> convert st ~name what
+ | _ -> []
-and mk_fwd_rewrite st dtext name tl direction =
+let mk_fwd_rewrite st dtext name tl direction =
assert (List.length tl = 6);
let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
let e = Cn.mk_pattern 1 predicate in
match where with
| C.ARel (_, _, _, premise) ->
- let script, what = mk_arg st what in
- T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
+ let script = mk_arg st what in
+ let where = Some (premise, name) in
+ T.Rewrite (direction, what, where, e, dtext) :: script
| _ -> assert false
-and mk_rewrite st dtext script t what qs tl direction =
+let mk_rewrite st dtext what qs tl direction =
assert (List.length tl = 5);
let predicate = List.nth tl 2 in
let e = Cn.mk_pattern 1 predicate in
- List.rev script @ convert st t @
[T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
-and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
- if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
- if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
- let ty = get_type "TC1" st hd in
- begin match get_inner_types st v with
- | Some (ity, _) ->
- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | _ ->
- let (classes, rc) as h = Cl.classify st.context ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- [T.LetIn (name, v, dtext ^ text)]
- end
- | C.AMutCase _ -> assert false
- | C.ACast _ -> assert false
- | v ->
- match get_inner_types st v with
+let rec proc_lambda st name v t =
+ let entry = Some (name, C.Decl (cic v)) in
+ let intro = get_intro name in
+ proc_proof (add st entry intro) t
+
+and proc_letin st what name v t =
+ let intro = get_intro name in
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let hyp, rqv = match get_inner_types st v with
| Some (ity, _) ->
- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | _ ->
- [T.LetIn (name, v, dtext)]
-
-and mk_proof st = function
- | C.ALambda (_, name, v, t) ->
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name in
- mk_proof (add st entry intro) t
- | C.ALetIn (_, name, v, t) as what ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let entry = Some (name, C.Def (cic v, None)) in
- let intro = get_intro name in
- let q = mk_proof (next (add st entry intro)) t in
- List.rev_append (mk_fwd_proof st dtext intro v) q
- else
- [T.Apply (what, dtext)]
- in
- mk_intros st script
- | C.ARel _ as what ->
- let _, dtext = test_depth st in
- let text = "assumption" in
- let script = [T.Apply (what, dtext ^ text)] in
- mk_intros st script
- | C.AMutConstruct _ as what ->
- let _, dtext = test_depth st in
- let script = [T.Apply (what, dtext)] in
- mk_intros st script
- | C.AAppl (_, hd :: tl) as t ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let ty = get_type "TC2" st hd in
- let (classes, rc) as h = Cl.classify st.context ty in
- let decurry = List.length classes - List.length tl in
- if decurry <> 0 then begin
- let msg = Printf.sprintf "Decurry: %i\nTerm: %s\nContext: %s"
- decurry (Pp.ppterm (cic t)) (Pp.ppcontext st.context)
+ let rqv = match v with
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
+ mk_fwd_rewrite st dtext intro tl true
+ | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl ->
+ mk_fwd_rewrite st dtext intro tl false
+ | v ->
+ let qs = [[T.Id ""]; proc_proof (next st) v] in
+ [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
in
- HLog.warn msg; assert false
- end;
- let synth = I.S.singleton 0 in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- match rc with
- | Some (i, j) ->
- let classes, tl, _, what = split2_last classes tl in
- let script, what = mk_arg st what in
- let synth = I.S.add 1 synth in
- let qs = mk_bkd_proofs (next st) synth classes tl in
- if is_rewrite_right hd then
- mk_rewrite st dtext script t what qs tl false
- else if is_rewrite_left hd then
- mk_rewrite st dtext script t what qs tl true
- else
- let l = succ (List.length tl) in
- let predicate = List.nth tl (l - i) in
- let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
- let using = Some hd in
- List.rev script @ convert st t @
- [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
- | None ->
- let qs = mk_bkd_proofs (next st) synth classes tl in
- let script, hd = mk_arg st hd in
- List.rev script @ convert st t @
- [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
- else
- [T.Apply (t, dtext)]
+ C.Decl (get_type "TC1" st v), rqv
+ | None ->
+ C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
in
- mk_intros st script
- | C.AMutCase _ -> assert false
- | C.ACast _ -> assert false
- | t ->
- let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
- let script = [T.Note text] in
- mk_intros st script
-
-and mk_bkd_proofs st synth classes ts =
+ let entry = Some (name, hyp) in
+ let qt = proc_proof (next (add st entry intro)) t in
+ List.rev_append rqv qt
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_intros st script
+
+and proc_rel st what =
+ let _, dtext = test_depth st in
+ let text = "assumption" in
+ let script = [T.Apply (what, dtext ^ text)] in
+ mk_intros st script
+
+and proc_mutconstruct st what =
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_intros st script
+
+and proc_appl st what hd tl =
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let ty = get_type "TC2" st hd in
+ let (classes, rc) as h = Cl.classify st.context ty in
+ let argsno = List.length classes in
+ let diff = argsno - List.length tl in
+ if diff <> 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
+ let synth = I.S.singleton 0 in
+ let text = Printf.sprintf "%u %s" argsno (Cl.to_string h) in
+ let script = List.rev (mk_arg st hd) @ convert st what in
+ match rc with
+ | Some (i, j) ->
+ let classes, tl, _, where = split2_last classes tl in
+ let script = List.rev (mk_arg st where) @ script in
+ let synth = I.S.add 1 synth in
+ let qs = proc_bkd_proofs (next st) synth classes tl in
+ if is_rewrite_right hd then
+ script @ mk_rewrite st dtext where qs tl false
+ else if is_rewrite_left hd then
+ script @ mk_rewrite st dtext where qs tl true
+ else
+ let predicate = List.nth tl (argsno - i) in
+ let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
+ let using = Some hd in
+ script @
+ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
+ | None ->
+ let qs = proc_bkd_proofs (next st) synth classes tl in
+ script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_intros st script
+
+and proc_other st what =
+ let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
+ let script = [T.Note text] in
+ mk_intros st script
+
+
+and proc_proof st = function
+ | C.ALambda (_, name, w, t) -> proc_lambda st name w t
+ | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t
+ | C.ARel _ as what -> proc_rel st what
+ | C.AMutConstruct _ as what -> proc_mutconstruct st what
+ | C.AAppl (_, hd :: tl) as what -> proc_appl st what hd tl
+ | what -> proc_other st what
+
+and proc_bkd_proofs st synth classes ts =
try
let _, dtext = test_depth st in
let aux (inv, _) v =
if I.overlaps synth inv then None else
- if I.S.is_empty inv then Some (mk_proof st v) else
+ if I.S.is_empty inv then Some (proc_proof st v) else
Some [T.Apply (v, dtext ^ "dependent")]
in
T.list_map2_filter aux classes ts
-with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
+with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs"
(* object costruction *******************************************************)
List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
-let mk_obj st = function
+let proc_obj st = function
| C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
- let ast = mk_proof st v in
+ let ast = proc_proof st v in
let count = T.count_steps 0 ast in
let text = Printf.sprintf "tactics: %u" count in
T.Theorem (s, t, text) :: ast @ [T.Qed ""]
context = [];
intros = []
} in
- HLog.debug "Level 2 transformation";
- let steps = mk_obj st aobj in
- HLog.debug "grafite rendering";
+ HLog.debug "Procedural: level 2 transformation";
+ let steps = proc_obj st aobj in
+ HLog.debug "Procedural: grafite rendering";
List.rev (T.render_steps [] steps)
module I = CicInspect
module PEH = ProofEngineHelpers
+module H = ProceduralHelpers
+
type dependence = I.S.t * bool
type conclusion = (int * int) option
in
Array.iteri map b;
prerr_newline ()
-
-(****************************************************************************)
-
-let identity x = x
-let fst3 (x, _, _) = x
+(* classification ***********************************************************)
let classify_conclusion vs =
let rec get_argsno = function
let rc = classify_conclusion vs in
let map (b, h) (c, v) =
let _, argsno = PEH.split_with_whd (c, v) in
- (I.get_rels_from_premise h v, I.S.empty, argsno > 0) :: b, succ h
+ let iu = H.is_unsafe h (List.hd vs) in
+ (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h
in
let l, h = List.fold_left map ([], 0) vs in
let b = Array.of_list (List.rev l) in
let mk_closure b h =
- let map j = if j < h then I.S.union (fst3 b.(j)) else identity in
+ let map j = if j < h then I.S.union (H.fst3 b.(j)) else H.identity in
for i = pred h downto 0 do
let direct, unused, fa = b.(i) in
b.(i) <- I.S.fold map direct direct, unused, fa
--- /dev/null
+(* 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 Rf = CicRefine
+module Un = CicUniv
+module Pp = CicPp
+module TC = CicTypeChecker
+module PEH = ProofEngineHelpers
+module E = CicEnvironment
+module UM = UriManager
+
+(* fresh name generator *****************************************************)
+
+let split name =
+ let rec aux i =
+ if i <= 0 then assert false else
+ let c = name.[pred i] in
+ if c >= '0' && c <= '9' then aux (pred i)
+ else Str.string_before name i, Str.string_after name i
+ in
+ let before, after = aux (String.length name) in
+ let i = if after = "" then -1 else int_of_string after in
+ before, i
+
+let join (s, i) =
+ C.Name (if i < 0 then s else s ^ string_of_int i)
+
+let mk_fresh_name context name =
+ let rec aux i = function
+ | [] -> name, i
+ | Some (C.Name s, _) :: entries ->
+ let m, j = split s in
+ if m = name && j >= i then aux (succ j) entries else aux i entries
+ | _ :: entries -> aux i entries
+ in
+ join (aux (-1) context)
+
+let mk_fresh_name context = function
+ | C.Anonymous -> C.Anonymous
+ | C.Name s -> mk_fresh_name context s
+
+(* 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 compose f g x = f (g x)
+
+let fst3 (x, _, _) = 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_unsafe h (c, t) = true
+
+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
--- /dev/null
+(* 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 mk_fresh_name:
+ Cic.context -> Cic.name -> Cic.name
+val list_map_cps:
+ ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b
+val identity:
+ 'a -> 'a
+val compose:
+ ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val fst3:
+ 'a * 'b * 'c -> 'a
+val refine:
+ Cic.context -> Cic.term -> Cic.term
+val get_type:
+ Cic.context -> Cic.term -> Cic.term
+val is_proof:
+ Cic.context -> Cic.term -> bool
+val is_unsafe:
+ int -> Cic.context * Cic.term -> bool
+val is_not_atomic:
+ Cic.term -> bool
+val get_ind_type:
+ UriManager.uri -> int -> int * Cic.inductiveType
+val get_default_eliminator:
+ Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
+val get_ind_parameters:
+ Cic.context -> Cic.term -> Cic.term list * int
* 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
let source_id_of_id id = "#source#" ^ id;;
-exception NotEnoughElements;;
+exception NotEnoughElements of string;;
(*CSC: cut&paste da cicPp.ml *)
(* get_nth l n returns the nth element of the list l if it exists or *)
(* raises NotEnoughElements if l has less than n elements *)
-let rec get_nth l n =
+let rec get_nth msg l n =
match (n,l) with
(1, he::_) -> he
- | (n, he::tail) when n > 1 -> get_nth tail (n-1)
- | (_,_) -> raise NotEnoughElements
+ | (n, he::tail) when n > 1 -> get_nth msg tail (n-1)
+ | (_,_) -> raise (NotEnoughElements msg)
;;
match tt with
C.Rel n ->
let id =
- match get_nth context n with
+ match get_nth "1" context n with
(Some (C.Name s,_)) -> s
| _ -> "__" ^ string_of_int n
in
match t with
C.Rel n ->
let idref,id =
- match get_nth context n with
+ match get_nth "2" context n with
idref,(Some (C.Name s,_)) -> idref,s
| idref,_ -> idref,"__" ^ string_of_int n
in
* http://cs.unibo.it/helm/.
*)
-exception NotEnoughElements
+exception NotEnoughElements of string
val source_id_of_id : string -> string
projects / helm.git / commitdiff