diff options
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | TODO | 2 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 12 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml4 | 8 | ||||
| -rw-r--r-- | dev/Makefile.devel | 10 | ||||
| -rw-r--r-- | kernel/cooking.ml | 37 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 7 | ||||
| -rw-r--r-- | kernel/declarations.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 7 | ||||
| -rw-r--r-- | kernel/modops.ml | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 11 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 5 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 7 | ||||
| -rw-r--r-- | lib/system.ml | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 |
17 files changed, 96 insertions, 37 deletions
@@ -304,10 +304,13 @@ 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) -COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ - $(COQINTERFACE) +# COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE) + +COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) + +#\ +# $(COQINTERFACE) coqbinaries:: ${COQBINARIES} @@ -620,7 +623,8 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(CORRECTNESSVO) $(FOURIERVO) \ - $(JPROVERVO) $(INTERFACEV0) $(CCVO) + $(JPROVERVO) $(CCVO) +# $(INTERFACEV0) $(CONTRIBVO): states/initial.coq @@ -16,6 +16,8 @@ Vernac: - Print / Print Proof en fait identiques ; Print ne devrait pas afficher les constantes opaques (devrait afficher qqchose comme <opaque>) +- Print Module d'un module a l'interier d'un type de module ne devrait pas + afficher son corps (il n'a pas de corps!) Theories: diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index f574cecae..e1848589d 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -665,20 +665,22 @@ let extract_constant kn r = DdummyType r | (Logic,_) -> axiom_warning_message kn; Dterm (r, MLdummy')) - | Some body -> + | Some l_body -> (match flag_of_type env typ with | (Logic, Arity) -> DdummyType 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 t = extract_type_arity env db body (List.length s) in Dtype (r, vl, t) | (Logic, _) -> Dterm (r, MLdummy') | (Info, _) -> - let a = extract_term env body in - if a <> MLdummy' then - Dterm (r, kill_prop_lams_eta a (signature_of_kn kn)) - else Dterm (r, a)) + let body = Lazy.force_val 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)) + else Dterm (r, a)) let extract_constant_cache kn r = try lookup_constant kn diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4 index 14d0f94ac..8710a9e1f 100644 --- a/contrib/xml/xmlcommand.ml4 +++ b/contrib/xml/xmlcommand.ml4 @@ -739,7 +739,9 @@ let print (_,qid as locqid) fn = begin match val0 with None -> print_axiom id typ [] hyps env inner_types - | Some c -> print_definition id c typ [] hyps env inner_types + | Some lc -> + let c = Lazy.force_val lc in + print_definition id c typ [] hyps env inner_types end | Ln.IndRef (kn,_) -> let sp = Nt.sp_of_global None (Ln.IndRef(kn,0)) in @@ -856,7 +858,9 @@ let print_object lobj id (sp,kn) dn fv env = begin match val0 with None -> print_axiom id typ fv hyps env inner_types - | Some c -> print_definition id c typ fv hyps env inner_types + | Some lc -> + let c = Lazy.force_val lc in + print_definition id c typ fv hyps env inner_types end | "INDUCTIVE" -> let diff --git a/dev/Makefile.devel b/dev/Makefile.devel index ce80836ab..db25167f5 100644 --- a/dev/Makefile.devel +++ b/dev/Makefile.devel @@ -51,13 +51,23 @@ ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),) include $(TOPDIR)/dev/Makefile.local endif + usage:: @echo " total -- runs coqtop with all theories required" total: ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th)))) + usage:: @echo " run -- makes and runs bytecode coqtop using ledit and the history file" @echo " if you want to pass arguments to coqtop, use make run ARG=<args>" run: $(TOPDIR)/coqtop ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS) + + +usage:: + @echo " vars -- echos commands to set COQTOP and COQBIN variables" +vars: + @(cd $(TOPDIR); \ + echo export COQTOP=`pwd`/ ; \ + echo export COQBIN=`pwd`/bin/ )
\ No newline at end of file diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 616be45f1..eb37adbd3 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 -> body + | Some body -> Lazy.force_val body | None -> assert false in let c' = modify_opers expfun modlist c in @@ -119,23 +119,44 @@ let expmod_type modlist c = type_app (expmod_constr modlist) c let abstract_constant ids_to_abs hyps (body,typ) = - let abstract_once ((hyps,body,typ) as sofar) id = + let abstract_once_typ ((hyps,typ) as sofar) id = match hyps with | (hyp,c,t as decl)::rest when hyp = id -> - let body' = option_app (mkNamedLambda_or_LetIn decl) body in let typ' = mkNamedProd_wo_LetIn decl typ in - (rest, body', typ') + (rest, typ') | _ -> sofar in - let (_,body',typ') = - List.fold_left abstract_once (hyps,body,typ) ids_to_abs in - (body',typ') + let abstract_once_body ((hyps,body) as sofar) id = + match hyps with + | (hyp,c,t as decl)::rest when hyp = id -> + let body' = mkNamedLambda_or_LetIn decl body in + (rest, body') + | _ -> + sofar + in + let (_,typ') = + List.fold_left abstract_once_typ (hyps,typ) ids_to_abs + in + 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')) + in + (body',typ') let cook_constant env r = let cb = r.d_from in let typ = expmod_type r.d_modlist cb.const_type in - let body = option_app (expmod_constr r.d_modlist) cb.const_body in + let body = + option_app + (fun lconstr -> lazy (expmod_constr r.d_modlist (Lazy.force_val lconstr))) + cb.const_body + in let hyps = Sign.fold_named_context (fun d ctxt -> diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 3cd03fc9a..1787478b9 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 option * constr * constraints * bool + env -> recipe -> constr Lazy.t option * constr * constraints * bool (*s Utility functions used in module [Discharge]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 05989bc82..d3c7681c0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -23,7 +23,7 @@ open Sign type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr option; + const_body : constr Lazy.t option; const_type : types; const_constraints : constraints; const_opaque : bool } @@ -88,9 +88,12 @@ 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 (Term.subst_mps sub) cb.const_body; + { const_body = option_app (lazy_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 eeec64875..715a83a4a 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -23,7 +23,7 @@ open Sign type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr option; + const_body : constr Lazy.t option; const_type : types; const_constraints : constraints; const_opaque : bool } diff --git a/kernel/environ.ml b/kernel/environ.ml index 6449c183f..dd9a72bd1 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 body -> body + | Some l_body -> Lazy.force_val 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 0fb79376a..b8399ab32 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -91,13 +91,14 @@ and merge_with env mtb with_decl = cst2 in SPBconst {cb with - const_body = Some j.uj_val; + const_body = + Some (Lazy.lazy_from_val j.uj_val); const_constraints = cst} | Some b -> - let cst1 = Reduction.conv env' c b in + let cst1 = Reduction.conv env' c (Lazy.force_val b) in let cst = Constraint.union cb.const_constraints cst1 in SPBconst {cb with - const_body = Some c; + const_body = Some (Lazy.lazy_from_val c); const_constraints = cst} end | With_Module (id, mp) -> diff --git a/kernel/modops.ml b/kernel/modops.ml index d4338f0fb..40a0e84c5 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -163,7 +163,10 @@ and add_module mp mb env = let strengthen_const env mp l cb = match cb.const_body with | Some _ -> cb - | None -> {cb with const_body = Some (mkConst (make_kn mp empty_dirpath l))} + | None -> {cb with const_body = + let const = mkConst (make_kn mp empty_dirpath l) in + Some (Lazy.lazy_from_val const) + } let strengthen_mind env mp l mib = match mib.mind_equiv with | Some _ -> mib diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d8a00d7b7..70faa24b4 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -119,9 +119,14 @@ type global_declaration = | GlobalRecipe of Cooking.recipe let hcons_constant_body cb = - { cb with - const_body = option_app hcons1_constr cb.const_body; - const_type = hcons1_constr cb.const_type } + 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)) + in + { cb with + const_body = body; + const_type = hcons1_constr cb.const_type } let add_constant dir l decl senv = check_label l senv.labset; diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2a81ebee0..6e20ceeb4 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -160,9 +160,10 @@ let check_constant cst env msid1 l info1 cb2 spec2 = let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in match cb2.const_body with | None -> cst - | Some c2 -> + | Some lc2 -> + let c2 = Lazy.force_val lc2 in let c1 = match cb1.const_body with - | Some c1 -> c1 + | Some c1 -> Lazy.force_val c1 | 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 1abe65c20..aabefe6bf 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 j.uj_val, typ, cst, c.const_entry_opaque + Some (Lazy.lazy_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 @@ -90,7 +90,10 @@ let build_constant_declaration env (body,typ,cst,op) = let ids = match body with | None -> global_vars_set env typ | Some b -> - Idset.union (global_vars_set env b) (global_vars_set env typ) in + Idset.union + (global_vars_set env (Lazy.force_val b)) + (global_vars_set env typ) + in let hyps = keep_hyps env ids in { const_body = body; const_type = typ; diff --git a/lib/system.ml b/lib/system.ml index 35584bf89..eb2305112 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 [] +let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures] 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 0808001bb..565d0ec9f 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 c -> prterm c + | Some lc -> prterm (Lazy.force_val lc) | None -> (str"<no body>") let print_typed_body (val_0,typ) = |