aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/acic.ml
blob: 3e2c8ade792e7bdbf002c0e1a9224f6a5491d088 (plain)
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 *)