aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml2
-rw-r--r--plugins/extraction/common.ml16
-rw-r--r--plugins/extraction/common.mli2
-rw-r--r--plugins/extraction/extract_env.ml3
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/extraction/ocaml.ml89
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/micromega/coq_micromega.ml26
-rw-r--r--plugins/ssrmatching/ssrmatching.ml422
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
11 files changed, 82 insertions, 94 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index aedcb7575..aa71a4565 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -444,7 +444,7 @@ and applist_projection c l =
let p = Projection.make (fst c) false in
(match l with
| [] -> (* Expand the projection *)
- let ty,_ = Typeops.type_of_constant (Global.env ()) c in
+ let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
let pb = Environ.lookup_projection p (Global.env()) in
let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9446cf667..de97ba97c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -308,15 +308,16 @@ end
module DupMap = Map.Make(DupOrd)
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
let index = ref 0 and dups = ref DupMap.empty in
register_cleanup (fun () -> index := 0; dups := DupMap.empty);
let add mp l =
incr index;
let ren = "Coq__" ^ string_of_int !index in
dups := DupMap.add (mp,l) ren !dups
- and check mp l = DupMap.find (mp, l) !dups
- in (add,check)
+ and get mp l =
+ try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+ in (add,get)
type reset_kind = AllButExternal | Everything
@@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab =
(* Here rls=s::rls', we search the label for s inside mp *)
List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
in
- try dottify (check_duplicate prefix lbl :: rls')
- with Not_found ->
- assert (get_phase () == Pre); (* otherwise it's too late *)
- add_duplicate prefix lbl; dottify rls
+ match get_duplicate prefix lbl with
+ | Some ren -> dottify (ren :: rls')
+ | None ->
+ assert (get_phase () == Pre); (* otherwise it's too late *)
+ add_duplicate prefix lbl; dottify rls
let fstlev_ks k = function
| [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f5601964..b8e95afb3 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path
val push_visible : module_path -> module_path list -> unit
val pop_visible : unit -> unit
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : module_path -> Label.t -> string option
type reset_kind = AllButExternal | Everything
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 52f22ee60..e019bb3c2 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
in
(* First, a dry run, for computing objects to rename or duplicate *)
set_phase Pre;
- let devnull = formatter true None in
- pp_with devnull (d.pp_struct struc);
+ ignore (d.pp_struct struc);
let opened = opened_libraries () in
(* Print the implementation *)
let cout = if dry then None else Option.map open_out fn in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 8744eacd3..92ece7ccf 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -267,7 +267,7 @@ let rec extract_type env db j c args =
| Const (kn,u as c) ->
let r = ConstRef kn in
let cb = lookup_constant kn env in
- let typ,_ = Typeops.type_of_constant env c in
+ let typ = Typeops.type_of_constant_in env c in
(match flag_of_type env typ with
| (Logic,_) -> assert false (* Cf. logical cases above *)
| (Info, TypeScheme) ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc2..d89bf95ee 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -555,24 +555,6 @@ let pp_decl = function
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
-let pp_alias_decl ren = function
- | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
- | Dtype (r, l, _) ->
- let name = pp_global Type r in
- let l = rename_tvars keywords l in
- let ids = pp_parameters l in
- hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
- str (ren^".") ++ name)
- | Dterm (r, a, t) ->
- let name = pp_global Term r in
- hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
- | Dfix (rv, _, _) ->
- prvecti (fun i r -> if is_inline_custom r then mt () else
- let name = pp_global Term r in
- hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
- fnl ())
- rv
-
let pp_spec = function
| Sval (r,_) when is_inline_custom r -> mt ()
| Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,42 +579,32 @@ let pp_spec = function
in
hov 2 (str "type " ++ ids ++ name ++ def)
-let pp_alias_spec ren = function
- | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
- | Stype (r,l,_) ->
- let name = pp_global Type r in
- let l = rename_tvars keywords l in
- let ids = pp_parameters l in
- hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
- str (ren^".") ++ name)
- | Sval _ -> assert false
-
let rec pp_specif = function
| (_,Spec (Sval _ as s)) -> pp_spec s
| (l,Spec s) ->
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_spec s
+ | Some ren ->
hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
fnl () ++ str "end" ++ fnl () ++
- pp_alias_spec ren s
- with Not_found -> pp_spec s)
+ str ("include module type of struct include "^ren^" end"))
| (l,Smodule mt) ->
let def = pp_module_type [] mt in
- let def' = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
- with Not_found -> Pp.mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren ->
+ fnl () ++
+ hov 1 (str ("module "^ren^" :") ++ spc () ++
+ str "module type of struct include " ++ name ++ str " end"))
| (l,Smodtype mt) ->
let def = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module type "^ren^" = ") ++ name
- with Not_found -> Pp.mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_type params = function
| MTident kn ->
@@ -653,8 +625,10 @@ and pp_module_type params = function
let l = List.rev l in
pop_visible ();
str "sig" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+ ++ str "end"
| MTwith(mt,ML_With_type(idl,vl,typ)) ->
let ids = pp_parameters (rename_tvars keywords vl) in
let mp_mt = msid_of_mt mt in
@@ -681,12 +655,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
let rec pp_structure_elem = function
| (l,SEdecl d) ->
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_decl d
+ | Some ren ->
hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
- fnl () ++ str "end" ++ fnl () ++
- pp_alias_decl ren d
- with Not_found -> pp_decl d)
+ fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
| (l,SEmodule m) ->
let typ =
(* virtual printing of the type, in order to have a correct mli later*)
@@ -699,18 +672,16 @@ let rec pp_structure_elem = function
hov 1
(str "module " ++ name ++ typ ++ str " =" ++
(if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module "^ren^" = ") ++ name
- with Not_found -> mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+ | None -> mt ())
| (l,SEmodtype m) ->
let def = pp_module_type [] m in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module type "^ren^" = ") ++ name
- with Not_found -> mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_expr params = function
| MEident mp -> pp_modname mp
@@ -732,8 +703,10 @@ and pp_module_expr params = function
let l = List.rev l in
pop_visible ();
str "struct" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+ ++ str "end"
let rec prlist_sep_nonempty sep f = function
| [] -> mt ()
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 344a04a6a..260e86ad6 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
open Genarg
open Ppconstr
open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2a66ba852..0a288c76e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -86,7 +86,9 @@ let def_of_const t =
let type_of_const sigma t =
match (EConstr.kind sigma t) with
- Const sp -> Typeops.type_of_constant (Global.env()) sp
+ | Const sp ->
+ (* FIXME discarding universe constraints *)
+ Typeops.type_of_constant_in (Global.env()) sp
|_ -> assert false
let constr_of_global x =
@@ -1449,7 +1451,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let ids = pf_ids_of_hyps g in
let terminate_constr = constr_of_global term_f in
let terminate_constr = EConstr.of_constr terminate_constr in
- let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const sigma terminate_constr))) (*FIXME*) in
+ let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in
let x = n_x_id ids nargs in
observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
h_intros x;
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 82218a35c..5b56fb35b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1535,26 +1535,26 @@ let rec apply_ids t ids =
| i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
let coq_Node =
- EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
+ lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node"))
let coq_Leaf =
- EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
+ lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf"))
let coq_Empty =
- EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
+ lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty"))
let coq_VarMap =
- EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
+ lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"))
let rec dump_varmap typ m =
match m with
- | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
- | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
- | Mc.Node(l,o,r) ->
- Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+ | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+ | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+ | Mc.Node(l,o,r) ->
+ Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
let vm_of_list env =
@@ -1727,7 +1727,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
- ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|]));
+ ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl))
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c40a1a9d9..1094d50af 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -359,7 +359,7 @@ let nf_open_term sigma0 ise c =
!s', Evd.evar_universe_context s, EConstr.of_constr c'
let unif_end env sigma0 ise0 pt ok =
- let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+ let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
let s, uc, t = nf_open_term sigma0 ise pt in
let ise1 = create_evar_defs s in
let ise1 = Evd.set_universe_context ise1 uc in
@@ -395,7 +395,8 @@ let iter_constr_LR f c = match kind_of_term c with
| Case (_, p, v, b) -> f v; f p; Array.iter f b
| Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
- | _ -> ()
+ | Proj(_,a) -> f a
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> ()
(* The comparison used to determine which subterms matches is KEYED *)
(* CONVERSION. This looks for convertible terms that either have the same *)
@@ -439,7 +440,7 @@ let proj_nparams c =
try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
let isFixed c = match kind_of_term c with
- | Var _ | Ind _ | Construct _ | Const _ -> true
+ | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
| _ -> false
let isRigid c = match kind_of_term c with
@@ -493,6 +494,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
let np = proj_nparams p in
if np = 0 || np > List.length a then KpatConst, f, a else
let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
+ | Proj (p,arg) -> KpatProj (Projection.constant p), f, a
| Var _ | Ind _ | Construct _ -> KpatFixed, f, a
| Evar (k, _) ->
if Evd.mem sigma0 k then KpatEvar k, f, a else
@@ -530,7 +532,13 @@ let nb_cs_proj_args pc f u =
try match kind_of_term f with
| Prod _ -> na Prod_cs
| Sort s -> na (Sort_cs (family_of_sort s))
- | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f))
+ | Const (c',_) when Constant.equal c' pc ->
+ begin match kind_of_term u.up_f with
+ | App(_,args) -> Array.length args
+ | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
+ the number of arguments including the projected *)
+ | _ -> assert false
+ end
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
| _ -> -1
with Not_found -> -1
@@ -573,6 +581,10 @@ let filter_upat i0 f n u fpats =
if np < na then fpats else
let () = if !i0 < np then i0 := n in (u, np) :: fpats
+let eq_prim_proj c t = match kind_of_term t with
+ | Proj(p,_) -> Constant.equal (Projection.constant p) c
+ | _ -> false
+
let filter_upat_FO i0 f n u fpats =
let np = nb_args u.up_FO in
if n < np then fpats else
@@ -583,7 +595,7 @@ let filter_upat_FO i0 f n u fpats =
| KpatLet -> isLetIn f
| KpatLam -> isLambda f
| KpatRigid -> isRigid f
- | KpatProj pc -> Term.eq_constr f (mkConst pc)
+ | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
| KpatFlex -> i0 := n; true in
if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index fa0c2f5b1..894cdb943 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
(** Very low level APIs.
these are calls to evarconv's [the_conv_x] followed by
- [consider_remaining_unif_problems] and [resolve_typeclasses].
+ [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
In case of failure they raise [NoMatch] *)
val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 19:13:06 +0000