]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nCic.ml
select honors the substitution
[helm.git] / helm / software / components / ng_kernel / nCic.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 (********************************* TERMS ************************************)
15
16 type universe = (bool * NUri.uri) list 
17   (* Max of non-empty list of named universes, or their successor (when true) 
18    * The empty list represents type0 *)
19
20 type sort = Prop | Type of universe
21
22 type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ]
23
24 type lc_kind = Irl of int | Ctx of term list
25
26 and local_context = int * lc_kind             (* shift (0 -> no shift), 
27                                                  subst (Irl n means id of
28                                                  length n) *) 
29 and term =
30  | Rel      of int                            (* DeBruijn index, 1 based    *)
31  | Meta     of int * local_context
32  | Appl     of term list                      (* arguments                  *)
33  | Prod     of string * term * term           (* binder, source, target     *)
34  | Lambda   of string * term * term           (* binder, source, target     *)
35  | LetIn    of string * term * term * term    (* binder, type, term, body   *)
36 (* Cast \def degenerate LetIn *)
37  | Const    of NReference.reference           (* ref has (indtype|constr)no *)
38  | Sort     of sort                           (* sort                       *)
39  | Implicit of implicit_annotation            (* ...                        *)
40  | Match    of NReference.reference *         (* ind. reference,            *)
41     term * term *                             (*  outtype, ind. term        *)
42     term list                                 (*  patterns                  *)
43
44
45 (********************************* TYPING ***********************************)
46
47 type context_entry =                       (* A declaration or definition *)
48  | Decl of term                            (* type *)
49  | Def  of term * term                     (* body, type *)
50
51 type hypothesis = string * context_entry   (* name, entry *)
52
53 type context = hypothesis list
54
55 type conjecture = string option * context * term
56
57 type metasenv = (int * conjecture) list
58
59 type subst_entry = string option * context * term * term (* name,ctx,bo,ty *)
60
61 type substitution = (int * subst_entry) list
62
63
64 (******************************** OBJECTS **********************************)
65
66 type relevance = bool list (* relevance of arguments for conversion *)
67
68                     (* relevance, name, recno, ty, bo *)
69 type inductiveFun = relevance * string * int * term * term 
70   (* if coinductive, the int has no meaning and must be set to -1 *)
71
72 type constructor = relevance * string * term  (* id, type *)
73
74 type inductiveType = 
75  relevance * string * term * constructor list    
76  (* relevance, typename, arity, constructors *)
77
78 type def_flavour = (* presentational *)
79   [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
80
81 type def_pragma = (* pragmatic of the object *)
82   [ `Coercion of int
83   | `Elim of sort       (* elimination principle; universe is not relevant *)
84   | `Projection         (* record projection *)
85   | `InversionPrinciple (* inversion principle *)
86   | `Variant 
87   | `Local 
88   | `Regular ]            (* Local = hidden technicality *)
89  
90 type ind_pragma = (* pragmatic of the object *)
91   [ `Record of (string * bool * int) list | `Regular ]
92   (* inductive type that encodes a record; the arguments are the record 
93    * fields names and if they are coercions and then the coercion arity *)
94
95 type generated = [ `Generated | `Provided ]
96
97 type c_attr = generated * def_flavour * def_pragma
98 type f_attr = generated * def_flavour
99 type i_attr = generated * ind_pragma
100
101  (* invariant: metasenv and substitution have disjoint domains *)
102 type obj_kind =
103  | Constant  of relevance * string * term option * term * c_attr
104  | Fixpoint  of bool * inductiveFun list * f_attr
105                 (* true -> fix, funcs, arrts *)
106  | Inductive of bool * int * inductiveType list * i_attr
107                 (* true -> inductive, leftno, types *)
108
109  (* the int must be 0 if the object has no body *)
110 type obj = NUri.uri * int * metasenv * substitution * obj_kind