diff options
author | 2002-11-05 16:59:25 +0000 | |
---|---|---|
committer | 2002-11-05 16:59:25 +0000 | |
commit | 9f2ec7fc9f1ed08be8bc5a09d352951073a69633 (patch) | |
tree | c5f06d5b112ed9731f71c98910d6f69852b3de5b /contrib/xml/acic.ml | |
parent | 1f95f087d79d6c2c79012921ce68553caf20b090 (diff) |
Intégration de la branche mowgli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/acic.ml')
-rw-r--r-- | contrib/xml/acic.ml | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml new file mode 100644 index 000000000..693b7cb3c --- /dev/null +++ b/contrib/xml/acic.ml @@ -0,0 +1,94 @@ +open Names +open Term + +(* Maps fron \em{unshared} [constr] to ['a]. *) +module CicHash = + Hashtbl.Make + (struct + type t = Term.constr + let equal = (==) + let hash = Hashtbl.hash + end) +;; + +type id = string (* the type of the (annotated) node identifiers *) +type uri = string + +type 'constr context_entry = + Decl of 'constr (* Declaration *) + | Def of 'constr * 'constr (* Definition; the second argument (the type) *) + (* is not present in the DTD, but is needed *) + (* to use Coq functions during exportation. *) + +type 'constr hypothesis = identifier * 'constr context_entry +type context = constr hypothesis list + +type conjecture = int * context * constr +type metasenv = conjecture list + +(* list of couples section path -- variables defined in that section *) +type params = (string * uri list) list + +type obj = + Constant of string * (* id, *) + constr option * constr * (* value, type, *) + params (* parameters *) + | Variable of + string * constr option * constr * (* name, body, type *) + params (* parameters *) + | CurrentProof of + string * metasenv * (* name, conjectures, *) + constr * constr (* value, type *) + | InductiveDefinition of + inductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and inductiveType = + identifier * bool * constr * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + identifier * constr (* id, type *) + +type aconstr = + | ARel of id * int * id * identifier + | AVar of id * uri + | AEvar of id * int * aconstr list + | ASort of id * sorts + | ACast of id * aconstr * aconstr + | AProds of (id * name * aconstr) list * aconstr + | ALambdas of (id * name * aconstr) list * aconstr + | ALetIns of (id * name * aconstr) list * aconstr + | AApp of id * aconstr list + | AConst of id * explicit_named_substitution * uri + | AInd of id * explicit_named_substitution * uri * int + | AConstruct of id * explicit_named_substitution * uri * int * int + | ACase of id * uri * int * aconstr * aconstr * aconstr list + | AFix of id * int * ainductivefun list + | ACoFix of id * int * acoinductivefun list +and ainductivefun = + id * identifier * int * aconstr * aconstr +and acoinductivefun = + id * identifier * aconstr * aconstr +and explicit_named_substitution = id option * (uri * aconstr) list + +type acontext = (id * aconstr hypothesis) list +type aconjecture = id * int * acontext * aconstr +type ametasenv = aconjecture list + +type aobj = + AConstant of id * string * (* id, *) + aconstr option * aconstr * (* value, type, *) + params (* parameters *) + | AVariable of id * + string * aconstr option * aconstr * (* name, body, type *) + params (* parameters *) + | ACurrentProof of id * + string * ametasenv * (* name, conjectures, *) + aconstr * aconstr (* value, type *) + | AInductiveDefinition of id * + anninductiveType list * (* inductive types , *) + params * int (* parameters,n ind. pars*) +and anninductiveType = + id * identifier * bool * aconstr * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + identifier * aconstr (* id, type *) |