summaryrefslogtreecommitdiff
path: root/checker/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.ml')
-rw-r--r--checker/term.ml41
1 files changed, 16 insertions, 25 deletions
diff --git a/checker/term.ml b/checker/term.ml
index 61369586..4a3f47a3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
(* This module instantiates the structure of generic deBruijn terms to Coq *)
open Util
@@ -31,15 +29,15 @@ type case_printing =
{ ind_nargs : int; (* length of the arity of the inductive type *)
style : case_style }
type case_info =
- { ci_ind : inductive;
- ci_npar : int;
- ci_cstr_nargs : int array; (* number of real args of each constructor *)
- ci_pp_info : case_printing (* not interpreted by the kernel *)
+ { ci_ind : inductive;
+ ci_npar : int;
+ ci_cstr_ndecls : int array; (* number of pattern var of each constructor *)
+ ci_pp_info : case_printing (* not interpreted by the kernel *)
}
let val_ci =
let val_cstyle = val_enum "case_style" 5 in
- let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
- val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+ let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
+ val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
(* Sorts. *)
@@ -73,13 +71,14 @@ type 'constr pfixpoint =
type 'constr pcofixpoint =
int * 'constr prec_declaration
-let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
let val_prec f =
- val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+ val_tuple ~name:"prec_declaration"
+ [|val_array val_name; val_array f; val_array f|]
let val_fix f =
- val_tuple"pfixpoint"
- [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+ val_tuple ~name:"pfixpoint"
+ [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
type cast_kind = VMcast | DEFAULTcast
let val_cast = val_enum "cast_kind" 2
@@ -262,7 +261,7 @@ let rec exliftn el c = match c with
(* Lifting the binding depth across k bindings *)
let liftn k n =
- match el_liftn (pred n) (el_shft k ELID) with
+ match el_liftn (pred n) (el_shft k el_id) with
| ELID -> (fun c -> c)
| el -> exliftn el
@@ -313,22 +312,15 @@ let subst1 lam = substl [lam]
(***************************************************************************)
let val_ndecl =
- val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+ val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|]
let val_rdecl =
- val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+ val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
let val_nctxt = val_list val_ndecl
let val_rctxt = val_list val_rdecl
type named_declaration = identifier * constr option * constr
type rel_declaration = name * constr option * constr
-let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-
type named_context = named_declaration list
let empty_named_context = []
let fold_named_context f l ~init = List.fold_right f l init
@@ -439,7 +431,6 @@ let decompose_prod_n_assum n =
(***************************)
type arity = rel_context * sorts
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign