let malformed s =
X.error ("engine: malformed term: " ^ s)
-let missing s =
- X.log ("engine: missing macro for " ^ s)
+let missing s l =
+ X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
(* generic term processing *)
let get_macro s l =
let rec aux = function
- | [] -> ""
- | (r, m, a) :: _ when r = s && a = l -> m
- | _ :: tl -> aux tl
+ | [] ->
+ if !G.log_missing then missing s l;
+ "", 0
+ | (r, m, a, x) :: _ when r = s && a = l -> m, x
+ | _ :: tl -> aux tl
in
aux !G.macro_gref
let get_head = function
| C.Const c :: ts ->
let s, _ = K.resolve_reference c in
- let macro = get_macro s (L.length ts) in
- if macro <> "" then Some (macro, s, ts) else begin
- if !G.log_missing then missing s;
- None
+ let l = L.length ts in
+ let macro, x = get_macro s l in
+ begin match macro with
+ | ""
+ | "APPL" -> None
+ | _ ->
+ let ts1, ts2 = X.split_at x ts in
+ Some (macro, s, ts1, ts2)
end
| _ -> None
T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
| C.Appl ts ->
begin match get_head ts with
- | Some (macro, s, ts) ->
- let riss = L.rev_map (proc_term st []) ts in
- T.Macro macro :: T.free s :: T.mk_rev_args riss is
- | None ->
+ | None ->
let riss = L.rev_map (proc_term st []) ts in
T.Macro "APPL" :: T.mk_rev_args riss is
+ | Some (macro, s, [], ts)
+ | Some (macro, s, ts, []) ->
+ let riss = L.rev_map (proc_term st []) ts in
+ T.Macro macro :: T.free s :: T.mk_rev_args riss is
+ | Some (macro, s, ts1, ts2) ->
+ let riss1 = L.rev_map (proc_term st []) ts1 in
+ let riss2 = L.rev_map (proc_term st []) ts2 in
+ T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
end
| C.Prod (s, w, t) ->
let is_w = proc_term st [] w in
proc_sort st is s
| C.Const c ->
let s, name = K.resolve_reference c in
- T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
+ let macro, _ = get_macro s 0 in
+ if macro = "" || macro = "APPL" then
+ T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
+ else
+ T.Macro macro :: T.free s :: is
| C.Match (w, u, v, ts) ->
let is_w = proc_term st [] (C.Const w) in
let is_u = proc_term st [] u 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 *)
open_out (F.concat !G.out_dir fname)
let proc_pair s ss u = function
- | None ->
+ | None ->
+ let text_u =
+ if K.not_prop1 [] u then proc_item "assumption"
+ else proc_item "axiom"
+ in
let name = X.rev_map_concat X.id "." "type" ss in
let och = open_out_tex name in
- O.out_text och (proc_item "axiom" s name u);
+ O.out_text och (text_u s name u);
close_out och
| Some t ->
let text_u, text_t =