(*i $Id$ i*) open Pp open Util open Names open Term open Sign open Declarations open Instantiate open Environ open Reduction (*s Cooking the constants. *) type modification_action = ABSTRACT | ERASE type 'a modification = | NOT_OCCUR | DO_ABSTRACT of 'a * modification_action list | DO_REPLACE type work_list = (section_path * section_path modification) list * (inductive_path * inductive_path modification) list * (constructor_path * constructor_path modification) list type recipe = { d_from : section_path; d_abstract : identifier list; d_modlist : work_list } let interp_modif absfun mkfun (sp,modif) cl = let rec interprec = function | ([], cl) -> mkfun (sp, Array.of_list cl) | (ERASE::tlm, c::cl) -> interprec (tlm,cl) | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c | _ -> assert false in interprec (modif, Array.to_list cl) let failure () = anomalylabstrm "generic__modify_opers" [< 'sTR"An oper which was never supposed to appear has just appeared" ; 'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC; 'sTR"report this error," ; 'sPC ; 'sTR"Or you are using a user-written tactic which calls" ; 'sPC ; 'sTR"generic__modify_opers, in which case the user-written code" ; 'sPC ; 'sTR"is broken - this function is an internal system" ; 'sPC ; 'sTR"for internal system use only" >] let modify_opers replfun absfun (constl,indl,cstrl) = let rec substrec c = let op, cl = splay_constr c in let cl' = Array.map substrec cl in match op with | OpMutCase (n,(spi,a,b,c,d) as oper) -> (try match List.assoc spi indl with | DO_ABSTRACT (spi',_) -> gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl') | _ -> raise Not_found with | Not_found -> gather_constr (op,cl')) | OpMutInd spi -> (try (match List.assoc spi indl with | NOT_OCCUR -> failure () | DO_ABSTRACT (oper',modif) -> assert (List.length modif <= Array.length cl); interp_modif absfun mkMutInd (oper',modif) cl' | DO_REPLACE -> assert false) with | Not_found -> mkMutInd (spi,cl')) | OpMutConstruct spi -> (try (match List.assoc spi cstrl with | NOT_OCCUR -> failure () | DO_ABSTRACT (oper',modif) -> assert (List.length modif <= Array.length cl); interp_modif absfun mkMutConstruct (oper',modif) cl' | DO_REPLACE -> assert false) with | Not_found -> mkMutConstruct (spi,cl')) | OpConst sp -> (try (match List.assoc sp constl with | NOT_OCCUR -> failure () | DO_ABSTRACT (oper',modif) -> assert (List.length modif <= Array.length cl); interp_modif absfun mkConst (oper',modif) cl' | DO_REPLACE -> substrec (replfun (sp,cl'))) with | Not_found -> mkConst (sp,cl')) | _ -> gather_constr (op, cl') in if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec let expmod_constr oldenv modlist c = let sigma = Evd.empty in let simpfun = if modlist = ([],[],[]) then fun x -> x else nf_betaiota oldenv sigma in let expfun cst = try constant_value oldenv cst with NotEvaluableConst Opaque -> let (sp,_) = 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" >]; in let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in match kind_of_term c' with | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ) | _ -> simpfun c' let expmod_type oldenv modlist c = type_app (expmod_constr oldenv modlist) c let abstract_constant ids_to_abs hyps (body,typ) = let abstract_once ((hyps,body,typ) as sofar) id = match hyps with | (hyp,c,t as decl)::rest when hyp = id -> let body' = match body with | None -> None | Some c -> Some (mkNamedLambda_or_LetIn decl c) in let typ' = mkNamedProd_wo_LetIn decl typ in (rest, body', typ') | _ -> sofar in let (_,body',typ') = List.fold_left abstract_once (hyps,body,typ) ids_to_abs in (body',typ') let cook_constant env r = let cb = lookup_constant r.d_from env in let typ = expmod_type env r.d_modlist cb.const_type in let body = option_app (expmod_constr env r.d_modlist) cb.const_body in let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in abstract_constant r.d_abstract hyps (body,typ)