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