X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;fp=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=b78d1380a603395b6c6d22a00e086375a28acf94;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
deleted file mode 100644
index b78d1380a..000000000
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ /dev/null
@@ -1,388 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(**************************************************************************)
-(*                                                                        *)
-(*                           PROJECT HELM                                 *)
-(*                                                                        *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             27/6/2003                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-(* the type cexpr is inspired by OpenMath. A few primitive constructors
-   have been added, in order to take into account some special features
-   of functional expressions. Most notably: case, let in, let rec, and 
-   explicit substitutons *)
-
-type cexpr =
-    Symbol of string option * string * subst option * string option
-                             (* h:xref, name, subst, definitionURL *)
-  | LocalVar of (string option) * string        (* h:xref, name *)
-  | Meta of string option * string            (* h:xref, name *)
-  | Num of string option * string             (* h:xref, value *)
-  | Appl of string option * cexpr list        (* h:xref, args *)
-  | Binder of string option * string * decl * cexpr   
-                                       (* h:xref, name, decl, body *)
-  | Letin of string option * def * cexpr          (* h:xref, def, body *)
-  | Letrec of string option * def list * cexpr    (* h:xref, def list, body *)
-  | Case of string option * cexpr * ((string * cexpr) list)
-	                       (* h:xref, case_expr, named-pattern list *)
-
-and 
-  decl = string * cexpr               (* name, type *)
-and
-  def = string * cexpr               (* name, body *)
-and
-  subst = (UriManager.uri * cexpr) list
-;;
-
-(* NOTATION *)
-
-let symbol_table = Hashtbl.create 503;;
-
-(* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "eq",
-          None, Some "cic:/Coq/Init/Logic/eq.ind"))
-     :: List.map acic2cexpr (List.tl args)));;   
-
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "eq",
-          None, Some "cic:/Coq/Init/Logic/eqT.ind"))
-     :: List.map acic2cexpr (List.tl args)));;
-
-(* and *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "and",
-          None, Some "cic:/Coq/Init/Logic/and.ind"))
-     :: List.map acic2cexpr args));;
-
-(* or *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "or",
-          None, Some "cic:/Coq/Init/Logic/or.ind"))
-     :: List.map acic2cexpr args));;
-
-(* iff *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "iff",
-          None, Some "cic:/Coq/Init/Logic/iff.con"))
-     :: List.map acic2cexpr args));;
-
-(* not *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "not",
-          None, Some "cic:/Coq/Init/Logic/not.con"))
-     :: List.map acic2cexpr args));;
-
-(* exists *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   match (List.tl args) with
-     [Cic.ALambda (_,Cic.Name n,s,t)] ->
-       Binder 
-        (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
-  | _ -> raise Not_found);;
-
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   match (List.tl args) with
-     [Cic.ALambda (_,Cic.Name n,s,t)] ->
-       Binder 
-        (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
-  | _ -> raise Not_found);;
-
-(* leq *) 
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" 
-  (fun aid sid args acic2cexpr ->
-   Appl
-    (Some aid, (Symbol (Some sid, "leq",
-          None, Some "cic:/Coq/Init/Peano/le.ind"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "leq",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
-     :: List.map acic2cexpr args));;
-
-(* lt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "lt",
-          None, Some "cic:/Coq/Init/Peano/lt.con"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "lt",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
-     :: List.map acic2cexpr args));;
-
-(* geq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "geq",
-          None, Some "cic:/Coq/Init/Peano/ge.con"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "geq",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
-     :: List.map acic2cexpr args));;
-
-(* gt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "gt",
-          None, Some "cic:/Coq/Init/Peano/gt.con"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "gt",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
-     :: List.map acic2cexpr args));;
-
-(* plus *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "plus",
-          None, Some "cic:/Coq/Init/Peano/plus.con"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "plus",
-          None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
-     :: List.map acic2cexpr args));;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "plus",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
-     :: List.map acic2cexpr args));;
-
-(* times *) 
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "times",
-          None, Some "cic:/Coq/Init/Peano/mult.con"))
-     :: List.map acic2cexpr args));;
-
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "times",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
-     :: List.map acic2cexpr args));;
-(* minus *)
-Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" 
-  (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "minus",
-          None, Some "cic:/Coq/Arith/Minus/mult.con"))
-     :: List.map acic2cexpr args));;
-
-
-
-
-(* END NOTATION *)
-
- 
-let string_of_sort =
-  function 
-    Cic.Prop -> "Prop"
-  | Cic.Set  -> "Set"
-  | Cic.Type -> "Type"
-;;
-
-let get_constructors uri i =
-  let inductive_types =
-    (match CicEnvironment.get_obj uri with
-         Cic.Constant _ -> assert false
-     | Cic.Variable _ -> assert false
-     | Cic.CurrentProof _ -> assert false
-     | Cic.InductiveDefinition (l,_,_) -> l 
-    ) in
-   let (_,_,_,constructors) = List.nth inductive_types i in
-   constructors
-;;
-
-exception NotImplemented;;
-
-let acic2cexpr ids_to_inner_sorts t =
-  let rec acic2cexpr t =
-    let module C = Cic in
-    let module X = Xml in
-    let module U = UriManager in
-    let module C2A = Cic2acic in
-    let make_subst = 
-      function 
-          [] -> None
-        | l -> Some (List.map (function (uri,t) -> (uri, acic2cexpr t)) l) in
-    match t with 
-      C.ARel (id,idref,n,b) -> LocalVar (Some id,b)
-    | C.AVar (id,uri,subst) ->
-        Symbol (Some id, UriManager.name_of_uri uri, 
-          make_subst subst, Some (UriManager.string_of_uri uri))
-    | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
-    | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
-    | C.AImplicit _ -> raise NotImplemented
-    | C.AProd (id,n,s,t) ->
-        (match n with
-           Cic.Anonymous ->
-             Appl (Some id, [Symbol (None, "arrow",None,None); 
-               acic2cexpr s; acic2cexpr t])
-         | Cic.Name name -> 
-             let sort = 
-               (try Hashtbl.find ids_to_inner_sorts id 
-                with Not_found -> 
-                   (* if the Prod does not have the sort, it means
-                      that it has been generated by cic2content, and
-                      thus is a statement *)
-                  "Prop") in
-             let binder = if sort = "Prop" then "Forall" else "Prod" in
-             let decl = (name, acic2cexpr s) in 
-             Binder (Some id,binder,decl,acic2cexpr t)) 
-    | C.ACast (id,v,t) -> acic2cexpr v
-    | C.ALambda (id,n,s,t) ->
-        let name =
-          (match n with
-             Cic.Anonymous -> "_"
-           | Cic.Name name -> name) in
-        let decl = (name, acic2cexpr s) in 
-        Binder (Some id,"Lambda",decl,acic2cexpr t)
-    | C.ALetIn (id,n,s,t) ->
-        (match n with
-           Cic.Anonymous -> assert false
-         | Cic.Name name ->
-             let def = (name, acic2cexpr s) in
-             Letin (Some id,def,acic2cexpr t))
-    | C.AAppl (aid,C.AConst (sid,uri,subst)::tl) ->
-        let uri_str = UriManager.string_of_uri uri in
-        (try 
-          (let f = Hashtbl.find symbol_table uri_str in
-           f aid sid tl acic2cexpr)
-        with notfound ->
-          Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri, 
-          make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
-    | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
-        let inductive_types = 
-          (match CicEnvironment.get_obj uri with
-             Cic.Constant _ -> assert false
-           | Cic.Variable _ -> assert false
-           | Cic.CurrentProof _ -> assert false
-           | Cic.InductiveDefinition (l,_,_) -> l 
-          ) in
-        let (name,_,_,_) = List.nth inductive_types i in
-        let uri_str = UriManager.string_of_uri uri in
-        let puri_str =
-         uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
-        (try 
-          (let f = Hashtbl.find symbol_table puri_str in
-           f aid sid tl acic2cexpr)
-         with notfound ->
-           Appl (Some aid, Symbol (Some sid, name, 
-           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
-    | C.AAppl (id,li) ->
-        Appl (Some id, List.map acic2cexpr li)
-    | C.AConst (id,uri,subst) ->
-        Symbol (Some id, UriManager.name_of_uri uri, 
-          make_subst subst, Some (UriManager.string_of_uri uri))
-    | C.AMutInd (id,uri,i,subst) ->
-        let inductive_types = 
-          (match CicEnvironment.get_obj uri with
-             Cic.Constant _ -> assert false
-           | Cic.Variable _ -> assert false
-           | Cic.CurrentProof _ -> assert false
-           | Cic.InductiveDefinition (l,_,_) -> l 
-          ) in
-        let (name,_,_,_) = List.nth inductive_types i in
-        let uri_str = UriManager.string_of_uri uri in
-        Symbol (Some id, name, make_subst subst, Some uri_str)
-    | C.AMutConstruct (id,uri,i,j,subst) ->
-        let constructors = get_constructors uri i in
-        let (name,_) = List.nth constructors (j-1) in
-        let uri_str = UriManager.string_of_uri uri in
-        Symbol (Some id, name, make_subst subst, Some uri_str)
-    | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
-        let constructors = get_constructors uri typeno in
-        let named_patterns =
-          List.map2 (fun c p -> (fst c, acic2cexpr p)) 
-            constructors patterns in
-        Case (Some id, acic2cexpr te, named_patterns)
-    | C.AFix (id, no, funs) -> 
-        let defs = 
-          List.map (function (id1,n,_,_,bo) -> (n, acic2cexpr bo)) funs in
-        let (name,_) = List.nth defs no in
-        let body = LocalVar (None, name)  in
-        Letrec (Some id, defs, body)
-    | C.ACoFix (id,no,funs) -> 
-        let defs = 
-          List.map (function (id1,n,_,bo) -> (n, acic2cexpr bo)) funs in
-        let (name,_) = List.nth defs no in
-        let body = LocalVar (None, name)  in
-        Letrec (Some id, defs, body) in
-  acic2cexpr t
-;;
-
-
-
-
-
-
-
-
-
-
-