+contentTable.cmi: cicAst.cmo
cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi
content2pres.cmi: mpresentation.cmi
sequent2pres.cmi: mpresentation.cmi
cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi
+acic2Ast.cmi: cicAst.cmo
+cicAstPp.cmi: cicAst.cmo
+contentTable.cmo: cicAst.cmo contentTable.cmi
+contentTable.cmx: cicAst.cmx contentTable.cmi
cic2Xml.cmo: cic2Xml.cmi
cic2Xml.cmx: cic2Xml.cmi
content_expressions.cmo: content_expressions.cmi
sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi
applyTransformation.cmx: content2pres.cmx misc.cmx mpresentation.cmx \
sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi
+acic2Ast.cmo: cicAst.cmo acic2Ast.cmi
+acic2Ast.cmx: cicAst.cmx acic2Ast.cmi
+cicAstPp.cmo: cicAst.cmo cicAstPp.cmi
+cicAstPp.cmx: cicAst.cmx cicAstPp.cmi
PACKAGE = cic_transformations
-REQUIRES = helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt
+REQUIRES = \
+ helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt
PREDICATES =
-INTERFACE_FILES = cic2Xml.mli content_expressions.mli \
- mpresentation.mli cexpr2pres.mli content2pres.mli \
- sequent2pres.mli \
- cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \
- applyStylesheets.mli applyTransformation.mli
-IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+# modules which have both a .ml and a .mli
+INTERFACE_FILES = \
+ contentTable.mli \
+ cic2Xml.mli content_expressions.mli \
+ mpresentation.mli cexpr2pres.mli content2pres.mli \
+ sequent2pres.mli \
+ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \
+ applyStylesheets.mli applyTransformation.mli \
+ acic2Ast.mli cicAstPp.mli
+IMPLEMENTATION_FILES = \
+ cicAst.ml $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
--- /dev/null
+(* Copyright (C) 2004, 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://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+let symbol_table = Hashtbl.create 1024
+
+let sort_of_string = function
+ | "Prop" -> `Prop
+ | "Set" -> `Set
+ | "Type" -> `Type
+ | "CProp" -> `CProp
+ | _ -> assert false
+
+let get_types uri =
+ match CicEnvironment.get_obj uri with
+ | Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
+
+let name_of_inductive_type uri i =
+ let types = get_types uri in
+ let (name, _, _, _) = try List.nth types i with Not_found -> assert false in
+ name
+
+ (* returns <name, type> pairs *)
+let constructors_of_inductive_type uri i =
+ let types = get_types uri in
+ let (_, _, _, constructors) =
+ try List.nth types i with Not_found -> assert false
+ in
+ constructors
+
+ (* returns name only *)
+let constructor_of_inductive_type uri i j =
+ (try
+ fst (List.nth (constructors_of_inductive_type uri i) (j-1))
+ with Not_found -> assert false)
+
+let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
+ let register_uri id uri = Hashtbl.add ids_to_uris id uri in
+ let sort_of_id id =
+ try
+ sort_of_string (Hashtbl.find ids_to_inner_sorts id)
+ with Not_found -> assert false
+ in
+ let module Ast = CicAst in
+ let idref id t = Ast.AttributedTerm (`IdRef id, t) in
+ let rec aux = function
+ | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+ | Cic.AVar (id,uri,subst) ->
+ register_uri id (UriManager.string_of_uri uri);
+ idref id
+ (Ast.Ident (UriManager.name_of_uri uri, astsubst_of_cicsubst subst))
+ | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
+ | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
+ | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
+ | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type)
+ | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
+ | Cic.AImplicit _ -> assert false
+ | Cic.AProd (id,n,s,t) ->
+ let binder_kind =
+ match sort_of_id id with
+ | `Set | `Type -> `Pi
+ | `Prop | `CProp -> `Forall
+ in
+ idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
+ | Cic.ACast (id,v,t) -> idref id (aux v)
+ | Cic.ALambda (id,n,s,t) ->
+ idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
+ | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))
+ | Cic.AAppl (aid,Cic.AConst (sid,uri,subst)::tl) ->
+ let uri_str = UriManager.string_of_uri uri in
+ register_uri sid uri_str;
+ (try
+ let f = Hashtbl.find symbol_table uri_str in
+ f aid sid tl aux
+ with Not_found ->
+ idref aid
+ (Ast.Appl (idref sid
+ (Ast.Ident (UriManager.name_of_uri uri,
+ astsubst_of_cicsubst subst)) :: (List.map aux tl))))
+ | Cic.AAppl (aid,Cic.AMutInd (sid,uri,i,subst)::tl) ->
+ let name = name_of_inductive_type uri i in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str =
+ uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
+ register_uri sid puri_str;
+ (try
+ (let f = Hashtbl.find symbol_table puri_str in
+ f aid sid tl aux)
+ with Not_found ->
+ idref aid
+ (Ast.Appl (idref sid
+ (Ast.Ident (name,
+ astsubst_of_cicsubst subst)) :: (List.map aux tl))))
+ | Cic.AAppl (id,li) -> idref id (Ast.Appl (List.map aux li))
+ | Cic.AConst (id,uri,subst) ->
+ let uri_str = UriManager.string_of_uri uri in
+ register_uri id uri_str;
+ (try
+ let f = Hashtbl.find symbol_table uri_str in
+ f "dummy" id [] aux
+ with Not_found ->
+ idref id
+ (Ast.Ident
+ (UriManager.name_of_uri uri, astsubst_of_cicsubst subst)))
+ | Cic.AMutInd (id,uri,i,subst) ->
+ let name = name_of_inductive_type uri i in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str =
+ uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
+ register_uri id puri_str;
+ (try
+ let f = Hashtbl.find symbol_table puri_str in
+ f "dummy" id [] aux
+ with Not_found ->
+ idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
+ | Cic.AMutConstruct (id,uri,i,j,subst) ->
+ let name = constructor_of_inductive_type uri i j in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
+ register_uri id puri_str;
+ (try
+ let f = Hashtbl.find symbol_table puri_str in
+ f "dummy" id [] aux
+ with Not_found ->
+ idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
+ | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
+ let name = name_of_inductive_type uri typeno in
+ let constructors = constructors_of_inductive_type uri typeno in
+ let rec eat_branch ty pat =
+ match (ty, pat) with
+ | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
+ let (cv, rhs) = eat_branch t t' in
+ (name, Some (aux s)) :: cv, rhs
+ | _, _ -> [], aux pat
+ in
+ let patterns =
+ List.map2
+ (fun (name, ty) pat ->
+ let (capture_variables, rhs) = eat_branch ty pat in
+ ((name, capture_variables), rhs))
+ constructors patterns
+ in
+ idref id (Ast.Case (aux te, name, Some (aux ty), patterns))
+ | Cic.AFix (id, no, funs) ->
+ let defs =
+ List.map
+ (fun (_, n, decr_idx, ty, bo) ->
+ ((Cic.Name n, Some (aux ty)), aux bo, decr_idx))
+ funs
+ in
+ let name =
+ try
+ (match List.nth defs no with
+ | (Cic.Name n, _), _, _ -> n
+ | _ -> assert false)
+ with Not_found -> assert false
+ in
+ idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+ | Cic.ACoFix (id, no, funs) ->
+ let defs =
+ List.map
+ (fun (_, n, ty, bo) -> ((Cic.Name n, Some (aux ty)), aux bo, 0))
+ funs
+ in
+ let name =
+ try
+ (match List.nth defs no with
+ | (Cic.Name n, _), _, _ -> n
+ | _ -> assert false)
+ with Not_found -> assert false
+ in
+ idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+
+ and astsubst_of_cicsubst subst =
+ List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
+ subst
+
+ and astcontext_of_ciccontext context =
+ List.map
+ (function
+ | None -> None
+ | Some annterm -> Some (aux annterm))
+ context
+
+ in
+ aux acic, ids_to_uris
+
--- /dev/null
+(* Copyright (C) 2004, 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://helm.cs.unibo.it/
+ *)
+
+val ast_of_acic :
+ (Cic.id, string) Hashtbl.t -> (* id -> sort *)
+ (Cic.id, string) Hashtbl.t -> (* id -> uri *)
+(*
+ (string,
+ Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) ->
+ CicAst.term)
+ Hashtbl.t ->
+*)
+ Cic.annterm -> CicAst.term * (Cic.id, string) Hashtbl.t
+
--- /dev/null
+(* Copyright (C) 2004, 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://helm.cs.unibo.it/
+ *)
+
+ (* when an 'ident option is None, the default is to apply the tactic
+ to the current goal *)
+
+type reduction_kind = [ `Reduce | `Simpl | `Whd ]
+
+type 'term pattern =
+ | Pattern of 'term
+
+type location = int * int
+
+type ('term, 'ident) tactic =
+ | LocatedTactic of location * ('term, 'ident) tactic
+
+ | Absurd
+ | Apply of 'term
+ | Assumption
+ | Change of 'term * 'term * 'ident option (* what, with what, where *)
+ | Change_pattern of 'term pattern * 'term * 'ident option
+ (* what, with what, where *)
+ | Contradiction
+ | Cut of 'term
+ | Decompose of 'ident * 'ident list (* which hypothesis, which principles *)
+ | Discriminate of 'ident
+ | Elim of 'term * 'term option (* what to elim, which principle to use *)
+ | ElimType of 'term
+ | Exact of 'term
+ | Exists
+ | Fold of reduction_kind * 'term
+ | Fourier
+ | Injection of 'ident
+ | Intros of int option
+ | Left
+ | LetIn of 'term * 'ident (* TODO clashes with term below *)
+ | Named_intros of 'ident list
+ | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *)
+ | Reflexivity
+ | Replace of 'term * 'term (* what, with what *)
+ | Replace_pattern of 'term pattern * 'term
+ | RewriteLeft of 'term * 'ident option
+ | RewriteRight of 'term * 'ident option
+ | Right
+ | Ring
+ | Split
+ | Symmetry
+ | Transitivity of 'term
+
+type 'tactic tactical =
+ | LocatedTactical of location * 'tactic tactical
+
+ | Fail
+ | For of int * 'tactic tactical
+ | IdTac
+ | Repeat of 'tactic tactical
+ | Seq of 'tactic tactical list (* sequential composition *)
+ | Tactic of 'tactic
+ | Then of 'tactic tactical * 'tactic tactical list
+ | Tries of 'tactic tactical list
+ (* try a sequence of tacticals until one succeeds, fail otherwise *)
+ | Try of 'tactic tactical (* try a tactical and mask failures *)
+
+type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
+type induction_kind = [ `Inductive | `CoInductive ]
+type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+
+type term_attribute =
+ [ `Loc of location (* source file location *)
+ | `IdRef of string (* ACic pointer *)
+ ]
+
+type term =
+ | AttributedTerm of term_attribute * term
+
+ | Appl of term list
+ | Binder of binder_kind * capture_variable * term (* kind, name, body *)
+ | Case of term * string * term option * (case_pattern * term) list
+ (* what to match, inductive type, out type, <pattern,action> list *)
+ | LetIn of capture_variable * term * term (* name, body, where *)
+ | LetRec of induction_kind * (capture_variable * term * int) list * term
+ (* (name, body, decreasing argument) list, where *)
+ | Ident of string * subst list (* literal, substitutions *)
+ | Implicit
+ | Meta of int * meta_subst list
+ | Num of string * int (* literal, instance *)
+ | Sort of sort_kind
+ | Symbol of string * int (* canonical name, instance *)
+
+and capture_variable = Cic.name * term option (* name, type *)
+and meta_subst = term option
+and subst = string * term
+and case_pattern = string * capture_variable list
+
--- /dev/null
+(* Copyright (C) 2004, 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://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+let pp_binder = function
+ | `Lambda -> "lambda"
+ | `Pi -> "pi"
+ | `Exists -> "exists"
+ | `Forall -> "forall"
+
+let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s
+
+let rec pp_term = function
+ | CicAst.AttributedTerm (_, term) -> pp_term term
+
+ | CicAst.Appl terms ->
+ sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+ | CicAst.Binder (kind, var, body) ->
+ sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
+ (pp_term body)
+ | CicAst.Case (term, indtype, typ, patterns) ->
+ sprintf "%smatch %s with %s"
+ (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
+ (pp_term term) (pp_patterns patterns)
+ | CicAst.LetIn (var, t1, t2) ->
+ sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
+ (pp_term t2)
+ | CicAst.LetRec (kind, definitions, term) ->
+ sprintf "let %s %s in %s"
+ (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (String.concat " and "
+ (List.map
+ (fun (var, body, _) ->
+ sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
+ definitions))
+ (pp_term term)
+ | CicAst.Ident (name, []) -> name
+ | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+ | CicAst.Implicit -> "?"
+ | CicAst.Meta (index, substs) ->
+ sprintf "%d[%s]" index
+ (String.concat "; "
+ (List.map (function None -> "_" | Some term -> pp_term term) substs))
+ | CicAst.Num (num, _) -> num
+ | CicAst.Sort `Set -> "Set"
+ | CicAst.Sort `Prop -> "Prop"
+ | CicAst.Sort `Type -> "Type"
+ | CicAst.Sort `CProp -> "CProp"
+ | CicAst.Symbol (name, _) -> name
+
+and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
+and pp_substs substs = String.concat "; " (List.map pp_subst substs)
+
+and pp_pattern ((head, vars), term) =
+ sprintf "%s -> %s"
+ (match vars with
+ | [] -> head
+ | _ ->
+ sprintf "(%s %s)" head
+ (String.concat " " (List.map pp_capture_variable vars)))
+ (pp_term term)
+
+and pp_patterns patterns =
+ sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
+
+and pp_capture_variable = function
+ | name, None -> pp_name name
+ | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")"
+
--- /dev/null
+(* Copyright (C) 2004, 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://helm.cs.unibo.it/
+ *)
+
+val pp_term: CicAst.term -> string
+
--- /dev/null
+
+(* NOTATION *)
+
+let symbol_table = Hashtbl.create 503 ;;
+let lookup_symbol = Hashtbl.find symbol_table ;;
+
+let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;
+
+let add_symbol uri mnemonic =
+ Hashtbl.add symbol_table uri
+ (fun aid sid args ast_of_acic ->
+ idref aid (CicAst.Appl
+ (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args)))
+;;
+
+(* eq *)
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
+ (fun aid sid args ast_of_acic ->
+ idref aid (CicAst.Appl
+ (idref sid (CicAst.Symbol ("eq", 0)) ::
+ List.map ast_of_acic (List.tl args)))) ;;
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
+ (fun aid sid args ast_of_acic ->
+ idref aid (CicAst.Appl
+ (idref sid (CicAst.Symbol ("eq", 0)) ::
+ List.map ast_of_acic (List.tl args)))) ;;
+
+(* and *)
+add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;;
+
+(* or *)
+add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;
+
+(* iff *)
+add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;
+
+(* not *)
+add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;
+
+(* Rinv *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;
+
+(* Ropp *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;;
+
+(* exists *)
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
+ (fun aid sid args ast_of_acic ->
+ match (List.tl args) with
+ [Cic.ALambda (_,n,s,t)] ->
+ idref aid
+ (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
+ | _ -> raise Not_found);;
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
+ (fun aid sid args ast_of_acic ->
+ match (List.tl args) with
+ [Cic.ALambda (_,n,s,t)] ->
+ idref aid
+ (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
+ | _ -> raise Not_found);;
+
+(* leq *)
+add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;
+
+(* lt *)
+add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;
+
+(* geq *)
+add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;
+
+(* gt *)
+add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;
+
+(* plus *)
+add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
+add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;;
+
+let rplus_uri =
+ UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
+let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
+ (fun aid sid args ast_of_acic ->
+ let appl () =
+ idref aid (CicAst.Appl
+ (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
+ (match n with
+ | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+ idref aid (CicAst.Num (string_of_int (acc+2), 0))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
+ when UriManager.eq uri rplus_uri ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+;;
+
+(* zero and one *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
+ (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
+ (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
+
+(* times *)
+add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;;
+
+(* minus *)
+add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;
+
+(* div *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;
+
--- /dev/null
+
+val lookup_symbol:
+ string ->
+ (Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) ->
+ CicAst.term)
+
projects / helm.git / commitdiff