aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml5
-rw-r--r--library/impargs.ml79
-rw-r--r--library/impargs.mli3
-rw-r--r--parsing/g_vernacnew.ml47
-rw-r--r--toplevel/vernacexpr.ml2
-rw-r--r--translate/ppvernacnew.ml17
6 files changed, 81 insertions, 32 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ec9e88c77..3ebad5ae3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1674,7 +1674,10 @@ let xlate_vernac =
(reference_to_ct_ID id,
match opt_positions with
None -> CT_int_list[]
- | Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+ | Some l ->
+ CT_int_list
+ (List.map (function ExplByPos x -> CT_int x | ExplByName _ ->
+ xlate_error "TODO: explicit argument by name") l))
| VernacReserve _ -> xlate_error "TODO: Default Variable Type"
| VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
diff --git a/library/impargs.ml b/library/impargs.ml
index f2c37374d..831b34e05 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
open Lib
open Nametab
open Pp
+open Topconstr
(*s Flags governing the computation of implicit arguments *)
@@ -208,13 +209,20 @@ let add_free_rels_until strict bound env m pos acc =
(* calcule la liste des arguments implicites *)
+let my_concrete_name avoid names t = function
+ | Anonymous -> Anonymous, avoid, Anonymous::names
+ | na ->
+ let id = Termops.next_name_not_occuring false na avoid names t in
+ Name id, id::avoid, Name id::names
+
let compute_implicits_gen strict contextual env t =
- let rec aux env n names t =
+ let rec aux env avoid n names t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
- | Prod (x,a,b) ->
+ | Prod (na,a,b) ->
+ let na',avoid' = Termops.concrete_name false avoid names na b in
add_free_rels_until strict n env a (Hyp (n+1))
- (aux (push_rel (x,None,a) env) (n+1) (x::names) b)
+ (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
| _ ->
let names = List.rev names in
let v = Array.map (fun na -> na,None) (Array.of_list names) in
@@ -222,8 +230,9 @@ let compute_implicits_gen strict contextual env t =
else v
in
match kind_of_term (whd_betadeltaiota env t) with
- | Prod (x,a,b) ->
- let v = aux (push_rel (x,None,a) env) 1 [x] b in
+ | Prod (na,a,b) ->
+ let na',avoid = Termops.concrete_name false [] [] na b in
+ let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
Array.to_list v
| _ -> []
@@ -435,31 +444,55 @@ let implicits_of_global_out r =
(* Declare manual implicits *)
-let check_range n i =
- if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+(*
+let check_range n = function
+ | loc,ExplByPos i ->
+ if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+ | loc,ExplByName id ->
+()
+*)
+
+let rec list_remove a = function
+ | b::l when a = b -> l
+ | b::l -> b::list_remove a l
+ | [] -> raise Not_found
+let set_implicit id imp =
+ Some (id,match imp with None -> Manual | Some imp -> imp)
let declare_manual_implicits r l =
let t = Global.type_of_global r in
let autoimps = compute_implicits_gen false true (Global.env()) t in
let n = List.length autoimps in
- if not (list_distinct l) then error ("Some numbers occur several time");
- List.iter (check_range n) l;
- let l = List.sort (-) l in
+ if not (list_distinct l) then
+ error ("Some parameters are referred more than once");
+(* List.iter (check_range n) l;*)
+(* let l = List.sort (-) l in*)
(* Compare with automatic implicits to recover printing data and names *)
- let rec merge k = function
- | [], [] -> []
- | ((na,imp)::imps, p::l) when k=p ->
- let id = match na with
- | Name id -> id
- | _ -> errorlabstrm ""
- (str "Cannot set implicit argument number " ++ int p ++
- str ": it has no name") in
- let imp = match imp with None -> (id,Manual) | Some imp -> (id,imp) in
- Some imp :: merge (k+1) (imps,l)
- | _::imps, l' -> None :: merge (k+1) (imps,l')
- | [], _ -> assert false in
- let l = Impl_manual (merge 1 (autoimps,l)) in
+ let rec merge k l = function
+ | (Name id,imp)::imps ->
+ let l',imp =
+ try list_remove (ExplByPos k) l, set_implicit id imp
+ with Not_found ->
+ try list_remove (ExplByName id) l, set_implicit id imp
+ with Not_found ->
+ l, None in
+ imp :: merge (k+1) l' imps
+ | (Anonymous,imp)::imps ->
+ None :: merge (k+1) l imps
+ | [] when l = [] -> []
+ | _ ->
+ match List.hd l with
+ | ExplByName id ->
+ error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+ | ExplByPos i ->
+ if i<1 or i>n then
+ error ("Bad implicit argument number: "^(string_of_int i))
+ else
+ errorlabstrm ""
+ (str "Cannot set implicit argument number " ++ int i ++
+ str ": it has no name") in
+ let l = Impl_manual (merge 1 l autoimps) in
let (_,oimp_out) = implicits_of_global_gen r in
let l = l, if !Options.v7_only then oimp_out else l in
add_anonymous_leaf (in_implicits [r,l])
diff --git a/library/impargs.mli b/library/impargs.mli
index 83ca8dfb9..1ee82c384 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -54,7 +54,8 @@ val declare_mib_implicits : mutual_inductive -> unit
val declare_implicits : global_reference -> unit
(* Manual declaration of which arguments are expected implicit *)
-val declare_manual_implicits : global_reference -> int list -> unit
+val declare_manual_implicits : global_reference ->
+ Topconstr.explicitation list -> unit
(* Get implicit arguments *)
val is_implicit_constant : constant -> implicits_flags
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4c096964d..cca57911b 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -436,8 +436,9 @@ GEXTEND Gram
VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
*)
| IDENT "Implicit"; IDENT "Arguments"; qid = global;
- pos = OPT [ "["; l = LIST0 natural; "]" -> l ] ->
- VernacDeclareImplicits (qid,pos)
+ pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
+ let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+ VernacDeclareImplicits (qid,pos)
| IDENT "Implicit"; ["Type" | "Types"];
idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c)
@@ -681,7 +682,7 @@ GEXTEND Gram
"["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
| IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *)
- op = STRING; p = global;
+ op = STRING; ":="; p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3d5068304..d142f1d87 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -234,7 +234,7 @@ type vernac_expr =
| VernacHintDestruct of locality_flag *
identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
| VernacSyntacticDefinition of identifier * constr_expr * int option
- | VernacDeclareImplicits of reference * int list option
+ | VernacDeclareImplicits of reference * explicitation list option
| VernacReserve of identifier list * constr_expr
| VernacSetOpacity of opacity_flag * reference list
| VernacUnsetOption of Goptions.option_name
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 81818bb08..0e5e1c99d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -169,6 +169,10 @@ let pr_search a b pr_p = match a with
let pr_locality local = if local then str "Local " else str ""
+let pr_explanation imps = function
+ | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
+ | ExplByName id -> pr_id id
+
let pr_class_rawexpr = function
| FunClass -> str"Funclass"
| SortClass -> str"Sortclass"
@@ -555,7 +559,7 @@ let rec pr_vernac = function
(match a with None -> [] | Some a -> [SetAssoc a]),s
| None -> [],s in
hov 0 (hov 0 (str"Infix " ++ pr_locality local
- ++ qsnew s ++ spc() ++ pr_reference q) ++
+ ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
pr_syntax_modifiers mv8 ++
(match sn with
| None -> mt()
@@ -971,8 +975,11 @@ pr_vbinders bl ++ spc())
| VernacDeclareImplicits (q,None) ->
hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
| VernacDeclareImplicits (q,Some l) ->
+ let r = Nametab.global q in
+ Impargs.declare_manual_implicits r l;
+ let imps = Impargs.implicits_of_global r in
hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
- str"[" ++ prlist_with_sep sep int l ++ str"]")
+ str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
| VernacReserve (idl,c) ->
hov 1 (str"Implicit Type" ++
str (if List.length idl > 1 then "s " else " ") ++
@@ -1100,7 +1107,11 @@ let pr_vernac = function
(* Obsolete modules *)
List.mem (string_of_id r)
["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide";
- "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"] -> mt()
+ "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep";
+ "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax";
+ "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"] ->
+ warning ("Forgetting obsolete module "^(string_of_id r));
+ mt()
| VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x
| x -> pr_vernac x ++ sep_end ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 03:14:41 +0000