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