+ | Failure "name_of_reference" -> malformed "T3"
+
+(* proof processing *)
+
+let typeof c = function
+ | C.Appl [t]
+ | t -> A.typeof c t
+
+let init () = {
+ n = ""; s = [1]
+}
+
+let push st n = {
+ n = n; s = 1 :: st.s;
+}
+
+let next st = {
+ 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 st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
+
+let mk_dec kind w s ris =
+ let w = if !G.no_types then [] else w in
+ T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
+
+let mk_inferred st c t ris =
+ let u = typeof c t in
+ let is_u = proc_term c u in
+ mk_dec "DECL" is_u st.n ris
+
+let rec proc_proof st ris c 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 (C.Appl [t])
+ | C.Lambda (s, w, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ let ris = mk_open st ris in
+ proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
+ | C.Appl ts ->
+ let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
+ let ris = T.Macro "STEP" :: mk_inferred st c t ris in
+ let tts = L.rev_map (proc_term c) rts in
+ mk_exit st (T.rev_mk_args tts ris)
+ | C.Match (w, u, v, ts) ->
+ let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
+ let ris = T.Macro "DEST" :: mk_inferred st c t ris in
+ let tts = L.rev_map (proc_term c) rts in
+ mk_exit st (T.rev_mk_args tts ris)
+ | C.LetIn (s, w, v, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ let ris = mk_open st ris in
+ if A.not_prop1 c w then
+ let is_v = proc_term c v in
+ let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
+ proc_proof (next st) ris (K.add_def s w v c) t
+ else
+ let ris_v = proc_proof (push st s) ris c v in
+ proc_proof (next st) ris_v (K.add_def s w v c) t
+
+let proc_proof rs c t = try proc_proof (init ()) rs c 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 proc_top_type s t =
+ [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
+
+let proc_top_body s t = proc_term [] t
+
+let proc_top_proof s t =
+ let tt = A.process_top_term s t in (* anticipation *)
+ L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt)