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 substitutions *)
  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/Ropp.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 let rplus_uri =
 225   UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
 226 let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;;
 227 let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
 228
 229 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
 230   (fun aid sid args acic2cexpr ->
 231    let appl () =
 232      Appl
 233       (Some aid, (Symbol (Some sid, "plus",
 234             None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
 235        :: List.map acic2cexpr args)
 236    in
 237     let rec aux acc = function
 238       | [ Cic.AConst (nid, uri, []); n] when
 239           UriManager.eq uri r1_uri ->
 240             (match n with
 241             | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
 242                 Num (Some aid, string_of_int (acc + 2))
 243             | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
 244                 UriManager.eq uri rplus_uri ->
 245                   aux (acc + 1) args
 246             | _ -> appl ())
 247       | _ -> appl ()
 248     in
 249     aux 0 args)
 250 ;;
 251
 252 (* zero and one *)
 253
 254 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
 255   (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
 256
 257 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
 258   (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
 259
 260 (* times *)
 261 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
 262   (fun aid sid args acic2cexpr ->
 263    Appl
 264     (Some aid, (Symbol (Some sid, "times",
 265           None, Some "cic:/Coq/Init/Peano/mult.con"))
 266      :: List.map acic2cexpr args));;
 267
 268
 269 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
 270   (fun aid sid args acic2cexpr ->
 271    Appl
 272     (Some aid, (Symbol (Some sid, "times",
 273           None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
 274      :: List.map acic2cexpr args));;
 275 (* minus *)
 276 Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
 277   (fun aid sid args acic2cexpr ->
 278    Appl
 279     (Some aid, (Symbol (Some sid, "minus",
 280           None, Some "cic:/Coq/Arith/Minus/mult.con"))
 281      :: List.map acic2cexpr args));;
 282
 283 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
 284   (fun aid sid args acic2cexpr ->
 285    Appl
 286     (Some aid, (Symbol (Some sid, "minus",
 287           None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
 288      :: List.map acic2cexpr args));;
 289
 290 (* div *)
 291 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
 292   (fun aid sid args acic2cexpr ->
 293    Appl
 294     (Some aid, (Symbol (Some sid, "div",
 295           None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
 296      :: List.map acic2cexpr args));;
 297
 298
 299
 300
 301 (* END NOTATION *)
 302
 303
 304 let string_of_sort =
 305   function
 306     Cic.Prop  -> "Prop"
 307   | Cic.Set   -> "Set"
 308   | Cic.Type  -> "Type"
 309   | Cic.CProp -> "Type"
 310 ;;
 311
 312 let get_constructors uri i =
 313   let inductive_types =
 314     (match CicEnvironment.get_obj uri with
 315          Cic.Constant _ -> assert false
 316      | Cic.Variable _ -> assert false
 317      | Cic.CurrentProof _ -> assert false
 318      | Cic.InductiveDefinition (l,_,_) -> l
 319     ) in
 320    let (_,_,_,constructors) = List.nth inductive_types i in
 321    constructors
 322 ;;
 323
 324 exception NotImplemented;;
 325
 326 let acic2cexpr ids_to_inner_sorts t =
 327   let rec acic2cexpr t =
 328     let module C = Cic in
 329     let module X = Xml in
 330     let module U = UriManager in
 331     let module C2A = Cic2acic in
 332     let make_subst =
 333       function
 334           [] -> None
 335         | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
 336     match t with
 337       C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
 338     | C.AVar (id,uri,subst) ->
 339         Symbol (Some id, UriManager.name_of_uri uri,
 340           make_subst subst, Some (UriManager.string_of_uri uri))
 341     | C.AMeta (id,n,l) ->
 342        let l' =
 343         List.rev_map
 344          (function
 345              None -> None
 346            | Some t -> Some (acic2cexpr t)
 347          ) l
 348        in
 349         Meta (Some id,("?" ^ (string_of_int n)),l')
 350     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
 351     | C.AImplicit _ -> raise NotImplemented
 352     | C.AProd (id,n,s,t) ->
 353         (match n with
 354            Cic.Anonymous ->
 355              Appl (Some id, [Symbol (None, "arrow",None,None);
 356                acic2cexpr s; acic2cexpr t])
 357          | Cic.Name name ->
 358              let sort =
 359                (try Hashtbl.find ids_to_inner_sorts id
 360                 with Not_found ->
 361                    (* if the Prod does not have the sort, it means
 362                       that it has been generated by cic2content, and
 363                       thus is a statement *)
 364                   "Prop") in
 365              let binder = if sort = "Prop" then "Forall" else "Prod" in
 366              let decl = (name, acic2cexpr s) in
 367              Binder (Some id,binder,decl,acic2cexpr t))
 368     | C.ACast (id,v,t) -> acic2cexpr v
 369     | C.ALambda (id,n,s,t) ->
 370         let name =
 371           (match n with
 372              Cic.Anonymous -> "_"
 373            | Cic.Name name -> name) in
 374         let decl = (name, acic2cexpr s) in
 375         Binder (Some id,"Lambda",decl,acic2cexpr t)
 376     | C.ALetIn (id,n,s,t) ->
 377         (match n with
 378            Cic.Anonymous -> assert false
 379          | Cic.Name name ->
 380              let def = (name, acic2cexpr s) in
 381              Letin (Some id,def,acic2cexpr t))
 382     | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
 383         let uri_str = UriManager.string_of_uri uri in
 384         (try
 385           (let f = Hashtbl.find symbol_table uri_str in
 386            f aid sid tl acic2cexpr)
 387         with Not_found ->
 388           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
 389           make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 390     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
 391         let inductive_types =
 392           (match CicEnvironment.get_obj uri with
 393              Cic.Constant _ -> assert false
 394            | Cic.Variable _ -> assert false
 395            | Cic.CurrentProof _ -> assert false
 396            | Cic.InductiveDefinition (l,_,_) -> l
 397           ) in
 398         let (name,_,_,_) = List.nth inductive_types i in
 399         let uri_str = UriManager.string_of_uri uri in
 400         let puri_str =
 401          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
 402         (try
 403           (let f = Hashtbl.find symbol_table puri_str in
 404            f aid sid tl acic2cexpr)
 405          with Not_found ->
 406            Appl (Some aid, Symbol (Some sid, name,
 407            make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 408     | C.AAppl (id,li) ->
 409         Appl (Some id, List.map acic2cexpr li)
 410     | C.AConst (id,uri,subst) ->
 411         let uri_str = UriManager.string_of_uri uri in
 412         (try
 413           let f = Hashtbl.find symbol_table uri_str in
 414           f "dummy" id [] acic2cexpr
 415         with Not_found ->
 416           Symbol (Some id, UriManager.name_of_uri uri,
 417             make_subst subst, Some (UriManager.string_of_uri uri)))
 418     | C.AMutInd (id,uri,i,subst) ->
 419         let inductive_types =
 420           (match CicEnvironment.get_obj uri with
 421              Cic.Constant _ -> assert false
 422            | Cic.Variable _ -> assert false
 423            | Cic.CurrentProof _ -> assert false
 424            | Cic.InductiveDefinition (l,_,_) -> l
 425           ) in
 426         let (name,_,_,_) = List.nth inductive_types i in
 427         let uri_str = UriManager.string_of_uri uri in
 428         Symbol (Some id, name, make_subst subst, Some uri_str)
 429     | C.AMutConstruct (id,uri,i,j,subst) ->
 430         let constructors = get_constructors uri i in
 431         let (name,_) = List.nth constructors (j-1) in
 432         let uri_str = UriManager.string_of_uri uri in
 433         Symbol (Some id, name, make_subst subst, Some uri_str)
 434     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 435         let constructors = get_constructors uri typeno in
 436         let named_patterns =
 437           List.map2 (fun c p -> (fst c, acic2cexpr p))
 438             constructors patterns in
 439         Case (Some id, acic2cexpr te, named_patterns)
 440     | C.AFix (id, no, funs) ->
 441         let defs =
 442           List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
 443         let (name,_) = List.nth defs no in
 444         let body = LocalVar (None, name)  in
 445         Letrec (Some id, defs, body)
 446     | C.ACoFix (id,no,funs) ->
 447         let defs =
 448           List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
 449         let (name,_) = List.nth defs no in
 450         let body = LocalVar (None, name)  in
 451         Letrec (Some id, defs, body) in
 452   acic2cexpr t
 453 ;;
 454
 455
 456
 457
 458
 459
 460
 461
 462
 463
 464