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 S = String
  15
  16 module U = NUri
  17 module R = NReference
  18 module C = NCic
  19 module P = NCicPp
  20 module E = NCicEnvironment
  21
  22 module G = Options
  23 module T = TeX
  24 module O = TeXOutput
  25
  26 let status = new P.status
  27
  28 (* internal functions *******************************************************)
  29
  30 let rec segments_of_string ss l s =
  31    match try Some (S.index s '/') with Not_found -> None with
  32       | None   -> s :: ss
  33       | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
  34
  35 let segments_of_uri u =
  36    let s = U.string_of_uri u in
  37    let s = F.chop_extension s in
  38    let l = S.length s in
  39    let i = S.index s ':' in
  40    let s = S.sub s (i+2) (l-i-2) in
  41    segments_of_string [] (l-i-2) s
  42
  43 let rec mk_string sep r = function
  44    | []      -> r
  45    | s :: ss -> mk_string sep (s ^ sep ^ r) ss
  46
  47 let alpha c s = s
  48
  49 let malformed s =
  50    failwith ("MaTeX: malformed term: " ^ s)
  51
  52 let not_supported () =
  53    failwith "MaTeX: object not supported"
  54
  55 let proc_sort = function
  56    | C.Prop             -> [T.Macro "Prop"]
  57    | C.Type [`Type, u]  -> [T.Macro "Type"; T.arg (U.string_of_uri u)]
  58    | C.Type [`CProp, u] -> [T.Macro "Crop"; T.arg (U.string_of_uri u)]
  59    | C.Type _           -> malformed "1"
  60
  61 let proc_gref ss = function
  62    | C.Constant _             , R.Decl          ->
  63       T.Macro "GRef" :: T.mk_segs ("type" :: ss)
  64    | C.Constant _             , R.Def _         ->
  65       T.Macro "GRef" :: T.mk_segs ("body" :: ss)
  66    | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
  67       let _, name, _, _ = L.nth us i in
  68       T.Macro "IRef" :: T.mk_segs (name :: ss)
  69    | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
  70       let _, _, _, ts = L.nth us i in
  71       let _, name, _ = L.nth ts (pred j) in
  72       T.Macro "IRef" :: T.mk_segs (name :: ss)
  73    | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
  74       let _, name, _, _, _ = L.nth ts i in
  75       T.Macro "IRef" :: T.mk_segs (name :: ss)
  76    | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
  77       let _, name, _, _, _ = L.nth ts i in
  78       T.Macro "IRef" :: T.mk_segs (name :: ss)
  79    | _                                          ->
  80       malformed "2"
  81
  82 let rec proc_term c = function
  83    | C.Appl []
  84    | C.Meta _
  85    | C.Implicit _          -> malformed "3"
  86    | C.Rel m               ->
  87       let name = L.nth c (m-1) in
  88       [T.Macro "LRef"; T.arg name]
  89    | C.Appl ts             ->
  90       let riss = L.rev_map (proc_term c) ts in
  91       T.Macro "Appl" :: T.mk_rev_args riss
  92   | C.Prod (s, w, t)       ->
  93       let s = alpha c s in
  94       let is_w = proc_term c w in
  95       let is_t = proc_term (s::c) t in
  96       T.Macro "Prod" :: T.arg s :: T.Group is_w :: is_t
  97   | C.Lambda (s, w, t)     ->
  98       let s = alpha c s in
  99       let is_w = proc_term c w in
 100       let is_t = proc_term (s::c) t in
 101       T.Macro "Abst" :: T.arg s :: T.Group is_w :: is_t
 102   | C.LetIn (s, w, v, t)   ->
 103       let s = alpha c s in
 104       let is_w = proc_term c w in
 105       let is_v = proc_term c v in
 106       let is_t = proc_term (s::c) t in
 107       T.Macro "Abbr" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
 108   | C.Sort s               ->
 109       proc_sort s
 110   | C.Const (R.Ref (u, r)) ->
 111       let ss = segments_of_uri u in
 112       let _, _, _, _, obj = E.get_checked_obj status u in
 113       proc_gref ss (obj, r)
 114   | C.Match (w, u, v, ts)  ->
 115       let is_w = proc_term c (C.Const w) in
 116       let is_u = proc_term c u in
 117       let is_v = proc_term c v in
 118       let riss = L.rev_map (proc_term c) ts in
 119       T.Macro "Case" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
 120
 121 let proc_term c t = try proc_term c t with
 122    | E.ObjectNotFound _
 123    | Failure "nth"
 124    | Invalid_argument "List.nth" -> malformed "4"
 125
 126 let open_out_tex s =
 127    open_out (F.concat !G.out_dir (s ^ T.file_ext))
 128
 129 let proc_obj u =
 130    let ss = segments_of_uri u in
 131    let _, _, _, _, obj = E.get_checked_obj status u in
 132    match obj with
 133       | C.Constant (_, _, None, u, _)   -> not_supported ()
 134       | C.Constant (_, _, Some t, u, _) ->
 135          let name = mk_string "." "body" ss in
 136          let och = open_out_tex name in
 137          O.out_text och (proc_term [] t);
 138          O.out_text och T.newline;
 139          close_out och;
 140          let name = mk_string "." "type" ss in
 141          let och = open_out_tex name in
 142          O.out_text och (proc_term [] u);
 143          O.out_text och T.newline;
 144          close_out och
 145       | C.Fixpoint (_, _, _)            -> not_supported ()
 146       | C.Inductive (_, _, _, _)        -> not_supported ()
 147
 148 (* interface functions ******************************************************)
 149
 150 let process = proc_obj