helm/ocaml/cic_transformations/content_expressions.ml

   1 (* Copyright (C) 2000, 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 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             27/6/2003                                   *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35
  36 (* the type cexpr is inspired by OpenMath. A few primitive constructors
  37    have been added, in order to take into account some special features
  38    of functional expressions. Most notably: case, let in, let rec, and
  39    explicit substitutons *)
  40
  41 type cexpr =
  42     Symbol of string option * string * subst option * string option
  43                              (* h:xref, name, subst, definitionURL *)
  44   | LocalVar of (string option) * string        (* h:xref, name *)
  45   | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
  46   | Num of string option * string             (* h:xref, value *)
  47   | Appl of string option * cexpr list        (* h:xref, args *)
  48   | Binder of string option * string * decl * cexpr
  49                                        (* h:xref, name, decl, body *)
  50   | Letin of string option * def * cexpr          (* h:xref, def, body *)
  51   | Letrec of string option * def list * cexpr    (* h:xref, def list, body *)
  52   | Case of string option * cexpr * ((string * cexpr) list)
  53                                (* h:xref, case_expr, named-pattern list *)
  54
  55 and
  56   decl = string * cexpr               (* name, type *)
  57 and
  58   def = string * cexpr               (* name, body *)
  59 and
  60   subst = (UriManager.uri * cexpr) list
  61 and
  62   meta_subst = cexpr option list
  63 ;;
  64
  65 (* NOTATION *)
  66
  67 let symbol_table = Hashtbl.create 503;;
  68
  69 (* eq *)
  70 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
  71   (fun aid sid args acic2cexpr ->
  72    Appl
  73     (Some aid, (Symbol (Some sid, "eq",
  74           None, Some "cic:/Coq/Init/Logic/eq.ind"))
  75      :: List.map acic2cexpr (List.tl args)));;
  76
  77 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
  78   (fun aid sid args acic2cexpr ->
  79    Appl
  80     (Some aid, (Symbol (Some sid, "eq",
  81           None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
  82      :: List.map acic2cexpr (List.tl args)));;
  83
  84 (* and *)
  85 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
  86   (fun aid sid args acic2cexpr ->
  87    Appl
  88     (Some aid, (Symbol (Some sid, "and",
  89           None, Some "cic:/Coq/Init/Logic/and.ind"))
  90      :: List.map acic2cexpr args));;
  91
  92 (* or *)
  93 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
  94   (fun aid sid args acic2cexpr ->
  95    Appl
  96     (Some aid, (Symbol (Some sid, "or",
  97           None, Some "cic:/Coq/Init/Logic/or.ind"))
  98      :: List.map acic2cexpr args));;
  99
 100 (* iff *)
 101 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con"
 102   (fun aid sid args acic2cexpr ->
 103    Appl
 104     (Some aid, (Symbol (Some sid, "iff",
 105           None, Some "cic:/Coq/Init/Logic/iff.con"))
 106      :: List.map acic2cexpr args));;
 107
 108 (* not *)
 109 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
 110   (fun aid sid args acic2cexpr ->
 111    Appl
 112     (Some aid, (Symbol (Some sid, "not",
 113           None, Some "cic:/Coq/Init/Logic/not.con"))
 114      :: List.map acic2cexpr args));;
 115
 116 (* exists *)
 117 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
 118   (fun aid sid args acic2cexpr ->
 119    match (List.tl args) with
 120      [Cic.ALambda (_,Cic.Name n,s,t)] ->
 121        Binder
 122         (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
 123   | _ -> raise Not_found);;
 124
 125 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
 126   (fun aid sid args acic2cexpr ->
 127    match (List.tl args) with
 128      [Cic.ALambda (_,Cic.Name n,s,t)] ->
 129        Binder
 130         (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
 131   | _ -> raise Not_found);;
 132
 133 (* leq *)
 134 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)"
 135   (fun aid sid args acic2cexpr ->
 136    Appl
 137     (Some aid, (Symbol (Some sid, "leq",
 138           None, Some "cic:/Coq/Init/Peano/le.ind"))
 139      :: List.map acic2cexpr args));;
 140
 141 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
 142   (fun aid sid args acic2cexpr ->
 143    Appl
 144     (Some aid, (Symbol (Some sid, "leq",
 145           None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
 146      :: List.map acic2cexpr args));;
 147
 148 (* lt *)
 149 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con"
 150   (fun aid sid args acic2cexpr ->
 151    Appl
 152     (Some aid, (Symbol (Some sid, "lt",
 153           None, Some "cic:/Coq/Init/Peano/lt.con"))
 154      :: List.map acic2cexpr args));;
 155
 156 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con"
 157   (fun aid sid args acic2cexpr ->
 158    Appl
 159     (Some aid, (Symbol (Some sid, "lt",
 160           None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
 161      :: List.map acic2cexpr args));;
 162
 163 (* geq *)
 164 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con"
 165   (fun aid sid args acic2cexpr ->
 166    Appl
 167     (Some aid, (Symbol (Some sid, "geq",
 168           None, Some "cic:/Coq/Init/Peano/ge.con"))
 169      :: List.map acic2cexpr args));;
 170
 171 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con"
 172   (fun aid sid args acic2cexpr ->
 173    Appl
 174     (Some aid, (Symbol (Some sid, "geq",
 175           None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
 176      :: List.map acic2cexpr args));;
 177
 178 (* gt *)
 179 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con"
 180   (fun aid sid args acic2cexpr ->
 181    Appl
 182     (Some aid, (Symbol (Some sid, "gt",
 183           None, Some "cic:/Coq/Init/Peano/gt.con"))
 184      :: List.map acic2cexpr args));;
 185
 186 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con"
 187   (fun aid sid args acic2cexpr ->
 188    Appl
 189     (Some aid, (Symbol (Some sid, "gt",
 190           None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
 191      :: List.map acic2cexpr args));;
 192
 193 (* plus *)
 194 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con"
 195   (fun aid sid args acic2cexpr ->
 196    Appl
 197     (Some aid, (Symbol (Some sid, "plus",
 198           None, Some "cic:/Coq/Init/Peano/plus.con"))
 199      :: List.map acic2cexpr args));;
 200
 201 Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
 202   (fun aid sid args acic2cexpr ->
 203    Appl
 204     (Some aid, (Symbol (Some sid, "plus",
 205           None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
 206      :: List.map acic2cexpr args));;
 207
 208 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
 209   (fun aid sid args acic2cexpr ->
 210    Appl
 211     (Some aid, (Symbol (Some sid, "plus",
 212           None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
 213      :: List.map acic2cexpr args));;
 214
 215 (* times *)
 216 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
 217   (fun aid sid args acic2cexpr ->
 218    Appl
 219     (Some aid, (Symbol (Some sid, "times",
 220           None, Some "cic:/Coq/Init/Peano/mult.con"))
 221      :: List.map acic2cexpr args));;
 222
 223
 224 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
 225   (fun aid sid args acic2cexpr ->
 226    Appl
 227     (Some aid, (Symbol (Some sid, "times",
 228           None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
 229      :: List.map acic2cexpr args));;
 230 (* minus *)
 231 Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
 232   (fun aid sid args acic2cexpr ->
 233    Appl
 234     (Some aid, (Symbol (Some sid, "minus",
 235           None, Some "cic:/Coq/Arith/Minus/mult.con"))
 236      :: List.map acic2cexpr args));;
 237
 238 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
 239   (fun aid sid args acic2cexpr ->
 240    Appl
 241     (Some aid, (Symbol (Some sid, "minus",
 242           None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
 243      :: List.map acic2cexpr args));;
 244
 245 (* div *)
 246 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
 247   (fun aid sid args acic2cexpr ->
 248    Appl
 249     (Some aid, (Symbol (Some sid, "div",
 250           None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
 251      :: List.map acic2cexpr args));;
 252
 253
 254
 255
 256 (* END NOTATION *)
 257
 258
 259 let string_of_sort =
 260   function
 261     Cic.Prop -> "Prop"
 262   | Cic.Set  -> "Set"
 263   | Cic.Type -> "Type"
 264 ;;
 265
 266 let get_constructors uri i =
 267   let inductive_types =
 268     (match CicEnvironment.get_obj uri with
 269          Cic.Constant _ -> assert false
 270      | Cic.Variable _ -> assert false
 271      | Cic.CurrentProof _ -> assert false
 272      | Cic.InductiveDefinition (l,_,_) -> l
 273     ) in
 274    let (_,_,_,constructors) = List.nth inductive_types i in
 275    constructors
 276 ;;
 277
 278 exception NotImplemented;;
 279
 280 let acic2cexpr ids_to_inner_sorts t =
 281   let rec acic2cexpr t =
 282     let module C = Cic in
 283     let module X = Xml in
 284     let module U = UriManager in
 285     let module C2A = Cic2acic in
 286     let make_subst =
 287       function
 288           [] -> None
 289         | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
 290     match t with
 291       C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
 292     | C.AVar (id,uri,subst) ->
 293         Symbol (Some id, UriManager.name_of_uri uri,
 294           make_subst subst, Some (UriManager.string_of_uri uri))
 295     | C.AMeta (id,n,l) ->
 296        let l' =
 297         List.rev_map
 298          (function
 299              None -> None
 300            | Some t -> Some (acic2cexpr t)
 301          ) l
 302        in
 303         Meta (Some id,("?" ^ (string_of_int n)),l')
 304     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
 305     | C.AImplicit _ -> raise NotImplemented
 306     | C.AProd (id,n,s,t) ->
 307         (match n with
 308            Cic.Anonymous ->
 309              Appl (Some id, [Symbol (None, "arrow",None,None);
 310                acic2cexpr s; acic2cexpr t])
 311          | Cic.Name name ->
 312              let sort =
 313                (try Hashtbl.find ids_to_inner_sorts id
 314                 with Not_found ->
 315                    (* if the Prod does not have the sort, it means
 316                       that it has been generated by cic2content, and
 317                       thus is a statement *)
 318                   "Prop") in
 319              let binder = if sort = "Prop" then "Forall" else "Prod" in
 320              let decl = (name, acic2cexpr s) in
 321              Binder (Some id,binder,decl,acic2cexpr t))
 322     | C.ACast (id,v,t) -> acic2cexpr v
 323     | C.ALambda (id,n,s,t) ->
 324         let name =
 325           (match n with
 326              Cic.Anonymous -> "_"
 327            | Cic.Name name -> name) in
 328         let decl = (name, acic2cexpr s) in
 329         Binder (Some id,"Lambda",decl,acic2cexpr t)
 330     | C.ALetIn (id,n,s,t) ->
 331         (match n with
 332            Cic.Anonymous -> assert false
 333          | Cic.Name name ->
 334              let def = (name, acic2cexpr s) in
 335              Letin (Some id,def,acic2cexpr t))
 336     | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
 337         let uri_str = UriManager.string_of_uri uri in
 338         (try
 339           (let f = Hashtbl.find symbol_table uri_str in
 340            f aid sid tl acic2cexpr)
 341         with notfound ->
 342           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
 343           make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 344     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
 345         let inductive_types =
 346           (match CicEnvironment.get_obj uri with
 347              Cic.Constant _ -> assert false
 348            | Cic.Variable _ -> assert false
 349            | Cic.CurrentProof _ -> assert false
 350            | Cic.InductiveDefinition (l,_,_) -> l
 351           ) in
 352         let (name,_,_,_) = List.nth inductive_types i in
 353         let uri_str = UriManager.string_of_uri uri in
 354         let puri_str =
 355          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
 356         (try
 357           (let f = Hashtbl.find symbol_table puri_str in
 358            f aid sid tl acic2cexpr)
 359          with notfound ->
 360            Appl (Some aid, Symbol (Some sid, name,
 361            make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 362     | C.AAppl (id,li) ->
 363         Appl (Some id, List.map acic2cexpr li)
 364     | C.AConst (id,uri,subst) ->
 365         Symbol (Some id, UriManager.name_of_uri uri,
 366           make_subst subst, Some (UriManager.string_of_uri uri))
 367     | C.AMutInd (id,uri,i,subst) ->
 368         let inductive_types =
 369           (match CicEnvironment.get_obj uri with
 370              Cic.Constant _ -> assert false
 371            | Cic.Variable _ -> assert false
 372            | Cic.CurrentProof _ -> assert false
 373            | Cic.InductiveDefinition (l,_,_) -> l
 374           ) in
 375         let (name,_,_,_) = List.nth inductive_types i in
 376         let uri_str = UriManager.string_of_uri uri in
 377         Symbol (Some id, name, make_subst subst, Some uri_str)
 378     | C.AMutConstruct (id,uri,i,j,subst) ->
 379         let constructors = get_constructors uri i in
 380         let (name,_) = List.nth constructors (j-1) in
 381         let uri_str = UriManager.string_of_uri uri in
 382         Symbol (Some id, name, make_subst subst, Some uri_str)
 383     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 384         let constructors = get_constructors uri typeno in
 385         let named_patterns =
 386           List.map2 (fun c p -> (fst c, acic2cexpr p))
 387             constructors patterns in
 388         Case (Some id, acic2cexpr te, named_patterns)
 389     | C.AFix (id, no, funs) ->
 390         let defs =
 391           List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
 392         let (name,_) = List.nth defs no in
 393         let body = LocalVar (None, name)  in
 394         Letrec (Some id, defs, body)
 395     | C.ACoFix (id,no,funs) ->
 396         let defs =
 397           List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
 398         let (name,_) = List.nth defs no in
 399         let body = LocalVar (None, name)  in
 400         Letrec (Some id, defs, body) in
 401   acic2cexpr t
 402 ;;
 403
 404
 405
 406
 407
 408
 409
 410
 411
 412
 413