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 = function
 172    | [] -> F.fprintf frm "{}"
 173    | vs ->
 174       let map v = F.fprintf frm "{%a}" xat v in
 175       List.iter map vs
 176
 177 in
 178 xat frm t
 179
 180 let xx frm = function
 181    | None   -> assert false
 182    | Some r -> F.fprintf frm "%s" (quote r)
 183
 184 let xh how =
 185    if how then "\\dx" else "\\sx"
 186
 187 let tex_of_steps frm sorts l =
 188
 189 let xat frm t = tex_of_annterm frm sorts t in
 190
 191 let rec xl frm = function
 192    | []                                                    -> ()
 193    | T.Note _ :: l
 194    | T.Statement _ :: l
 195    | T.Qed _ :: l                                          ->
 196       xl frm l
 197    | T.Reflexivity _ :: l                                  ->
 198       F.fprintf frm "\\Reflexivity"; xl frm l
 199    | T.Exact (t, _) :: l                                   ->
 200       F.fprintf frm "\\Exact{%a}" xat t; xl frm l
 201    | T.Intros (_, [r], _) :: l                             ->
 202       F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
 203    | T.LetIn (r, v, _) :: l                                ->
 204       F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
 205    | T.LApply (r, v, _) :: l                               ->
 206       F.fprintf frm "\\LApply{%a}{%a}{%a}" xx r xat v xl l
 207    | T.Change (u, _, None, _, _) :: l                      ->
 208       F.fprintf frm "\\Change{%a}{}{%a}" xat u xl l
 209    | T.Change (u, _, Some (s, _), _, _) :: l               ->
 210       F.fprintf frm "\\Change{%a}{%s}{%a}" xat u (quote s) xl l
 211    | T.Rewrite (b, t, None, _, _) :: l                     ->
 212       F.fprintf frm "\\Rewrite{%s}{%a}{}{}{%a}" (xh b) xat t xl l
 213    | T.Rewrite (b, t, Some (s1, Some s2), _, _) :: l       ->
 214       F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
 215          (xh b) xat t (quote s1) (quote s2) xl l
 216    | T.Rewrite (b, t, Some (s1, None), _, _) :: l          ->
 217       F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
 218          (xh b) xat t (quote s1) (quote s1) xl l
 219    | T.Apply (t, _) :: T.Branch (ls, _) :: l               ->
 220       let z = num (List.length ls) in
 221       F.fprintf frm "\\%sApply{%a}%a" z xat t xls ls; xl frm l
 222    | T.Apply (t, _) :: l                                   ->
 223       F.fprintf frm "\\Apply{%a}{%a}" xat t xl l
 224    | T.Cases (v, _, _) :: T.Branch (ls, _) :: l            ->
 225       let z = num (List.length ls) in
 226       F.fprintf frm "\\%sCases{%a}%a" z xat v xls ls; xl frm l
 227    | T.Cases (v, _, _) :: l                                ->
 228       F.fprintf frm "\\Cases{%a}{%a}" xat v xl l
 229    | T.Elim (v, Some t, _, _) :: T.Branch (ls, _) :: l     ->
 230       let z = num (List.length ls) in
 231       F.fprintf frm "\\%sElim{%a}{%a}{}{}%a" z xat v xat t xls ls; xl frm l
 232    | T.Elim (v, Some t, _, _) :: l                         ->
 233       F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
 234    | T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
 235       F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
 236    | T.Record _ :: _                                       -> assert false
 237    | T.Inductive _ :: _                                    -> assert false
 238    | T.Id _ :: _                                           -> assert false
 239    | T.Clear _ :: _                                        -> assert false
 240    | T.ClearBody _ :: _                                    -> assert false
 241    | T.Branch _ :: _                                       -> assert false
 242    | T.Intros _ :: _                                       -> assert false
 243    | T.Elim _ :: _                                         -> assert false
 244    | T.Cut _ :: _                                          -> assert false
 245
 246 and xls frm = function
 247    | [] -> F.fprintf frm "{}"
 248    | ls ->
 249       let map l = F.fprintf frm "{%a}" xl l in
 250       List.iter map (List.rev ls)
 251
 252 in
 253 F.fprintf frm "%a@\n" xl l