+ | Failure "name_of_reference" -> malformed "T3"
+
+(* proof processing *)
+
+let typeof st = function
+ | C.Appl [t]
+ | t -> K.whd_typeof st.c t
+
+let init i = {
+ i = i;
+ n = ""; s = [1]; c = [];
+}
+
+let push st n = {st with
+ n = n; s = 1 :: st.s;
+}
+
+let next st f = {st with
+ c = f st.c;
+ n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
+}
+
+let scope st =
+ X.rev_map_concat string_of_int "." "" (L.tl st.s)
+
+let mk_exit st ris =
+ if st.n <> "" || L.tl st.s = [] then ris else
+ T.free (scope st) :: T.Macro "EXIT" :: ris
+
+let mk_open st ris =
+ if st.n = "" then ris else
+ T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
+
+let mk_dec st kind w s ris =
+ let w = if !G.no_types then [] else w in
+ T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
+
+let mk_inferred st t ris =
+ let u = typeof st t in
+ let is_u = proc_term st [] u in
+ mk_dec st "DECL" is_u st.n ris
+
+let rec proc_proof st ris t = match t with
+ | C.Appl []
+ | C.Meta _
+ | C.Implicit _
+ | C.Sort _
+ | C.Prod _ -> malformed "P1"
+ | C.Const _
+ | C.Rel _ -> proc_proof st ris (C.Appl [t])
+ | C.Lambda (s, w, t) ->
+ let is_w = proc_term st [] w in
+ let ris = mk_open st ris in
+ proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
+ | C.Appl (t0 :: ts) ->
+ let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
+ let ris = T.Macro "STEP" :: mk_inferred st t ris in
+ let tts = L.rev_map (proc_term st []) rts in
+ mk_exit st (T.rev_mk_args tts ris)
+ | C.Match (_w, _u, v, ts) ->
+ let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
+ let ris = T.Macro "DEST" :: mk_inferred st t ris in
+ let tts = L.rev_map (proc_term st []) rts in
+ mk_exit st (T.rev_mk_args tts ris)
+ | C.LetIn (s, w, v, t) ->
+ let is_w = proc_term st [] w in
+ let ris = mk_open st ris in
+ if K.not_prop1 st.c w then
+ let is_v = proc_term st [] v in
+ let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
+ proc_proof (next st (K.add_def s w v)) ris t
+ else
+ let ris_v = proc_proof (push st s) ris v in
+ proc_proof (next st (K.add_def s w v)) ris_v t
+
+let proc_proof st rs t = try proc_proof st rs t with
+ | E.ObjectNotFound _
+ | Invalid_argument "List.nth"
+ | Failure "nth"
+ | Failure "name_of_reference" -> malformed "P2"
+ | V.TypeCheckerFailure s
+ | V.AssertFailure s -> malformed (Lazy.force s)
+ | Failure "hd"
+ | Failure "tl" -> internal "P2"
+
+(* top level processing *)
+
+let note = T.Note "This file was automatically generated by MaTeX: do not edit"
+
+let proc_item item s ss t =
+ let st = init ss in
+ let tt = N.process_top_term s t in (* alpha-conversion *)
+ let is = [T.Macro "end"; T.arg item] in
+ note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
+
+let proc_top_proof s ss t =
+ if !G.no_proofs then [] else
+ let st = init ss in
+ let t0 = A.process_top_term s t in (* anticipation *)
+ let tt = N.process_top_term s t0 in (* alpha-conversion *)
+ let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
+ L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)