summaryrefslogtreecommitdiff
path: root/kernel/cooking.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /kernel/cooking.ml
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'kernel/cooking.ml')
-rw-r--r--kernel/cooking.ml36
1 files changed, 24 insertions, 12 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d35c011a..02330339 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -1,12 +1,17 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cooking.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jean-Christophe FilliĆ¢tre out of V6.3 file constants.ml
+ as part of the rebuilding of Coq around a purely functional
+ abstract type-checker, Nov 1999 *)
+
+(* This module implements kernel-level discharching of local
+ declarations over global constants and inductive types *)
open Pp
open Util
@@ -99,7 +104,7 @@ let expmod_constr modlist c =
in
if modlist = empty_modlist then c
- else under_outer_cast nf_betaiota (substrec c)
+ else substrec c
let abstract_constant_type =
List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
@@ -112,16 +117,24 @@ type recipe = {
d_abstract : named_context;
d_modlist : work_list }
-let on_body f =
- Option.map (fun c -> Declarations.from_val (f (Declarations.force c)))
+let on_body f = function
+ | Undef inl -> Undef inl
+ | Def cs -> Def (Declarations.from_val (f (Declarations.force cs)))
+ | OpaqueDef lc ->
+ OpaqueDef (Declarations.opaque_from_val (f (Declarations.force_opaque lc)))
+
+let constr_of_def = function
+ | Undef _ -> assert false
+ | Def cs -> Declarations.force cs
+ | OpaqueDef lc -> Declarations.force_opaque lc
let cook_constant env r =
let cb = r.d_from in
let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
- let body =
- on_body (fun c ->
- abstract_constant_body (expmod_constr r.d_modlist c) hyps)
- cb.const_body in
+ let body = on_body
+ (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
+ cb.const_body
+ in
let typ = match cb.const_type with
| NonPolymorphicType t ->
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
@@ -129,8 +142,7 @@ let cook_constant env r =
| PolymorphicArity (ctx,s) ->
let t = mkArity (ctx,Type s.poly_level) in
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
- let j = make_judge (force (Option.get body)) typ in
+ let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
- let boxed = Cemitcodes.is_boxed cb.const_body_code in
- (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
+ (body, typ, cb.const_constraints)