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