diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | parsing/astterm.ml | 123 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/symbols.ml | 72 | ||||
| -rw-r--r-- | parsing/symbols.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
7 files changed, 141 insertions, 73 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index d8663f09d..5060b17a8 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1908,6 +1908,8 @@ let xlate_vernac = coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*) | VernacOpenScope sc -> xlate_error "TODO: open scope" + | VernacArgumentsScope _ -> xlate_error "TODO: Arguments Scope" + | VernacDelimiters _ -> xlate_error "TODO: Delimiters" | VernacNotation _ -> xlate_error "TODO: Notation" diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 03e652cce..40c2162da 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -30,6 +30,7 @@ open Evarutil open Ast open Coqast open Nametab +open Symbols (*Takes a list of variables which must not be globalized*) let from_list l = List.fold_right Idset.add l Idset.empty @@ -246,30 +247,22 @@ let maybe_constructor allow_var env = function | _ -> anomaly "ast_to_pattern: badly-formed ast for Cases pattern" -let ast_to_global loc c = - match c with - | ("CONST", [sp]) -> - let ref = ConstRef (ast_to_sp sp) in - let imps = implicits_of_global ref in - RRef (loc, ref), imps - | ("SECVAR", [Nvar (_,s)]) -> - let ref = VarRef s in - let imps = implicits_of_global ref in - RRef (loc, ref), imps - | ("MUTIND", [sp;Num(_,tyi)]) -> - let ref = IndRef (ast_to_sp sp, tyi) in - let imps = implicits_of_global ref in - RRef (loc, ref), imps - | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) -> - let ref = ConstructRef ((ast_to_sp sp,ti),n) in - let imps = implicits_of_global ref in - RRef (loc, ref), imps - | ("EVAR", [(Num (_,ev))]) -> - REvar (loc, ev), [] - | ("SYNCONST", [sp]) -> - Syntax_def.search_syntactic_definition loc (ast_to_sp sp), [] - | _ -> anomaly_loc (loc,"ast_to_global", - (str "Bad ast for this global a reference")) +let ast_to_global loc = function + | ("SYNCONST", [sp]) -> + Syntax_def.search_syntactic_definition loc (ast_to_sp sp), [], [] + | ("EVAR", [(Num (_,ev))]) -> + REvar (loc, ev), [], [] + | ast -> + let ref = match ast with + | ("CONST", [sp]) -> ConstRef (ast_to_sp sp) + | ("SECVAR", [Nvar (_,s)]) -> VarRef s + | ("MUTIND", [sp;Num(_,tyi)]) -> IndRef (ast_to_sp sp, tyi) + | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) -> + ConstructRef ((ast_to_sp sp,ti),n) + | _ -> anomaly_loc (loc,"ast_to_global", + (str "Bad ast for this global a reference")) + in + RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref (* let ref_from_constr c = match kind_of_term c with @@ -286,29 +279,29 @@ let ref_from_constr c = match kind_of_term c with abstracted until this point *) let ast_to_var (env,impls,_) (vars1,vars2) loc id = - let imps = + let imps, subscopes = if Idset.mem id env or List.mem id vars1 then - try List.assoc id impls - with Not_found -> [] + try List.assoc id impls, [] + with Not_found -> [], [] else let _ = lookup_named id vars2 in (* Car Fixpoint met les fns définies tmporairement comme vars de sect *) try let ref = VarRef id in - implicits_of_global ref - with _ -> [] - in RVar (loc, id), imps + implicits_of_global ref, find_arguments_scope ref + with _ -> [], [] + in RVar (loc, id), imps, subscopes (**********************************************************************) let rawconstr_of_var env vars loc id = try - ast_to_var env vars loc id + let (r,_,_) = ast_to_var env vars loc id in r with Not_found -> Pretype_errors.error_var_not_found_loc loc id -let rawconstr_of_qualid env vars loc qid = +let rawconstr_of_qualid_gen env vars loc qid = (* Is it a bound variable? *) try match repr_qualid qid with @@ -319,13 +312,15 @@ let rawconstr_of_qualid env vars loc qid = try match Nametab.extended_locate qid with | TrueGlobal ref -> if !dump then add_glob loc ref; - let imps = implicits_of_global ref in - RRef (loc, ref), imps + RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref | SyntacticDef sp -> - Syntax_def.search_syntactic_definition loc sp, [] + Syntax_def.search_syntactic_definition loc sp, [], [] with Not_found -> error_global_not_found_loc loc qid +let rawconstr_of_qualid env vars loc qid = + let (r,_,_) = rawconstr_of_qualid_gen env vars loc qid in r + let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some x,b)]) let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)]) @@ -335,6 +330,11 @@ let destruct_binder = function | Node(_,"BINDER",c::idl) -> List.map (fun id -> (nvar_of_ast id,c)) idl | _ -> anomaly "BINDER is expected" +let apply_scope_env (ids,impls,scopes as env) = function + | [] -> env, [] + | (Some sc)::scl -> (ids,impls,sc::scopes), scl + | None::scl -> env, scl + (* [merge_aliases] returns the sets of all aliases encountered at this point and a substitution mapping extra aliases to the first one *) let merge_aliases (ids,subst as aliases) = function @@ -442,10 +442,10 @@ let build_expression loc1 loc2 (ref,impls) args = let ast_to_rawconstr sigma env allow_soapp lvar = let rec dbrec (ids,impls,scopes as env) = function | Nvar(loc,s) -> - fst (rawconstr_of_var env lvar loc s) + rawconstr_of_var env lvar loc s | Node(loc,"QUALID", l) -> - fst (rawconstr_of_qualid env lvar loc (interp_qualid l)) + rawconstr_of_qualid env lvar loc (interp_qualid l) | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) -> let (lf,ln,lA,lt) = ast_to_fix ldecl in @@ -501,21 +501,26 @@ let ast_to_rawconstr sigma env allow_soapp lvar = dbrec (ids,impls,sc::scopes) e | Node(loc,"APPLISTEXPL", f::args) -> - RApp (loc,dbrec env f,ast_to_args env args) + let (f,_,subscopes) = match f with + | Node(locs,"QUALID",p) -> + rawconstr_of_qualid_gen env lvar locs (interp_qualid p) + | _ -> + (dbrec env f, [], []) in + RApp (loc,f,ast_to_args env subscopes args) | Node(loc,"APPLIST", f::args) -> - let (c, impargs) = + let (c, impargs, subscopes) = match f with | Node(locs,"QUALID",p) -> - rawconstr_of_qualid env lvar locs (interp_qualid p) + rawconstr_of_qualid_gen env lvar locs (interp_qualid p) (* For globalized references (e.g. in Infix) *) | Node(loc, ("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key), l) -> ast_to_global loc (key,l) - | _ -> (dbrec env f, []) + | _ -> (dbrec env f, [], []) in - RApp (loc, c, ast_to_impargs c env impargs args) + RApp (loc, c, ast_to_impargs c env impargs subscopes args) | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) -> let po = match p with @@ -545,7 +550,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar = (* This case mainly parses things build in a quotation *) | Node(loc,("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) -> - fst (ast_to_global loc (key,l)) + let (r,_,_) = ast_to_global loc (key,l) in r | Node(loc,"CAST", [c1;c2]) -> RCast (loc,dbrec env c1,dbrec env c2) @@ -602,14 +607,16 @@ let ast_to_rawconstr sigma env allow_soapp lvar = | _ -> assert false) | body -> dbrec env body - and ast_to_impargs c env l args = - let rec aux n l args = match (l,args) with + and ast_to_impargs c env l subscopes args = + let rec aux n l subscopes args = + let (enva,subscopes') = apply_scope_env env subscopes in + match (l,args) with | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') -> if i=n & j>=i then - if j=i then - (dbrec env a)::(aux (n+1) l' args') + if j=i then + (dbrec enva a)::(aux (n+1) l' subscopes' args') else - (RHole (set_hole_implicit i c))::(aux (n+1) l' args) + (RHole (set_hole_implicit i c))::(aux (n+1) l' subscopes' args) else if i<>n then error ("Bad explicitation number: found "^ @@ -619,19 +626,21 @@ let ast_to_rawconstr sigma env allow_soapp lvar = (string_of_int j)^" but was expecting "^(string_of_int i)) | (i::l',a::args') -> if i=n then - (RHole (set_hole_implicit i c))::(aux (n+1) l' args) + (RHole (set_hole_implicit i c))::(aux (n+1) l' subscopes' args) else - (dbrec env a)::(aux (n+1) l args') - | ([],args) -> ast_to_args env args + (dbrec enva a)::(aux (n+1) l subscopes' args') + | ([],args) -> ast_to_args env subscopes args | (_,[]) -> [] in - aux 1 l args + aux 1 l subscopes args - and ast_to_args env = function + and ast_to_args env subscopes = function | Node(loc, "EXPL", _)::args' -> (* To deal with errors *) error_expl_impl_loc loc - | a::args -> (dbrec env a) :: (ast_to_args env args) + | a::args -> + let enva, subscopes = apply_scope_env env subscopes in + (dbrec enva a) :: (ast_to_args env subscopes args) | [] -> [] and interp_binding env = function @@ -643,7 +652,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar = errorlabstrm "bind_interp" (str "Not the expected form in binding" ++ print_ast x) - in + in dbrec env (**************************************************************************) @@ -781,7 +790,9 @@ let constrOut = function (str "Not a Dynamic ast: " ++ print_ast ast) let interp_global_constr env (loc,qid) = - let c,_ = rawconstr_of_qualid (Idset.empty,[],Symbols.current_scopes()) ([],env) loc qid in + let c = + rawconstr_of_qualid (Idset.empty,[],current_scopes()) ([],env) loc qid + in understand Evd.empty env c let interp_constr sigma env c = diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index bac489217..4b5c98ba7 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -223,6 +223,9 @@ GEXTEND Gram | IDENT "Delimiters"; left = STRING; sc = IDENT; right = STRING -> VernacDelimiters (sc,(left,right)) + | IDENT "Arguments"; IDENT "Scope"; qid = qualid; + "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) + (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *) | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = qualid; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc) @@ -235,6 +238,9 @@ GEXTEND Gram to factorize with other "Print"-based vernac entries *) ] ] ; + opt_scope: + [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ] + ; (* Syntax entries for Grammar. Only grammar_entry is exported *) grammar_entry: [[ nont = located_ident; etyp = set_entry_type; ":="; diff --git a/parsing/symbols.ml b/parsing/symbols.ml index e13fd3df4..075cd322d 100644 --- a/parsing/symbols.ml +++ b/parsing/symbols.ml @@ -78,13 +78,18 @@ let lookup_numeral_interpreter s = (* For loading without opening *) let declare_scope scope = try let _ = Stringmap.find scope !scope_map in () - with Not_found -> scope_map := Stringmap.add scope empty_scope !scope_map + with Not_found -> +(* Options.if_verbose message ("Creating scope "^scope);*) + scope_map := Stringmap.add scope empty_scope !scope_map + +let find_scope scope = + try Stringmap.find scope !scope_map + with Not_found -> error ("Scope "^scope^" is not declared") + +let check_scope sc = let _ = find_scope sc in () let declare_delimiters scope dlm = - let sc = - try Stringmap.find scope !scope_map - with Not_found -> empty_scope - in + let sc = find_scope scope in if sc.delimiters <> None && Options.is_verbose () then warning ("Overwriting previous delimiters in "^scope); let sc = { sc with delimiters = Some dlm } in @@ -93,10 +98,7 @@ let declare_delimiters scope dlm = (* The mapping between notations and production *) let declare_notation nt c scope = - let sc = - try Stringmap.find scope !scope_map - with Not_found -> empty_scope - in + let sc = find_scope scope in if Stringmap.mem nt sc.notations && Options.is_verbose () then warning ("Notation "^nt^" is already used in scope "^scope); let sc = { sc with notations = Stringmap.add nt c sc.notations } in @@ -110,7 +112,7 @@ let rec subst_meta_rawconstr subst = function let rec find_interpretation f = function | scope::scopes -> - (try f (Stringmap.find scope !scope_map) + (try f (find_scope scope) with Not_found -> find_interpretation f scopes) | [] -> raise Not_found @@ -224,10 +226,8 @@ let rec interp_numeral_as_pattern loc n name = function (* Exportation of scopes *) let cache_scope (_,sc) = - if Stringmap.mem sc !scope_map then - scope_stack := sc :: !scope_stack - else - error ("Unknown scope: "^sc) + check_scope sc; + scope_stack := sc :: !scope_stack let subst_scope (_,subst,sc) = sc @@ -243,13 +243,51 @@ let (inScope,outScope) = let open_scope sc = Lib.add_anonymous_leaf (inScope sc) + +(* Special scopes associated to arguments of a global reference *) + +open Libnames + +module RefOrdered = + struct + type t = global_reference + let compare = Pervasives.compare + end + +module Refmap = Map.Make(RefOrdered) + +let arguments_scope = ref Refmap.empty + +let cache_arguments_scope (_,(r,scl)) = + List.iter (option_iter check_scope) scl; + arguments_scope := Refmap.add r scl !arguments_scope + +let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl) + +let (inArgumentsScope,outArgumentsScope) = + declare_object {(default_object "ARGUMENTS-SCOPE") with + cache_function = cache_arguments_scope; + open_function = (fun i o -> if i=1 then cache_arguments_scope o); + subst_function = subst_arguments_scope; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +let declare_arguments_scope r scl = + Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) + +let find_arguments_scope r = + try Refmap.find r !arguments_scope + with Not_found -> [] + + (* Synchronisation with reset *) -let freeze () = (!scope_map, !scope_stack) +let freeze () = (!scope_map, !scope_stack, !arguments_scope) -let unfreeze (scm,scs) = +let unfreeze (scm,scs,asc) = scope_map := scm; - scope_stack := scs + scope_stack := scs; + arguments_scope := asc let init () = () (* diff --git a/parsing/symbols.mli b/parsing/symbols.mli index c0d8eea29..d8edb3179 100644 --- a/parsing/symbols.mli +++ b/parsing/symbols.mli @@ -46,3 +46,9 @@ val find_notation : scope_name -> notation -> scopes -> (delimiters option * scopes) option val exists_notation_in_scope : scope_name -> notation -> bool val exists_notation : notation -> bool + +(* Declare and look for scopes associated to arguments of a global ref *) +open Libnames +val declare_arguments_scope: global_reference -> scope_name option list -> unit +val find_arguments_scope : global_reference -> scope_name option list + diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b0f53b839..b3825dd93 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -289,6 +289,9 @@ let vernac_delimiters = Metasyntax.add_delimiters let vernac_open_scope = Symbols.open_scope +let vernac_arguments_scope qid scl = + Symbols.declare_arguments_scope (global qid) scl + let vernac_infix assoc n inf qid sc = let sp = sp_of_global None (global qid) in let dir = repr_dirpath (dirpath sp) in @@ -1032,6 +1035,7 @@ let interp c = match c with | VernacGrammar (univ,al) -> vernac_grammar univ al | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc + | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc | VernacNotation (assoc,n,inf,c,sc) -> vernac_notation assoc n inf c sc diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e0f0dc00e..d2ad10bb6 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -186,6 +186,7 @@ type vernac_expr = | VernacSyntax of string * syntax_entry_ast list | VernacOpenScope of scope_name | VernacDelimiters of scope_name * (string * string) + | VernacArgumentsScope of qualid located * scope_name option list | VernacInfix of grammar_associativity * int * string * qualid located * scope_name option | VernacDistfix of |