matita/components/binaries/matex/engine.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module F = Filename
  13 module L = List
  14 module P = Printf
  15 module S = String
  16
  17 module U = NUri
  18 module R = NReference
  19 module C = NCic
  20 module E = NCicEnvironment
  21 module V = NCicTypeChecker
  22
  23 module X = Ground
  24 module G = Options
  25 module K = Kernel
  26 module T = TeX
  27 module O = TeXOutput
  28 module A = Anticipate
  29 module M = Meta
  30 module N = Alpha
  31
  32 type status = {
  33    i: string;   (* item name *)
  34    n: string;   (* reference name *)
  35    s: int list; (* scope *)
  36    c: C.context (* context for kernel calls *)
  37 }
  38
  39 (* internal functions *******************************************************)
  40
  41 let internal s =
  42    X.error ("engine: malformed stack: " ^ s)
  43
  44 let malformed s =
  45    X.error ("engine: malformed term: " ^ s)
  46
  47 let missing s l =
  48    X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
  49
  50 (* generic term processing *)
  51
  52 let rec rename s = function
  53    | []                        -> s
  54    | (s1, s2) :: _ when s1 = s -> s2
  55    | _ :: tl                   -> rename s tl
  56
  57 let mk_lname s = s
  58
  59 let mk_gname s =
  60    rename s !G.alpha_gref
  61
  62 let mk_ptr st name =
  63    if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
  64
  65 let get_macro s l =
  66    let rec aux = function
  67       | []                                    ->
  68          if !G.log_missing then missing s l;
  69          "", 0
  70       | (r, m, a, x) :: _ when r = s && a = l -> m, x
  71       | _ :: tl                               -> aux tl
  72    in
  73    aux !G.macro_gref
  74
  75 let get_head = function
  76    | C.Const c :: ts ->
  77       let s, _ = K.resolve_reference c in
  78       let l = L.length ts in
  79       let macro, x = get_macro s l in
  80       begin match macro with
  81          | ""
  82          | "APPL" -> None
  83          | _      ->
  84             let ts1, ts2 = X.split_at x ts in
  85             Some (macro, s, ts1, ts2)
  86       end
  87    | _               -> None
  88
  89 let proc_sort st is = function
  90    | C.Prop             -> T.Macro "PROP" :: is
  91    | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
  92    | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
  93    | C.Type _           -> malformed "T1"
  94
  95 let rec proc_term st is = function
  96    | C.Appl []
  97    | C.Meta _
  98    | C.Implicit _           -> malformed "T2"
  99    | C.Rel m                ->
 100       let s = K.resolve_lref st.c m in
 101       T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
 102    | C.Appl ts              ->
 103       begin match get_head ts with
 104          | None                      ->
 105             let riss = L.rev_map (proc_term st []) ts in
 106             T.Macro "APPL" :: T.mk_rev_args riss is
 107          | Some (macro, s, [], ts)
 108          | Some (macro, s, ts, [])   ->
 109             let riss = L.rev_map (proc_term st []) ts in
 110             T.Macro macro :: T.free s :: T.mk_rev_args riss is
 111          | Some (macro, s, ts1, ts2) ->
 112             let riss1 = L.rev_map (proc_term st []) ts1 in
 113             let riss2 = L.rev_map (proc_term st []) ts2 in
 114             T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
 115       end
 116    | C.Prod (s, w, t)       ->
 117       let is_w = proc_term st [] w in
 118       let c = K.add_dec s w st.c in
 119       let is_t = proc_term {st with c=c} is t in
 120       let macro = if K.not_prop1 c t then "PROD" else "FALL" in
 121       T.Macro macro :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
 122    | C.Lambda (s, w, t)     ->
 123       let is_w = proc_term st [] w in
 124       let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
 125       T.Macro "ABST" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
 126    | C.LetIn (s, w, v, t)   ->
 127       let is_w = proc_term st [] w in
 128       let is_v = proc_term st [] v in
 129       let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
 130       T.Macro "ABBR" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
 131    | C.Sort s               ->
 132       proc_sort st is s
 133    | C.Const c              ->
 134       let s, name = K.resolve_reference c in
 135       let macro, _ = get_macro s 0 in
 136       if macro = "" || macro = "APPL" then
 137          T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
 138       else
 139          T.Macro macro :: T.free s :: is
 140    | C.Match (w, u, v, ts)  ->
 141       let is_w = proc_term st [] (C.Const w) in
 142       let is_u = proc_term st [] u in
 143       let is_v = proc_term st [] v in
 144       let riss = X.rev_mapi (proc_case st [] w) K.fst_con ts in
 145       let macro = if ts = [] then "CAZE" else "CASE" in
 146       T.Macro macro :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
 147
 148 and proc_case st is w i t =
 149    let v = R.mk_constructor i w in
 150    let is_v = proc_term st [] (C.Const v) in
 151    let is_t = proc_term st [] t in
 152    T.Macro "PAIR" :: T.Group is_v :: T.Group is_t :: is
 153
 154 let proc_term st is t = try proc_term st is t with
 155    | E.ObjectNotFound _
 156    | Invalid_argument "List.nth"
 157    | Failure "nth"
 158    | Failure "name_of_reference" -> malformed "T3"
 159
 160 (* proof processing *)
 161
 162 let typeof st = function
 163    | C.Appl [t]
 164    | t          -> K.whd_typeof st.c t
 165
 166 let init i = {
 167    i = i;
 168    n =  ""; s = [1]; c = [];
 169 }
 170
 171 let push st n = {st with
 172    n = n; s = 1 :: st.s;
 173 }
 174
 175 let next st f = {st with
 176    c = f st.c;
 177    n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
 178 }
 179
 180 let scope st =
 181    X.rev_map_concat string_of_int "." "" (L.tl st.s)
 182
 183 let mk_exit st ris =
 184    if st.n <> "" || L.tl st.s = [] then ris else
 185    T.free (scope st) :: T.Macro "EXIT" :: ris
 186
 187 let mk_open st ris =
 188    if st.n = "" then ris else
 189    T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
 190
 191 let mk_dec st kind w s ris =
 192    let w = if !G.no_types then [] else w in
 193    T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
 194
 195 let mk_inferred st t ris =
 196    let u = typeof st t in
 197    let is_u = proc_term st [] u in
 198    mk_dec st "DECL" is_u st.n ris
 199
 200 let rec proc_proof st ris t = match t with
 201    | C.Appl []
 202    | C.Meta _
 203    | C.Implicit _
 204    | C.Sort _
 205    | C.Prod _              -> malformed "P1"
 206    | C.Const _
 207    | C.Rel _               -> proc_proof st ris (C.Appl [t])
 208    | C.Lambda (s, w, t)    ->
 209       let is_w = proc_term st [] w in
 210       let ris = mk_open st ris in
 211       proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
 212    | C.Appl (t0 :: ts)     ->
 213       let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
 214       let ris = T.Macro "STEP" :: mk_inferred st t ris in
 215       let tts = L.rev_map (proc_term st []) rts in
 216       mk_exit st (T.rev_mk_args tts ris)
 217    | C.Match (w, u, v, ts) ->
 218       let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
 219       let ris = T.Macro "DEST" :: mk_inferred st t ris in
 220       let tts = L.rev_map (proc_term st []) rts in
 221       mk_exit st (T.rev_mk_args tts ris)
 222    | C.LetIn (s, w, v, t)  ->
 223       let is_w = proc_term st [] w in
 224       let ris = mk_open st ris in
 225       if K.not_prop1 st.c w then
 226          let is_v = proc_term st [] v in
 227          let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
 228          proc_proof (next st (K.add_def s w v)) ris t
 229       else
 230          let ris_v = proc_proof (push st s) ris v in
 231          proc_proof (next st (K.add_def s w v)) ris_v t
 232
 233 let proc_proof st rs t = try proc_proof st rs t with
 234    | E.ObjectNotFound _
 235    | Invalid_argument "List.nth"
 236    | Failure "nth"
 237    | Failure "name_of_reference" -> malformed "P2"
 238    | V.TypeCheckerFailure s
 239    | V.AssertFailure s           -> malformed (Lazy.force s)
 240    | Failure "hd"
 241    | Failure "tl"                -> internal "P2"
 242
 243 (* top level processing *)
 244
 245 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
 246
 247 let proc_item item s ss t =
 248    let st = init ss in
 249    let tt = N.process_top_term s t in (* alpha-conversion *)
 250    let is = [T.Macro "end"; T.arg item] in
 251    note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
 252
 253 let proc_top_proof s ss t =
 254    if !G.no_proofs then [] else
 255    let st = init ss in
 256    let t0 = A.process_top_term s t in  (* anticipation *)
 257    let tt = N.process_top_term s t0 in (* alpha-conversion *)
 258    let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
 259    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
 260
 261 let open_out_tex s =
 262    let fname = s ^ T.file_ext in
 263    begin match !G.list_och with
 264       | None     -> ()
 265       | Some och -> P.fprintf och "%s\n" fname
 266    end;
 267    open_out (F.concat !G.out_dir fname)
 268
 269 let proc_pair s ss u = function
 270    | None   ->
 271       let text_u =
 272          if K.not_prop1 [] u then proc_item "assumption"
 273          else proc_item "axiom"
 274       in
 275       let name = X.rev_map_concat X.id "." "type" ss in
 276       let och = open_out_tex name in
 277          O.out_text och (text_u s name u);
 278       close_out och
 279    | Some t ->
 280       let text_u, text_t =
 281          if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
 282          else proc_item "proposition", proc_top_proof
 283       in
 284       let name = X.rev_map_concat X.id "." "type" ss in
 285       let och = open_out_tex name in
 286          O.out_text och (text_u s name u);
 287       close_out och;
 288       let name = X.rev_map_concat X.id "." "body" ss in
 289       let och = open_out_tex name in
 290          O.out_text och (text_t s name t);
 291       close_out och
 292
 293 let proc_fun ss (r, s, i, u, t) =
 294    proc_pair s (s :: ss) u (Some t)
 295
 296 let proc_constructor ss (r, s, u) =
 297    proc_pair s (s :: ss) u None
 298
 299 let proc_type ss (r, s, u, cs) =
 300    proc_pair s (s :: ss) u None;
 301    L.iter (proc_constructor ss) cs
 302
 303 let proc_obj u =
 304    let ss = K.segments_of_uri u in
 305    let _, _, _, _, obj = E.get_checked_obj G.status u in
 306    match obj with
 307       | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
 308       | C.Fixpoint (_, fs, _)       -> L.iter (proc_fun ss) fs
 309       | C.Inductive (_, _, ts, _)   -> L.iter (proc_type ss) ts
 310
 311 (* interface functions ******************************************************)
 312
 313 let process = proc_obj