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
 239
 240
 241 (* END NOTATION *)
 242
 243
 244 let string_of_sort =
 245   function
 246     Cic.Prop -> "Prop"
 247   | Cic.Set  -> "Set"
 248   | Cic.Type -> "Type"
 249 ;;
 250
 251 let get_constructors uri i =
 252   let inductive_types =
 253     (match CicEnvironment.get_obj uri with
 254          Cic.Constant _ -> assert false
 255      | Cic.Variable _ -> assert false
 256      | Cic.CurrentProof _ -> assert false
 257      | Cic.InductiveDefinition (l,_,_) -> l
 258     ) in
 259    let (_,_,_,constructors) = List.nth inductive_types i in
 260    constructors
 261 ;;
 262
 263 exception NotImplemented;;
 264
 265 let acic2cexpr ids_to_inner_sorts t =
 266   let rec acic2cexpr t =
 267     let module C = Cic in
 268     let module X = Xml in
 269     let module U = UriManager in
 270     let module C2A = Cic2acic in
 271     let make_subst =
 272       function
 273           [] -> None
 274         | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
 275     match t with
 276       C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
 277     | C.AVar (id,uri,subst) ->
 278         Symbol (Some id, UriManager.name_of_uri uri,
 279           make_subst subst, Some (UriManager.string_of_uri uri))
 280     | C.AMeta (id,n,l) ->
 281        let l' =
 282         List.rev_map
 283          (function
 284              None -> None
 285            | Some t -> Some (acic2cexpr t)
 286          ) l
 287        in
 288         Meta (Some id,("?" ^ (string_of_int n)),l')
 289     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
 290     | C.AImplicit _ -> raise NotImplemented
 291     | C.AProd (id,n,s,t) ->
 292         (match n with
 293            Cic.Anonymous ->
 294              Appl (Some id, [Symbol (None, "arrow",None,None);
 295                acic2cexpr s; acic2cexpr t])
 296          | Cic.Name name ->
 297              let sort =
 298                (try Hashtbl.find ids_to_inner_sorts id
 299                 with Not_found ->
 300                    (* if the Prod does not have the sort, it means
 301                       that it has been generated by cic2content, and
 302                       thus is a statement *)
 303                   "Prop") in
 304              let binder = if sort = "Prop" then "Forall" else "Prod" in
 305              let decl = (name, acic2cexpr s) in
 306              Binder (Some id,binder,decl,acic2cexpr t))
 307     | C.ACast (id,v,t) -> acic2cexpr v
 308     | C.ALambda (id,n,s,t) ->
 309         let name =
 310           (match n with
 311              Cic.Anonymous -> "_"
 312            | Cic.Name name -> name) in
 313         let decl = (name, acic2cexpr s) in
 314         Binder (Some id,"Lambda",decl,acic2cexpr t)
 315     | C.ALetIn (id,n,s,t) ->
 316         (match n with
 317            Cic.Anonymous -> assert false
 318          | Cic.Name name ->
 319              let def = (name, acic2cexpr s) in
 320              Letin (Some id,def,acic2cexpr t))
 321     | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
 322         let uri_str = UriManager.string_of_uri uri in
 323         (try
 324           (let f = Hashtbl.find symbol_table uri_str in
 325            f aid sid tl acic2cexpr)
 326         with notfound ->
 327           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
 328           make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 329     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
 330         let inductive_types =
 331           (match CicEnvironment.get_obj uri with
 332              Cic.Constant _ -> assert false
 333            | Cic.Variable _ -> assert false
 334            | Cic.CurrentProof _ -> assert false
 335            | Cic.InductiveDefinition (l,_,_) -> l
 336           ) in
 337         let (name,_,_,_) = List.nth inductive_types i in
 338         let uri_str = UriManager.string_of_uri uri in
 339         let puri_str =
 340          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
 341         (try
 342           (let f = Hashtbl.find symbol_table puri_str in
 343            f aid sid tl acic2cexpr)
 344          with notfound ->
 345            Appl (Some aid, Symbol (Some sid, name,
 346            make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 347     | C.AAppl (id,li) ->
 348         Appl (Some id, List.map acic2cexpr li)
 349     | C.AConst (id,uri,subst) ->
 350         Symbol (Some id, UriManager.name_of_uri uri,
 351           make_subst subst, Some (UriManager.string_of_uri uri))
 352     | C.AMutInd (id,uri,i,subst) ->
 353         let inductive_types =
 354           (match CicEnvironment.get_obj uri with
 355              Cic.Constant _ -> assert false
 356            | Cic.Variable _ -> assert false
 357            | Cic.CurrentProof _ -> assert false
 358            | Cic.InductiveDefinition (l,_,_) -> l
 359           ) in
 360         let (name,_,_,_) = List.nth inductive_types i in
 361         let uri_str = UriManager.string_of_uri uri in
 362         Symbol (Some id, name, make_subst subst, Some uri_str)
 363     | C.AMutConstruct (id,uri,i,j,subst) ->
 364         let constructors = get_constructors uri i in
 365         let (name,_) = List.nth constructors (j-1) in
 366         let uri_str = UriManager.string_of_uri uri in
 367         Symbol (Some id, name, make_subst subst, Some uri_str)
 368     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 369         let constructors = get_constructors uri typeno in
 370         let named_patterns =
 371           List.map2 (fun c p -> (fst c, acic2cexpr p))
 372             constructors patterns in
 373         Case (Some id, acic2cexpr te, named_patterns)
 374     | C.AFix (id, no, funs) ->
 375         let defs =
 376           List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
 377         let (name,_) = List.nth defs no in
 378         let body = LocalVar (None, name)  in
 379         Letrec (Some id, defs, body)
 380     | C.ACoFix (id,no,funs) ->
 381         let defs =
 382           List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
 383         let (name,_) = List.nth defs no in
 384         let body = LocalVar (None, name)  in
 385         Letrec (Some id, defs, body) in
 386   acic2cexpr t
 387 ;;
 388
 389
 390
 391
 392
 393
 394
 395
 396
 397
 398