aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile14
-rw-r--r--contrib/extraction/extraction.ml4
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/xml/xmlcommand.ml44
-rw-r--r--kernel/cooking.ml17
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml28
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/mod_typing.ml6
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml4
-rw-r--r--lib/system.ml2
-rw-r--r--parsing/prettyp.ml2
16 files changed, 64 insertions, 41 deletions
diff --git a/Makefile b/Makefile
index e660dbea8..32b831596 100644
--- a/Makefile
+++ b/Makefile
@@ -304,13 +304,10 @@ COQTOPBYTE=bin/coqtop.byte$(EXE)
COQTOPOPT=bin/coqtop.opt$(EXE)
BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
COQTOP=bin/coqtop$(EXE)
+COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE)
-# COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE)
-
-COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP)
-
-#\
-# $(COQINTERFACE)
+COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
+ $(COQINTERFACE)
coqbinaries:: ${COQBINARIES}
@@ -393,7 +390,7 @@ clean::
# tests
###########################################################################
-check:: world bin/parser
+check:: world
cd test-suite; ./check -$(BEST) | tee check.log
if grep -F 'Error!' test-suite/check.log ; then false; fi
@@ -623,8 +620,7 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
$(CORRECTNESSVO) $(FOURIERVO) \
- $(JPROVERVO) $(CCVO)
-# $(INTERFACEV0)
+ $(JPROVERVO) $(INTERFACEV0) $(CCVO)
$(CONTRIBVO): states/initial.coq
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index e1848589d..4888c8fef 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -671,12 +671,12 @@ let extract_constant kn r =
| (Info, Arity) ->
let s,vl = type_sign_vl env typ in
let db = db_from_sign s in
- let body = Lazy.force_val l_body in
+ let body = Declarations.force l_body in
let t = extract_type_arity env db body (List.length s)
in Dtype (r, vl, t)
| (Logic, _) -> Dterm (r, MLdummy')
| (Info, _) ->
- let body = Lazy.force_val l_body in
+ let body = Declarations.force l_body in
let a = extract_term env body in
if a <> MLdummy' then
Dterm (r, kill_prop_lams_eta a (signature_of_kn kn))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index b35a5f56f..0ae3b2d82 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -177,7 +177,7 @@ let constant_to_ast_list kn =
None ->
make_variable_ast (id_of_label (label kn)) typ l
| Some c1 ->
- make_definition_ast (id_of_label (label kn)) (Lazy.force_val c1) typ l)
+ make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
let variable_to_ast_list sp =
let ((id, c, v), _) = get_variable sp in
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 8710a9e1f..5ca89dd3f 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -740,7 +740,7 @@ let print (_,qid as locqid) fn =
match val0 with
None -> print_axiom id typ [] hyps env inner_types
| Some lc ->
- let c = Lazy.force_val lc in
+ let c = Declarations.force lc in
print_definition id c typ [] hyps env inner_types
end
| Ln.IndRef (kn,_) ->
@@ -859,7 +859,7 @@ let print_object lobj id (sp,kn) dn fv env =
match val0 with
None -> print_axiom id typ fv hyps env inner_types
| Some lc ->
- let c = Lazy.force_val lc in
+ let c = Declarations.force lc in
print_definition id c typ fv hyps env inner_types
end
| "INDUCTIVE" ->
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index eb37adbd3..7c3b8e60f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -107,7 +107,7 @@ let expmod_constr modlist c =
str"and then require that theorems which use them" ++ spc () ++
str"be transparent");
match cb.const_body with
- | Some body -> Lazy.force_val body
+ | Some body -> Declarations.force body
| None -> assert false
in
let c' = modify_opers expfun modlist c in
@@ -141,11 +141,12 @@ let abstract_constant ids_to_abs hyps (body,typ) =
let body' = match body with
None -> None
| Some l_body ->
- Some (lazy (let body = Lazy.force_val l_body in
- let (_,body') =
- List.fold_left abstract_once_body (hyps,body) ids_to_abs
- in
- body'))
+ Some (Declarations.from_val
+ (let body = Declarations.force l_body in
+ let (_,body') =
+ List.fold_left abstract_once_body (hyps,body) ids_to_abs
+ in
+ body'))
in
(body',typ')
@@ -154,7 +155,9 @@ let cook_constant env r =
let typ = expmod_type r.d_modlist cb.const_type in
let body =
option_app
- (fun lconstr -> lazy (expmod_constr r.d_modlist (Lazy.force_val lconstr)))
+ (fun lconstr ->
+ Declarations.from_val
+ (expmod_constr r.d_modlist (Declarations.force lconstr)))
cb.const_body
in
let hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 1787478b9..b54189ba6 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -32,7 +32,7 @@ type recipe = {
d_modlist : work_list }
val cook_constant :
- env -> recipe -> constr Lazy.t option * constr * constraints * bool
+ env -> recipe -> constr_substituted option * constr * constraints * bool
(*s Utility functions used in module [Discharge]. *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d3c7681c0..e6dd40c8a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,9 +21,30 @@ open Sign
(*s Constants (internal representation) (Definition/Axiom) *)
+type subst_internal =
+ | Constr of constr
+ | LazyConstr of substitution * constr
+
+type constr_substituted = subst_internal ref
+
+let from_val c = ref (Constr c)
+
+let force cs = match !cs with
+ Constr c -> c
+ | LazyConstr (subst,c) ->
+ let c' = subst_mps subst c in
+ cs := Constr c';
+ c'
+
+let subst_constr_subst subst cs = match !cs with
+ Constr c -> ref (LazyConstr (subst,c))
+ | LazyConstr (subst',c) ->
+ let subst'' = join subst' subst in
+ ref (LazyConstr (subst'',c))
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
- const_body : constr Lazy.t option;
+ const_body : constr_substituted option;
const_type : types;
const_constraints : constraints;
const_opaque : bool }
@@ -88,12 +109,9 @@ type mutual_inductive_body = {
mind_equiv : kernel_name option
}
-let lazy_subst sub l_constr =
- lazy (subst_mps sub (Lazy.force_val l_constr))
-
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb =
- { const_body = option_app (lazy_subst sub) cb.const_body;
+ { const_body = option_app (subst_constr_subst sub) cb.const_body;
const_type = type_app (Term.subst_mps sub) cb.const_type;
const_hyps = (assert (cb.const_hyps=[]); []);
const_constraints = cb.const_constraints;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 715a83a4a..a40b65f6b 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -21,9 +21,15 @@ open Sign
(*s Constants (Definition/Axiom) *)
+type constr_substituted
+
+val from_val : constr -> constr_substituted
+val force : constr_substituted -> constr
+val subst_constr_subst : substitution -> constr_substituted -> constr_substituted
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
- const_body : constr Lazy.t option;
+ const_body : constr_substituted option;
const_type : types;
const_constraints : constraints;
const_opaque : bool }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd9a72bd1..e4b1af8fe 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -141,7 +141,7 @@ let constant_value env kn =
let cb = lookup_constant kn env in
if cb.const_opaque then raise (NotEvaluableConst Opaque);
match cb.const_body with
- | Some l_body -> Lazy.force_val l_body
+ | Some l_body -> Declarations.force l_body
| None -> raise (NotEvaluableConst NoBody)
let constant_opt_value env cst =
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b8399ab32..ba4dcf0b7 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,13 +92,13 @@ and merge_with env mtb with_decl =
in
SPBconst {cb with
const_body =
- Some (Lazy.lazy_from_val j.uj_val);
+ Some (Declarations.from_val j.uj_val);
const_constraints = cst}
| Some b ->
- let cst1 = Reduction.conv env' c (Lazy.force_val b) in
+ let cst1 = Reduction.conv env' c (Declarations.force b) in
let cst = Constraint.union cb.const_constraints cst1 in
SPBconst {cb with
- const_body = Some (Lazy.lazy_from_val c);
+ const_body = Some (Declarations.from_val c);
const_constraints = cst}
end
| With_Module (id, mp) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 40a0e84c5..758bf2159 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -165,7 +165,7 @@ let strengthen_const env mp l cb = match cb.const_body with
| Some _ -> cb
| None -> {cb with const_body =
let const = mkConst (make_kn mp empty_dirpath l) in
- Some (Lazy.lazy_from_val const)
+ Some (Declarations.from_val const)
}
let strengthen_mind env mp l mib = match mib.mind_equiv with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 70faa24b4..663c6b695 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -121,8 +121,8 @@ type global_declaration =
let hcons_constant_body cb =
let body = match cb.const_body with
None -> None
- | Some l_constr -> let constr = Lazy.force_val l_constr in
- Some (Lazy.lazy_from_val (hcons1_constr constr))
+ | Some l_constr -> let constr = Declarations.force l_constr in
+ Some (Declarations.from_val (hcons1_constr constr))
in
{ cb with
const_body = body;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6e20ceeb4..0e24da587 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -161,9 +161,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
match cb2.const_body with
| None -> cst
| Some lc2 ->
- let c2 = Lazy.force_val lc2 in
+ let c2 = Declarations.force lc2 in
let c1 = match cb1.const_body with
- | Some c1 -> Lazy.force_val c1
+ | Some lc1 -> Declarations.force lc1
| None -> mkConst (make_kn (MPself msid1) empty_dirpath l)
in
check_conv cst conv env c1 c2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index aabefe6bf..1145ee94b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -81,7 +81,7 @@ let infer_declaration env dcl =
| DefinitionEntry c ->
let (j,cst) = infer env c.const_entry_body in
let (typ,cst) = constrain_type env j cst c.const_entry_type in
- Some (Lazy.lazy_from_val j.uj_val), typ, cst, c.const_entry_opaque
+ Some (Declarations.from_val j.uj_val), typ, cst, c.const_entry_opaque
| ParameterEntry t ->
let (j,cst) = infer env t in
None, Typeops.assumption_of_judgment env j, cst, false
@@ -91,7 +91,7 @@ let build_constant_declaration env (body,typ,cst,op) =
| None -> global_vars_set env typ
| Some b ->
Idset.union
- (global_vars_set env (Lazy.force_val b))
+ (global_vars_set env (Declarations.force b))
(global_vars_set env typ)
in
let hyps = keep_hyps env ids in
diff --git a/lib/system.ml b/lib/system.ml
index eb2305112..35584bf89 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -140,7 +140,7 @@ let try_remove f =
with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
str f ++ str" which is corrupted!" )
-let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures]
+let marshal_out ch v = Marshal.to_channel ch v []
let marshal_in ch =
try Marshal.from_channel ch
with End_of_file -> error "corrupted file: reached end of file"
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 565d0ec9f..f6b4b2c60 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -266,7 +266,7 @@ let print_section_variable sp =
(print_named_decl d ++ print_impl_args l)
let print_body = function
- | Some lc -> prterm (Lazy.force_val lc)
+ | Some lc -> prterm (Declarations.force lc)
| None -> (str"<no body>")
let print_typed_body (val_0,typ) =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 09:28:22 +0000