diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 89 | ||||
| -rw-r--r-- | stm/lemmas.mli | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 23 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 1 |
4 files changed, 59 insertions, 58 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 8f16ad5a4b..2aeb8141e8 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -73,7 +73,7 @@ let find_mutually_recursive_statements thms = | Some (Some (_,id),CStructRec) -> let i,b,typ = lookup_rel_id id hyps in (match kind_of_term t with - | Ind (kn,_ as ind) when + | Ind ((kn,_ as ind), u) when let mind = Global.lookup_mind kn in mind.mind_finite && Option.is_empty b -> [ind,x,i],[] @@ -90,7 +90,7 @@ let find_mutually_recursive_statements thms = let ind_hyps = List.flatten (List.map_i (fun i (_,b,t) -> match kind_of_term t with - | Ind (kn,_ as ind) when + | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite && Option.is_empty b -> [ind,x,i] @@ -100,7 +100,7 @@ let find_mutually_recursive_statements thms = let cclenv = push_rel_context hyps (Global.env()) in let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in match kind_of_term whnf_ccl with - | Ind (kn,_ as ind) when + | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && not mind.mind_finite -> [ind,x,0] @@ -167,9 +167,11 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save id const do_guard (locality,kind) hook = +let save id const cstrs do_guard (locality,poly,kind) hook = let const = adjust_guardness_conditions const do_guard in let k = Kindops.logical_kind_of_goal_kind kind in + (* Add global constraints necessary to check the type of the proof *) + let () = Global.add_constraints cstrs in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in @@ -198,14 +200,14 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) -let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imps))) = match body with | None -> (match locality with | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl) in + let c = SectionLocalAssum ((t_i,ctx_i),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -215,7 +217,8 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = | Global -> false | Discharge -> assert false in - let decl = (ParameterEntry (None,t_i,None), k) in + let ctx = Univ.ContextSet.to_context ctx_i in + let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -230,27 +233,26 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = Future.from_val (body_i,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some t_i; + const_entry_proj = None; const_entry_opaque = opaq; - const_entry_inline_code = false; const_entry_feedback = None; + const_entry_inline_code = false; + const_entry_polymorphic = p; + const_entry_universes = Univ.ContextSet.to_context ctx_i } in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) | Local | Global -> + let ctx = Univ.ContextSet.to_context ctx_i in let local = match locality with | Local -> true | Global -> false | Discharge -> assert false in - let const = { const_entry_body = - Future.from_val (body_i,Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_inline_code = false; - const_entry_feedback = None; - } in + let const = + Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -258,8 +260,8 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named proof = - let id,const,do_guard,persistence,hook = proof in - save id const do_guard persistence hook + let id,const,cstrs,do_guard,persistence,hook = proof in + save id const cstrs do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then @@ -267,25 +269,29 @@ let check_anonymity id save_ident = let save_anonymous proof save_ident = - let id,const,do_guard,persistence,hook = proof in + let id,const,cstrs,do_guard,persistence,hook = proof in check_anonymity id save_ident; - save save_ident const do_guard persistence hook + save save_ident const cstrs do_guard persistence hook let save_anonymous_with_strength proof kind save_ident = - let id,const,do_guard,_,hook = proof in + let id,const,cstrs,do_guard,_,hook = proof in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook + save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook (* Admitted *) let admit hook () = let (id,k,typ) = Pfedit.current_proof_statement () in - let e = Pfedit.get_used_variables(), typ, None in - let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in - let () = match fst k with - | Global -> () - | Local | Discharge -> + let ctx = + let evd = fst (Pfedit.get_current_goal_context ()) in + Evd.universe_context evd + in + let e = Pfedit.get_used_variables(), pi2 k, (typ, ctx), None in + let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in + let () = match k with + | Global, _, _ -> () + | Local, _, _ | Discharge, _, _ -> msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ str "declared as an axiom.") in @@ -302,7 +308,8 @@ let get_proof proof do_guard hook opacity = let (id,(const,persistence)) = Pfedit.cook_this_proof proof in - id,{const with const_entry_opaque = opacity},do_guard,persistence,hook + (** FIXME *) + id,{const with const_entry_opaque = opacity},Univ.Constraint.empty,do_guard,persistence,hook let standard_proof_terminator compute_guard hook = let open Proof_global in function @@ -325,13 +332,14 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = | Some sign -> sign | None -> initialize_named_context_for_proof () in - !start_hook c; + !start_hook (fst c); Pfedit.start_proof id kind sign c ?init_tac terminator +(* FIXME: forgetting about the universes here *) let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with + match List.map (fun (id,(t,_)) -> (id,fst t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -339,7 +347,7 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + in match List.map2 (fun (id,(t,_)) n -> (id,n,fst t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false @@ -382,19 +390,24 @@ let start_proof_with_initialization kind recguard thms snl hook = start_proof id kind t ?init_tac hook ~compute_guard:guard let start_proof_com kind thms hook = - let evdref = ref Evd.empty in let env0 = Global.env () in + let evdref = ref (Evd.from_env env0) in let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in let t', imps' = interp_type_evars_impls ~impls evdref env t in check_evars_are_solved env Evd.empty !evdref; let ids = List.map pi1 ctx in - (compute_proof_name (fst kind) sopt, + (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms in let recguard,thms,snl = look_for_possibly_mutual_statements thms in + let evd, nf = Evarutil.nf_evars_and_universes !evdref in + let ctxset = Evd.get_universe_context_set evd in + let thms = List.map (fun (n, (t, info)) -> (n, ((nf t, ctxset), info))) + thms + in start_proof_with_initialization kind recguard thms snl hook @@ -419,13 +432,3 @@ let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) - - - - - - - - - - diff --git a/stm/lemmas.mli b/stm/lemmas.mli index bbe383a857..f8694a0961 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -17,7 +17,7 @@ open Pfedit (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types Univ.in_universe_context_set -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit @@ -27,7 +27,7 @@ val start_proof_com : goal_kind -> val start_proof_with_initialization : goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list + (Id.t * (types Univ.in_universe_context_set * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val standard_proof_terminator : diff --git a/stm/stm.ml b/stm/stm.ml index 6fe3fd03a8..0218c923bf 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -741,8 +741,9 @@ end = struct let l = Future.force (build_proof_here exn_info loc eop) in List.iter (fun (_,se) -> Declareops.iter_side_effects (function | Declarations.SEsubproof(_, - { Declarations.const_body = Declarations.OpaqueDef f } ) -> - Opaqueproof.join_opaque f + { Declarations.const_body = Declarations.OpaqueDef f; + const_universes = univs } ) -> + Opaqueproof.join_opaque f; ignore (Future.join univs) (* FIXME: MS: needed?*) | _ -> ()) se) l; l, Unix.gettimeofday () -. wall_clock in @@ -814,7 +815,7 @@ end = struct let extra = Future.join uc in u.(bucket) <- uc; p.(bucket) <- pr; - u, Univ.union_constraints cst extra, false + u, Univ.union_constraint cst extra, false | _ -> assert false let check_task name l i = @@ -982,13 +983,13 @@ end = struct Pp.feedback (Interface.InProgress ~-1) *) last_task := None; raise KillRespawn - | _, RespGetCounterFreshLocalUniv -> - marshal_more_data oc (MoreDataLocalUniv - (CList.init 10 (fun _ -> Univ.fresh_local_univ ()))); - if !cancel_switch then raise KillRespawn else loop () + | _, RespGetCounterFreshLocalUniv -> assert false (* Deprecated function *) + (* marshal_more_data oc (MoreDataLocalUniv *) + (* (CList.init 10 (fun _ -> Universes.fresh_local_univ ()))); *) + (* loop () *) | _, RespGetCounterNewUnivLevel -> marshal_more_data oc (MoreDataUnivLevel - (CList.init 10 (fun _ -> Termops.new_univ_level ()))); + (CList.init 10 (fun _ -> Universes.new_univ_level (Global.current_dirpath ())))); loop () | _, RespFeedback {id = State state_id; content = msg} -> Pp.feedback ~state_id msg; @@ -1082,14 +1083,10 @@ end = struct Marshal.to_channel oc (RespFeedback fb) []; flush oc in Pp.set_feeder (slave_feeder !slave_oc); - Termops.set_remote_new_univ_level (bufferize (fun () -> + Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response !slave_oc RespGetCounterNewUnivLevel; match unmarshal_more_data !slave_ic with | MoreDataUnivLevel l -> l | _ -> assert false)); - Univ.set_remote_fresh_local_univ (bufferize (fun () -> - marshal_response !slave_oc RespGetCounterFreshLocalUniv; - match unmarshal_more_data !slave_ic with - | MoreDataLocalUniv l -> l | _ -> assert false)); let working = ref false in slave_handshake (); while true do diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 49cbcd246b..3bd83f46bc 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -66,6 +66,7 @@ let rec classify_vernac e = (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e + | VernacPolymorphic (b, e) -> classify_vernac e | VernacTimeout (_,e) -> classify_vernac e | VernacTime e -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) |