1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
(************************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(* *)
(* Copyright (C) 2000-2004, HELM Team. *)
(* http://helm.cs.unibo.it *)
(************************************************************************)
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 = Id.t * 'constr context_entry
type context = constr hypothesis list
type conjecture = existential_key * 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 =
Id.t * bool * constr * (* typename, inductive, arity *)
constructor list (* constructors *)
and constructor =
Id.t * constr (* id, type *)
type aconstr =
| ARel of id * int * id * Id.t
| AVar of id * uri
| AEvar of id * existential_key * 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 * Id.t * int * aconstr * aconstr
and acoinductivefun =
id * Id.t * aconstr * aconstr
and explicit_named_substitution = id option * (uri * aconstr) list
type acontext = (id * aconstr hypothesis) list
type aconjecture = id * existential_key * 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 * Id.t * bool * aconstr * (* typename, inductive, arity *)
annconstructor list (* constructors *)
and annconstructor =
Id.t * aconstr (* id, type *)
|
