From d8f3098a13d52841ad0022617e7f7ce3c7848670 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 12 Feb 2008 18:02:14 +0000 Subject: [PATCH] nCic almost finished --- helm/software/components/ng_kernel/nCic.ml | 83 +++++++++++++++++----- 1 file changed, 65 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 28e2fbd05..8d974ca10 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -31,35 +31,82 @@ type sort = type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] -type name = Name of string | Anonymous - type local_context = int * (term list) option (* shift (0 -> no shift), subst (None means id) *) - and term = | Rel of int (* DeBruijn index, 1 based *) - | Meta of int * string option * local_context + | Meta of int * local_context | Appl of term list (* arguments *) - | Prod of name * term * term (* binder, source, target *) - | Lambda of name * term * term (* binder, source, target *) - | LetIn of name * term * term * term (* binder, type, term, body *) + | Prod of string * term * term (* binder, source, target *) + | Lambda of string * term * term (* binder, source, target *) + | LetIn of string * term * term * term (* binder, type, term, body *) (* Cast \def degenerate LetIn *) - | Const of NReference.reference (* reference contains indtypeno/constrno *) + | Const of NReference.reference (* reference contains indtypeno/constrno *) | Sort of sort (* sort *) | Implicit of implicit_annotation (* ... *) - | Match of NReference.reference * (* ind. reference, *) + | Match of NReference.reference * (* ind. reference, *) term * term * (* outtype, ind. term *) term list (* patterns *) -and obj = - | Constant of term option * term - | FixpointDefinition of ... - | InductiveDefinition of inductiveType list (* inductive types, *) -and inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) -and constructor = - string * term (* id, type *) +type context_entry = (* A declaration or definition *) + | Decl of term + | Def of term * term option (* body, type (if known) *) + +type hypothesis = string * context_entry (* None means no more accessible *) + +type context = hypothesis list + +type conjecture = int * string option * context * term + +type metasenv = conjecture list + +type substitution = (int * (string option * context * term * term)) list + + + + +type inductiveFun = + string * int * term * term (* if coinductive, the int has no meaning and must be set to -1 *) + +type constructor = string * term (* id, type *) + +type inductiveType = + string * bool * term * (* typename, inductive, arity *) + constructor list (* constructors *) + +type def_flavour = (* presentational *) + [ `Definition + | `Fact + | `Lemma + | `Remark + | `Theorem + ] + +type def_pragma = (* pragmatic of the object *) + [ `Coercion of int + | `Elim of sort (** elimination principle; if sort is Type, the universe is not relevant *) + | `Projection (** record projection *) + | `InversionPrinciple (** inversion principle *) + | `Variant + ] + +type ind_pragma = (* pragmatic of the object *) + [ `Record of (string * bool * int) list (** + inductive type that encodes a record; the arguments are + the record fields names and if they are coercions and + then the coercion arity *) + ] + +type generated = [ `Generated | `Provided ] + +type c_attr = generated * def_flavour * def_pragma +type f_attr = generated * def_flavour +type i_attr = generated * ind_pragma + +type obj = + | Constant of NUri.uri * metasenv * substitution * string * term option * term * c_attr + | Fixpoint of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr + | Inductive of NUri.uri * metasenv * substitution * inductiveType list * i_attr -- 2.39.2