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 N = Alpha
  30
  31 type status = {
  32    i: string;   (* item name *)
  33    n: string;   (* reference name *)
  34    s: int list; (* scope *)
  35    c: C.context (* context for kernel calls *)
  36 }
  37
  38 (* internal functions *******************************************************)
  39
  40 let internal s =
  41    X.error ("engine: malformed stack: " ^ s)
  42
  43 let malformed s =
  44    X.error ("engine: malformed term: " ^ s)
  45
  46 let missing s =
  47    X.log ("engine: missing macro for " ^ s)
  48
  49 (* generic term processing *)
  50
  51 let mk_ptr st name =
  52    if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
  53
  54 let get_macro s l =
  55    let rec aux = function
  56       | []                                 -> ""
  57       | (r, m, a) :: _ when r = s && a = l -> m
  58       | _ :: tl                            -> aux tl
  59    in
  60    aux !G.macro_gref
  61
  62 let get_head = function
  63    | C.Const c :: ts ->
  64       let s, _ = K.resolve_reference c in
  65       let macro = get_macro s (L.length ts) in
  66       if macro <> "" then Some (macro, s, ts) else begin
  67          if !G.log_missing then missing s;
  68          None
  69       end
  70    | _               -> None
  71
  72 let proc_sort st is = function
  73    | C.Prop             -> T.Macro "PROP" :: is
  74    | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
  75    | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
  76    | C.Type _           -> malformed "T1"
  77
  78 let rec proc_term st is = function
  79    | C.Appl []
  80    | C.Meta _
  81    | C.Implicit _           -> malformed "T2"
  82    | C.Rel m                ->
  83       let name = K.resolve_lref st.c m in
  84       T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
  85    | C.Appl ts              ->
  86       begin match get_head ts with
  87          | Some (macro, s, ts) ->
  88             let riss = L.rev_map (proc_term st []) ts in
  89             T.Macro macro :: T.free s :: T.mk_rev_args riss is
  90          | None                ->
  91             let riss = L.rev_map (proc_term st []) ts in
  92             T.Macro "APPL" :: T.mk_rev_args riss is
  93       end
  94    | C.Prod (s, w, t)       ->
  95       let is_w = proc_term st [] w in
  96       let c = K.add_dec s w st.c in
  97       let is_t = proc_term {st with c=c} is t in
  98       let macro = if K.not_prop1 c t then "PROD" else "FALL" in
  99       T.Macro macro :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
 100    | C.Lambda (s, w, t)     ->
 101       let is_w = proc_term st [] w in
 102       let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
 103       T.Macro "ABST" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
 104    | C.LetIn (s, w, v, t)   ->
 105       let is_w = proc_term st [] w in
 106       let is_v = proc_term st [] v in
 107       let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
 108       T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
 109    | C.Sort s               ->
 110       proc_sort st is s
 111    | C.Const c              ->
 112       let s, name = K.resolve_reference c in
 113       T.Macro "GREF" :: T.arg name :: T.free s :: is
 114    | C.Match (w, u, v, ts)  ->
 115       let is_w = proc_term st [] (C.Const w) in
 116       let is_u = proc_term st [] u in
 117       let is_v = proc_term st [] v in
 118       let riss = L.rev_map (proc_term st []) ts in
 119       T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
 120
 121 let proc_term st is t = try proc_term st is t with
 122    | E.ObjectNotFound _
 123    | Invalid_argument "List.nth"
 124    | Failure "nth"
 125    | Failure "name_of_reference" -> malformed "T3"
 126
 127 (* proof processing *)
 128
 129 let typeof st = function
 130    | C.Appl [t]
 131    | t          -> K.whd_typeof st.c t
 132
 133 let init i = {
 134    i = i;
 135    n =  ""; s = [1]; c = [];
 136 }
 137
 138 let push st n = {st with
 139    n = n; s = 1 :: st.s;
 140 }
 141
 142 let next st f = {st with
 143    c = f st.c;
 144    n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
 145 }
 146
 147 let scope st =
 148    X.rev_map_concat string_of_int "." "" (L.tl st.s)
 149
 150 let mk_exit st ris =
 151    if st.n <> "" || L.tl st.s = [] then ris else
 152    T.free (scope st) :: T.Macro "EXIT" :: ris
 153
 154 let mk_open st ris =
 155    if st.n = "" then ris else
 156    T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris
 157
 158 let mk_dec st kind w s ris =
 159    let w = if !G.no_types then [T.Macro "NONE"] else w in
 160    T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris
 161
 162 let mk_inferred st t ris =
 163    let u = typeof st t in
 164    let is_u = proc_term st [] u in
 165    mk_dec st "DECL" is_u st.n ris
 166
 167 let rec proc_proof st ris t = match t with
 168    | C.Appl []
 169    | C.Meta _
 170    | C.Implicit _
 171    | C.Sort _
 172    | C.Prod _              -> malformed "P1"
 173    | C.Const _
 174    | C.Rel _               -> proc_proof st ris (C.Appl [t])
 175    | C.Lambda (s, w, t)    ->
 176       let is_w = proc_term st [] w in
 177       let ris = mk_open st ris in
 178       proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
 179    | C.Appl (t0 :: ts)     ->
 180       let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
 181       let ris = T.Macro "STEP" :: mk_inferred st t ris in
 182       let tts = L.rev_map (proc_term st []) rts in
 183       mk_exit st (T.rev_mk_args tts ris)
 184    | C.Match (w, u, v, ts) ->
 185       let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
 186       let ris = T.Macro "DEST" :: mk_inferred st t ris in
 187       let tts = L.rev_map (proc_term st []) rts in
 188       mk_exit st (T.rev_mk_args tts ris)
 189    | C.LetIn (s, w, v, t)  ->
 190       let is_w = proc_term st [] w in
 191       let ris = mk_open st ris in
 192       if K.not_prop1 st.c w then
 193          let is_v = proc_term st [] v in
 194          let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
 195          proc_proof (next st (K.add_def s w v)) ris t
 196       else
 197          let ris_v = proc_proof (push st s) ris v in
 198          proc_proof (next st (K.add_def s w v)) ris_v t
 199
 200 let proc_proof st rs t = try proc_proof st rs t with
 201    | E.ObjectNotFound _
 202    | Invalid_argument "List.nth"
 203    | Failure "nth"
 204    | Failure "name_of_reference" -> malformed "P2"
 205    | V.TypeCheckerFailure s
 206    | V.AssertFailure s           -> malformed (Lazy.force s)
 207    | Failure "hd"
 208    | Failure "tl"                -> internal "P2"
 209
 210 (* top level processing *)
 211
 212 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
 213
 214 let proc_item item s ss t =
 215    let st = init ss in
 216    let tt = N.process_top_term s t in (* alpha-conversion *)
 217    let is = [T.Macro "end"; T.arg item] in
 218    note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term st is tt
 219
 220 let proc_top_proof s ss t =
 221    let st = init ss in
 222    let t0 = A.process_top_term s t in  (* anticipation *)
 223    let tt = N.process_top_term s t0 in (* alpha-conversion *)
 224    let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
 225    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
 226
 227 let open_out_tex s =
 228    let fname = s ^ T.file_ext in
 229    begin match !G.list_och with
 230       | None     -> ()
 231       | Some och -> P.fprintf och "%s\n" fname
 232    end;
 233    open_out (F.concat !G.out_dir fname)
 234
 235 let proc_pair s ss u = function
 236    | None   ->
 237       let name = X.rev_map_concat X.id "." "type" ss in
 238       let och = open_out_tex name in
 239          O.out_text och (proc_item "axiom" s name u);
 240       close_out och
 241    | Some t ->
 242       let text_u, text_t =
 243          if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
 244          else proc_item "proposition", proc_top_proof
 245       in
 246       let name = X.rev_map_concat X.id "." "type" ss in
 247       let och = open_out_tex name in
 248          O.out_text och (text_u s name u);
 249       close_out och;
 250       let name = X.rev_map_concat X.id "." "body" ss in
 251       let och = open_out_tex name in
 252          O.out_text och (text_t s name t);
 253       close_out och
 254
 255 let proc_fun ss (r, s, i, u, t) =
 256    proc_pair s (s :: ss) u (Some t)
 257
 258 let proc_constructor ss (r, s, u) =
 259    proc_pair s (s :: ss) u None
 260
 261 let proc_type ss (r, s, u, cs) =
 262    proc_pair s (s :: ss) u None;
 263    L.iter (proc_constructor ss) cs
 264
 265 let proc_obj u =
 266    let ss = K.segments_of_uri u in
 267    let _, _, _, _, obj = E.get_checked_obj G.status u in
 268    match obj with
 269       | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
 270       | C.Fixpoint (_, fs, _)       -> L.iter (proc_fun ss) fs
 271       | C.Inductive (_, _, ts, _)   -> L.iter (proc_type ss) ts
 272
 273 (* interface functions ******************************************************)
 274
 275 let process = proc_obj