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