--- /dev/null
+(* 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 substitutions *)
+
+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 * meta_subst (* h:xref, name, meta_subst *)
+ | 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
+and
+ meta_subst = cexpr option list
+;;
+
+(* NOTATION *)
+
+let symbol_table = Hashtbl.create 503;;
+
+(* eq *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "eq",
+ None, Some HelmLibraryObjects.Logic.eq_SURI))
+ :: List.map acic2cexpr (List.tl args)));;
+
+(* and *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "and",
+ None, Some HelmLibraryObjects.Logic.and_SURI))
+ :: List.map acic2cexpr args));;
+
+(* or *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "or",
+ None, Some HelmLibraryObjects.Logic.or_SURI))
+ :: List.map acic2cexpr args));;
+
+(* iff *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "iff",
+ None, Some HelmLibraryObjects.Logic.iff_SURI))
+ :: List.map acic2cexpr args));;
+
+(* not *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "not",
+ None, Some HelmLibraryObjects.Logic.not_SURI))
+ :: List.map acic2cexpr args));;
+
+(* Rinv *)
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "inv",
+ None, Some HelmLibraryObjects.Reals.rinv_SURI))
+ :: List.map acic2cexpr args));;
+
+(* Ropp *)
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "opp",
+ None, Some HelmLibraryObjects.Reals.ropp_SURI))
+ :: List.map acic2cexpr args));;
+
+(* exists *)
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
+ (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 HelmLibraryObjects.Peano.le_XURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "leq",
+ None, Some HelmLibraryObjects.Peano.le_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "leq",
+ None, Some HelmLibraryObjects.Reals.rle_SURI))
+ :: List.map acic2cexpr args));;
+
+(* lt *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "lt",
+ None, Some HelmLibraryObjects.Peano.lt_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "lt",
+ None, Some HelmLibraryObjects.Reals.rlt_SURI))
+ :: List.map acic2cexpr args));;
+
+(* geq *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "geq",
+ None, Some HelmLibraryObjects.Peano.ge_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "geq",
+ None, Some HelmLibraryObjects.Reals.rge_SURI))
+ :: List.map acic2cexpr args));;
+
+(* gt *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "gt",
+ None, Some HelmLibraryObjects.Peano.gt_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "gt",
+ None, Some HelmLibraryObjects.Reals.rgt_SURI))
+ :: List.map acic2cexpr args));;
+
+(* plus *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "plus",
+ None, Some HelmLibraryObjects.Peano.plus_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "plus",
+ None, Some HelmLibraryObjects.BinInt.zplus_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
+ (fun aid sid args acic2cexpr ->
+ let appl () =
+ Appl
+ (Some aid, (Symbol (Some sid, "plus",
+ None, Some HelmLibraryObjects.Reals.rplus_SURI))
+ :: List.map acic2cexpr args)
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ (match n with
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ Num (Some aid, string_of_int (acc + 2))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+;;
+
+(* zero and one *)
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
+ (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+ (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
+
+(* times *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "times",
+ None, Some HelmLibraryObjects.Peano.mult_SURI))
+ :: List.map acic2cexpr args));;
+
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "times",
+ None, Some HelmLibraryObjects.Reals.rmult_SURI))
+ :: List.map acic2cexpr args));;
+(* minus *)
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "minus",
+ None, Some HelmLibraryObjects.Peano.minus_SURI))
+ :: List.map acic2cexpr args));;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "minus",
+ None, Some HelmLibraryObjects.Reals.rminus_SURI))
+ :: List.map acic2cexpr args));;
+
+(* div *)
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "div",
+ None, Some HelmLibraryObjects.Reals.rdiv_SURI))
+ :: List.map acic2cexpr args));;
+
+
+
+
+(* END NOTATION *)
+
+
+let string_of_sort =
+ function
+ Cic.Prop -> "Prop"
+ | Cic.Set -> "Set"
+ | Cic.Type _ -> "Type" (* TASSI *)
+ | Cic.CProp -> "Type"
+;;
+
+let get_constructors uri i =
+ let inductive_types =
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o 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) ->
+ let l' =
+ List.rev_map
+ (function
+ None -> None
+ | Some t -> Some (acic2cexpr t)
+ ) l
+ in
+ Meta (Some id,("?" ^ (string_of_int n)),l')
+ | 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 Not_found ->
+ 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 =
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o 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 Not_found ->
+ 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) ->
+ let uri_str = UriManager.string_of_uri uri in
+ (try
+ let f = Hashtbl.find symbol_table uri_str in
+ f "dummy" id [] acic2cexpr
+ with Not_found ->
+ 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 =
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o 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
+;;
+
+
+
+
+
+
+
+
+
+
+
projects / helm.git / blobdiff