diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 102 |
1 files changed, 63 insertions, 39 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5b3f15a08c..8a91e9e63f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,6 @@ open Pp open Util open Redexpr open Constrintern -open Pretyping (* Commands of the interface: Constant definitions *) @@ -40,10 +39,50 @@ let check_imps ~impsty ~impsbody = | [], [] -> () in aux impsty impsbody +let protect_pattern_in_binder bl c ctypopt = + (* We turn "Definition d binders := body : typ" into *) + (* "Definition d := fun binders => body:type" *) + (* This is a hack while waiting for LocalPattern in regular environments *) + if List.exists (function Constrexpr.CLocalPattern _ -> true | _ -> false) bl + then + let t = match ctypopt with + | None -> CAst.make ?loc:c.CAst.loc (Constrexpr.CHole (None,Namegen.IntroAnonymous,None)) + | Some t -> t in + let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in + let c = CAst.make ?loc @@ Constrexpr.CCast (c, Glob_term.CastConv t) in + let loc = match List.hd bl with + | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc + | Constrexpr.CLocalPattern {CAst.loc} -> loc + | Constrexpr.CLocalAssum ([],_,_) -> assert false in + let apply_under_binders f env evd c = + let rec aux env evd c = + let open Constr in + let open EConstr in + let open Context.Rel.Declaration in + match kind evd c with + | Lambda (x,t,c) -> + let evd,c = aux (push_rel (LocalAssum (x,t)) env) evd c in + evd, mkLambda (x,t,c) + | LetIn (x,b,t,c) -> + let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in + evd, mkLetIn (x,t,b,c) + | Case (ci,p,a,bl) -> + let evd,bl = Array.fold_left_map (aux env) evd bl in + evd, mkCase (ci,p,a,bl) + | Cast (c,_,_) -> f env evd c (* we remove the cast we had set *) + (* This last case may happen when reaching the proof of an + impossible case, as when pattern-matching on a vector of length 1 *) + | _ -> (evd,c) in + aux env evd c in + ([], Constrexpr_ops.mkLambdaCN ?loc:(Loc.merge_opt loc c.CAst.loc) bl c, None, apply_under_binders) + else + (bl, c, ctypopt, fun f env evd c -> f env evd c) + let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let env = Global.env() in (* Explicitly bound universes and constraints *) let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in + let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in (* Build the parameters *) let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in (* Build the type *) @@ -63,46 +102,31 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = evd, c, imps1@impsty, Some ty in (* Do the reduction *) - let evd, c = red_constant_body red_option env_bl evd c in + let evd, c = apply_under_binders (red_constant_body red_option) env_bl evd c in (* Declare the definition *) let c = EConstr.it_mkLambda_or_LetIn c ctx in let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in + (c, tyopt), evd, udecl, imps - let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in - - (ce, evd, udecl, imps) - -let check_definition ~program_mode (ce, evd, _, imps) = - let env = Global.env () in - check_evars_are_solved ~program_mode env evd; - ce +let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = false in + let (body, types), evd, udecl, impargs = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + in + let kind = Decls.IsDefinition kind in + let _ : Names.GlobRef.t = + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + ~opaque:false ~poly evd ~udecl ~types ~body + in () -let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = - let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt +let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = true in + let (body, types), evd, udecl, impargs = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - if program_mode then - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - Obligations.check_evars env evd; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env evd c - in - let obls, _, c, cty = - Obligations.eterm_obligations env name evd 0 c typ - in - let ctx = Evd.evar_universe_context evd in - ignore(Obligations.add_definition - ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) - else - let ce = check_definition ~program_mode def in - let uctx = Evd.evar_universe_context evd in - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) + let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let _ : DeclareObl.progress = + Obligations.add_definition + ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls + in () |