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 HelmLibraryObjects.Logic.eq_XURI
  71   (fun aid sid args acic2cexpr ->
  72    Appl
  73     (Some aid, (Symbol (Some sid, "eq",
  74           None, Some HelmLibraryObjects.Logic.eq_SURI))
  75      :: List.map acic2cexpr (List.tl args)));;
  76
  77 (* and *)
  78 Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI
  79   (fun aid sid args acic2cexpr ->
  80    Appl
  81     (Some aid, (Symbol (Some sid, "and",
  82           None, Some HelmLibraryObjects.Logic.and_SURI))
  83      :: List.map acic2cexpr args));;
  84
  85 (* or *)
  86 Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI
  87   (fun aid sid args acic2cexpr ->
  88    Appl
  89     (Some aid, (Symbol (Some sid, "or",
  90           None, Some HelmLibraryObjects.Logic.or_SURI))
  91      :: List.map acic2cexpr args));;
  92
  93 (* iff *)
  94 Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
  95   (fun aid sid args acic2cexpr ->
  96    Appl
  97     (Some aid, (Symbol (Some sid, "iff",
  98           None, Some HelmLibraryObjects.Logic.iff_SURI))
  99      :: List.map acic2cexpr args));;
 100
 101 (* not *)
 102 Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
 103   (fun aid sid args acic2cexpr ->
 104    Appl
 105     (Some aid, (Symbol (Some sid, "not",
 106           None, Some HelmLibraryObjects.Logic.not_SURI))
 107      :: List.map acic2cexpr args));;
 108
 109 (* Rinv *)
 110 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
 111   (fun aid sid args acic2cexpr ->
 112    Appl
 113     (Some aid, (Symbol (Some sid, "inv",
 114           None, Some HelmLibraryObjects.Reals.rinv_SURI))
 115      :: List.map acic2cexpr args));;
 116
 117 (* Ropp *)
 118 Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
 119   (fun aid sid args acic2cexpr ->
 120    Appl
 121     (Some aid, (Symbol (Some sid, "opp",
 122           None, Some HelmLibraryObjects.Reals.ropp_SURI))
 123      :: List.map acic2cexpr args));;
 124
 125 (* exists *)
 126 Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
 127   (fun aid sid args acic2cexpr ->
 128    match (List.tl args) with
 129      [Cic.ALambda (_,Cic.Name n,s,t)] ->
 130        Binder
 131         (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
 132   | _ -> raise Not_found);;
 133
 134 (* leq *)
 135 Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI
 136   (fun aid sid args acic2cexpr ->
 137    Appl
 138     (Some aid, (Symbol (Some sid, "leq",
 139           None, Some HelmLibraryObjects.Peano.le_SURI))
 140      :: List.map acic2cexpr args));;
 141
 142 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
 143   (fun aid sid args acic2cexpr ->
 144    Appl
 145     (Some aid, (Symbol (Some sid, "leq",
 146           None, Some HelmLibraryObjects.Reals.rle_SURI))
 147      :: List.map acic2cexpr args));;
 148
 149 (* lt *)
 150 Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
 151   (fun aid sid args acic2cexpr ->
 152    Appl
 153     (Some aid, (Symbol (Some sid, "lt",
 154           None, Some HelmLibraryObjects.Peano.lt_SURI))
 155      :: List.map acic2cexpr args));;
 156
 157 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
 158   (fun aid sid args acic2cexpr ->
 159    Appl
 160     (Some aid, (Symbol (Some sid, "lt",
 161           None, Some HelmLibraryObjects.Reals.rlt_SURI))
 162      :: List.map acic2cexpr args));;
 163
 164 (* geq *)
 165 Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
 166   (fun aid sid args acic2cexpr ->
 167    Appl
 168     (Some aid, (Symbol (Some sid, "geq",
 169           None, Some HelmLibraryObjects.Peano.ge_SURI))
 170      :: List.map acic2cexpr args));;
 171
 172 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
 173   (fun aid sid args acic2cexpr ->
 174    Appl
 175     (Some aid, (Symbol (Some sid, "geq",
 176           None, Some HelmLibraryObjects.Reals.rge_SURI))
 177      :: List.map acic2cexpr args));;
 178
 179 (* gt *)
 180 Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
 181   (fun aid sid args acic2cexpr ->
 182    Appl
 183     (Some aid, (Symbol (Some sid, "gt",
 184           None, Some HelmLibraryObjects.Peano.gt_SURI))
 185      :: List.map acic2cexpr args));;
 186
 187 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
 188   (fun aid sid args acic2cexpr ->
 189    Appl
 190     (Some aid, (Symbol (Some sid, "gt",
 191           None, Some HelmLibraryObjects.Reals.rgt_SURI))
 192      :: List.map acic2cexpr args));;
 193
 194 (* plus *)
 195 Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
 196   (fun aid sid args acic2cexpr ->
 197    Appl
 198     (Some aid, (Symbol (Some sid, "plus",
 199           None, Some HelmLibraryObjects.Peano.plus_SURI))
 200      :: List.map acic2cexpr args));;
 201
 202 Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
 203   (fun aid sid args acic2cexpr ->
 204    Appl
 205     (Some aid, (Symbol (Some sid, "plus",
 206           None, Some HelmLibraryObjects.BinInt.zplus_SURI))
 207      :: List.map acic2cexpr args));;
 208
 209 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
 210   (fun aid sid args acic2cexpr ->
 211    let appl () =
 212      Appl
 213       (Some aid, (Symbol (Some sid, "plus",
 214             None, Some HelmLibraryObjects.Reals.rplus_SURI))
 215        :: List.map acic2cexpr args)
 216    in
 217     let rec aux acc = function
 218       | [ Cic.AConst (nid, uri, []); n] when
 219           UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
 220             (match n with
 221             | Cic.AConst (_, uri, []) when
 222                UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
 223                 Num (Some aid, string_of_int (acc + 2))
 224             | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
 225                 UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
 226                   aux (acc + 1) args
 227             | _ -> appl ())
 228       | _ -> appl ()
 229     in
 230     aux 0 args)
 231 ;;
 232
 233 (* zero and one *)
 234
 235 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
 236   (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
 237
 238 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
 239   (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
 240
 241 (* times *)
 242 Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
 243   (fun aid sid args acic2cexpr ->
 244    Appl
 245     (Some aid, (Symbol (Some sid, "times",
 246           None, Some HelmLibraryObjects.Peano.mult_SURI))
 247      :: List.map acic2cexpr args));;
 248
 249
 250 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
 251   (fun aid sid args acic2cexpr ->
 252    Appl
 253     (Some aid, (Symbol (Some sid, "times",
 254           None, Some HelmLibraryObjects.Reals.rmult_SURI))
 255      :: List.map acic2cexpr args));;
 256 (* minus *)
 257 Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
 258   (fun aid sid args acic2cexpr ->
 259    Appl
 260     (Some aid, (Symbol (Some sid, "minus",
 261           None, Some HelmLibraryObjects.Peano.minus_SURI))
 262      :: List.map acic2cexpr args));;
 263
 264 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
 265   (fun aid sid args acic2cexpr ->
 266    Appl
 267     (Some aid, (Symbol (Some sid, "minus",
 268           None, Some HelmLibraryObjects.Reals.rminus_SURI))
 269      :: List.map acic2cexpr args));;
 270
 271 (* div *)
 272 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
 273   (fun aid sid args acic2cexpr ->
 274    Appl
 275     (Some aid, (Symbol (Some sid, "div",
 276           None, Some HelmLibraryObjects.Reals.rdiv_SURI))
 277      :: List.map acic2cexpr args));;
 278
 279
 280
 281
 282 (* END NOTATION *)
 283
 284
 285 let string_of_sort =
 286   function
 287     Cic.Prop  -> "Prop"
 288   | Cic.Set   -> "Set"
 289   | Cic.Type _ -> "Type" (* TASSI *)
 290   | Cic.CProp -> "Type"
 291 ;;
 292
 293 let get_constructors uri i =
 294   let inductive_types =
 295     (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 296        match o with
 297            Cic.Constant _ -> assert false
 298          | Cic.Variable _ -> assert false
 299          | Cic.CurrentProof _ -> assert false
 300          | Cic.InductiveDefinition (l,_,_) -> l
 301     ) in
 302    let (_,_,_,constructors) = List.nth inductive_types i in
 303    constructors
 304 ;;
 305
 306 exception NotImplemented;;
 307
 308 let acic2cexpr ids_to_inner_sorts t =
 309   let rec acic2cexpr t =
 310     let module C = Cic in
 311     let module X = Xml in
 312     let module U = UriManager in
 313     let module C2A = Cic2acic in
 314     let make_subst =
 315       function
 316           [] -> None
 317         | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
 318     match t with
 319       C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
 320     | C.AVar (id,uri,subst) ->
 321         Symbol (Some id, UriManager.name_of_uri uri,
 322           make_subst subst, Some (UriManager.string_of_uri uri))
 323     | C.AMeta (id,n,l) ->
 324        let l' =
 325         List.rev_map
 326          (function
 327              None -> None
 328            | Some t -> Some (acic2cexpr t)
 329          ) l
 330        in
 331         Meta (Some id,("?" ^ (string_of_int n)),l')
 332     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
 333     | C.AImplicit _ -> raise NotImplemented
 334     | C.AProd (id,n,s,t) ->
 335         (match n with
 336            Cic.Anonymous ->
 337              Appl (Some id, [Symbol (None, "arrow",None,None);
 338                acic2cexpr s; acic2cexpr t])
 339          | Cic.Name name ->
 340              let sort =
 341                (try Hashtbl.find ids_to_inner_sorts id
 342                 with Not_found ->
 343                    (* if the Prod does not have the sort, it means
 344                       that it has been generated by cic2content, and
 345                       thus is a statement *)
 346                   "Prop") in
 347              let binder = if sort = "Prop" then "Forall" else "Prod" in
 348              let decl = (name, acic2cexpr s) in
 349              Binder (Some id,binder,decl,acic2cexpr t))
 350     | C.ACast (id,v,t) -> acic2cexpr v
 351     | C.ALambda (id,n,s,t) ->
 352         let name =
 353           (match n with
 354              Cic.Anonymous -> "_"
 355            | Cic.Name name -> name) in
 356         let decl = (name, acic2cexpr s) in
 357         Binder (Some id,"Lambda",decl,acic2cexpr t)
 358     | C.ALetIn (id,n,s,t) ->
 359         (match n with
 360            Cic.Anonymous -> assert false
 361          | Cic.Name name ->
 362              let def = (name, acic2cexpr s) in
 363              Letin (Some id,def,acic2cexpr t))
 364     | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
 365         let uri_str = UriManager.string_of_uri uri in
 366         (try
 367           (let f = Hashtbl.find symbol_table uri_str in
 368            f aid sid tl acic2cexpr)
 369         with Not_found ->
 370           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
 371           make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 372     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
 373         let inductive_types =
 374           (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 375             match o with
 376              Cic.Constant _ -> assert false
 377            | Cic.Variable _ -> assert false
 378            | Cic.CurrentProof _ -> assert false
 379            | Cic.InductiveDefinition (l,_,_) -> l
 380           ) in
 381         let (name,_,_,_) = List.nth inductive_types i in
 382         let uri_str = UriManager.string_of_uri uri in
 383         let puri_str =
 384          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
 385         (try
 386           (let f = Hashtbl.find symbol_table puri_str in
 387            f aid sid tl acic2cexpr)
 388          with Not_found ->
 389            Appl (Some aid, Symbol (Some sid, name,
 390            make_subst subst, Some uri_str)::List.map acic2cexpr tl))
 391     | C.AAppl (id,li) ->
 392         Appl (Some id, List.map acic2cexpr li)
 393     | C.AConst (id,uri,subst) ->
 394         let uri_str = UriManager.string_of_uri uri in
 395         (try
 396           let f = Hashtbl.find symbol_table uri_str in
 397           f "dummy" id [] acic2cexpr
 398         with Not_found ->
 399           Symbol (Some id, UriManager.name_of_uri uri,
 400             make_subst subst, Some (UriManager.string_of_uri uri)))
 401     | C.AMutInd (id,uri,i,subst) ->
 402         let inductive_types =
 403           (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 404             match o with
 405              Cic.Constant _ -> assert false
 406            | Cic.Variable _ -> assert false
 407            | Cic.CurrentProof _ -> assert false
 408            | Cic.InductiveDefinition (l,_,_) -> l
 409           ) in
 410         let (name,_,_,_) = List.nth inductive_types i in
 411         let uri_str = UriManager.string_of_uri uri in
 412         Symbol (Some id, name, make_subst subst, Some uri_str)
 413     | C.AMutConstruct (id,uri,i,j,subst) ->
 414         let constructors = get_constructors uri i in
 415         let (name,_) = List.nth constructors (j-1) in
 416         let uri_str = UriManager.string_of_uri uri in
 417         Symbol (Some id, name, make_subst subst, Some uri_str)
 418     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 419         let constructors = get_constructors uri typeno in
 420         let named_patterns =
 421           List.map2 (fun c p -> (fst c, acic2cexpr p))
 422             constructors patterns in
 423         Case (Some id, acic2cexpr te, named_patterns)
 424     | C.AFix (id, no, funs) ->
 425         let defs =
 426           List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
 427         let (name,_) = List.nth defs no in
 428         let body = LocalVar (None, name)  in
 429         Letrec (Some id, defs, body)
 430     | C.ACoFix (id,no,funs) ->
 431         let defs =
 432           List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
 433         let (name,_) = List.nth defs no in
 434         let body = LocalVar (None, name)  in
 435         Letrec (Some id, defs, body) in
 436   acic2cexpr t
 437 ;;
 438
 439
 440
 441
 442
 443
 444
 445
 446
 447
 448