From a74e055acf48583c6fece5d22c805736679376b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Aug 2019 20:27:52 +0200 Subject: [api] Move handling of variable implicit data to impargs We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function. --- plugins/funind/gen_principle.ml | 2 +- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/glob_termops.ml | 1 - plugins/ltac/g_tactic.mlg | 5 ++--- plugins/ltac/pptactic.ml | 3 +-- plugins/ssr/ssrcommon.ml | 1 - plugins/ssr/ssrparser.mlg | 15 +++++++-------- plugins/ssr/ssrvernac.mlg | 1 - plugins/ssrmatching/ssrmatching.ml | 1 - plugins/syntax/numeral.ml | 2 +- plugins/syntax/string_notation.ml | 2 +- 11 files changed, 14 insertions(+), 21 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730ae48393..a836335d4d 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1600,7 +1600,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( [CAst.make @@ Name a; CAst.make @@ Name b], - Constrexpr.Default Decl_kinds.Explicit, + Constrexpr.Default Glob_term.Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, [ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6eb8c42d1d..ddd6ecfb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt = | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt)], + Constrexpr.Default Explicit, rt)], CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index d36d86a65b..fbf63c69dd 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -4,7 +4,6 @@ open Glob_term open CErrors open Util open Names -open Decl_kinds (* Some basic functions to rebuild glob_constr diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 7cd43cb5cd..9b52b710c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -24,7 +24,6 @@ open Tactypes open Tactics open Inv open Locus -open Decl_kinds open Pcoq @@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram | -> { true } ] ] ; simple_binder: - [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) } ] ] ; fixdecl: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0e38ce575b..6df068883c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,7 +20,6 @@ open Stdarg open Notation_gram open Tactypes open Locus -open Decl_kinds open Genredexpr open Ppconstr open Pputils @@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with - Glob_term.GProd(na,Explicit,a,b) -> + Glob_term.GProd(na,Glob_term.Explicit,a,b) -> strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 33e9f871fd..473612fda7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term -open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 175a863ad8..a1f707ffa8 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -32,7 +32,6 @@ open Ppconstr open Namegen open Tactypes -open Decl_kinds open Constrexpr open Constrexpr_ops @@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde | [ ssrbvar(bv) ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ")" ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> { let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> { let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram ssrbinder: [ [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; END @@ -1391,7 +1390,7 @@ let push_binders c2 bs = let rec fix_binders = let open CAst in function | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> - CLocalAssum (xs, Default Explicit, t) :: fix_binders bs + CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs | _ -> [] @@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0adabb0673..f3f1d713e9 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -27,7 +27,6 @@ open Notation_ops open Notation_term open Glob_term open Stdarg -open Decl_kinds open Pp open Ppconstr open Printer diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 17db25660f..4d7a04f5ee 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -36,7 +36,6 @@ open Ppconstr open Printer open Globnames open Namegen -open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index a148a3bc73..9808c61255 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts = let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 8c0f9a3339..c92acb0f55 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope = let of_ty = Smartlocate.global_with_alias g in let cty = cref ty in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let constructors = get_constructors tyc in (* Check the type of f *) -- cgit v1.2.3