From 57bee17f928fc67a599d2116edb42a59eeb21477 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Oct 2013 18:30:54 +0200 Subject: Rework handling of universes on top of the STM, allowing for delayed computation in case of non-polymorphic proofs. Also fix plugins after forgotten merge conflicts. Still does not compile everything. --- plugins/funind/functional_principles_types.ml | 14 +------ plugins/setoid_ring/newring.ml4 | 58 +++++++++++++-------------- plugins/syntax/ascii_syntax.ml | 2 +- plugins/syntax/z_syntax.ml | 6 +-- 4 files changed, 33 insertions(+), 47 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 2adc82505..88693c196 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -340,19 +340,7 @@ let generate_functional_principle let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = - { const_entry_body = - Future.from_val (value,Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = None; - const_entry_polymorphic = false; - const_entry_universes = Univ.UContext.empty (*FIXME*); - const_entry_proj = None; - const_entry_opaque = false; - const_entry_feedback = None; - const_entry_inline_code = false - } - in + let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *) ignore( Declare.declare_constant name diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 7ed8e03a9..ae05fbdc3 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -152,18 +152,10 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in - mkConst(declare_constant (Id.of_string na) (DefinitionEntry - { const_entry_body = Future.from_val (c, Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = None; - const_entry_polymorphic = false; - const_entry_universes = Univ.ContextSet.to_context ctx; - const_entry_proj = None; - const_entry_opaque = true; - const_entry_inline_code = false; - const_entry_feedback = None; - }, - IsProof Lemma)) + mkConst(declare_constant (Id.of_string na) + (DefinitionEntry (definition_entry ~opaque:true + ~univs:(Univ.ContextSet.to_context ctx) c), + IsProof Lemma)) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = @@ -442,11 +434,11 @@ let theory_to_obj : ring_info -> obj = let setoid_of_relation env evd a r = try - let evm = !evd, Int.Set.empty in - let evm, refl = Rewrite.PropGlobal.get_reflexive_proof env evm a r in - let evm, sym = Rewrite.PropGlobal.get_symmetric_proof env evm a r in - let evm, trans = Rewrite.PropGlobal.get_transitive_proof env evm a r in - evd := fst evm; + let evm = !evd in + let evm, refl = Rewrite.get_reflexive_proof env evm a r in + let evm, sym = Rewrite.get_symmetric_proof env evm a r in + let evm, trans = Rewrite.get_transitive_proof env evm a r in + evd := evm; lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] with Not_found -> error "cannot find setoid relation" @@ -682,9 +674,9 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = let lemma2 = params.(4) in let lemma1 = - decl_constant (Id.to_string name^"_ring_lemma1") ctx (Future.from_val ( lemma1,Declareops.no_seff)) in + decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in let lemma2 = - decl_constant (Id.to_string name^"_ring_lemma2") ctx (Future.from_val ( lemma2,Declareops.no_seff)) in + decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -724,10 +716,16 @@ type 'constr ring_mod = | Div_spec of Constrexpr.constr_expr +let ic_coeff_spec = function + | Computational t -> Computational (ic_unsafe t) + | Morphism t -> Morphism (ic_unsafe t) + | Abstract -> Abstract + + VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic_unsafe eq_test)) ] + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic_unsafe morph)) ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] @@ -754,7 +752,7 @@ let process_ring_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_kind k -> set_once "ring kind" kind k + Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t @@ -1026,18 +1024,18 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power let lemma4 = params.(6) in let cond_lemma = match inj with - | Some thm -> mkApp(constr_of params.(8),[|thm|]) - | None -> constr_of params.(7) in + | Some thm -> mkApp(params.(8),[|thm|]) + | None -> params.(7) in let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") - ctx (Future.from_val (lemma1,Declareops.no_seff)) in + ctx lemma1 in let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") - ctx (Future.from_val (lemma2,Declareops.no_seff)) in + ctx lemma2 in let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") - ctx (Future.from_val (lemma3,Declareops.no_seff)) in + ctx lemma3 in let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") - ctx (Future.from_val (lemma4,Declareops.no_seff)) in + ctx lemma4 in let cond_lemma = decl_constant (Id.to_string name^"_lemma5") - ctx (Future.from_val (cond_lemma,Declareops.no_seff)) in + ctx cond_lemma in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -1083,7 +1081,7 @@ let process_field_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind k + Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) | Ring_mod(Const_tac t) -> set_once "tactic recognizing constants" cst_tac t | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 5c060c3d6..67c9dd0a3 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,7 +37,7 @@ let interp_ascii dloc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None) + GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None) :: (aux (n-1) (p/2)) in GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 5131a5f38..2b1410be6 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -182,8 +182,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (Loc.ghost, glob_ZERO, None, None); - GRef (Loc.ghost, glob_POS, None, None); - GRef (Loc.ghost, glob_NEG, None, None)], + ([GRef (Loc.ghost, glob_ZERO, None); + GRef (Loc.ghost, glob_POS, None); + GRef (Loc.ghost, glob_NEG, None)], uninterp_z, true) -- cgit v1.2.3