*)
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 : (Cic.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
+ context: C.context;
+ intros: string list;
+ ety: C.annterm option
}
(* helpers ******************************************************************)
+let id x = x
+
+let comp f g x = f (g x)
+
let cic = D.deannotate_term
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"
let string_of_head = function
| C.ASort _ -> "sort"
| C.AMeta _ -> "meta"
| C.AImplicit _ -> "implict"
-let next st = {st with depth = succ st.depth; intros = []}
+let clear st = {st with intros = []; ety = None}
+
+let next st = {(clear st) with depth = succ st.depth}
+
+let set_ety st ety =
+ if st.ety = None then {st with ety = ety} else st
-let add st entry intro =
- {st with entries = entry :: st.entries; intros = intro :: st.intros}
+let add st entry intro ety =
+ let st = set_ety st ety in
+ {st with context = entry :: st.context; intros = intro :: st.intros}
let test_depth st =
+try
let msg = Printf.sprintf "Depth %u: " st.depth in
match st.max_depth with
| None -> true, ""
- | Some d ->
- if st.depth < d then true, msg else false, "DEPTH EXCEDED"
+ | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
+with Invalid_argument _ -> failwith "A2P.test_depth"
+
+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 get_itype st v =
- let id = T.id_of_annterm v in
- try Some ((Hashtbl.find st.types id).A.annsynthesized)
+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 = 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_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 get_intro name t = match name with
+let defined_premise = "DEFINED"
+
+let assumed_premise = "ASSUMED"
+
+let expanded_premise = "EXPANDED"
+
+let eta_expand n t =
+ let ty = C.AImplicit ("", None) in
+ let name i = Printf.sprintf "%s%u" expanded_premise i in
+ let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in
+ let arg i n = T.mk_arel (n - i) (name i) in
+ let rec aux i f a =
+ if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
+ in
+ let absts, args = aux 0 id [] in
+ match Cn.lift 1 n t with
+ | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
+ | t -> absts (C.AAppl ("", t :: args))
+
+let appl_expand n = function
+ | C.AAppl (id, ts) ->
+ let before, after = T.list_split (List.length ts + n) ts in
+ C.AAppl ("", C.AAppl (id, before) :: after)
+ | _ -> assert false
+
+let get_intro name t =
+try
+match name with
| C.Anonymous -> unused_premise
| C.Name s ->
if DTI.does_not_occur 1 (cic t) then unused_premise else s
+with Invalid_argument _ -> failwith "A2P.get_intro"
let mk_intros st script =
+try
if st.intros = [] then script else
let count = List.length st.intros in
- P.Intros (Some count, List.rev st.intros, "") :: script
-
-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 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 is_rewrite_left = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
- | _ -> false
+let rec mk_atomic st dtext what =
+ if T.is_atomic what then [], what else
+ let name = defined_premise in
+ mk_fwd_proof st dtext name what, T.mk_arel 0 name
-let mk_premise = function
- | C.ARel (_, _, _, binder) -> binder
- | _ -> assert false
+and mk_fwd_rewrite st dtext name tl direction =
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let rewrite premise =
+ let script, what = mk_atomic st dtext what in
+ T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+ 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 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.context (cic hd) Un.empty_ugraph in
+ 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
| 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
- | C.ALetIn (_, name, v, t) as what ->
+ 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 st) 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 ->
+ | 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.AAppl (_, hd :: tl) as t ->
+ | 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.context (cic hd) Un.empty_ugraph 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 mk_proof (clear st) (appl_expand decurry t) else
+ if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
+ 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 ->
+ | Some (i, j) when i > 1 && i <= List.length classes ->
let classes, tl, _, what = split2_last classes tl in
- let synth = L.S.add 1 synth in
+ let script, what = mk_atomic st dtext what 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, "")]
+ List.rev script @
+ [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, "")]
+ List.rev script @
+ [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
else
let using = Some hd in
- [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")]
- | _ ->
+ List.rev script @
+ [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, "")]
+ let script, hd = mk_atomic st dtext hd in
+ List.rev script @
+ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
else
- [P.Apply (t, dtext)]
+ [T.Apply (t, dtext)]
in
mk_intros st script
- | t ->
+ | 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
- 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 is_theorem pars =
+ 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
- | C.AConstant (_, _, s, Some v, t, [], _) ->
- let ast = mk_proof st v in
- let count = P.count_steps 0 ast in
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
+ 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 ""]
- | _ -> assert false
+ T.Theorem (s, t, text) :: ast @ [T.Qed ""]
+ | _ ->
+ failwith "not a theorem"
(* interface functions ******************************************************)
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj =
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
let st = {
sorts = ids_to_inner_sorts;
types = ids_to_inner_types;
prefix = prefix;
- max_depth = None;
+ max_depth = depth;
depth = 0;
- entries = [];
- intros = []
+ context = [];
+ 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