(* 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 *) (* 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 ;;