diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 32 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.mli | 6 | ||||
| -rw-r--r-- | plugins/micromega/micromega_plugin.mlpack | 2 |
3 files changed, 22 insertions, 18 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7adae148bd..7db47e13a5 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Context open Tactypes (** @@ -876,11 +877,9 @@ struct * This is the big generic function for expression parsers. *) - let parse_expr sigma parse_constant parse_exp ops_spec env term = + let parse_expr cenv sigma parse_constant parse_exp ops_spec env term = if debug - then ( - let _, env = Pfedit.get_current_context () in - Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env cenv sigma term); (* let constant_or_variable env term = @@ -999,8 +998,7 @@ struct | _ -> raise ParseError - let rconstant sigma term = - let _, env = Pfedit.get_current_context () in + let rconstant env sigma term = if debug then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in @@ -1009,7 +1007,7 @@ struct res - let parse_zexpr sigma = parse_expr sigma + let parse_zexpr env sigma = parse_expr env sigma (zconstant sigma) (fun expr x -> let exp = (parse_z sigma x) in @@ -1018,7 +1016,7 @@ struct | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) zop_spec - let parse_qexpr sigma = parse_expr sigma + let parse_qexpr env sigma = parse_expr env sigma (qconstant sigma) (fun expr x -> let exp = parse_z sigma x in @@ -1033,8 +1031,8 @@ struct Mc.PEpow(expr,exp)) qop_spec - let parse_rexpr sigma = parse_expr sigma - (rconstant sigma) + let parse_rexpr env sigma = parse_expr env sigma + (rconstant env sigma) (fun expr x -> let exp = Mc.N.of_nat (parse_nat sigma x) in Mc.PEpow(expr,exp)) @@ -1047,8 +1045,8 @@ struct match EConstr.kind sigma cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr sigma env lhs in - let (e2,env) = parse_expr sigma env rhs in + let (e1,env) = parse_expr gl.env sigma env lhs in + let (e2,env) = parse_expr gl.env sigma env rhs in ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) | _ -> failwith "error : parse_arith(2)" @@ -1243,7 +1241,7 @@ let dump_rexpr = lazy let prodn n env b = let rec prodrec = function | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) + | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (make_annot v Sorts.Relevant,t,b)) | _ -> assert false in prodrec (n,env,b) @@ -1293,8 +1291,8 @@ let make_goal_of_formula sigma dexpr form = | FF -> Lazy.force coq_False | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) + | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (xdump (pi+1) (xi+1) y) + | N(x) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) | A(x,_,_) -> dump_cstr xi x | X(t) -> let idx = Env.get_rank props sigma t in EConstr.mkRel (pi+idx) in @@ -1327,7 +1325,7 @@ let make_goal_of_formula sigma dexpr form = | (e::l) -> let (name,expr,typ) = e in xset (EConstr.mkNamedLetIn - (Names.Id.of_string name) + (make_annot (Names.Id.of_string name) Sorts.Relevant) expr typ acc) l in xset concl l @@ -1614,7 +1612,7 @@ let abstract_formula hyps f = | I(f1,hyp,f2) -> (match xabs f1 , hyp, xabs f2 with | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) + | X a1 , None , X a2 -> X (EConstr.mkArrow a1 Sorts.Relevant a2) | af1 , _ , af2 -> I(af1,hyp,af2) ) | FF -> FF diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index b91feb3984..d1776b8ca4 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -20,3 +20,9 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic + + +(** {5 Use Micromega independently from tactics. } *) + +(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *) +val dump_proof_term : Micromega.zArithProof -> EConstr.t diff --git a/plugins/micromega/micromega_plugin.mlpack b/plugins/micromega/micromega_plugin.mlpack index 2baf6608a4..e3aa0dab7d 100644 --- a/plugins/micromega/micromega_plugin.mlpack +++ b/plugins/micromega/micromega_plugin.mlpack @@ -1,8 +1,8 @@ +Micromega Mutils Itv Vect Sos_types -Micromega Polynomial Mfourier Simplex |