diff options
Diffstat (limited to 'plugins')
24 files changed, 1238 insertions, 1275 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 23f8fe04a3..ac2058ba1b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -115,7 +115,7 @@ module Bool = struct | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in - Names.eq_ind i (Lazy.force ind) + Names.Ind.CanOrd.equal i (Lazy.force ind) in if is_bool then Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 6f5c910297..129b220680 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -145,7 +145,7 @@ let rec term_equal t1 t2 = | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> - Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) + Int.equal i1 i2 && Int.equal j1 j2 && Construct.CanOrd.equal c1 c2 (* FIXME check eq? *) | _ -> false open Hashset.Combine @@ -155,7 +155,7 @@ let rec hash_term = function | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.CanOrd.hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dca1d5e49..6869f9c47e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints then var2var' (snd schema) else instantiation schema in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f8449bcda1..e56d66ca2d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn' | ConstRef _ | VarRef _ -> false let repr_of_r = let open GlobRef in function diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index f13901c36d..4adad53899 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -38,7 +38,7 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else GlobRef.Ordered.compare id1 id2 + else GlobRef.CanOrd.compare id1 id2 module OrderedInstance= struct diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index db3631daa4..99c5f85125 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -62,7 +62,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - let c = GlobRef.Ordered.compare id1 id2 in + let c = GlobRef.CanOrd.compare id1 id2 in if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e50c6087bb..73eb943418 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos |Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in build_proof_args env sigma do_finalize new_infos - | Const (c, _) when not (List.mem_f Constant.equal c fnames) -> + | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) build_proof_args env sigma do_finalize new_infos diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1ab747ca09..0ab9ac65d7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match Constr.kind c with - | Ind ((u, _), _) -> MutInd.equal u rel_as_kn - | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn + | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn + | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn | _ -> false in let get_fun_num c = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 012fcee486..314c8abcaf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in List.map - (function - | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes) + (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes) funs in let ind_list = @@ -2228,7 +2228,8 @@ let build_case_scheme fa = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal funs this_block_funs_indexes + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in + List.assoc_f eq funs this_block_funs_indexes in let ind, sf = let ind = (first_fun_kn, funs_indexes) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6ed61043f9..767a9ec39b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env = let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find - (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) + (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types : types list = @@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ = let constructors = Inductiveops.get_constructors env indf in let constructor = List.find - (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) + (fun cs -> + Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types : types list = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8e1331ace9..164a446fe3 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -444,7 +444,8 @@ let rec are_unifiable_aux = function match (DAst.get l, DAst.get r) with | PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs @@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function match (DAst.get l, DAst.get r) with | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5d631aac84..118a917381 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -27,12 +27,13 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App (i, args) when isInd sigma i -> let ((kn', num) as ind'), u = destInd sigma i in - if MutInd.equal kn kn' then + if Environ.QMutInd.equal env kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) let info = match find_Function_of_graph ind' with diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 6cf5d30a95..2d74323689 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -402,7 +402,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in 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 + let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in ComTactic.solve g ~info t ~with_end_tac } END @@ -415,7 +415,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof VtProofStep{ proof_block_detection = pbr } } -> { let t, abstract = rm_abstract t in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5ef76dbdc1..a1970cbce2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -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) } @@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> + | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta env sigma (mkApp (v, args)) @@ -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 diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index d58a76fe13..6823b6411f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -31,18 +31,6 @@ type argument = Genarg.ArgT.any Extend.user_symbol (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - let atactic n = if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) @@ -70,28 +58,37 @@ let check_separator ?loc = function | Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") let rec parse_user_entry ?loc s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + let open CString in + let matches pre suf s = + String.length s > (String.length pre + String.length suf) && + is_prefix pre s && is_suffix suf s + in + let basename pre suf s = + let plen = String.length pre in + String.sub s plen (String.length s - (plen + String.length suf)) + in + let tactic_len = String.length "tactic" in + if matches "ne_" "_list" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in check_separator ?loc sep; Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in + else if matches "ne_" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in Ulist1sep (entry, get_separator sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + else if matches "" "_list" s then + let entry = parse_user_entry ?loc (basename "" "_list" s) None in check_separator ?loc sep; Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in + else if matches "" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in Ulist0sep (entry, get_separator sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + else if matches "" "_opt" s then + let entry = parse_user_entry ?loc (basename "" "_opt" s) None in check_separator ?loc sep; Uopt entry - else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in + else if String.length s = tactic_len + 1 && is_prefix "tactic" s + && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then + let n = Char.code s.[tactic_len] - Char.code '0' in check_separator ?loc sep; Uentryl ("tactic", n) else @@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in - assert (coincide (ArgT.repr tag) "tactic" 0); + assert (CString.is_suffix "tactic" (ArgT.repr tag)); get_tacentry n lev (** Tactic grammar extensions *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..22b9abda20 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2019,7 +2019,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 01d7306c9d..dba9c938ec 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -131,7 +131,7 @@ type tactic_expr = { ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr ComTactic.tactic_interpreter +val hide_interp : tactic_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) 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/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d464ec4c06..61f90608b1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term = | Cast(a,_,_) -> make_form env sigma atom_env a | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) @@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term = begin try let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then + else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Disjunct (fa,fb) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 38b26d06b9..a7ebd5f9f5 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with let same_proj sigma t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with - | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2 | _ -> false let all_ok _ _ = true diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4a907b2795..91cd5b251c 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -309,9 +309,15 @@ END ~category:"deprecated" ~default:CWarnings.Enabled (fun () -> (Pp.strbrk - "SSReflect's Search command has been moved to the \ - ssrsearch module; please Require that module if you \ - still want to use SSReflect's Search command")) + "In previous versions of Coq, loading SSReflect had the effect of \ + replacing the built-in 'Search' command with an SSReflect version \ + of that command. \ + Coq's own search feature was still available via 'SearchAbout' \ + (but that alias is deprecated). \ + This replacement no longer happens; now 'Search' calls Coq's own search \ + feature even when SSReflect is loaded. \ + If you want to use SSReflect's deprecated Search command \ + instead of the built-in one, please Require the ssrsearch module.")) open G_vernac } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index cdd15acb0d..bd514f15d5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -463,8 +463,8 @@ let nb_cs_proj_args pc f u = try match kind f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) - | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -508,7 +508,7 @@ let filter_upat i0 f n u fpats = let () = if !i0 < np then i0 := n in (u, np) :: fpats let eq_prim_proj c t = match kind t with - | Proj(p,_) -> Constant.equal (Projection.constant p) c + | Proj(p,_) -> Constant.CanOrd.equal (Projection.constant p) c | _ -> false let filter_upat_FO i0 f n u fpats = |