diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 15:10:08 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 15:10:08 +0000 |
commit | a4436a6a355ecb3fffb52d1ca3f2d983a5bcfefd (patch) | |
tree | 0252d3bb7d7f9c55dad753f39e83de5efba41de4 /toplevel | |
parent | f09ca438e24bc4016b4e778dd8fd4de4641b7636 (diff) |
- constantes avec recettes
- discharge en deux temps, avec état remis comme au début de la section
(mais c'est toujours buggé)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/class.ml | 3 | ||||
-rw-r--r-- | toplevel/command.ml | 35 | ||||
-rw-r--r-- | toplevel/discharge.ml | 194 |
3 files changed, 139 insertions, 93 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index d4cd6fec6..7912b2fdf 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -289,7 +289,8 @@ let build_id_coercion idf_opt ids = id_of_string ("Id_"^(string_of_id ids)^"_"^ (string_of_cl (fst (constructor_at_head t)))) in - let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in + let constr_entry = + { const_entry_body = Cooked constr_f; const_entry_type = None } in declare_constant idf (constr_entry,NeverDischarge); idf diff --git a/toplevel/command.ml b/toplevel/command.ml index 882033919..776864d70 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -32,10 +32,10 @@ let constant_entry_of_com com = let env = Global.env() in match com with | Node(_,"CAST",[_;t]) -> - { const_entry_body = constr_of_com sigma env com; + { const_entry_body = Cooked (constr_of_com sigma env com); const_entry_type = Some (constr_of_com1 true sigma env t) } | _ -> - { const_entry_body = constr_of_com sigma env com; + { const_entry_body = Cooked (constr_of_com sigma env com); const_entry_type = None } let definition_body ident n com = @@ -44,9 +44,13 @@ let definition_body ident n com = let red_constant_entry ce = function | None -> ce - | Some red -> + | Some red -> + let body = match ce.const_entry_body with + | Cooked c -> c + | Recipe _ -> assert false + in { const_entry_body = - reduction_of_redexp red (Global.env()) Evd.empty ce.const_entry_body; + Cooked (reduction_of_redexp red (Global.env()) Evd.empty body); const_entry_type = ce.const_entry_type } @@ -233,9 +237,11 @@ let build_recursive lnameargsardef = let varrec = Array.of_list larrec in let rec declare i = function | fi::lf -> - let ce = { const_entry_body = - mkFixDlam (Array.of_list nvrec) i varrec recvec; - const_entry_type = None } in + let ce = + { const_entry_body = + Cooked (mkFixDlam (Array.of_list nvrec) i varrec recvec); + const_entry_type = None } + in declare_constant fi (ce, n); declare (i+1) lf | _ -> () @@ -249,7 +255,7 @@ let build_recursive lnameargsardef = let _ = List.fold_left (fun subst (f,def) -> - let ce = { const_entry_body = Generic.replace_vars subst def; + let ce = { const_entry_body = Cooked (Generic.replace_vars subst def); const_entry_type = None } in declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); @@ -297,9 +303,11 @@ let build_corecursive lnameardef = in let rec declare i = function | fi::lf -> - let ce = { const_entry_body = - mkCoFixDlam i (Array.of_list larrec) recvec; - const_entry_type = None } in + let ce = + { const_entry_body = + Cooked (mkCoFixDlam i (Array.of_list larrec) recvec); + const_entry_type = None } + in declare_constant fi (ce,n); declare (i+1) lf | _ -> () @@ -312,7 +320,7 @@ let build_corecursive lnameardef = let _ = List.fold_left (fun subst (f,def) -> - let ce = { const_entry_body = Generic.replace_vars subst def; + let ce = { const_entry_body = Cooked (Generic.replace_vars subst def); const_entry_type = None } in declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); @@ -337,7 +345,8 @@ let build_scheme lnamedepindsort = let rec declare i = function | fi::lf -> let ce = - { const_entry_body = listdecl.(i); const_entry_type = None } in + { const_entry_body = Cooked listdecl.(i); const_entry_type = None } + in declare_constant fi (ce,n); declare (i+1) lf | _ -> () diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 84b357c5d..f0a97c218 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -74,7 +74,14 @@ let abstract_constant ids_to_abs hyps (body,typ) = let name = Name id in let var = snd (hd_sign hyps) in let cvar = incast_type var in - let body' = mkLambda name cvar (subst_var id body) in + let body' = match body with + | None -> None + | Some { contents = Cooked c } -> + Some (ref (Cooked (mkLambda name cvar (subst_var id c)))) + | Some { contents = Recipe f } -> + Some (ref (Recipe + (fun () -> mkLambda name cvar (subst_var id (f()))))) + in let typ' = { body = mkProd name cvar (subst_var id typ.body); typ = sort_of_product_without_univ var.typ typ.typ } @@ -88,29 +95,21 @@ let abstract_constant ids_to_abs hyps (body,typ) = (* Substitutions. *) -let expmod_constr modlist c = - let env = Global.env() in +let expmod_constr oldenv modlist c = let sigma = Evd.empty in - let simpfun = if modlist = [] then fun x -> x else nf_betaiota env sigma in - let expfun c = - let (sp,_) = destConst c in + let simpfun = + if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in + let expfun cst = try - constant_value env c - with Failure _ -> begin - mSGERRNL + constant_value oldenv cst + with Failure _ -> + let (sp,_) = destConst cst in + errorlabstrm "expmod_constr" [< 'sTR"Cannot unfold the value of " ; 'sTR(string_of_path sp) ; 'sPC; 'sTR"You cannot declare local lemmas as being opaque"; 'sPC; 'sTR"and then require that theorems which use them"; 'sPC; 'sTR"be transparent" >]; - let cb = Global.lookup_constant sp in - cb.const_opaque <- false; - (try - let v = constant_value env c in - cb.const_opaque <- true; - v - with _ -> anomaly "expmod_constr") - end in let under_casts f = function | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t)) @@ -118,27 +117,34 @@ let expmod_constr modlist c = in let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in match c' with - | DOP2(Cast,val_0,typ) -> DOP2(Cast,simpfun val_0,simpfun typ) - | DOP2(XTRA "IND",c,DLAMV(na,lc)) -> - DOP2(XTRA "IND",under_casts simpfun c, - DLAMV(na,Array.map (under_casts simpfun) lc)) + | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ) | _ -> simpfun c' -let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s} +let expmod_type oldenv modlist {body=c;typ=s} = + { body = expmod_constr oldenv modlist c; typ = s } +let expmod_constant_value opaque oldenv modlist = function + | None -> None + | Some { contents = Cooked c } -> + if opaque then + Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c))) + else + Some (ref (Cooked (expmod_constr oldenv modlist c))) + | Some { contents = Recipe f } -> + Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ())))) (* Discharge of inductive types. *) -let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib = +let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = assert (Array.length mib.mind_packets > 0); let finite = mib.mind_packets.(0).mind_finite in let inds = array_map_to_list (fun mip -> (mip.mind_typename, - expmod_type modlist mip.mind_arity, + expmod_type oldenv modlist mip.mind_arity, Array.to_list mip.mind_consnames, - under_dlams (expmod_constr modlist) mip.mind_lc)) + under_dlams (expmod_constr oldenv modlist) mip.mind_lc)) mib.mind_packets in let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in @@ -162,22 +168,22 @@ let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib = (* Discharge of constants. *) -let process_constant osecsp nsecsp (ids_to_discard,modlist) cb = - let body = global_reference CCI (basename osecsp) in - let typ = expmod_type modlist cb.const_type in +let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb = + let body = + expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in + let typ = expmod_type oldenv modlist cb.const_type in let (body',typ',modl) = abstract_constant ids_to_discard cb.const_hyps (body,typ) in let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in - ({ const_entry_body = body'; const_entry_type = Some typ'.body }, - mods) + (body', typ'.body, mods) (* Discharge of the various objects of the environment. *) -let constant_message sp = +let constant_message id = if Options.verbose() then - pPNL [< print_id (basename sp); 'sTR " is discharged." >] + pPNL [< print_id id; 'sTR " is discharged." >] let inductive_message inds = if Options.verbose() then @@ -189,74 +195,80 @@ let inductive_message inds = (fun (id,_,_,_) -> print_id id) l; 'sPC; 'sTR "are discharged.">])) -let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) = +type discharge_operation = + | Variable of identifier * constr * strength * bool + | Parameter of identifier * constr + | Constant of identifier * constant_entry * strength + | Inductive of mutual_inductive_entry + | Class of cl_typ * cl_info_typ + | Struc of section_path * struc_typ + | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) + * identifier * int + +let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) = let tag = object_tag lobj in match tag with | "VARIABLE" -> let (id,a,stre,sticky) = out_variable sp in if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then - (id::ids_to_discard,work_alist) - else begin - let expmod_a = expmod_constr work_alist a.body in - declare_variable id (expmod_a,stre,sticky); - (ids_to_discard,work_alist) - end + (ops,id::ids_to_discard,work_alist) + else + let expmod_a = expmod_constr oldenv work_alist a.body in + (Variable (id,expmod_a,stre,sticky) :: ops, + ids_to_discard,work_alist) | "CONSTANT" -> let stre = constant_strength sp in if stre = (DischargeAt sec_sp) then - (ids_to_discard, (Const sp, DO_REPLACE) :: work_alist) - else begin - let cb = Global.lookup_constant sp in + (ops, ids_to_discard, (Const sp, DO_REPLACE) :: work_alist) + else + let cb = Environ.lookup_constant sp oldenv in let spid = basename sp in let newsp = recalc_sp sp in - let (ce,mods) = - process_constant sp newsp (ids_to_discard,work_alist) cb in - declare_constant spid (ce,stre); - constant_message sp; - (ids_to_discard,mods@work_alist) - end + let (body,typ,mods) = + process_constant sp newsp oldenv (ids_to_discard,work_alist) cb in + let op = match body with + | None -> + Parameter (spid,typ) + | Some { contents = b } -> + let ce = + { const_entry_body = b; const_entry_type = Some typ } in + Constant (spid,ce,stre) + in + (op::ops, ids_to_discard, mods@work_alist) | "INDUCTIVE" -> - let mib = Global.lookup_mind sp in + let mib = Environ.lookup_mind sp oldenv in let newsp = recalc_sp sp in let (mie,mods) = - process_inductive sp newsp (ids_to_discard,work_alist) mib in - let _ = declare_mind mie in - inductive_message mie.mind_entry_inds; - (ids_to_discard,mods@work_alist) + process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in + ((Inductive mie)::ops, ids_to_discard, mods@work_alist) | "CLASS" -> let ((cl,clinfo) as x) = outClass lobj in if clinfo.cL_STRE = (DischargeAt sec_sp) then - (ids_to_discard,work_alist) - else begin - let y = process_class sec_sp x in - Lib.add_anonymous_leaf (inClass y); - (ids_to_discard,work_alist) - end + (ops,ids_to_discard,work_alist) + else + let (y1,y2) = process_class sec_sp x in + ((Class (y1,y2))::ops, ids_to_discard, work_alist) | "COERCION" -> let (((_,coeinfo),_,_)as x) = outCoercion lobj in if coeinfo.cOE_STRE = (DischargeAt sec_sp) then - (ids_to_discard,work_alist) - else begin - let ((_,_,clt) as y),idf,ps = process_coercion sec_sp x in - Lib.add_anonymous_leaf (inCoercion y); - coercion_syntax idf ps clt; - (ids_to_discard,work_alist) - end + (ops,ids_to_discard,work_alist) + else + let (y,idf,ps) = process_coercion sec_sp x in + ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist) | "STRUCTURE" -> let (sp,info) = outStruc lobj in let newsp = recalc_sp sp in - let mib = Global.lookup_mind (ccisp_of newsp) in + let mib = Environ.lookup_mind newsp oldenv in let strobj = - { s_CONST= info.s_CONST; - s_PARAM= mib.mind_nparams; - s_PROJ= List.map (option_app recalc_sp) info.s_PROJ} in - Lib.add_anonymous_leaf (inStruc (newsp,strobj)); - (ids_to_discard,work_alist) + { s_CONST = info.s_CONST; + s_PARAM = mib.mind_nparams; + s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in + ((Struc (newsp,strobj))::ops, ids_to_discard, work_alist) (***TODO | "OBJDEF1" -> @@ -266,14 +278,38 @@ let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) = (ids_to_discard,work_alist) ***) - | _ -> - (ids_to_discard,work_alist) + | _ -> (ops,ids_to_discard,work_alist) -let process_item sec_sp acc = function - | (sp,Leaf lobj) -> process_object sec_sp acc (sp,lobj) +let process_item oldenv sec_sp acc = function + | (sp,Leaf lobj) -> process_object oldenv sec_sp acc (sp,lobj) | (_,_) -> acc +let process_operation = function + | Variable (id,expmod_a,stre,sticky) -> + declare_variable id (expmod_a,stre,sticky) + | Parameter (spid,typ) -> + declare_parameter spid typ; + constant_message spid + | Constant (spid,ce,stre) -> + declare_constant spid (ce,stre); + constant_message spid + | Inductive mie -> + let _ = declare_mind mie in + inductive_message mie.mind_entry_inds + | Class (y1,y2) -> + Lib.add_anonymous_leaf (inClass (y1,y2)) + | Struc (newsp,strobj) -> + Lib.add_anonymous_leaf (inStruc (newsp,strobj)) + | Coercion ((_,_,clt) as y,idf,ps) -> + Lib.add_anonymous_leaf (inCoercion y); + coercion_syntax idf ps clt + let close_section _ s = - let (sec_sp,decls) = close_section s in - let _ = List.fold_left (process_item sec_sp) ([],[]) decls in - () + let oldenv = Global.env() in + let (sec_sp,decls,frozen) = close_section s in + let (ops,_,_) = + List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in + Summary.unfreeze_summaries frozen; + List.iter process_operation (List.rev ops) + + |