diff options
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 41 |
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 |