From: Stefano Zacchiroli Date: Wed, 4 Feb 2004 09:44:38 +0000 (+0000) Subject: moved here CicAst and pretty printer X-Git-Tag: V_0_2_3~77 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97790db29ad0dc3d31e61acc69894aa5e6109a9e;p=helm.git moved here CicAst and pretty printer --- diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 3f0bc48d7..c1a5eeb97 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,7 +1,12 @@ +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 @@ -36,3 +41,7 @@ applyTransformation.cmo: content2pres.cmi misc.cmi mpresentation.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 diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 384a6f00e..5c60d22a8 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -1,13 +1,19 @@ 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 = diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml new file mode 100644 index 000000000..fc6d95531 --- /dev/null +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -0,0 +1,213 @@ +(* 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 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 + diff --git a/helm/ocaml/cic_transformations/acic2Ast.mli b/helm/ocaml/cic_transformations/acic2Ast.mli new file mode 100644 index 000000000..3db26629a --- /dev/null +++ b/helm/ocaml/cic_transformations/acic2Ast.mli @@ -0,0 +1,36 @@ +(* 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 + diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml new file mode 100644 index 000000000..f5aeb5d84 --- /dev/null +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -0,0 +1,116 @@ +(* 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, 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 + diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml new file mode 100644 index 000000000..b1e658876 --- /dev/null +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -0,0 +1,92 @@ +(* 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 ^ ")" + diff --git a/helm/ocaml/cic_transformations/cicAstPp.mli b/helm/ocaml/cic_transformations/cicAstPp.mli new file mode 100644 index 000000000..bc6e4c96f --- /dev/null +++ b/helm/ocaml/cic_transformations/cicAstPp.mli @@ -0,0 +1,27 @@ +(* 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 + diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml new file mode 100644 index 000000000..7950ce284 --- /dev/null +++ b/helm/ocaml/cic_transformations/contentTable.ml @@ -0,0 +1,122 @@ + +(* 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" ;; + diff --git a/helm/ocaml/cic_transformations/contentTable.mli b/helm/ocaml/cic_transformations/contentTable.mli new file mode 100644 index 000000000..bce877981 --- /dev/null +++ b/helm/ocaml/cic_transformations/contentTable.mli @@ -0,0 +1,6 @@ + +val lookup_symbol: + string -> + (Cic.id -> Cic.id -> Cic.annterm list -> (Cic.annterm -> CicAst.term) -> + CicAst.term) +