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