diff options
Diffstat (limited to 'plugins')
28 files changed, 1280 insertions, 1337 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index ee50476b10..f671860bd5 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -28,7 +28,7 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Id.Set.empty -let pp_comment s = str";; "++h 0 s++fnl () +let pp_comment s = str ";; " ++ h s ++ fnl () let pp_header_comment = function | None -> mt () diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index a1094e39a4..bbc4df7dde 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -151,7 +151,7 @@ let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Gena Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) } diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 1ea803f561..012fcee486 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1860,13 +1860,13 @@ let do_generate_principle_aux pconstants on_error register_built let warn_cannot_define_graph = CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" (fun (names, error) -> - Pp.(strbrk "Cannot define graph(s) for " ++ h 1 names ++ error)) + Pp.(strbrk "Cannot define graph(s) for " ++ hv 1 names ++ error)) let warn_cannot_define_principle = CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" (fun (names, error) -> Pp.( - strbrk "Cannot define induction principle(s) for " ++ h 1 names ++ error)) + strbrk "Cannot define induction principle(s) for " ++ hv 1 names ++ error)) let warning_error names e = let e_explain e = @@ -1898,7 +1898,7 @@ let error_error names e = CErrors.user_err Pp.( str "Cannot define graph(s) for " - ++ h 1 + ++ hv 1 (prlist_with_sep (fun _ -> str "," ++ spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> raise e diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index f1f538ab39..b7ac71181a 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -20,8 +20,6 @@ open Tacarg open Names open Logic -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 863c4d37d8..ad4374dba3 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -47,7 +47,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in - register "hyp" wit_var; + register "hyp" wit_hyp; register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; @@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences GLOB_PRINTED BY { pr_occurrences } | [ ne_integer_list(l) ] -> { ArgArg l } -| [ var(id) ] -> { ArgVar id } +| [ hyp(id) ] -> { ArgVar id } END { diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4f20e5a800..a2a47c0bf4 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -33,8 +33,6 @@ open Proofview.Notations open Attributes open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -450,7 +448,7 @@ END (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ne_hyp_list(l) ] -> { subst l } | [ "subst" ] -> { subst_all () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 2e72ceae5a..44472a1995 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -18,8 +18,6 @@ open Pcoq.Constr open Pltac open Hints -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8d197e6056..8c2e633be5 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -31,12 +31,12 @@ let set_transparency cl b = } VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> { +| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> { set_transparency cl true } END VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> { +| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> { set_transparency cl false } END @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth @@ -87,11 +87,13 @@ END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - { typeclasses_eauto ~strategy:Bfs ~depth:d l } + { typeclasses_eauto ~depth:d ~strategy:Bfs l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } + typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d88cda177e..6cf5d30a95 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -48,14 +48,14 @@ let reference_to_id qid = CErrors.user_err ?loc:qid.CAst.loc (str "This expression should be a simple identifier.") -let tactic_mode = Entry.create "vernac:tactic_command" +let tactic_mode = Entry.create "tactic_command" let new_entry name = let e = Entry.create name in e -let toplevel_selector = new_entry "vernac:toplevel_selector" -let tacdef_body = new_entry "tactic:tacdef_body" +let toplevel_selector = new_entry "toplevel_selector" +let tacdef_body = new_entry "tacdef_body" (* Registers [tactic_mode] as a parser for proof editing *) let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode @@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram open Stdarg open Tacarg open Vernacextend -open Goptions open Libnames -let print_info_trace = - declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"] - -let vernac_solve ~pstate n info tcom b = - let open Goal_select in - let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info (print_info_trace ()) in - let (p,status) = - Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) pstate in - if not status then Feedback.feedback Feedback.AddedAxiom; - pstate - let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s } @@ -409,34 +389,34 @@ END { -let is_anonymous_abstract = function - | TacAbstract (_,None) -> true - | TacSolve [TacAbstract (_,None)] -> true - | _ -> false let rm_abstract = function - | TacAbstract (t,_) -> t - | TacSolve [TacAbstract (t,_)] -> TacSolve [t] - | x -> x + | TacAbstract (t,_) -> t, true + | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true + | x -> x, false let is_explicit_terminator = function TacSolve _ -> true | _ -> false } VERNAC { tactic_mode } EXTEND VernacSolve STATE proof -| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def + let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in + let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + ComTactic.solve g ~info t ~with_end_tac } -| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +END + +VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof +| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] => { - let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in - let parallel = `Yes (solving_tac,anon_abstracting_tac) in let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr } + VtProofStep{ proof_block_detection = pbr } } -> { - let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def + let t, abstract = rm_abstract t in + let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index a6673699af..6bf330c830 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -56,7 +56,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = Genarg.create_arg "withtac" -let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) +let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac) } @@ -111,6 +111,8 @@ END VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" "of" ident(name) ] -> + { try_solve_obligations (Some name) None } | [ "Solve" "Obligations" "with" tactic(t) ] -> { try_solve_obligations None (Some (Tacinterp.interp t)) } | [ "Solve" "Obligations" ] -> diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 09cdc997ab..ee94fd565a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -29,8 +29,6 @@ open Pvernac.Vernac_ open Pltac open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -219,7 +217,7 @@ type binders_argtype = local_binder_expr list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) -let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) +let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders) let () = let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index e51b1f051d..c186a83a5c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ] ; naming_intropattern: - [ [ prefix = pattern_ident -> { IntroFresh prefix } + [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v } | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 47df3ec34f..f42c1f73a3 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -245,7 +245,8 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in + let c, uctx = Constrintern.interp_type env sigma com in + let sigma = Evd.from_ctx uctx in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in add_inversion_lemma ~poly na env sigma c sort bool tac diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 5b5ee64a56..b7b54143df 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -11,39 +11,37 @@ open Pcoq (* Main entry for extensions *) -let simple_tactic = Entry.create "tactic:simple_tactic" - -let make_gen_entry _ name = Entry.create ("tactic:" ^ name) +let simple_tactic = Entry.create "simple_tactic" (* Typically for tactic user extensions *) let open_constr = - make_gen_entry utactic "open_constr" + Entry.create "open_constr" let constr_with_bindings = - make_gen_entry utactic "constr_with_bindings" + Entry.create "constr_with_bindings" let bindings = - make_gen_entry utactic "bindings" + Entry.create "bindings" let hypident = Entry.create "hypident" -let constr_may_eval = make_gen_entry utactic "constr_may_eval" -let constr_eval = make_gen_entry utactic "constr_eval" +let constr_may_eval = Entry.create "constr_may_eval" +let constr_eval = Entry.create "constr_eval" let uconstr = - make_gen_entry utactic "uconstr" + Entry.create "uconstr" let quantified_hypothesis = - make_gen_entry utactic "quantified_hypothesis" -let destruction_arg = make_gen_entry utactic "destruction_arg" -let int_or_var = make_gen_entry utactic "int_or_var" + Entry.create "quantified_hypothesis" +let destruction_arg = Entry.create "destruction_arg" +let int_or_var = Entry.create "int_or_var" let simple_intropattern = - make_gen_entry utactic "simple_intropattern" -let in_clause = make_gen_entry utactic "in_clause" + Entry.create "simple_intropattern" +let in_clause = Entry.create "in_clause" let clause_dft_concl = - make_gen_entry utactic "clause" + Entry.create "clause" (* Main entries for ltac *) -let tactic_arg = Entry.create "tactic:tactic_arg" -let tactic_expr = make_gen_entry utactic "tactic_expr" -let binder_tactic = make_gen_entry utactic "binder_tactic" +let tactic_arg = Entry.create "tactic_arg" +let tactic_expr = Entry.create "tactic_expr" +let binder_tactic = Entry.create "binder_tactic" -let tactic = make_gen_entry utactic "tactic" +let tactic = Entry.create "tactic" (* Main entry for quotations *) let tactic_eoi = eoi_entry tactic diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 85bb901046..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) = | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc env sigma c) | ConstrTerm c when test c -> - h 0 (str "(" ++ prc env sigma c ++ str ")") + h (str "(" ++ prc env sigma c ++ str ")") | ConstrTerm c -> prc env sigma c @@ -1323,7 +1323,7 @@ let () = register_basic_print0 wit_smart_global (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_basic_print0 wit_hyp pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 0dbf16a821..9c15d24dd3 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -146,7 +146,7 @@ let header = fnl () let rec print_node ~filter all_total indent prefix (s, e) = - h 0 ( + h ( padr_with '-' 40 (prefix ^ s ^ " ") ++ padl 7 (format_ratio (e.local /. all_total)) ++ padl 7 (format_ratio (e.total /. all_total)) @@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node = in let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = - h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ + h (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ fnl () ++ header ++ diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 8de6cbc0a6..9bb435f4dc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -498,7 +498,7 @@ let rec decompose_app_rel env evd t = let decompose_app_rel env evd t = let (rel, t1, t2) = decompose_app_rel env evd t in - let ty = Retyping.get_type_of env evd rel in + let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in (rel, t1, t2) @@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation -let resolve_subrelation env avoid car rel sort prf rel' res = +let resolve_subrelation env car rel sort prf rel' res = if Termops.eq_constr (fst res.rew_evars) rel rel' then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in @@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res = rew_prf = RewPrf (rel', appsub); rew_evars = evars } -let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars = +let resolve_morphism env m args args' (b,cstr) evars = let evars, morph_instance, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with | Some i -> i @@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let proof = applist (proj, List.rev projargs) in let newt = applist (m', List.rev typeargs) in match respars with - [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt + [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt | _ -> assert(false) -let apply_constraint env avoid car rel prf cstr res = +let apply_constraint env car rel prf cstr res = match snd cstr with | None -> res - | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res + | Some r -> resolve_subrelation env car rel (fst cstr) prf r res -let coerce env avoid cstr res = +let coerce env cstr res = let evars, (rel, prf) = get_rew_prf res.rew_evars res in let res = { res with rew_evars = evars } in - apply_constraint env avoid res.rew_car rel prf cstr res + apply_constraint env res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in @@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy = then List.mem occ occs else not (List.mem occ occs) in - { strategy = fun { state = occ ; env ; unfresh ; + { strategy = fun { state = occ ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with @@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let res = Success (coerce env unfresh cstr res) in + let res = Success (coerce env cstr res) in (occ, res) } @@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | None -> false | Some r -> not (is_rew_cast r.rew_prf)) args' then - let evars', prf, car, rel, c1, c2 = - resolve_morphism env unfresh t m args args' (prop, cstr') evars' + let evars', prf, car, rel, c2 = + resolve_morphism env m args args' (prop, cstr') evars' in - let res = { rew_car = ty; rew_from = c1; + let res = { rew_car = ty; rew_from = t; rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = evars' } in Success res @@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let res = match prf with | RewPrf (rel, prf) -> - Success (apply_constraint env unfresh res.rew_car + Success (apply_constraint env res.rew_car rel prf (prop,cstr) res) | _ -> Success res in state, res @@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> res in state, res - (* if x' = None && flags.under_lambdas then *) - (* let lam = mkLambda (n, x, b) in *) - (* let lam', occ = aux env lam occ None in *) - (* let res = *) - (* match lam' with *) - (* | None -> None *) - (* | Some (prf, (car, rel, c1, c2)) -> *) - (* Some (resolve_morphism env sigma t *) - (* ~fnewt:unfold_all *) - (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *) - (* cstr evars) *) - (* in res, occ *) - (* else *) - | Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = @@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing dependent relations and using projections to get them out. *) - (* | Lambda (n, t, b) when flags.under_lambdas -> *) - (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *) - (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *) - (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *) - (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *) - (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *) - (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *) - (* (match b' with *) - (* | Some (Some r) -> *) - (* let prf = match r.rew_prf with *) - (* | RewPrf (rel, prf) -> *) - (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *) - (* let prf = mkLambda (n', t, prf) in *) - (* RewPrf (rel, prf) *) - (* | x -> x *) - (* in *) - (* Some (Some { r with *) - (* rew_prf = prf; *) - (* rew_car = mkProd (n, t, r.rew_car); *) - (* rew_from = mkLambda(n, t, r.rew_from); *) - (* rew_to = mkLambda (n, t, r.rew_to) }) *) - (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh = match n'.binder_name with + | Anonymous -> unfresh + | Name id -> Id.Set.add id unfresh + in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Success r -> let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in - state, Success (coerce env unfresh (prop,cstr) res) + state, Success (coerce env (prop,cstr) res) | Fail | Identity -> if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in @@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> Success (coerce env unfresh (prop,cstr) r) + | Success r -> Success (coerce env (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail @@ -2144,7 +2112,7 @@ let setoid_proof ty fn fallback = let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel - with e -> + with e when CErrors.noncritical e -> (* XXX what is the right test here as to whether e can be converted ? *) let e, info = Exninfo.capture e in Proofview.tclZERO ~info e diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index f7037176d2..ee28229cb7 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v = match out_gen (topwit wit_intro_pattern) v with | { CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + else if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () | Some c -> @@ -184,8 +184,8 @@ let id_of_name = function | Some (IntroNaming (IntroIdentifier id)) -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () @@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v = match is_intro_pattern v with | Some pat -> pat | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with | Some c when isVar sigma c -> @@ -259,8 +259,8 @@ let coerce_to_constr env v = ([], c) else if has_type v (topwit wit_constr_under_binders) then out_gen (topwit wit_constr_under_binders) v - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in (try [], constr_of_id env id with Not_found -> fail ()) else fail () @@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then @@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if is_variable env id then id else fail () else match Value.to_constr v with | Some c when isVar sigma c -> destVar sigma c @@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v = | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id | Some _ -> raise (CannotCoerceTo "a quantified hypothesis") | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in NamedHyp id else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 759cf67d5e..6823b6411f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -216,7 +216,9 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> user_err Pp.(str ("Unknown entry "^s^".")) + | None -> + if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *) + else user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> @@ -866,7 +868,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = let () = Pcoq.register_grammar wit e in e | Vernacextend.Arg_rules rules -> - let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in e in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index dea216045e..9c3b05fdf1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -835,7 +835,7 @@ let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; - Genintern.register_intern0 wit_var (lift intern_hyp); + Genintern.register_intern0 wit_hyp (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ff6a36a049..12bfb4d09e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg = match v with | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id | _ -> error () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in try_cast_id id else if has_type v (topwit wit_int) then keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) @@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun - with Not_found -> in_gen (topwit wit_var) id + with Not_found -> in_gen (topwit wit_hyp) id in let open Ftactic in force_vrec ist v >>= begin fun v -> @@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in (* Ad-hoc handling of some types. *) let tag = genarg_tag x in - if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then + if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then interp_genarg_var_list ist x else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then interp_genarg_constr_list ist x @@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in let lc = interp_hyp_list ist env sigma lc in - let lc = in_list (val_tag wit_var) lc in + let lc = in_list (val_tag wit_hyp) lc in Ftactic.return lc end @@ -1996,16 +1996,20 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t +(* MUST be marshallable! *) +type tactic_expr = { + global: bool; + ast: Tacexpr.raw_tactic_expr; +} + (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) -let hide_interp global t ot = +let hide_interp {global;ast} = let hide_interp env = let ist = Genintern.empty_glob_sign env in - let te = intern_pure_tactic ist t in + let te = intern_pure_tactic ist ast in let t = eval_tactic te in - match ot with - | None -> t - | Some t' -> Tacticals.New.tclTHEN t t' + t in if global then Proofview.tclENV >>= fun env -> @@ -2015,6 +2019,8 @@ let hide_interp global t ot = hide_interp (Proofview.Goal.env gl) end +let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp + (***************************************************************************) (** Register standard arguments *) @@ -2090,7 +2096,7 @@ let () = register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); - register_interp0 wit_var (lift interp_hyp); + register_interp0 wit_hyp (lift interp_hyp); register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index cbb17bf0fa..01d7306c9d 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) +type tactic_expr = { + global: bool; + ast: Tacexpr.raw_tactic_expr; +} -val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic +val hide_interp : tactic_expr ComTactic.tactic_interpreter (** Internals that can be useful for syntax extensions. *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fd869b225f..ec44ae4698 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -282,7 +282,7 @@ let () = Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); - Genintern.register_subst0 wit_var (fun _ v -> v); + Genintern.register_subst0 wit_hyp (fun _ v -> v); Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"]; Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern; Genintern.register_subst0 wit_tactic subst_tactic; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d2c49c4432..542b99075d 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -134,166 +134,161 @@ let selecti s m = *) (** - * MODULE END: M - *) -module M = struct - (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v *) - let constr_of_ref str = - EConstr.of_constr - (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) - - let coq_and = lazy (constr_of_ref "core.and.type") - let coq_or = lazy (constr_of_ref "core.or.type") - let coq_not = lazy (constr_of_ref "core.not.type") - let coq_iff = lazy (constr_of_ref "core.iff.type") - let coq_True = lazy (constr_of_ref "core.True.type") - let coq_False = lazy (constr_of_ref "core.False.type") - let coq_bool = lazy (constr_of_ref "core.bool.type") - let coq_true = lazy (constr_of_ref "core.bool.true") - let coq_false = lazy (constr_of_ref "core.bool.false") - let coq_andb = lazy (constr_of_ref "core.bool.andb") - let coq_orb = lazy (constr_of_ref "core.bool.orb") - let coq_implb = lazy (constr_of_ref "core.bool.implb") - let coq_eqb = lazy (constr_of_ref "core.bool.eqb") - let coq_negb = lazy (constr_of_ref "core.bool.negb") - let coq_cons = lazy (constr_of_ref "core.list.cons") - let coq_nil = lazy (constr_of_ref "core.list.nil") - let coq_list = lazy (constr_of_ref "core.list.type") - let coq_O = lazy (constr_of_ref "num.nat.O") - let coq_S = lazy (constr_of_ref "num.nat.S") - let coq_nat = lazy (constr_of_ref "num.nat.type") - let coq_unit = lazy (constr_of_ref "core.unit.type") - - (* let coq_option = lazy (init_constant "option")*) - let coq_None = lazy (constr_of_ref "core.option.None") - let coq_tt = lazy (constr_of_ref "core.unit.tt") - let coq_Inl = lazy (constr_of_ref "core.sum.inl") - let coq_Inr = lazy (constr_of_ref "core.sum.inr") - let coq_N0 = lazy (constr_of_ref "num.N.N0") - let coq_Npos = lazy (constr_of_ref "num.N.Npos") - let coq_xH = lazy (constr_of_ref "num.pos.xH") - let coq_xO = lazy (constr_of_ref "num.pos.xO") - let coq_xI = lazy (constr_of_ref "num.pos.xI") - let coq_Z = lazy (constr_of_ref "num.Z.type") - let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") - let coq_POS = lazy (constr_of_ref "num.Z.Zpos") - let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") - let coq_Q = lazy (constr_of_ref "rat.Q.type") - let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") - let coq_R = lazy (constr_of_ref "reals.R.type") - let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") - let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") - let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") - let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") - let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") - let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") - let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") - let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") - let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") - let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") - let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") - let coq_R0 = lazy (constr_of_ref "reals.R.R0") - let coq_R1 = lazy (constr_of_ref "reals.R.R1") - let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") - let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") - let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") - let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") - let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") - let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") - let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") - let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") - let coq_Zgt = lazy (constr_of_ref "num.Z.gt") - let coq_Zge = lazy (constr_of_ref "num.Z.ge") - let coq_Zle = lazy (constr_of_ref "num.Z.le") - let coq_Zlt = lazy (constr_of_ref "num.Z.lt") - let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") - let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") - let coq_Zleb = lazy (constr_of_ref "num.Z.leb") - let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") - let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") - let coq_eq = lazy (constr_of_ref "core.eq.type") - let coq_Zplus = lazy (constr_of_ref "num.Z.add") - let coq_Zminus = lazy (constr_of_ref "num.Z.sub") - let coq_Zopp = lazy (constr_of_ref "num.Z.opp") - let coq_Zmult = lazy (constr_of_ref "num.Z.mul") - let coq_Zpower = lazy (constr_of_ref "num.Z.pow") - let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") - let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") - let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") - let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") - let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") - let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") - let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") - let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") - let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") - let coq_Rge = lazy (constr_of_ref "reals.R.Rge") - let coq_Rle = lazy (constr_of_ref "reals.R.Rle") - let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") - let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") - let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") - let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") - let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") - let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") - let coq_Rpower = lazy (constr_of_ref "reals.R.pow") - let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") - let coq_IZR = lazy (constr_of_ref "reals.R.IZR") - let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") - let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") - let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") - let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") - let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") - let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") - let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") - let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") - let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") - let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") - let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") - let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") - let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") - let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") - let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") - let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") - let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") - let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") - let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") - let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") - let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") - let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") - let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") - let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") - - (* let coq_GT = lazy (m_constant "GT")*) - - let coq_DeclaredConstant = - lazy (constr_of_ref "micromega.DeclaredConstant.type") - - let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") - let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") - let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") - let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") - let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") - let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") - let coq_X = lazy (constr_of_ref "micromega.GFormula.X") - let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") - let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") - let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") - let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") - let coq_eKind = lazy (constr_of_ref "micromega.eKind") - - (** +let constr_of_ref str = + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) + +let coq_and = lazy (constr_of_ref "core.and.type") +let coq_or = lazy (constr_of_ref "core.or.type") +let coq_not = lazy (constr_of_ref "core.not.type") +let coq_iff = lazy (constr_of_ref "core.iff.type") +let coq_True = lazy (constr_of_ref "core.True.type") +let coq_False = lazy (constr_of_ref "core.False.type") +let coq_bool = lazy (constr_of_ref "core.bool.type") +let coq_true = lazy (constr_of_ref "core.bool.true") +let coq_false = lazy (constr_of_ref "core.bool.false") +let coq_andb = lazy (constr_of_ref "core.bool.andb") +let coq_orb = lazy (constr_of_ref "core.bool.orb") +let coq_implb = lazy (constr_of_ref "core.bool.implb") +let coq_eqb = lazy (constr_of_ref "core.bool.eqb") +let coq_negb = lazy (constr_of_ref "core.bool.negb") +let coq_cons = lazy (constr_of_ref "core.list.cons") +let coq_nil = lazy (constr_of_ref "core.list.nil") +let coq_list = lazy (constr_of_ref "core.list.type") +let coq_O = lazy (constr_of_ref "num.nat.O") +let coq_S = lazy (constr_of_ref "num.nat.S") +let coq_nat = lazy (constr_of_ref "num.nat.type") +let coq_unit = lazy (constr_of_ref "core.unit.type") + +(* let coq_option = lazy (init_constant "option")*) +let coq_None = lazy (constr_of_ref "core.option.None") +let coq_tt = lazy (constr_of_ref "core.unit.tt") +let coq_Inl = lazy (constr_of_ref "core.sum.inl") +let coq_Inr = lazy (constr_of_ref "core.sum.inr") +let coq_N0 = lazy (constr_of_ref "num.N.N0") +let coq_Npos = lazy (constr_of_ref "num.N.Npos") +let coq_xH = lazy (constr_of_ref "num.pos.xH") +let coq_xO = lazy (constr_of_ref "num.pos.xO") +let coq_xI = lazy (constr_of_ref "num.pos.xI") +let coq_Z = lazy (constr_of_ref "num.Z.type") +let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") +let coq_POS = lazy (constr_of_ref "num.Z.Zpos") +let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") +let coq_Q = lazy (constr_of_ref "rat.Q.type") +let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") +let coq_R = lazy (constr_of_ref "reals.R.type") +let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") +let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") +let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") +let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") +let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") +let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") +let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") +let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") +let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") +let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") +let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") +let coq_R0 = lazy (constr_of_ref "reals.R.R0") +let coq_R1 = lazy (constr_of_ref "reals.R.R1") +let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") +let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") +let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") +let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") +let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") +let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") +let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") +let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") +let coq_Zgt = lazy (constr_of_ref "num.Z.gt") +let coq_Zge = lazy (constr_of_ref "num.Z.ge") +let coq_Zle = lazy (constr_of_ref "num.Z.le") +let coq_Zlt = lazy (constr_of_ref "num.Z.lt") +let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") +let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") +let coq_Zleb = lazy (constr_of_ref "num.Z.leb") +let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") +let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") +let coq_eq = lazy (constr_of_ref "core.eq.type") +let coq_Zplus = lazy (constr_of_ref "num.Z.add") +let coq_Zminus = lazy (constr_of_ref "num.Z.sub") +let coq_Zopp = lazy (constr_of_ref "num.Z.opp") +let coq_Zmult = lazy (constr_of_ref "num.Z.mul") +let coq_Zpower = lazy (constr_of_ref "num.Z.pow") +let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") +let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") +let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") +let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") +let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") +let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") +let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") +let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") +let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") +let coq_Rge = lazy (constr_of_ref "reals.R.Rge") +let coq_Rle = lazy (constr_of_ref "reals.R.Rle") +let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") +let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") +let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") +let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") +let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") +let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") +let coq_Rpower = lazy (constr_of_ref "reals.R.pow") +let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") +let coq_IZR = lazy (constr_of_ref "reals.R.IZR") +let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") +let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") +let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") +let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") +let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") +let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") +let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") +let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") +let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") +let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") +let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") +let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") +let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") +let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") +let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") +let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") +let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") +let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") +let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") +let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") +let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") +let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") +let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") +let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") + +(* let coq_GT = lazy (m_constant "GT")*) + +let coq_DeclaredConstant = + lazy (constr_of_ref "micromega.DeclaredConstant.type") + +let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") +let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") +let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") +let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") +let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") +let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") +let coq_X = lazy (constr_of_ref "micromega.GFormula.X") +let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") +let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") +let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") +let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") +let coq_eKind = lazy (constr_of_ref "micromega.eKind") + +(** * Initialization : a few Caml symbols are derived from other libraries; * QMicromega, ZArithRing, RingMicromega. *) - let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") - let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") - let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") +let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") +let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") +let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") - (** +(** * Parsing and dumping : transformation functions between Caml and Coq * data-structures. * @@ -302,1048 +297,1018 @@ module M = struct * pp_* functions pretty-print Coq terms. *) - exception ParseError +exception ParseError - (* A simple but useful getter function *) +(* A simple but useful getter function *) - let get_left_construct sigma term = - match EConstr.kind sigma term with - | Construct ((_, i), _) -> (i, [||]) - | App (l, rst) -> ( - match EConstr.kind sigma l with - | Construct ((_, i), _) -> (i, rst) - | _ -> raise ParseError ) - | _ -> raise ParseError +let get_left_construct sigma term = + match EConstr.kind sigma term with + | Construct ((_, i), _) -> (i, [||]) + | App (l, rst) -> ( + match EConstr.kind sigma l with + | Construct ((_, i), _) -> (i, rst) + | _ -> raise ParseError ) + | _ -> raise ParseError - (* Access the Micromega module *) +(* Access the Micromega module *) - (* parse/dump/print from numbers up to expressions and formulas *) +(* parse/dump/print from numbers up to expressions and formulas *) - let rec parse_nat sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.O - | 2 -> Mc.S (parse_nat sigma c.(0)) - | i -> raise ParseError +let rec parse_nat sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.O + | 2 -> Mc.S (parse_nat sigma c.(0)) + | i -> raise ParseError - let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) +let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) - let rec dump_nat x = - match x with - | Mc.O -> Lazy.force coq_O - | Mc.S p -> EConstr.mkApp (Lazy.force coq_S, [|dump_nat p|]) +let rec dump_nat x = + match x with + | Mc.O -> Lazy.force coq_O + | Mc.S p -> EConstr.mkApp (Lazy.force coq_S, [|dump_nat p|]) - let rec parse_positive sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.XI (parse_positive sigma c.(0)) - | 2 -> Mc.XO (parse_positive sigma c.(0)) - | 3 -> Mc.XH - | i -> raise ParseError +let rec parse_positive sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.XI (parse_positive sigma c.(0)) + | 2 -> Mc.XO (parse_positive sigma c.(0)) + | 3 -> Mc.XH + | i -> raise ParseError - let rec dump_positive x = - match x with - | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> EConstr.mkApp (Lazy.force coq_xO, [|dump_positive p|]) - | Mc.XI p -> EConstr.mkApp (Lazy.force coq_xI, [|dump_positive p|]) +let rec dump_positive x = + match x with + | Mc.XH -> Lazy.force coq_xH + | Mc.XO p -> EConstr.mkApp (Lazy.force coq_xO, [|dump_positive p|]) + | Mc.XI p -> EConstr.mkApp (Lazy.force coq_xI, [|dump_positive p|]) - let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) +let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - let dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> EConstr.mkApp (Lazy.force coq_Npos, [|dump_positive p|]) +let dump_n x = + match x with + | Mc.N0 -> Lazy.force coq_N0 + | Mc.Npos p -> EConstr.mkApp (Lazy.force coq_Npos, [|dump_positive p|]) - (** [is_ground_term env sigma term] holds if the term [term] +(** [is_ground_term env sigma term] holds if the term [term] is an instance of the typeclass [DeclConstant.GT term] i.e. built from user-defined constants and functions. NB: This mechanism can be used to customise the reification process to decide what to consider as a constant (see [parse_constant]) *) - let is_declared_term env evd t = - match EConstr.kind evd t with - | Const _ | Construct _ -> ( - (* Restrict typeclass resolution to trivial cases *) - let typ = Retyping.get_type_of env evd t in - try - ignore - (Typeclasses.resolve_one_typeclass env evd - (EConstr.mkApp (Lazy.force coq_DeclaredConstant, [|typ; t|]))); - true - with Not_found -> false ) - | _ -> false - - let rec is_ground_term env evd term = - match EConstr.kind evd term with - | App (c, args) -> - is_declared_term env evd c && Array.for_all (is_ground_term env evd) args - | Const _ | Construct _ -> is_declared_term env evd term - | _ -> false - - let parse_z sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive sigma c.(0)) - | 3 -> Mc.Zneg (parse_positive sigma c.(0)) - | i -> raise ParseError - - let dump_z x = - match x with - | Mc.Z0 -> Lazy.force coq_ZERO - | Mc.Zpos p -> EConstr.mkApp (Lazy.force coq_POS, [|dump_positive p|]) - | Mc.Zneg p -> EConstr.mkApp (Lazy.force coq_NEG, [|dump_positive p|]) - - let pp_z o x = - Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x)) - - let dump_q q = +let is_declared_term env evd t = + match EConstr.kind evd t with + | Const _ | Construct _ -> ( + (* Restrict typeclass resolution to trivial cases *) + let typ = Retyping.get_type_of env evd t in + try + ignore + (Typeclasses.resolve_one_typeclass env evd + (EConstr.mkApp (Lazy.force coq_DeclaredConstant, [|typ; t|]))); + true + with Not_found -> false ) + | _ -> false + +let rec is_ground_term env evd term = + match EConstr.kind evd term with + | App (c, args) -> + is_declared_term env evd c && Array.for_all (is_ground_term env evd) args + | Const _ | Construct _ -> is_declared_term env evd term + | _ -> false + +let parse_z sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.Z0 + | 2 -> Mc.Zpos (parse_positive sigma c.(0)) + | 3 -> Mc.Zneg (parse_positive sigma c.(0)) + | i -> raise ParseError + +let dump_z x = + match x with + | Mc.Z0 -> Lazy.force coq_ZERO + | Mc.Zpos p -> EConstr.mkApp (Lazy.force coq_POS, [|dump_positive p|]) + | Mc.Zneg p -> EConstr.mkApp (Lazy.force coq_NEG, [|dump_positive p|]) + +let pp_z o x = + Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x)) + +let dump_q q = + EConstr.mkApp + ( Lazy.force coq_Qmake + , [|dump_z q.Micromega.qnum; dump_positive q.Micromega.qden|] ) + +let parse_q sigma term = + match EConstr.kind sigma term with + | App (c, args) -> + if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then + {Mc.qnum = parse_z sigma args.(0); Mc.qden = parse_positive sigma args.(1)} + else raise ParseError + | _ -> raise ParseError + +let rec pp_Rcst o cst = + match cst with + | Mc.C0 -> output_string o "C0" + | Mc.C1 -> output_string o "C1" + | Mc.CQ q -> output_string o "CQ _" + | Mc.CZ z -> pp_z o z + | Mc.CPlus (x, y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y + | Mc.CMinus (x, y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y + | Mc.CMult (x, y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y + | Mc.CPow (x, y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x + | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t + | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t + +let rec dump_Rcst cst = + match cst with + | Mc.C0 -> Lazy.force coq_C0 + | Mc.C1 -> Lazy.force coq_C1 + | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_CQ, [|dump_q q|]) + | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_CZ, [|dump_z z|]) + | Mc.CPlus (x, y) -> + EConstr.mkApp (Lazy.force coq_CPlus, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CMinus (x, y) -> + EConstr.mkApp (Lazy.force coq_CMinus, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CMult (x, y) -> + EConstr.mkApp (Lazy.force coq_CMult, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CPow (x, y) -> EConstr.mkApp - ( Lazy.force coq_Qmake - , [|dump_z q.Micromega.qnum; dump_positive q.Micromega.qden|] ) - - let parse_q sigma term = - match EConstr.kind sigma term with - | App (c, args) -> - if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then - { Mc.qnum = parse_z sigma args.(0) - ; Mc.qden = parse_positive sigma args.(1) } - else raise ParseError - | _ -> raise ParseError + ( Lazy.force coq_CPow + , [| dump_Rcst x + ; ( match y with + | Mc.Inl z -> + EConstr.mkApp + ( Lazy.force coq_Inl + , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_z z|] ) + | Mc.Inr n -> + EConstr.mkApp + ( Lazy.force coq_Inr + , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_nat n|] ) ) |] ) + | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_CInv, [|dump_Rcst t|]) + | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_COpp, [|dump_Rcst t|]) + +let rec dump_list typ dump_elt l = + match l with + | [] -> EConstr.mkApp (Lazy.force coq_nil, [|typ|]) + | e :: l -> + EConstr.mkApp + (Lazy.force coq_cons, [|typ; dump_elt e; dump_list typ dump_elt l|]) - let rec pp_Rcst o cst = - match cst with - | Mc.C0 -> output_string o "C0" - | Mc.C1 -> output_string o "C1" - | Mc.CQ q -> output_string o "CQ _" - | Mc.CZ z -> pp_z o z - | Mc.CPlus (x, y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y - | Mc.CMinus (x, y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y - | Mc.CMult (x, y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y - | Mc.CPow (x, y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x - | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t - | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t - - let rec dump_Rcst cst = - match cst with - | Mc.C0 -> Lazy.force coq_C0 - | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_CQ, [|dump_q q|]) - | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_CZ, [|dump_z z|]) - | Mc.CPlus (x, y) -> - EConstr.mkApp (Lazy.force coq_CPlus, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CMinus (x, y) -> - EConstr.mkApp (Lazy.force coq_CMinus, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CMult (x, y) -> - EConstr.mkApp (Lazy.force coq_CMult, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CPow (x, y) -> - EConstr.mkApp - ( Lazy.force coq_CPow - , [| dump_Rcst x - ; ( match y with - | Mc.Inl z -> - EConstr.mkApp - ( Lazy.force coq_Inl - , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_z z|] ) - | Mc.Inr n -> - EConstr.mkApp - ( Lazy.force coq_Inr - , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_nat n|] ) ) |] - ) - | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_CInv, [|dump_Rcst t|]) - | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_COpp, [|dump_Rcst t|]) - - let rec dump_list typ dump_elt l = +let pp_list op cl elt o l = + let rec _pp o l = match l with - | [] -> EConstr.mkApp (Lazy.force coq_nil, [|typ|]) - | e :: l -> - EConstr.mkApp - (Lazy.force coq_cons, [|typ; dump_elt e; dump_list typ dump_elt l|]) - - let pp_list op cl elt o l = - let rec _pp o l = - match l with - | [] -> () - | [e] -> Printf.fprintf o "%a" elt e - | e :: l -> Printf.fprintf o "%a ,%a" elt e _pp l - in - Printf.fprintf o "%s%a%s" op _pp l cl + | [] -> () + | [e] -> Printf.fprintf o "%a" elt e + | e :: l -> Printf.fprintf o "%a ,%a" elt e _pp l + in + Printf.fprintf o "%s%a%s" op _pp l cl - let dump_var = dump_positive +let dump_var = dump_positive - let dump_expr typ dump_z e = - let rec dump_expr e = - match e with - | Mc.PEX n -> EConstr.mkApp (Lazy.force coq_PEX, [|typ; dump_var n|]) - | Mc.PEc z -> EConstr.mkApp (Lazy.force coq_PEc, [|typ; dump_z z|]) - | Mc.PEadd (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEadd, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEsub (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEsub, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp (Lazy.force coq_PEopp, [|typ; dump_expr e|]) - | Mc.PEmul (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEmul, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEpow (e, n) -> - EConstr.mkApp (Lazy.force coq_PEpow, [|typ; dump_expr e; dump_n n|]) - in - dump_expr e +let dump_expr typ dump_z e = + let rec dump_expr e = + match e with + | Mc.PEX n -> EConstr.mkApp (Lazy.force coq_PEX, [|typ; dump_var n|]) + | Mc.PEc z -> EConstr.mkApp (Lazy.force coq_PEc, [|typ; dump_z z|]) + | Mc.PEadd (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEadd, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEsub (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEsub, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp (Lazy.force coq_PEopp, [|typ; dump_expr e|]) + | Mc.PEmul (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEmul, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEpow (e, n) -> + EConstr.mkApp (Lazy.force coq_PEpow, [|typ; dump_expr e; dump_n n|]) + in + dump_expr e - let dump_pol typ dump_c e = - let rec dump_pol e = - match e with - | Mc.Pc n -> EConstr.mkApp (Lazy.force coq_Pc, [|typ; dump_c n|]) - | Mc.Pinj (p, pol) -> - EConstr.mkApp - (Lazy.force coq_Pinj, [|typ; dump_positive p; dump_pol pol|]) - | Mc.PX (pol1, p, pol2) -> - EConstr.mkApp - ( Lazy.force coq_PX - , [|typ; dump_pol pol1; dump_positive p; dump_pol pol2|] ) - in - dump_pol e - - let pp_pol pp_c o e = - let rec pp_pol o e = - match e with - | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n - | Mc.Pinj (p, pol) -> - Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol - | Mc.PX (pol1, p, pol2) -> - Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 - in - pp_pol o e - - (* let pp_clause pp_c o (f: 'cst clause) = - List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) - - let pp_clause_tag o (f : 'cst clause) = - List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f - - (* let pp_cnf pp_c o (f:'cst cnf) = - List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) - - let pp_cnf_tag o (f : 'cst cnf) = - List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f - - let dump_psatz typ dump_z e = - let z = Lazy.force typ in - let rec dump_cone e = - match e with - | Mc.PsatzIn n -> EConstr.mkApp (Lazy.force coq_PsatzIn, [|z; dump_nat n|]) - | Mc.PsatzMulC (e, c) -> - EConstr.mkApp - (Lazy.force coq_PsatzMultC, [|z; dump_pol z dump_z e; dump_cone c|]) - | Mc.PsatzSquare e -> - EConstr.mkApp (Lazy.force coq_PsatzSquare, [|z; dump_pol z dump_z e|]) - | Mc.PsatzAdd (e1, e2) -> - EConstr.mkApp - (Lazy.force coq_PsatzAdd, [|z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE (e1, e2) -> - EConstr.mkApp - (Lazy.force coq_PsatzMulE, [|z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> EConstr.mkApp (Lazy.force coq_PsatzC, [|z; dump_z p|]) - | Mc.PsatzZ -> EConstr.mkApp (Lazy.force coq_PsatzZ, [|z|]) - in - dump_cone e - - let pp_psatz pp_z o e = - let rec pp_cone o e = - match e with - | Mc.PsatzIn n -> Printf.fprintf o "(In %a)%%nat" pp_nat n - | Mc.PsatzMulC (e, c) -> - Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c - | Mc.PsatzSquare e -> Printf.fprintf o "(%a^2)" (pp_pol pp_z) e - | Mc.PsatzAdd (e1, e2) -> - Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzMulE (e1, e2) -> - Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzC p -> Printf.fprintf o "(%a)%%positive" pp_z p - | Mc.PsatzZ -> Printf.fprintf o "0" - in - pp_cone o e +let dump_pol typ dump_c e = + let rec dump_pol e = + match e with + | Mc.Pc n -> EConstr.mkApp (Lazy.force coq_Pc, [|typ; dump_c n|]) + | Mc.Pinj (p, pol) -> + EConstr.mkApp (Lazy.force coq_Pinj, [|typ; dump_positive p; dump_pol pol|]) + | Mc.PX (pol1, p, pol2) -> + EConstr.mkApp + ( Lazy.force coq_PX + , [|typ; dump_pol pol1; dump_positive p; dump_pol pol2|] ) + in + dump_pol e - let dump_op = function - | Mc.OpEq -> Lazy.force coq_OpEq - | Mc.OpNEq -> Lazy.force coq_OpNEq - | Mc.OpLe -> Lazy.force coq_OpLe - | Mc.OpGe -> Lazy.force coq_OpGe - | Mc.OpGt -> Lazy.force coq_OpGt - | Mc.OpLt -> Lazy.force coq_OpLt +let pp_pol pp_c o e = + let rec pp_pol o e = + match e with + | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n + | Mc.Pinj (p, pol) -> + Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol + | Mc.PX (pol1, p, pol2) -> + Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 + in + pp_pol o e - let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} = - EConstr.mkApp - ( Lazy.force coq_Build - , [| typ - ; dump_expr typ dump_constant e1 - ; dump_op o - ; dump_expr typ dump_constant e2 |] ) +(* let pp_clause pp_c o (f: 'cst clause) = + List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) - let assoc_const sigma x l = - try - snd - (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with Not_found -> raise ParseError - - let zop_table_prop = - [ (coq_Zgt, Mc.OpGt) - ; (coq_Zge, Mc.OpGe) - ; (coq_Zlt, Mc.OpLt) - ; (coq_Zle, Mc.OpLe) ] - - let zop_table_bool = - [ (coq_Zgtb, Mc.OpGt) - ; (coq_Zgeb, Mc.OpGe) - ; (coq_Zltb, Mc.OpLt) - ; (coq_Zleb, Mc.OpLe) - ; (coq_Zeqb, Mc.OpEq) ] - - let rop_table_prop = - [ (coq_Rgt, Mc.OpGt) - ; (coq_Rge, Mc.OpGe) - ; (coq_Rlt, Mc.OpLt) - ; (coq_Rle, Mc.OpLe) ] - - let rop_table_bool = [] - - let qop_table_prop = - [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] - - let qop_table_bool = [] - - type gl = {env : Environ.env; sigma : Evd.evar_map} - - let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2 - - let parse_operator table_prop table_bool has_equality typ gl k (op, args) = - let sigma = gl.sigma in - match args with - | [|a1; a2|] -> - ( assoc_const sigma op - (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) - , a1 - , a2 ) - | [|ty; a1; a2|] -> - if - has_equality - && EConstr.eq_constr sigma op (Lazy.force coq_eq) - && is_convertible gl ty (Lazy.force typ) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> raise ParseError +let pp_clause_tag o (f : 'cst clause) = + List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f - let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z - let parse_rop = parse_operator rop_table_prop [] true coq_R - let parse_qop = parse_operator qop_table_prop [] false coq_R +(* let pp_cnf pp_c o (f:'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) - type 'a op = - | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) - | Opp - | Power - | Ukn of string +let pp_cnf_tag o (f : 'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f - let assoc_ops sigma x l = - try - snd - (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with Not_found -> Ukn "Oups" +let dump_psatz typ dump_z e = + let z = Lazy.force typ in + let rec dump_cone e = + match e with + | Mc.PsatzIn n -> EConstr.mkApp (Lazy.force coq_PsatzIn, [|z; dump_nat n|]) + | Mc.PsatzMulC (e, c) -> + EConstr.mkApp + (Lazy.force coq_PsatzMultC, [|z; dump_pol z dump_z e; dump_cone c|]) + | Mc.PsatzSquare e -> + EConstr.mkApp (Lazy.force coq_PsatzSquare, [|z; dump_pol z dump_z e|]) + | Mc.PsatzAdd (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PsatzAdd, [|z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzMulE (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PsatzMulE, [|z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzC p -> EConstr.mkApp (Lazy.force coq_PsatzC, [|z; dump_z p|]) + | Mc.PsatzZ -> EConstr.mkApp (Lazy.force coq_PsatzZ, [|z|]) + in + dump_cone e - (** +let pp_psatz pp_z o e = + let rec pp_cone o e = + match e with + | Mc.PsatzIn n -> Printf.fprintf o "(In %a)%%nat" pp_nat n + | Mc.PsatzMulC (e, c) -> + Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c + | Mc.PsatzSquare e -> Printf.fprintf o "(%a^2)" (pp_pol pp_z) e + | Mc.PsatzAdd (e1, e2) -> + Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 + | Mc.PsatzMulE (e1, e2) -> + Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 + | Mc.PsatzC p -> Printf.fprintf o "(%a)%%positive" pp_z p + | Mc.PsatzZ -> Printf.fprintf o "0" + in + pp_cone o e + +let dump_op = function + | Mc.OpEq -> Lazy.force coq_OpEq + | Mc.OpNEq -> Lazy.force coq_OpNEq + | Mc.OpLe -> Lazy.force coq_OpLe + | Mc.OpGe -> Lazy.force coq_OpGe + | Mc.OpGt -> Lazy.force coq_OpGt + | Mc.OpLt -> Lazy.force coq_OpLt + +let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} = + EConstr.mkApp + ( Lazy.force coq_Build + , [| typ + ; dump_expr typ dump_constant e1 + ; dump_op o + ; dump_expr typ dump_constant e2 |] ) + +let assoc_const sigma x l = + try + snd (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) + with Not_found -> raise ParseError + +let zop_table_prop = + [ (coq_Zgt, Mc.OpGt) + ; (coq_Zge, Mc.OpGe) + ; (coq_Zlt, Mc.OpLt) + ; (coq_Zle, Mc.OpLe) ] + +let zop_table_bool = + [ (coq_Zgtb, Mc.OpGt) + ; (coq_Zgeb, Mc.OpGe) + ; (coq_Zltb, Mc.OpLt) + ; (coq_Zleb, Mc.OpLe) + ; (coq_Zeqb, Mc.OpEq) ] + +let rop_table_prop = + [ (coq_Rgt, Mc.OpGt) + ; (coq_Rge, Mc.OpGe) + ; (coq_Rlt, Mc.OpLt) + ; (coq_Rle, Mc.OpLe) ] + +let rop_table_bool = [] +let qop_table_prop = [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] +let qop_table_bool = [] + +type gl = Environ.env * Evd.evar_map + +let is_convertible env sigma t1 t2 = Reductionops.is_conv env sigma t1 t2 + +let parse_operator table_prop table_bool has_equality typ (env, sigma) k + (op, args) = + match args with + | [|a1; a2|] -> + ( assoc_const sigma op + (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) + , a1 + , a2 ) + | [|ty; a1; a2|] -> + if + has_equality + && EConstr.eq_constr sigma op (Lazy.force coq_eq) + && is_convertible env sigma ty (Lazy.force typ) + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> raise ParseError + +let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z +let parse_rop = parse_operator rop_table_prop [] true coq_R +let parse_qop = parse_operator qop_table_prop [] false coq_R + +type 'a op = + | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) + | Opp + | Power + | Ukn of string + +let assoc_ops sigma x l = + try + snd (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) + with Not_found -> Ukn "Oups" + +(** * MODULE: Env is for environment. *) - module Env = struct - type t = - { vars : (EConstr.t * Mc.kind) list - ; (* The list represents a mapping from EConstr.t to indexes. *) - gl : gl - (* The evar_map may be updated due to unification of universes *) } - - let empty gl = {vars = []; gl} - - (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) - let eq_constr gl x y = - let evd = gl.sigma in - match EConstr.eq_constr_universes_proj gl.env evd x y with - | Some csts -> ( - let csts = - UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts - in - match Evd.add_constraints evd csts with - | evd -> Some {gl with sigma = evd} - | exception Univ.UniverseInconsistency _ -> None ) - | None -> None - - let compute_rank_add env v is_prop = - let rec _add gl vars n v = - match vars with - | [] -> (gl, [(v, is_prop)], n) - | (e, b) :: l -> ( - match eq_constr gl e v with - | Some gl' -> (gl', vars, n) - | None -> - let gl, l', n = _add gl l (n + 1) v in - (gl, (e, b) :: l', n) ) - in - let gl', vars', n = _add env.gl env.vars 1 v in - ({vars = vars'; gl = gl'}, CamlToCoq.positive n) - - let get_rank env v = - let gl = env.gl in - let rec _get_rank env n = - match env with - | [] -> raise (Invalid_argument "get_rank") - | (e, _) :: l -> ( - match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) - ) - in - _get_rank env.vars 1 - - let elements env = env.vars - - (* let string_of_env gl env = - let rec string_of_env i env acc = - match env with - | [] -> acc - | e::env -> string_of_env (i+1) env - (IMap.add i - (Pp.string_of_ppcmds - (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in - string_of_env 1 env IMap.empty - *) - let pp gl env = - let ppl = - List.mapi - (fun i (e, _) -> - Pp.str "x" - ++ Pp.int (i + 1) - ++ Pp.str ":" - ++ Printer.pr_econstr_env gl.env gl.sigma e) - env +module Env = struct + type t = + { vars : (EConstr.t * Mc.kind) list + ; (* The list represents a mapping from EConstr.t to indexes. *) + gl : gl (* The evar_map may be updated due to unification of universes *) + } + + let empty gl = {vars = []; gl} + + (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) + let eq_constr (env, sigma) x y = + match EConstr.eq_constr_universes_proj env sigma x y with + | Some csts -> ( + let csts = + UnivProblem.to_constraints ~force_weak:false (Evd.universes sigma) csts in - List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p) ppl (Pp.str "\n") - end + match Evd.add_constraints sigma csts with + | sigma -> Some (env, sigma) + | exception Univ.UniverseInconsistency _ -> None ) + | None -> None + + let compute_rank_add env v is_prop = + let rec _add gl vars n v = + match vars with + | [] -> (gl, [(v, is_prop)], n) + | (e, b) :: l -> ( + match eq_constr gl e v with + | Some gl' -> (gl', vars, n) + | None -> + let gl, l', n = _add gl l (n + 1) v in + (gl, (e, b) :: l', n) ) + in + let gl', vars', n = _add env.gl env.vars 1 v in + ({vars = vars'; gl = gl'}, CamlToCoq.positive n) + + let get_rank env v = + let gl = env.gl in + let rec _get_rank env n = + match env with + | [] -> raise (Invalid_argument "get_rank") + | (e, _) :: l -> ( + match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) ) + in + _get_rank env.vars 1 + + let elements env = env.vars + + (* let string_of_env gl env = + let rec string_of_env i env acc = + match env with + | [] -> acc + | e::env -> string_of_env (i+1) env + (IMap.add i + (Pp.string_of_ppcmds + (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in + string_of_env 1 env IMap.empty + *) + let pp (genv, sigma) env = + let ppl = + List.mapi + (fun i (e, _) -> + Pp.str "x" + ++ Pp.int (i + 1) + ++ Pp.str ":" + ++ Printer.pr_econstr_env genv sigma e) + env + in + List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p) ppl (Pp.str "\n") +end - (* MODULE END: Env *) +(* MODULE END: Env *) - (** +(** * This is the big generic function for expression parsers. *) - let parse_expr gl parse_constant parse_exp ops_spec env term = - if debug then - Feedback.msg_debug - (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term); - let parse_variable env term = - let env, n = Env.compute_rank_add env term Mc.IsBool in - (Mc.PEX n, env) +let parse_expr (genv, sigma) parse_constant parse_exp ops_spec env term = + if debug then + Feedback.msg_debug + (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env genv sigma term); + let parse_variable env term = + let env, n = Env.compute_rank_add env term Mc.IsBool in + (Mc.PEX n, env) + in + let rec parse_expr env term = + let combine env op (t1, t2) = + let expr1, env = parse_expr env t1 in + let expr2, env = parse_expr env t2 in + (op expr1 expr2, env) in - let rec parse_expr env term = - let combine env op (t1, t2) = - let expr1, env = parse_expr env t1 in - let expr2, env = parse_expr env t2 in - (op expr1 expr2, env) - in - try (Mc.PEc (parse_constant gl term), env) - with ParseError -> ( - match EConstr.kind gl.sigma term with - | App (t, args) -> ( - match EConstr.kind gl.sigma t with - | Const c -> ( - match assoc_ops gl.sigma t ops_spec with - | Binop f -> combine env f (args.(0), args.(1)) - | Opp -> + try (Mc.PEc (parse_constant (genv, sigma) term), env) + with ParseError -> ( + match EConstr.kind sigma term with + | App (t, args) -> ( + match EConstr.kind sigma t with + | Const c -> ( + match assoc_ops sigma t ops_spec with + | Binop f -> combine env f (args.(0), args.(1)) + | Opp -> + let expr, env = parse_expr env args.(0) in + (Mc.PEopp expr, env) + | Power -> ( + try let expr, env = parse_expr env args.(0) in - (Mc.PEopp expr, env) - | Power -> ( - try - let expr, env = parse_expr env args.(0) in - let power = parse_exp expr args.(1) in - (power, env) - with ParseError -> - (* if the exponent is a variable *) - let env, n = Env.compute_rank_add env term Mc.IsBool in - (Mc.PEX n, env) ) - | Ukn s -> - if debug then ( - Printf.printf "unknown op: %s\n" s; - flush stdout ); + let power = parse_exp expr args.(1) in + (power, env) + with ParseError -> + (* if the exponent is a variable *) let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) ) - | _ -> parse_variable env term ) + | Ukn s -> + if debug then ( + Printf.printf "unknown op: %s\n" s; + flush stdout ); + let env, n = Env.compute_rank_add env term Mc.IsBool in + (Mc.PEX n, env) ) | _ -> parse_variable env term ) - in - parse_expr env term - - let zop_spec = - [ (coq_Zplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Zminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Zmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Zopp, Opp) - ; (coq_Zpower, Power) ] - - let qop_spec = - [ (coq_Qplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Qminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Qmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Qopp, Opp) - ; (coq_Qpower, Power) ] - - let rop_spec = - [ (coq_Rplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Rminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Rmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Ropp, Opp) - ; (coq_Rpower, Power) ] - - let parse_constant parse gl t = parse gl.sigma t - - (** [parse_more_constant parse gl t] returns the reification of term [t]. + | _ -> parse_variable env term ) + in + parse_expr env term + +let zop_spec = + [ (coq_Zplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Zminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Zmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Zopp, Opp) + ; (coq_Zpower, Power) ] + +let qop_spec = + [ (coq_Qplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Qminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Qmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Qopp, Opp) + ; (coq_Qpower, Power) ] + +let rop_spec = + [ (coq_Rplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Rminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Rmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Ropp, Opp) + ; (coq_Rpower, Power) ] + +let parse_constant parse ((genv : Environ.env), sigma) t = parse sigma t + +(** [parse_more_constant parse gl t] returns the reification of term [t]. If [t] is a ground term, then it is first reduced to normal form before using a 'syntactic' parser *) - let parse_more_constant parse gl t = - try parse gl t - with ParseError -> - if debug then Feedback.msg_debug Pp.(str "try harder"); - if is_ground_term gl.env gl.sigma t then - parse gl (Redexpr.cbv_vm gl.env gl.sigma t) - else raise ParseError - - let zconstant = parse_constant parse_z - let qconstant = parse_constant parse_q - let nconstant = parse_constant parse_nat - - (** [parse_more_zexpr parse_constant gl] improves the parsing of exponent +let parse_more_constant parse (genv, sigma) t = + try parse (genv, sigma) t + with ParseError -> + if debug then Feedback.msg_debug Pp.(str "try harder"); + if is_ground_term genv sigma t then + parse (genv, sigma) (Redexpr.cbv_vm genv sigma t) + else raise ParseError + +let zconstant = parse_constant parse_z +let qconstant = parse_constant parse_q +let nconstant = parse_constant parse_nat + +(** [parse_more_zexpr parse_constant gl] improves the parsing of exponent which can be arithmetic expressions (without variables). [parse_constant_expr] returns a constant if the argument is an expression without variables. *) - let rec parse_zexpr gl = - parse_expr gl zconstant - (fun expr (x : EConstr.t) -> - let z = parse_zconstant gl x in - match z with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow (expr, Mc.Z.to_N z)) - zop_spec - - and parse_zconstant gl e = - let e, _ = parse_zexpr gl (Env.empty gl) e in - match Mc.zeval_const e with None -> raise ParseError | Some z -> z - - (* NB: R is a different story. - Because it is axiomatised, reducing would not be effective. - Therefore, there is a specific parser for constant over R - *) +let rec parse_zexpr gl = + parse_expr gl zconstant + (fun expr (x : EConstr.t) -> + let z = parse_zconstant gl x in + match z with + | Mc.Zneg _ -> Mc.PEc Mc.Z0 + | _ -> Mc.PEpow (expr, Mc.Z.to_N z)) + zop_spec + +and parse_zconstant gl e = + let e, _ = parse_zexpr gl (Env.empty gl) e in + match Mc.zeval_const e with None -> raise ParseError | Some z -> z + +(* NB: R is a different story. + Because it is axiomatised, reducing would not be effective. + Therefore, there is a specific parser for constant over R +*) - let rconst_assoc = - [ (coq_Rplus, fun x y -> Mc.CPlus (x, y)) - ; (coq_Rminus, fun x y -> Mc.CMinus (x, y)) - ; (coq_Rmult, fun x y -> Mc.CMult (x, y)) - (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] +let rconst_assoc = + [ (coq_Rplus, fun x y -> Mc.CPlus (x, y)) + ; (coq_Rminus, fun x y -> Mc.CMinus (x, y)) + ; (coq_Rmult, fun x y -> Mc.CMult (x, y)) + (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] - let rconstant gl term = - let sigma = gl.sigma in - let rec rconstant term = - match EConstr.kind sigma term with - | Const x -> - if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 - else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 - else raise ParseError - | App (op, args) -> ( - try - (* the evaluation order is important in the following *) - let f = assoc_const sigma op rconst_assoc in - let a = rconstant args.(0) in - let b = rconstant args.(1) in - f a b - with ParseError -> ( - match op with - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> - let arg = rconstant args.(0) in - if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0; Mc.qden = Mc.XH} - then raise ParseError - (* This is a division by zero -- no semantics *) - else Mc.CInv arg - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> - Mc.CPow - ( rconstant args.(0) - , Mc.Inr (parse_more_constant nconstant gl args.(1)) ) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> - Mc.CQ (qconstant gl args.(0)) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> - Mc.CZ (parse_more_constant zconstant gl args.(0)) - | _ -> raise ParseError ) ) - | _ -> raise ParseError - in - rconstant term - - let rconstant gl term = - if debug then - Feedback.msg_debug - ( Pp.str "rconstant: " - ++ Printer.pr_leconstr_env gl.env gl.sigma term - ++ fnl () ); - let res = rconstant gl term in - if debug then ( - Printf.printf "rconstant -> %a\n" pp_Rcst res; - flush stdout ); - res +let rconstant (genv, sigma) term = + let rec rconstant term = + match EConstr.kind sigma term with + | Const x -> + if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 + else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 + else raise ParseError + | App (op, args) -> ( + try + (* the evaluation order is important in the following *) + let f = assoc_const sigma op rconst_assoc in + let a = rconstant args.(0) in + let b = rconstant args.(1) in + f a b + with ParseError -> ( + match op with + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> + let arg = rconstant args.(0) in + if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0; Mc.qden = Mc.XH} + then raise ParseError (* This is a division by zero -- no semantics *) + else Mc.CInv arg + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> + Mc.CPow + ( rconstant args.(0) + , Mc.Inr (parse_more_constant nconstant (genv, sigma) args.(1)) ) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> + Mc.CQ (qconstant (genv, sigma) args.(0)) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> + Mc.CZ (parse_more_constant zconstant (genv, sigma) args.(0)) + | _ -> raise ParseError ) ) + | _ -> raise ParseError + in + rconstant term + +let rconstant (genv, sigma) term = + if debug then + Feedback.msg_debug + (Pp.str "rconstant: " ++ Printer.pr_leconstr_env genv sigma term ++ fnl ()); + let res = rconstant (genv, sigma) term in + if debug then ( + Printf.printf "rconstant -> %a\n" pp_Rcst res; + flush stdout ); + res - let parse_qexpr gl = - parse_expr gl qconstant - (fun expr x -> - let exp = zconstant gl x in - match exp with - | Mc.Zneg _ -> ( - match expr with - | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) - | _ -> raise ParseError ) - | _ -> - let exp = Mc.Z.to_N exp in - Mc.PEpow (expr, exp)) - qop_spec - - let parse_rexpr gl = - parse_expr gl rconstant - (fun expr x -> - let exp = Mc.N.of_nat (parse_nat gl.sigma x) in +let parse_qexpr gl = + parse_expr gl qconstant + (fun expr x -> + let exp = zconstant gl x in + match exp with + | Mc.Zneg _ -> ( + match expr with + | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) + | _ -> raise ParseError ) + | _ -> + let exp = Mc.Z.to_N exp in Mc.PEpow (expr, exp)) - rop_spec - - let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl = - let sigma = gl.sigma in - if debug then - Feedback.msg_debug - ( Pp.str "parse_arith: " - ++ Printer.pr_leconstr_env gl.env sigma cstr - ++ fnl () ); - match EConstr.kind sigma cstr with - | App (op, args) -> - let op, lhs, rhs = parse_op gl k (op, args) in - let e1, env = parse_expr gl env lhs in - let e2, env = parse_expr gl env rhs in - ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) - | _ -> failwith "error : parse_arith(2)" - - let parse_zarith = parse_arith parse_zop parse_zexpr - let parse_qarith = parse_arith parse_qop parse_qexpr - let parse_rarith = parse_arith parse_rop parse_rexpr - - (* generic parsing of arithmetic expressions *) - - let mkAND b f1 f2 = Mc.AND (b, f1, f2) - let mkOR b f1 f2 = Mc.OR (b, f1, f2) - let mkIff b f1 f2 = Mc.IFF (b, f1, f2) - let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) - let mkEQ f1 f2 = Mc.EQ (f1, f2) - - let mkformula_binary b g term f1 f2 = - match (f1, f2) with - | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) - | _ -> g f1 f2 + qop_spec + +let parse_rexpr (genv, sigma) = + parse_expr (genv, sigma) rconstant + (fun expr x -> + let exp = Mc.N.of_nat (parse_nat sigma x) in + Mc.PEpow (expr, exp)) + rop_spec + +let parse_arith parse_op parse_expr (k : Mc.kind) env cstr (genv, sigma) = + if debug then + Feedback.msg_debug + ( Pp.str "parse_arith: " + ++ Printer.pr_leconstr_env genv sigma cstr + ++ fnl () ); + match EConstr.kind sigma cstr with + | App (op, args) -> + let op, lhs, rhs = parse_op (genv, sigma) k (op, args) in + let e1, env = parse_expr (genv, sigma) env lhs in + let e2, env = parse_expr (genv, sigma) env rhs in + ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) + | _ -> failwith "error : parse_arith(2)" + +let parse_zarith = parse_arith parse_zop parse_zexpr +let parse_qarith = parse_arith parse_qop parse_qexpr +let parse_rarith = parse_arith parse_rop parse_rexpr + +(* generic parsing of arithmetic expressions *) + +let mkAND b f1 f2 = Mc.AND (b, f1, f2) +let mkOR b f1 f2 = Mc.OR (b, f1, f2) +let mkIff b f1 f2 = Mc.IFF (b, f1, f2) +let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) +let mkEQ f1 f2 = Mc.EQ (f1, f2) + +let mkformula_binary b g term f1 f2 = + match (f1, f2) with + | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) + | _ -> g f1 f2 - (** +(** * This is the big generic function for formula parsers. *) - let is_prop env sigma term = - let sort = Retyping.get_sort_of env sigma term in - Sorts.is_prop sort +let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in + Sorts.is_prop sort - type formula_op = - { op_and : EConstr.t - ; op_or : EConstr.t - ; op_iff : EConstr.t - ; op_not : EConstr.t - ; op_tt : EConstr.t - ; op_ff : EConstr.t } +type formula_op = + { op_and : EConstr.t + ; op_or : EConstr.t + ; op_iff : EConstr.t + ; op_not : EConstr.t + ; op_tt : EConstr.t + ; op_ff : EConstr.t } - let prop_op = - lazy - { op_and = Lazy.force coq_and - ; op_or = Lazy.force coq_or - ; op_iff = Lazy.force coq_iff - ; op_not = Lazy.force coq_not - ; op_tt = Lazy.force coq_True - ; op_ff = Lazy.force coq_False } - - let bool_op = - lazy - { op_and = Lazy.force coq_andb - ; op_or = Lazy.force coq_orb - ; op_iff = Lazy.force coq_eqb - ; op_not = Lazy.force coq_negb - ; op_tt = Lazy.force coq_true - ; op_ff = Lazy.force coq_false } - - let parse_formula gl parse_atom env tg term = - let sigma = gl.sigma in - let parse_atom b env tg t = - try - let at, env = parse_atom b env t gl in - (Mc.A (b, at, (tg, t)), env, Tag.next tg) - with ParseError -> (Mc.X (b, t), env, tg) - in - let prop_op = Lazy.force prop_op in - let bool_op = Lazy.force bool_op in - let eq = Lazy.force coq_eq in - let bool = Lazy.force coq_bool in - let rec xparse_formula op k env tg term = - match EConstr.kind sigma term with - | App (l, rst) -> ( - match rst with - | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkAND k) term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkOR k) term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkIff k) term f g, env, tg) - | [|ty; a; b|] - when EConstr.eq_constr sigma l eq && is_convertible gl ty bool -> - let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in - let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in - (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) - | [|a|] when EConstr.eq_constr sigma l op.op_not -> - let f, env, tg = xparse_formula op k env tg a in - (Mc.NOT (k, f), env, tg) - | _ -> parse_atom k env tg term ) - | Prod (typ, a, b) - when kind_is_prop k - && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) - -> +let prop_op = + lazy + { op_and = Lazy.force coq_and + ; op_or = Lazy.force coq_or + ; op_iff = Lazy.force coq_iff + ; op_not = Lazy.force coq_not + ; op_tt = Lazy.force coq_True + ; op_ff = Lazy.force coq_False } + +let bool_op = + lazy + { op_and = Lazy.force coq_andb + ; op_or = Lazy.force coq_orb + ; op_iff = Lazy.force coq_eqb + ; op_not = Lazy.force coq_negb + ; op_tt = Lazy.force coq_true + ; op_ff = Lazy.force coq_false } + +let parse_formula (genv, sigma) parse_atom env tg term = + let parse_atom b env tg t = + try + let at, env = parse_atom b env t (genv, sigma) in + (Mc.A (b, at, (tg, t)), env, Tag.next tg) + with ParseError -> (Mc.X (b, t), env, tg) + in + let prop_op = Lazy.force prop_op in + let bool_op = Lazy.force bool_op in + let eq = Lazy.force coq_eq in + let bool = Lazy.force coq_bool in + let rec xparse_formula op k env tg term = + match EConstr.kind sigma term with + | App (l, rst) -> ( + match rst with + | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> let f, env, tg = xparse_formula op k env tg a in let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) - | _ -> - if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) - else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) - else (Mc.X (k, term), env, tg) - in - xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term + (mkformula_binary k (mkAND k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkOR k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkIff k) term f g, env, tg) + | [|ty; a; b|] + when EConstr.eq_constr sigma l eq && is_convertible genv sigma ty bool + -> + let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in + let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in + (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) + | [|a|] when EConstr.eq_constr sigma l op.op_not -> + let f, env, tg = xparse_formula op k env tg a in + (Mc.NOT (k, f), env, tg) + | _ -> parse_atom k env tg term ) + | Prod (typ, a, b) + when kind_is_prop k + && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) + | _ -> + if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) + else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) + else (Mc.X (k, term), env, tg) + in + xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term - (* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) +(* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) - let dump_kind k = - Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) +let dump_kind k = + Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) - let dump_formula typ dump_atom f = - let app_ctor c args = - EConstr.mkApp - ( Lazy.force c - , Array.of_list - ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit - :: Lazy.force coq_unit :: args ) ) - in - let rec xdump f = - match f with - | Mc.TT k -> app_ctor coq_TT [dump_kind k] - | Mc.FF k -> app_ctor coq_FF [dump_kind k] - | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] - | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] - | Mc.IMPL (k, x, _, y) -> - app_ctor coq_IMPL - [ dump_kind k - ; xdump x - ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) - ; xdump y ] - | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] - | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] - | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] - | Mc.A (k, x, _) -> - app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] - | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] - in - xdump f - - let prop_env_of_formula gl form = - Mc.( - let rec doit env = function - | TT _ | FF _ | A (_, _, _) -> env - | X (b, t) -> fst (Env.compute_rank_add env t b) - | AND (b, f1, f2) - |OR (b, f1, f2) - |IMPL (b, f1, _, f2) - |IFF (b, f1, f2) -> - doit (doit env f1) f2 - | NOT (b, f) -> doit env f - | EQ (f1, f2) -> doit (doit env f1) f2 - in - doit (Env.empty gl) form) - - let var_env_of_formula form = - let rec vars_of_expr = function - | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) - | Mc.PEc z -> ISet.empty - | Mc.PEadd (e1, e2) | Mc.PEmul (e1, e2) | Mc.PEsub (e1, e2) -> - ISet.union (vars_of_expr e1) (vars_of_expr e2) - | Mc.PEopp e | Mc.PEpow (e, _) -> vars_of_expr e - in - let vars_of_atom {Mc.flhs; Mc.fop; Mc.frhs} = - ISet.union (vars_of_expr flhs) (vars_of_expr frhs) +let dump_formula typ dump_atom f = + let app_ctor c args = + EConstr.mkApp + ( Lazy.force c + , Array.of_list + ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit + :: Lazy.force coq_unit :: args ) ) + in + let rec xdump f = + match f with + | Mc.TT k -> app_ctor coq_TT [dump_kind k] + | Mc.FF k -> app_ctor coq_FF [dump_kind k] + | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] + | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] + | Mc.IMPL (k, x, _, y) -> + app_ctor coq_IMPL + [ dump_kind k + ; xdump x + ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) + ; xdump y ] + | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] + | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] + | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] + | Mc.A (k, x, _) -> + app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] + | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] + in + xdump f + +let prop_env_of_formula gl form = + Mc.( + let rec doit env = function + | TT _ | FF _ | A (_, _, _) -> env + | X (b, t) -> fst (Env.compute_rank_add env t b) + | AND (b, f1, f2) | OR (b, f1, f2) | IMPL (b, f1, _, f2) | IFF (b, f1, f2) + -> + doit (doit env f1) f2 + | NOT (b, f) -> doit env f + | EQ (f1, f2) -> doit (doit env f1) f2 in - Mc.( - let rec doit = function - | TT _ | FF _ | X _ -> ISet.empty - | A (_, a, (t, c)) -> vars_of_atom a - | AND (_, f1, f2) - |OR (_, f1, f2) - |IMPL (_, f1, _, f2) - |IFF (_, f1, f2) - |EQ (f1, f2) -> - ISet.union (doit f1) (doit f2) - | NOT (_, f) -> doit f - in - doit form) - - type 'cst dump_expr = - { (* 'cst is the type of the syntactic constants *) - interp_typ : EConstr.constr - ; dump_cst : 'cst -> EConstr.constr - ; dump_add : EConstr.constr - ; dump_sub : EConstr.constr - ; dump_opp : EConstr.constr - ; dump_mul : EConstr.constr - ; dump_pow : EConstr.constr - ; dump_pow_arg : Mc.n -> EConstr.constr - ; dump_op_prop : (Mc.op2 * EConstr.constr) list - ; dump_op_bool : (Mc.op2 * EConstr.constr) list } - - let dump_zexpr = - lazy - { interp_typ = Lazy.force coq_Z - ; dump_cst = dump_z - ; dump_add = Lazy.force coq_Zplus - ; dump_sub = Lazy.force coq_Zminus - ; dump_opp = Lazy.force coq_Zopp - ; dump_mul = Lazy.force coq_Zmult - ; dump_pow = Lazy.force coq_Zpower - ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool - } - - let dump_qexpr = - lazy - { interp_typ = Lazy.force coq_Q - ; dump_cst = dump_q - ; dump_add = Lazy.force coq_Qplus - ; dump_sub = Lazy.force coq_Qminus - ; dump_opp = Lazy.force coq_Qopp - ; dump_mul = Lazy.force coq_Qmult - ; dump_pow = Lazy.force coq_Qpower - ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool - } - - let rec dump_Rcst_as_R cst = - match cst with - | Mc.C0 -> Lazy.force coq_R0 - | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_IQR, [|dump_q q|]) - | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_IZR, [|dump_z z|]) - | Mc.CPlus (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rplus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CMinus (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rminus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CMult (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rmult, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CPow (x, y) -> ( - match y with - | Mc.Inl z -> - EConstr.mkApp (Lazy.force coq_powerZR, [|dump_Rcst_as_R x; dump_z z|]) - | Mc.Inr n -> - EConstr.mkApp (Lazy.force coq_Rpower, [|dump_Rcst_as_R x; dump_nat n|]) - ) - | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_Rinv, [|dump_Rcst_as_R t|]) - | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_Ropp, [|dump_Rcst_as_R t|]) - - let dump_rexpr = - lazy - { interp_typ = Lazy.force coq_R - ; dump_cst = dump_Rcst_as_R - ; dump_add = Lazy.force coq_Rplus - ; dump_sub = Lazy.force coq_Rminus - ; dump_opp = Lazy.force coq_Ropp - ; dump_mul = Lazy.force coq_Rmult - ; dump_pow = Lazy.force coq_Rpower - ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool - } - - let prodn n env b = - let rec prodrec = function - | 0, env, b -> b - | n, (v, t) :: l, b -> - prodrec (n - 1, l, EConstr.mkProd (make_annot v Sorts.Relevant, t, b)) - | _ -> assert false + doit (Env.empty gl) form) + +let var_env_of_formula form = + let rec vars_of_expr = function + | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) + | Mc.PEc z -> ISet.empty + | Mc.PEadd (e1, e2) | Mc.PEmul (e1, e2) | Mc.PEsub (e1, e2) -> + ISet.union (vars_of_expr e1) (vars_of_expr e2) + | Mc.PEopp e | Mc.PEpow (e, _) -> vars_of_expr e + in + let vars_of_atom {Mc.flhs; Mc.fop; Mc.frhs} = + ISet.union (vars_of_expr flhs) (vars_of_expr frhs) + in + Mc.( + let rec doit = function + | TT _ | FF _ | X _ -> ISet.empty + | A (_, a, (t, c)) -> vars_of_atom a + | AND (_, f1, f2) + |OR (_, f1, f2) + |IMPL (_, f1, _, f2) + |IFF (_, f1, f2) + |EQ (f1, f2) -> + ISet.union (doit f1) (doit f2) + | NOT (_, f) -> doit f in - prodrec (n, env, b) + doit form) + +type 'cst dump_expr = + { (* 'cst is the type of the syntactic constants *) + interp_typ : EConstr.constr + ; dump_cst : 'cst -> EConstr.constr + ; dump_add : EConstr.constr + ; dump_sub : EConstr.constr + ; dump_opp : EConstr.constr + ; dump_mul : EConstr.constr + ; dump_pow : EConstr.constr + ; dump_pow_arg : Mc.n -> EConstr.constr + ; dump_op_prop : (Mc.op2 * EConstr.constr) list + ; dump_op_bool : (Mc.op2 * EConstr.constr) list } + +let dump_zexpr = + lazy + { interp_typ = Lazy.force coq_Z + ; dump_cst = dump_z + ; dump_add = Lazy.force coq_Zplus + ; dump_sub = Lazy.force coq_Zminus + ; dump_opp = Lazy.force coq_Zopp + ; dump_mul = Lazy.force coq_Zmult + ; dump_pow = Lazy.force coq_Zpower + ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool + } + +let dump_qexpr = + lazy + { interp_typ = Lazy.force coq_Q + ; dump_cst = dump_q + ; dump_add = Lazy.force coq_Qplus + ; dump_sub = Lazy.force coq_Qminus + ; dump_opp = Lazy.force coq_Qopp + ; dump_mul = Lazy.force coq_Qmult + ; dump_pow = Lazy.force coq_Qpower + ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool + } + +let rec dump_Rcst_as_R cst = + match cst with + | Mc.C0 -> Lazy.force coq_R0 + | Mc.C1 -> Lazy.force coq_R1 + | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_IQR, [|dump_q q|]) + | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_IZR, [|dump_z z|]) + | Mc.CPlus (x, y) -> + EConstr.mkApp (Lazy.force coq_Rplus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CMinus (x, y) -> + EConstr.mkApp (Lazy.force coq_Rminus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CMult (x, y) -> + EConstr.mkApp (Lazy.force coq_Rmult, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CPow (x, y) -> ( + match y with + | Mc.Inl z -> + EConstr.mkApp (Lazy.force coq_powerZR, [|dump_Rcst_as_R x; dump_z z|]) + | Mc.Inr n -> + EConstr.mkApp (Lazy.force coq_Rpower, [|dump_Rcst_as_R x; dump_nat n|]) ) + | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_Rinv, [|dump_Rcst_as_R t|]) + | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_Ropp, [|dump_Rcst_as_R t|]) + +let dump_rexpr = + lazy + { interp_typ = Lazy.force coq_R + ; dump_cst = dump_Rcst_as_R + ; dump_add = Lazy.force coq_Rplus + ; dump_sub = Lazy.force coq_Rminus + ; dump_opp = Lazy.force coq_Ropp + ; dump_mul = Lazy.force coq_Rmult + ; dump_pow = Lazy.force coq_Rpower + ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool + } + +let prodn n env b = + let rec prodrec = function + | 0, env, b -> 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) - (** [make_goal_of_formula depxr vars props form] where +(** [make_goal_of_formula depxr vars props form] where - vars is an environment for the arithmetic variables occurring in form - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) - let eKind = function - | Mc.IsProp -> EConstr.mkProp - | Mc.IsBool -> Lazy.force coq_bool +let eKind = function + | Mc.IsProp -> EConstr.mkProp + | Mc.IsBool -> Lazy.force coq_bool - let make_goal_of_formula gl dexpr form = - let vars_idx = - List.mapi - (fun i v -> (v, i + 1)) - (ISet.elements (var_env_of_formula form)) - in - (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) - let props = prop_env_of_formula gl form in - let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in - let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in - let vars_n = - List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx - in - let props_n = - List.mapi - (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) - (Env.elements props) - in - let var_name_pos = - List.map2 (fun (idx, _) (id, _) -> (id, idx)) vars_idx vars_n - in - let dump_expr i e = - let rec dump_expr = function - | Mc.PEX n -> - EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) - | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd (e1, e2) -> - EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) - | Mc.PEsub (e1, e2) -> - EConstr.mkApp (dexpr.dump_sub, [|dump_expr e1; dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp (dexpr.dump_opp, [|dump_expr e|]) - | Mc.PEmul (e1, e2) -> - EConstr.mkApp (dexpr.dump_mul, [|dump_expr e1; dump_expr e2|]) - | Mc.PEpow (e, n) -> - EConstr.mkApp (dexpr.dump_pow, [|dump_expr e; dexpr.dump_pow_arg n|]) - in - dump_expr e - in - let mkop_prop op e1 e2 = - try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) - with Not_found -> - EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) - in - let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) - in - let mkop_bool op e1 e2 = - try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) - with Not_found -> - EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) - in - let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) - in - let rec xdump_prop pi xi f = - match f with - | Mc.TT _ -> Lazy.force coq_True - | Mc.FF _ -> Lazy.force coq_False - | Mc.AND (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.OR (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.IFF (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.IMPL (_, x, _, y) -> - EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant - (xdump_prop (pi + 1) (xi + 1) y) - | Mc.NOT (_, x) -> - EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant - (Lazy.force coq_False) - | Mc.EQ (x, y) -> - EConstr.mkApp - ( Lazy.force coq_eq - , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) - | Mc.A (_, x, _) -> dump_cstr_prop xi x - | Mc.X (_, t) -> - let idx = Env.get_rank props t in - EConstr.mkRel (pi + idx) - and xdump_bool pi xi f = - match f with - | Mc.TT _ -> Lazy.force coq_true - | Mc.FF _ -> Lazy.force coq_false - | Mc.AND (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.OR (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.IFF (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.IMPL (_, x, _, y) -> - EConstr.mkApp - (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.NOT (_, x) -> - EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) - | Mc.EQ (x, y) -> assert false - | Mc.A (_, x, _) -> dump_cstr_bool xi x - | Mc.X (_, t) -> - let idx = Env.get_rank props t in - EConstr.mkRel (pi + idx) - in - let nb_vars = List.length vars_n in - let nb_props = List.length props_n in - (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) - let subst_prop p = - let idx = Env.get_rank props p in - EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) +let make_goal_of_formula gl dexpr form = + let vars_idx = + List.mapi (fun i v -> (v, i + 1)) (ISet.elements (var_env_of_formula form)) + in + (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) + let props = prop_env_of_formula gl form in + let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in + let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in + let vars_n = + List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx + in + let props_n = + List.mapi + (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) + (Env.elements props) + in + let var_name_pos = + List.map2 (fun (idx, _) (id, _) -> (id, idx)) vars_idx vars_n + in + let dump_expr i e = + let rec dump_expr = function + | Mc.PEX n -> + EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) + | Mc.PEc z -> dexpr.dump_cst z + | Mc.PEadd (e1, e2) -> + EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) + | Mc.PEsub (e1, e2) -> + EConstr.mkApp (dexpr.dump_sub, [|dump_expr e1; dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp (dexpr.dump_opp, [|dump_expr e|]) + | Mc.PEmul (e1, e2) -> + EConstr.mkApp (dexpr.dump_mul, [|dump_expr e1; dump_expr e2|]) + | Mc.PEpow (e, n) -> + EConstr.mkApp (dexpr.dump_pow, [|dump_expr e; dexpr.dump_pow_arg n|]) in - let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in - ( prodn nb_props - (List.map (fun (x, y) -> (Name.Name x, y)) props_n) - (prodn nb_vars - (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) - (xdump_prop (List.length vars_n) 0 form)) - , List.rev props_n - , List.rev var_name_pos - , form' ) - - (** + dump_expr e + in + let mkop_prop op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) + in + let mkop_bool op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) + in + let rec xdump_prop pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_True + | Mc.FF _ -> Lazy.force coq_False + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (xdump_prop (pi + 1) (xi + 1) y) + | Mc.NOT (_, x) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant (Lazy.force coq_False) + | Mc.EQ (x, y) -> + EConstr.mkApp + ( Lazy.force coq_eq + , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) + | Mc.A (_, x, _) -> dump_cstr_prop xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + and xdump_bool pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_true + | Mc.FF _ -> Lazy.force coq_false + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkApp + (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.NOT (_, x) -> + EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) + | Mc.EQ (x, y) -> assert false + | Mc.A (_, x, _) -> dump_cstr_bool xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + in + let nb_vars = List.length vars_n in + let nb_props = List.length props_n in + (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) + let subst_prop p = + let idx = Env.get_rank props p in + EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) + in + let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in + ( prodn nb_props + (List.map (fun (x, y) -> (Name.Name x, y)) props_n) + (prodn nb_vars + (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) + (xdump_prop (List.length vars_n) 0 form)) + , List.rev props_n + , List.rev var_name_pos + , form' ) + +(** * Given a conclusion and a list of affectations, rebuild a term prefixed by * the appropriate letins. * TODO: reverse the list of bindings! *) - let set l concl = - let rec xset acc = function - | [] -> acc - | e :: l -> - let name, expr, typ = e in - xset - (EConstr.mkNamedLetIn - (make_annot (Names.Id.of_string name) Sorts.Relevant) - expr typ acc) - l - in - xset concl l -end - -open M +let set l concl = + let rec xset acc = function + | [] -> acc + | e :: l -> + let name, expr, typ = e in + xset + (EConstr.mkNamedLetIn + (make_annot (Names.Id.of_string name) Sorts.Relevant) + expr typ acc) + l + in + xset concl l let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch") let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt") @@ -1424,14 +1389,14 @@ let rec pp_proof_term o = function | Micromega.ExProof (p, prf) -> Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf -let rec parse_hyps gl parse_arith env tg hyps = +let rec parse_hyps (genv, sigma) parse_arith env tg hyps = match hyps with | [] -> ([], env, tg) | (i, t) :: l -> - let lhyps, env, tg = parse_hyps gl parse_arith env tg l in - if is_prop gl.env gl.sigma t then + let lhyps, env, tg = parse_hyps (genv, sigma) parse_arith env tg l in + if is_prop genv sigma t then try - let c, env, tg = parse_formula gl parse_arith env tg t in + let c, env, tg = parse_formula (genv, sigma) parse_arith env tg t in ((i, c) :: lhyps, env, tg) with ParseError -> (lhyps, env, tg) else (lhyps, env, tg) @@ -1852,19 +1817,22 @@ let clear_all_no_check = let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = Proofview.Goal.enter (fun gl -> let sigma = Tacmach.New.project gl in + let genv = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try - let gl0 = {env = Tacmach.New.pf_env gl; sigma} in let hyps, concl, env = - parse_goal gl0 parse_arith (Env.empty gl0) hyps concl + parse_goal (genv, sigma) parse_arith + (Env.empty (genv, sigma)) + hyps concl in let env = Env.elements env in let spec = Lazy.force spec in let dumpexpr = Lazy.force dumpexpr in - if debug then Feedback.msg_debug (Pp.str "Env " ++ Env.pp gl0 env); + if debug then + Feedback.msg_debug (Pp.str "Env " ++ Env.pp (genv, sigma) env); match - micromega_tauto pre_process cnf spec prover env hyps concl gl0 + micromega_tauto pre_process cnf spec prover env hyps concl (env, sigma) with | Unknown -> flush stdout; @@ -1873,7 +1841,7 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Prf (ids, ff', res') -> let arith_goal, props, vars, ff_arith = - make_goal_of_formula gl0 dumpexpr ff' + make_goal_of_formula (genv, sigma) dumpexpr ff' in let intro (id, _) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -1893,7 +1861,9 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = env' ff_arith ] in let goal_props = - List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + List.rev + (List.map fst + (Env.elements (prop_env_of_formula (genv, sigma) ff'))) in let goal_vars = List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars @@ -1971,12 +1941,14 @@ let micromega_genr prover tac = in Proofview.Goal.enter (fun gl -> let sigma = Tacmach.New.project gl in + let genv = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try - let gl0 = {env = Tacmach.New.pf_env gl; sigma} in let hyps, concl, env = - parse_goal gl0 parse_arith (Env.empty gl0) hyps concl + parse_goal (genv, sigma) parse_arith + (Env.empty (genv, sigma)) + hyps concl in let env = Env.elements env in let spec = Lazy.force spec in @@ -1997,7 +1969,7 @@ let micromega_genr prover tac = match micromega_tauto (fun _ x -> x) - Mc.cnfQ spec prover env hyps' concl' gl0 + Mc.cnfQ spec prover env hyps' concl' (genv, sigma) with | Unknown | Model _ -> flush stdout; @@ -2010,7 +1982,7 @@ let micromega_genr prover tac = in let ff' = abstract_wrt_formula ff' ff in let arith_goal, props, vars, ff_arith = - make_goal_of_formula gl0 (Lazy.force dump_rexpr) ff' + make_goal_of_formula (genv, sigma) (Lazy.force dump_rexpr) ff' in let intro (id, _) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -2030,7 +2002,9 @@ let micromega_genr prover tac = ; micromega_order_changer res' env' ff_arith ] in let goal_props = - List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + List.rev + (List.map fst + (Env.elements (prop_env_of_formula (genv, sigma) ff'))) in let goal_vars = List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index fa29e6080e..917961fdcd 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -464,13 +464,18 @@ module ECstOp = struct let cast x = CstOp x let dest = function CstOp x -> Some x | _ -> None + let isConstruct evd c = + match EConstr.kind evd c with + | Construct _ | Int _ | Float _ -> true + | _ -> false + let mk_elt evd i a = { source = a.(0) ; target = a.(1) ; inj = get_inj evd a.(3) ; cst = a.(4) ; cstinj = a.(5) - ; is_construct = EConstr.isConstruct evd a.(2) } + ; is_construct = isConstruct evd a.(2) } let get_key = 2 end @@ -979,17 +984,21 @@ let is_arrow env evd a p1 p2 = where c is the head symbol and [a] is the array of arguments. The function also transforms (x -> y) as (arrow x y) *) let get_operator barrow env evd e = - match EConstr.kind evd e with + let e' = EConstr.whd_evar evd e in + match EConstr.kind evd e' with | Prod (a, p1, p2) -> - if barrow && is_arrow env evd a p1 p2 then (arrow, [|p1; p2|]) + if barrow && is_arrow env evd a p1 p2 then (arrow, [|p1; p2|], false) else raise Not_found | App (c, a) -> ( - match EConstr.kind evd c with + let c' = EConstr.whd_evar evd c in + match EConstr.kind evd c' with | Construct _ (* e.g. Z0 , Z.pos *) | Const _ (* e.g. Z.max *) | Proj _ |Lambda _ (* e.g projections *) | Ind _ (* e.g. eq *) -> - (c, a) + (c', a, false) | _ -> raise Not_found ) - | Construct _ -> (EConstr.whd_evar evd e, [||]) + | Const _ -> (e', [||], false) + | Construct _ -> (e', [||], true) + | Int _ | Float _ -> (e', [||], true) | _ -> raise Not_found let decompose_app env evd e = @@ -1065,37 +1074,41 @@ let rec trans_expr env evd e = let inj = e.inj in let e = e.constr in try - let c, a = get_operator false env evd e in - let k, t = - find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) - in - let n = Array.length a in - match k with - | CstOp {deriv = c'} -> - ECstOpT.(if c'.is_construct then Term else Prf (c'.cst, c'.cstinj)) - | UnOp {deriv = unop} -> - let prf = - trans_expr env evd - { constr = a.(n - 1) - ; typ = unop.EUnOpT.source1 - ; inj = unop.EUnOpT.inj1_t } - in - app_unop evd e unop a.(n - 1) prf - | BinOp {deriv = binop} -> - let prf1 = - trans_expr env evd - { constr = a.(n - 2) - ; typ = binop.EBinOpT.source1 - ; inj = binop.EBinOpT.inj1 } - in - let prf2 = - trans_expr env evd - { constr = a.(n - 1) - ; typ = binop.EBinOpT.source2 - ; inj = binop.EBinOpT.inj2 } + let c, a, is_constant = get_operator false env evd e in + if is_constant then Term + else + let k, t = + find_option + (match_operator env evd c a) + (HConstr.find_all c !table_cache) in - app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 - | d -> mkvar evd inj e + let n = Array.length a in + match k with + | CstOp {deriv = c'} -> + ECstOpT.(if c'.is_construct then Term else Prf (c'.cst, c'.cstinj)) + | UnOp {deriv = unop} -> + let prf = + trans_expr env evd + { constr = a.(n - 1) + ; typ = unop.EUnOpT.source1 + ; inj = unop.EUnOpT.inj1_t } + in + app_unop evd e unop a.(n - 1) prf + | BinOp {deriv = binop} -> + let prf1 = + trans_expr env evd + { constr = a.(n - 2) + ; typ = binop.EBinOpT.source1 + ; inj = binop.EBinOpT.inj1 } + in + let prf2 = + trans_expr env evd + { constr = a.(n - 1) + ; typ = binop.EBinOpT.source2 + ; inj = binop.EBinOpT.inj2 } + in + app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 + | d -> mkvar evd inj e with Not_found -> (* Feedback.msg_debug Pp.(str "Not found " ++ Termops.Internal.debug_print_constr e); *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d859fe51ab..cb58b9bcb8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -280,7 +280,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in + let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index b32b58062a..7b584b5159 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id @@ -403,7 +403,7 @@ END let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt () let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod) -let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);; +let ssrmmod = Pcoq.create_generic_entry2 "ssrmmod" (Genarg.rawwit wit_ssrmmod);; } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5dedae6388..cdd15acb0d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -204,7 +204,8 @@ exception NoProgress (* comparison can be much faster than the HO one. *) let unif_EQ env sigma p c = - let evars = existential_opt_value0 sigma, Evd.universes sigma in + let env = Environ.set_universes (Evd.universes sigma) env in + let evars = existential_opt_value0 sigma in try let _ = Reduction.conv env p ~evars c in true with _ -> false let unif_EQ_args env sigma pa a = |