*)
module C = Cic
-module L = CicClassify
-module P = ProceduralTypes
module D = Deannotate
module DTI = DoubleTypeInference
module TC = CicTypeChecker
-module U = CicUniv
+module Un = CicUniv
module UM = UriManager
module Obj = LibraryObjects
module HObj = HelmLibraryObjects
module A = Cic2acic
-module T = CicUtil
+module Ut = CicUtil
+module E = CicEnvironment
+
+module Cl = CicClassify
+module T = ProceduralTypes
+module Cn = ProceduralConversion
type status = {
- sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t;
+ sorts : (C.id, A.sort_kind) Hashtbl.t;
types : (C.id, A.anntypes) Hashtbl.t;
prefix: string;
max_depth: int option;
depth: int;
entries: C.context;
- intros: string list
+ intros: string list;
+ ety: C.annterm option
}
(* helpers ******************************************************************)
let split2_last l1 l2 =
try
let n = pred (List.length l1) in
- let before1, after1 = P.list_split n l1 in
- let before2, after2 = P.list_split n l2 in
+ let before1, after1 = T.list_split n l1 in
+ let before2, after2 = T.list_split n l2 in
before1, before2, List.hd after1, List.hd after2
with Invalid_argument _ -> failwith "A2P.split2_last"
| C.AMeta _ -> "meta"
| C.AImplicit _ -> "implict"
-let next st = {st with depth = succ st.depth; intros = []}
+let next st = {st with depth = succ st.depth; intros = []; ety = None}
+
+let set_ety st ety =
+ if st.ety = None then {st with ety = ety} else st
-let add st entry intro =
+let add st entry intro ety =
+ let st = set_ety st ety in
{st with entries = entry :: st.entries; intros = intro :: st.intros}
let test_depth st =
if st.depth < d then true, msg else false, "DEPTH EXCEDED"
with Invalid_argument _ -> failwith "A2P.test_depth"
-let get_itype st v =
+let is_rewrite_right = function
+ | C.AConst (_, uri, []) ->
+ UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
+ | _ -> false
+
+let is_rewrite_left = function
+ | C.AConst (_, uri, []) ->
+ UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
+ | _ -> false
+(*
+let get_ind_name uri tno xcno =
+try
+ let ts = match E.get_obj Un.empty_ugraph uri with
+ | C.InductiveDefinition (ts, _, _,_), _ -> ts
+ | _ -> assert false
+ in
+ let tname, cs = match List.nth ts tno with
+ | (name, _, _, cs) -> name, cs
+ in
+ match xcno with
+ | None -> tname
+ | Some cno -> fst (List.nth cs (pred cno))
+with Invalid_argument _ -> failwith "A2P.get_ind_name"
+*)
+let get_inner_types st v =
try
- let id = T.id_of_annterm v in
- try Some ((Hashtbl.find st.types id).A.annsynthesized)
+ let id = Ut.id_of_annterm v in
+ try match Hashtbl.find st.types id with
+ | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
+ | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st)
with Not_found -> None
-with Invalid_argument _ -> failwith "A2P.get_itype"
+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"
(* proof construction *******************************************************)
let unused_premise = "UNUSED"
+let defined_premise = "DEFINED"
+
+let assumed_premise = "ASSUMED"
+
let get_intro name t =
try
match name with
try
if st.intros = [] then script else
let count = List.length st.intros in
- P.Intros (Some count, List.rev st.intros, "") :: script
+ let p0 = T.Whd (count, "") in
+ let p1 = T.Intros (Some count, List.rev st.intros, "") in
+ match st.ety with
+ | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
+ | _ -> p1 :: script
with Invalid_argument _ -> failwith "A2P.mk_intros"
+(*
+let rec mk_premise st dtext = function
+ | C.ARel (_, _, _, binder) -> [], binder
+ | where ->
+ let name = contracted_premise in
+ mk_fwd_proof st dtext name where, name
+*)
+let rec mk_fwd_rewrite st dtext name tl direction =
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let rewrite premise =
+ [T.Rewrite (direction, what, Some (premise, name), dtext)]
+ in
+ match where with
+ | C.ARel (_, _, _, binder) -> rewrite binder
+ | _ ->
+ assert (get_inner_sort st where = `Prop);
+ let pred, old = List.nth tl 2, List.nth tl 1 in
+ let pred_name = defined_premise in
+ let pred_text = "extracted" in
+ let p1 = T.LetIn (pred_name, pred, pred_text) in
+ let cut_name = assumed_premise in
+ let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
+ let cut_text = "" in
+ let p2 = T.Cut (cut_name, cut_type, cut_text) in
+ let qs = [rewrite cut_name; mk_proof (next st) where] in
+ [T.Branch (qs, ""); p2; p1]
-let is_rewrite_right = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
- | _ -> false
-
-let is_rewrite_left = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
- | _ -> false
-
-let mk_premise = function
- | C.ARel (_, _, _, binder) -> binder
- | C.AVar (_, uri, _)
- | C.AConst (_, uri, _) -> UM.name_of_uri uri
- | C.ASort (_, sort) -> assert false
- | C.AMutInd (_, uri, tno, _) -> assert false
- | C.AMutConstruct (_, uri, tno, cno, _) -> assert false
- | _ -> assert false
-
-let rec mk_fwd_proof st dtext name = function
+and mk_fwd_proof st dtext name = function
| C.AAppl (_, hd :: tl) as v ->
- if is_rewrite_right hd then
- let what, where = List.nth tl 5, List.nth tl 3 in
- let premise = mk_premise where in
- [P.Rewrite (true, what, Some (premise, name), dtext)]
- else if is_rewrite_left hd then
- let what, where = List.nth tl 5, List.nth tl 3 in
- let premise = mk_premise where in
- [P.Rewrite (false, what, Some (premise, name), dtext)]
- else begin match get_itype st v with
- | Some ty ->
- let qs = [[P.Id ""]; mk_proof (next st) v] in
- [P.Branch (qs, ""); P.Cut (name, ty, dtext)]
- | None ->
- let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
- let (classes, rc) as h = L.classify ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
- [P.LetIn (name, v, dtext ^ text)]
+ if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
+ if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+ 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)]
+ | None ->
+ let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
+ let (classes, rc) as h = Cl.classify ty in
+ let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
+ [T.LetIn (name, v, dtext ^ text)]
end
| v ->
- [P.LetIn (name, v, dtext)]
+ [T.LetIn (name, v, dtext)]
and mk_proof st = function
- | C.ALambda (_, name, v, t) ->
+ | C.ALambda (_, name, v, t) as what ->
let entry = Some (name, C.Decl (cic v)) in
let intro = get_intro name t in
- mk_proof (add st entry intro) t
+ let ety = match get_inner_types st what with
+ | Some (_, ety) -> Some ety
+ | None -> None
+ in
+ mk_proof (add st entry intro ety) 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 t in
- let q = mk_proof (next (add st entry intro)) t in
+ let q = mk_proof (next (add st entry intro None)) t in
List.rev_append (mk_fwd_proof st dtext intro v) q
else
- [P.Apply (what, dtext)]
+ [T.Apply (what, dtext)]
in
mk_intros st script
| C.ARel _ as what ->
let _, dtext = test_depth st in
- let script = [P.Apply (what, dtext)] 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, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
- let (classes, rc) as h = L.classify ty in
- let synth = L.S.singleton 0 in
- let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
+ let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
+ let (classes, rc) as h = Cl.classify ty in
+ let synth = Cl.S.singleton 0 in
+ let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
match rc with
| Some (i, j) when i > 1 ->
let classes, tl, _, what = split2_last classes tl in
- let synth = L.S.add 1 synth in
+ let synth = Cl.S.add 1 synth in
let qs = mk_bkd_proofs (next st) synth classes tl in
if is_rewrite_right hd then
- [P.Rewrite (false, what, None, dtext); P.Branch (qs, "")]
+ [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
else if is_rewrite_left hd then
- [P.Rewrite (true, what, None, dtext); P.Branch (qs, "")]
+ [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
else
let using = Some hd in
- [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")]
+ [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
| _ ->
let qs = mk_bkd_proofs (next st) synth classes tl in
- [P.Apply (hd, dtext ^ text); P.Branch (qs, "")]
+ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
else
- [P.Apply (t, dtext)]
+ [T.Apply (t, dtext)]
in
mk_intros st script
| t ->
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
- let script = [P.Note text] in
+ let script = [T.Note text] in
mk_intros st script
and mk_bkd_proofs st synth classes ts =
try
let _, dtext = test_depth st in
let aux inv v =
- if L.overlaps synth inv then None else
- if L.S.is_empty inv then Some (mk_proof st v) else
- Some [P.Apply (v, dtext ^ "dependent")]
+ if Cl.overlaps synth inv then None else
+ if Cl.S.is_empty inv then Some (mk_proof st v) else
+ Some [T.Apply (v, dtext ^ "dependent")]
in
let l1, l2 = List.length classes, List.length ts in
if l1 > l2 then failwith "partial application" else
if l1 < l2 then failwith "too many arguments" else
- P.list_map2_filter aux classes ts
+ T.list_map2_filter aux classes ts
with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
(* object costruction *******************************************************)
let mk_obj st = function
| C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
- let ast = mk_proof st v in
- let count = P.count_steps 0 ast in
+ let ast = mk_proof (set_ety st (Some t)) v in
+ let count = T.count_steps 0 ast in
let text = Printf.sprintf "tactics: %u" count in
- P.Theorem (s, t, text) :: ast @ [P.Qed ""]
+ T.Theorem (s, t, text) :: ast @ [T.Qed ""]
| _ ->
failwith "not a theorem"
max_depth = None;
depth = 0;
entries = [];
- intros = []
+ intros = [];
+ ety = None
} in
prerr_endline "Level 2 transformation";
let steps = mk_obj st aobj in
prerr_endline "grafite rendering";
- List.rev (P.render_steps [] steps)
+ List.rev (T.render_steps [] steps)
projects / helm.git / blobdiff