*)
module C = Cic
+module I = CicInspect
module D = Deannotate
module DTI = DoubleTypeInference
module TC = CicTypeChecker
[T.Branch (qs, ""); p2; p1]
and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
+ | C.AAppl (_, hd :: tl) as v ->
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
let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
[T.LetIn (name, v, dtext ^ text)]
end
- | v ->
- [T.LetIn (name, v, dtext)]
+ | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
+ begin match Cn.mk_ind st.context id uri tyno outty arg cases with
+ | None -> [T.LetIn (name, v, dtext)]
+ | Some v -> mk_fwd_proof st dtext name v
+ end
+ | v ->
+ [T.LetIn (name, v, dtext)]
and mk_proof st = function
- | C.ALambda (_, name, v, t) as what ->
+ | C.ALambda (_, name, v, t) as what ->
let entry = Some (name, C.Decl (cic v)) in
let intro = get_intro name t in
let ety = match get_inner_types st what with
| None -> None
in
mk_proof (add st entry intro ety) t
- | C.ALetIn (_, name, v, t) as what ->
+ | 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
[T.Apply (what, dtext)]
in
mk_intros st script
- | C.ARel _ as what ->
+ | 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 ->
+ | 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 ->
+ | 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.context (cic hd) Un.empty_ugraph 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 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) when i > 1 && i <= List.length classes ->
let classes, tl, _, what = split2_last classes tl in
let script, what = mk_atomic st dtext what in
- let synth = Cl.S.add 1 synth 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
List.rev script @ convert st t @
[T.Apply (t, dtext)]
in
mk_intros st script
- | t ->
+ | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
+ begin match Cn.mk_ind st.context id uri tyno outty arg cases with
+ | None ->
+ let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
+ let script = [T.Note text] in
+ mk_intros st script
+ | Some t -> mk_proof st t
+ end
+ | t ->
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
let script = [T.Note text] in
mk_intros st script
try
let _, dtext = test_depth st in
let aux inv v =
- if Cl.overlaps synth inv then None else
- if Cl.S.is_empty inv then Some (mk_proof st v) else
+ if I.overlaps synth inv then None else
+ if I.S.is_empty inv then Some (mk_proof st v) else
Some [T.Apply (v, dtext ^ "dependent")]
in
T.list_map2_filter aux classes ts