helm/software/components/acic_procedural/proceduralTeX.ml

   1 (* Copyright (C) 2003-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module F   = Format
  27 module C   = Cic
  28 module DTI = DoubleTypeInference
  29 module H   = ProceduralHelpers
  30 module T   = ProceduralTypes
  31
  32 type sorts = (Cic.id, Cic2acic.sort_kind) Hashtbl.t
  33
  34 let num n =
  35    if n < 2 then "" else
  36    if n < 27 then String.make 1 (Char.chr (n - 2 + Char.code 'b')) else
  37    assert false
  38
  39 let quote str =
  40    Pcre.replace ~pat:"_" ~templ:"\\_" str
  41
  42 let xn frm = function
  43    | C.Anonymous -> assert false
  44    | C.Name r    -> F.fprintf frm "%s" (quote r)
  45
  46 let xr c frm j =
  47    try match List.nth c (pred j) with
  48       | Some (r, _) -> xn frm r
  49       | None        -> assert false
  50    with Invalid_argument "nth" -> assert false
  51
  52 let xs frm = function
  53    | C.Set     -> F.fprintf frm "\\Set"
  54    | C.Prop    -> F.fprintf frm "\\Prop"
  55    | C.CProp _ -> F.fprintf frm "\\CProp"
  56    | C.Type _  -> F.fprintf frm "\\Type"
  57
  58 let rec xt c frm = function
  59    | C.Sort s                     ->
  60       xs frm s
  61    | C.Const (i, [])              ->
  62       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i None None))
  63    | C.MutInd (i, n, [])          ->
  64       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) None))
  65    | C.MutConstruct (i, n, m, []) ->
  66       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) (Some m)))
  67    | C.Rel j                      ->
  68       F.fprintf frm "\\LRef{%a}" (xr c) j
  69    | C.Cast (t, u)                ->
  70       F.fprintf frm "\\Cast{%a}{%a}" (xt c) u (xt c) t
  71    | C.Appl (t :: vs)             ->
  72       let z = num (List.length vs) in
  73       F.fprintf frm "\\%sAppl%a{%a}" z (xts c) vs (xt c) t
  74    | C.MutCase (_, _, u, v, ts)   ->
  75       let z = num (List.length ts) in
  76       F.fprintf frm "\\%sCase{%a}{%a}%a" z (xt c) u (xt c) v (xts c) ts
  77    | C.LetIn (r, v, w, t)         ->
  78       let d = Some (r, C.Def (v, w)) :: c in
  79       F.fprintf frm "\\Abbr{%a}{%a}{%a}" xn r (xt c) v (xt d) t
  80    | C.Lambda (r, w, t)           ->
  81       let d = Some (r, C.Decl w) :: c in
  82       if DTI.does_not_occur 1 t then
  83          F.fprintf frm "\\CFun{%a}{%a}" (xt c) w (xt d) t
  84       else
  85          F.fprintf frm "\\Abst{%a}{%a}{%a}" xn r (xt c) w (xt d) t
  86    | C.Prod (r, w, t)             ->
  87       let d = Some (r, C.Decl w) :: c in
  88       if DTI.does_not_occur 1 t then
  89          F.fprintf frm "\\LImp{%a}{%a}" (xt c) w (xt d) t
  90       else if H.is_prop d t then
  91          F.fprintf frm "\\LAll{%a}{%a}{%a}" xn r (xt c) w (xt d) t
  92       else
  93          F.fprintf frm "\\Prod{%a}{%a}{%a}" xn r (xt c) w (xt d) t
  94    | C.Const _                    -> assert false
  95    | C.MutInd _                   -> assert false
  96    | C.MutConstruct _             -> assert false
  97    | C.Var _                      -> assert false
  98    | C.Fix _                      -> assert false
  99    | C.CoFix _                    -> assert false
 100    | C.Meta _                     -> assert false
 101    | C.Implicit _                 -> assert false
 102    | C.Appl []                    -> assert false
 103
 104 and xts c frm vs =
 105    let map v = F.fprintf frm "{%a}" (xt c) v in
 106    List.iter map vs
 107
 108 let tex_of_term frm c t = xt c frm t
 109
 110 let tex_of_obj frm = function
 111    | C.InductiveDefinition (_, [], _, _) -> ()
 112    | C.Constant (_, None, _, [], _)      -> ()
 113    | C.Constant (_, Some t, _, [], _)    ->
 114       F.fprintf frm "%a@\n" (xt []) t
 115    | C.Constant _                        -> assert false
 116    | C.InductiveDefinition _             -> assert false
 117    | C.Variable _                        -> assert false
 118    | C.CurrentProof _                    -> assert false
 119
 120 let is_prop sorts id =
 121    try match Hashtbl.find sorts id with
 122       | `Prop -> true
 123       | _     -> false
 124    with Not_found -> false
 125
 126 let tex_of_annterm frm sorts t =
 127
 128 let rec xat frm = function
 129    | C.ASort (_, s)                   ->
 130       xs frm s
 131    | C.AConst (_ ,i, [])              ->
 132       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i None None))
 133    | C.AMutInd (_, i, n, [])          ->
 134       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) None))
 135    | C.AMutConstruct (_, i, n, m, []) ->
 136       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) (Some m)))
 137    | C.ARel (_,_, _, r)               ->
 138       F.fprintf frm "\\LRef{%s}" (quote r)
 139    | C.ACast (_, t, u)                ->
 140       F.fprintf frm "\\Cast{%a}{%a}" xat u xat t
 141    | C.AAppl (_, t :: vs)             ->
 142       let z = num (List.length vs) in
 143       F.fprintf frm "\\%sAppl%a{%a}" z xats vs xat t
 144    | C.AMutCase (_, _, _, u, v, ts)   ->
 145       let z = num (List.length ts) in
 146       F.fprintf frm "\\%sCase{%a}{%a}%a" z xat u xat v xats ts
 147    | C.ALetIn (_, r, v, w, t)         ->
 148       F.fprintf frm "\\Abbr{%a}{%a}{%a}" xn r xat v xat t
 149    | C.ALambda (_, r, w, t)           ->
 150       if DTI.does_not_occur 1 (H.cic t) then
 151          F.fprintf frm "\\CFun{%a}{%a}" xat w xat t
 152       else
 153          F.fprintf frm "\\Abst{%a}{%a}{%a}" xn r xat w xat t
 154    | C.AProd (id, r, w, t)            ->
 155       if DTI.does_not_occur 1 (H.cic t) then
 156          F.fprintf frm "\\LImp{%a}{%a}" xat w xat t
 157       else if true then
 158          F.fprintf frm "\\LAll{%a}{%a}{%a}" xn r xat w xat t
 159       else
 160          F.fprintf frm "\\Prod{%a}{%a}{%a}" xn r xat w xat t
 161    | C.AConst _                       -> assert false
 162    | C.AMutInd _                      -> assert false
 163    | C.AMutConstruct _                -> assert false
 164    | C.AVar _                         -> assert false
 165    | C.AFix _                         -> assert false
 166    | C.ACoFix _                       -> assert false
 167    | C.AMeta _                        -> assert false
 168    | C.AImplicit _                    -> assert false
 169    | C.AAppl (_, [])                  -> assert false
 170
 171 and xats frm vs =
 172    let map v = F.fprintf frm "{%a}" xat v in
 173    List.iter map vs
 174
 175 in
 176 xat frm t
 177
 178 let xx frm = function
 179    | None   -> assert false
 180    | Some r -> F.fprintf frm "%s" (quote r)
 181
 182 let tex_of_steps frm sorts l =
 183
 184 let xat frm t = tex_of_annterm frm sorts t in
 185
 186 let rec xl frm = function
 187    | []                        -> ()
 188    | T.Note _ :: l
 189    | T.Statement _ :: l
 190    | T.Qed _ :: l              -> xl frm l
 191    | T.Intros (_, [r], _) :: l ->
 192       F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
 193    | T.LetIn (r, v, _) :: l    ->
 194       F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
 195    | T.Inductive _ :: _        -> assert false
 196    | T.Id _ :: _               -> assert false
 197    | T.Clear _ :: _            -> assert false
 198    | T.ClearBody _ :: _        -> assert false
 199    | T.Branch _ :: _           -> assert false
 200    | T.Intros _ :: _           -> assert false
 201 in
 202 xl frm l