diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 134 |
1 files changed, 63 insertions, 71 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index fd2041d31..29edcc866 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -36,6 +36,7 @@ open Nametab open Typeops open Indtypes open Vernacexpr +open Decl_kinds let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) @@ -92,36 +93,34 @@ let red_constant_entry ce = function { ce with const_entry_body = reduction_of_redexp red (Global.env()) Evd.empty body } -let declare_global_definition ident ce n local = - let (_,kn) = declare_constant ident (DefinitionEntry ce,n) in - if local then +let declare_global_definition ident ce local = + let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in + if local = Local then msg_warning (pr_id ident ++ str" is declared as a global definition"); if_verbose message ((string_of_id ident) ^ " is defined"); ConstRef kn -let declare_definition ident (local,n) bl red_option c typopt = +let declare_definition ident local bl red_option c typopt = let ce = constant_entry_of_com (bl,c,typopt,false) in if bl<>[] && red_option <> None then error "Evaluation under a local context not supported"; let ce' = red_constant_entry ce red_option in - match n with - | NeverDischarge -> declare_global_definition ident ce' n local - | DischargeAt (disch_sp,_) -> - if Lib.is_section_p disch_sp then begin - let c = + match local with + | Global -> + declare_global_definition ident ce' Global + | Local -> + if Lib.is_section_p (Lib.cwd ()) then begin + let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in - let _ = declare_variable ident (Lib.cwd(), c, n) in - if_verbose message ((string_of_id ident) ^ " is defined"); + let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in + if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ - str" is not visible from current goals"); - VarRef ident + str" is not visible from current goals"); + VarRef ident end - else - declare_global_definition ident ce' n true - | NotDeclare -> - anomalylabstrm "Command.definition_body_red" - (str "Strength NotDeclare not for Definition, only for Let") + else + declare_global_definition ident ce' Local let syntax_definition ident c = let c = interp_rawconstr Evd.empty (Global.env()) c in @@ -133,33 +132,34 @@ let syntax_definition ident c = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption ident n bl c = +let declare_assumption ident (local,kind) bl c = let c = prod_rawconstr c bl in let c = interp_type Evd.empty (Global.env()) c in - match n with - | NeverDischarge -> - let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident; - ConstRef kn - | DischargeAt (disch_sp,_) -> - if Lib.is_section_p disch_sp then begin - let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in - assumption_message ident; + match local with + | Global -> + let (_,kn) = + declare_constant ident (ParameterEntry c, IsAssumption kind) in + assumption_message ident; + ConstRef kn + | Local -> + if Lib.is_section_p (Lib.cwd ()) then begin + let r = + declare_variable ident + (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ - str" is not visible from current goals"); - VarRef ident + str" is not visible from current goals"); + VarRef ident end - else - let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident; - if_verbose - msg_warning (pr_id ident ++ str" is declared as a parameter" ++ - str" because it is at a global level"); - ConstRef kn - | NotDeclare -> - anomalylabstrm "Command.hypothesis_def_var" - (str "Strength NotDeclare not for Variable, only for Let") + else + let (_,kn) = + declare_constant ident (ParameterEntry c, IsAssumption kind) in + assumption_message ident; + if_verbose + msg_warning (pr_id ident ++ str" is declared as a parameter" ++ + str" because it is at a global level"); + ConstRef kn (* 3| Mutual Inductive definitions *) @@ -280,8 +280,7 @@ let build_mutual lind finite = let _ = declare_mutual_with_eliminations mie in List.iter (fun id -> - Class.try_add_new_coercion - (locate (make_short_qualid id)) NeverDischarge) coes + Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes (* try to find non recursive definitions *) @@ -333,7 +332,7 @@ let build_recursive lnameargsardef = let raw_arity = mkProdCit lparams arityc in let arity = interp_type sigma env0 raw_arity in let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arity, NeverDischarge) in + (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> @@ -351,7 +350,6 @@ let build_recursive lnameargsardef = States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in - let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in @@ -360,7 +358,7 @@ let build_recursive lnameargsardef = { const_entry_body = mkFix ((nvrec,i),recdecls); const_entry_type = Some arrec.(i); const_entry_opaque = false } in - let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in + let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in (* declare the recursive definitions *) @@ -374,7 +372,7 @@ let build_recursive lnameargsardef = let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce,n) in + let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -394,7 +392,7 @@ let build_corecursive lnameardef = let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in let arity = arj.utj_val in let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arj.utj_val,NeverDischarge) in + (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> @@ -412,7 +410,6 @@ let build_corecursive lnameardef = States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,_)) = collect_non_rec env0 lrecnames recdef arityl [] in - let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in @@ -422,7 +419,7 @@ let build_corecursive lnameardef = const_entry_type = Some (arrec.(i)); const_entry_opaque = false } in - let _,kn = declare_constant fi (DefinitionEntry ce,n) in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in let lrefrec = Array.mapi declare namerec in @@ -434,7 +431,7 @@ let build_corecursive lnameardef = let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce,n) in + let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -454,7 +451,6 @@ let build_scheme lnamedepindsort = (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort in - let n = NeverDischarge in let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in @@ -462,7 +458,7 @@ let build_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false } in - let _,kn = declare_constant fi (DefinitionEntry ce,n) in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in ConstRef kn :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in @@ -480,7 +476,7 @@ let rec binders_length = function | LocalRawDef _::bl -> 1 + binders_length bl | LocalRawAssum (idl,_)::bl -> List.length idl + binders_length bl -let start_proof_com sopt (local,stre) (bl,t) hook = +let start_proof_com sopt kind (bl,t) hook = let env = Global.env () in let sign = Global.named_context () in let sign = clear_proofs sign in @@ -496,7 +492,7 @@ let start_proof_com sopt (local,stre) (bl,t) hook = in let c = interp_type Evd.empty env (generalize_rawconstr t bl) in let _ = Typeops.infer_type env c in - Pfedit.start_proof id (local,stre) sign c hook + Pfedit.start_proof id kind sign c hook let apply_tac_not_declare id pft = function | None -> error "Type of Let missing" @@ -506,26 +502,22 @@ let apply_tac_not_declare id pft = function Pfedit.delete_current_proof (); Pfedit.by (Refiner.tclTHENSV cutt [|introduction id;exat|]) -let save id const (local,strength) hook = +let save id const kind hook = let {const_entry_body = pft; const_entry_type = tpo; const_entry_opaque = opacity } = const in - begin match strength with - | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && local -> + begin match kind with + | IsLocal -> let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, strength) in - hook strength (VarRef id) - | NeverDischarge | DischargeAt _ -> - let _,kn = declare_constant id (DefinitionEntry const,strength) in - let ref = ConstRef kn in - hook strength ref - | NotDeclare -> apply_tac_not_declare id pft tpo + let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in + hook Local (VarRef id) + | IsGlobal k -> + let k = theorem_kind_of_goal_kind k in + let _,kn = declare_constant id (DefinitionEntry const, k) in + hook Global (ConstRef kn) end; - if not (strength = NotDeclare) then - begin - Pfedit.delete_current_proof (); - if_verbose message ((string_of_id id) ^ " is defined") - end + Pfedit.delete_current_proof (); + if_verbose message ((string_of_id id) ^ " is defined") let save_named opacity = let id,(const,persistence,hook) = Pfedit.cook_proof () in @@ -545,12 +537,12 @@ let save_anonymous opacity save_ident = check_anonymity id save_ident; save save_ident const persistence hook -let save_anonymous_with_strength strength opacity save_ident = +let save_anonymous_with_strength kind opacity save_ident = let id,(const,_,hook) = Pfedit.cook_proof () in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const (not opacity,strength) hook + save save_ident const (IsGlobal (Proof kind)) hook let get_current_context () = try Pfedit.get_current_goal_context () |