+++ /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 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
-;;
-
-
-
-
-
-
-
-
-
-
-
projects / helm.git / blobdiff