- mk_intros st script
- | 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
- | C.ACast (_, t, _) ->
- mk_proof st t
- | 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 synth = mk_synth I.S.empty decurry in
+ let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
+ let script = List.rev (mk_arg st hd) in
+ match rc with
+ | Some (i, j, uri, tyno) ->
+ 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 names = get_ind_names uri tyno in
+ let qs = proc_bkd_proofs (next st) synth names classes tl in
+ if is_rewrite_right hd then
+ script @ mk_rewrite st dtext where qs tl false what
+ else if is_rewrite_left hd then
+ script @ mk_rewrite st dtext where qs tl true what
+ else
+ let predicate = List.nth tl (parsno - i) in
+ let e = Cn.mk_pattern j predicate in
+ let using = Some hd in
+ (* convert_elim st what what e @ *) script @
+ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
+ | None ->
+ let qs = proc_bkd_proofs (next st) synth [] classes tl in
+ let hd = mk_exp_args hd tl classes synth in
+ script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_intros st what 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 what script
+
+and proc_proof st t =
+ let f st =
+ let xtypes, note = match get_inner_types st t with
+ | Some (it, et) -> Some (H.cic it, H.cic et),
+ (Printf.sprintf "\nInferred: %s\nExpected: %s"
+ (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
+ | None -> None, "\nNo types"
+ in
+ let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
+ let note = Pp.ppcontext st.context ^ note in
+ {st with context = context; clears = clears; clears_note = note; }
+ in
+ match t with
+ | C.ALambda (_, name, w, t) -> proc_lambda st name w t
+ | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
+ | C.ARel _ as what -> proc_rel (f st) what
+ | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
+ | C.AConst _ as what -> proc_const (f st) what
+ | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
+ | what -> proc_other (f st) what
+
+and proc_bkd_proofs st synth names classes ts =