- st, C.Decl (H.cic ity), rqv
- | None ->
- st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
- in
- 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 what 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 what script
-
-and proc_mutconstruct st what =
- let _, dtext = test_depth st in
- let script = [T.Apply (what, dtext)] in
- mk_intros st what script
-
-and proc_const st what =
- let _, dtext = test_depth st in
- let script = [T.Apply (what, dtext)] in
- mk_intros st what 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 = Cl.classify st.context ty in
- let goal_arity, goal = match get_inner_types st what with
- | None -> 0, None
- | Some (ity, ety) ->
- snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ety)
- in
- let parsno, argsno = List.length classes, List.length tl in
- let decurry = parsno - argsno in
- let diff = goal_arity - decurry in
- if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
- let classes = Cl.adjust st.context tl ?goal classes in
- let rec mk_synth a n =
- if n < 0 then a else mk_synth (I.S.add n a) (pred n)
- in
- 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 classes2, tl2, _, where = split2_last classes tl in
- let script2 = List.rev (mk_arg st where) @ script in
- let synth2 = I.S.add 1 synth in
- let names = get_ind_names uri tyno in
- let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
- if List.length qs <> List.length names then
- 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 if is_rewrite_right hd then
- script2 @ mk_rewrite st dtext where qs tl2 false what
- else if is_rewrite_left hd then
- script2 @ mk_rewrite st dtext where qs tl2 true what
- else
- let predicate = List.nth tl2 (parsno - i) in
- let e = Cn.mk_pattern j predicate in
- let using = Some hd in
- (* convert_elim st what what e @ *) script2 @
- [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
+ T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
+ | flavour when List.mem flavour def_flavours ->
+ [T.Statement (flavour, Some s, t, Some v, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"
+ end
+ | C.AConstant (_, _, s, None, t, [], attrs) ->
+ [T.Statement (`Axiom, Some s, t, None, "")]
+ | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
+ begin match is_record attrs with
+ | None -> [T.Inductive (types, lpsno, "")]
+ | Some fs -> [T.Record (types, lpsno, fs, "")]
+ end
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"