diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 | ||||
| -rw-r--r-- | interp/symbols.ml | 11 | ||||
| -rw-r--r-- | interp/symbols.mli | 3 | ||||
| -rw-r--r-- | parsing/extend.ml | 66 | ||||
| -rw-r--r-- | parsing/extend.mli | 18 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 13 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 24 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 31 | ||||
| -rw-r--r-- | toplevel/command.ml | 23 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 113 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 19 |
16 files changed, 237 insertions, 116 deletions
@@ -158,11 +158,10 @@ TACTICS=\ TOPLEVEL=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ + toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ toplevel/command.cmo toplevel/record.cmo toplevel/recordobj.cmo \ - toplevel/discharge.cmo toplevel/vernacexpr.cmo \ - translate/ppvernacnew.cmo \ + toplevel/discharge.cmo translate/ppvernacnew.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ - toplevel/metasyntax.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ toplevel/toplevel.cmo toplevel/usage.cmo \ diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index ed6980657..ff361e8f4 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -116,7 +116,7 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in let sp = sp_of_global (IndRef (sp, tyi)) in - (basename sp, + (basename sp, None, convert_env(List.rev params), (extern_constr true envpar arity), convert_constructors envpar cstrnames cstrtypes);; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 07deebf4a..5692f780d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1536,10 +1536,12 @@ let xlate_vernac = *) | VernacInductive (isind, lmi) -> let co_or_ind = if isind then "Inductive" else "CoInductive" in - let strip_mutind (s, parameters, c, constructors) = + let strip_mutind (s, notopt, parameters, c, constructors) = + if notopt = None then CT_ind_spec (xlate_ident s, cvt_vernac_binders parameters, xlate_formula c, - build_constructors constructors) in + build_constructors constructors) + else xlate_error "TODO: Notation in Inductive" in CT_mind_decl (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) | VernacFixpoint [] -> xlate_error "mutual recursive" diff --git a/interp/symbols.ml b/interp/symbols.ml index 0c988f315..ef2cf6b0b 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -396,6 +396,17 @@ let locate_notation prraw ntn = fnl ())) l +let find_notation_level ntn = + let l = + Stringmap.fold + (fun _ sc l -> + try fst (snd (Stringmap.find ntn sc.notations)) :: l + with Not_found -> l) !scope_map [] in + match l with + | [] -> raise Not_found + | [prec] -> prec + | prec::_ -> warning ("Several parsing rules for notation \""^ntn^"\""); prec + (**********************************************************************) (* Mapping notations to concrete syntax *) diff --git a/interp/symbols.mli b/interp/symbols.mli index 42eedaf81..fa3d778f1 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -117,6 +117,9 @@ val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds +(* [raise Not_found] if non existing notation *) +val find_notation_level : notation -> level + (**********************************************************************) (*s Printing rules for notations *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 076f7f026..6a557f368 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -24,14 +24,20 @@ type production_position = | BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *) | InternalProd -type 'pos constr_entry_key = +type production_level = + | NextLevel + | NumLevel of int + +type ('lev,'pos) constr_entry_key = | ETIdent | ETReference | ETBigint - | ETConstr of (int * 'pos) + | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string -type constr_production_entry = production_position constr_entry_key -type constr_entry = unit constr_entry_key +type constr_production_entry = + (production_level,production_position) constr_entry_key +type constr_entry = (int,unit) constr_entry_key +type simple_constr_production_entry = (production_level,unit) constr_entry_key type nonterm_prod = | ProdList0 of nonterm_prod @@ -80,10 +86,10 @@ let act_of_ast vars = function let to_act_check_vars = act_of_ast type syntax_modifier = - | SetItemLevel of string list * int + | SetItemLevel of string list * production_level | SetLevel of int | SetAssoc of Gramext.g_assoc - | SetEntryType of string * constr_entry + | SetEntryType of string * simple_constr_production_entry | SetOnlyParsing type nonterm = @@ -162,44 +168,50 @@ let rename_command_entry nt = (* This translates constr0, constr1, ... level into camlp4 levels of constr *) -let explicitize_prod_entry pos univ nt = +let explicitize_prod_entry inj pos univ nt = if univ = "prim" & nt = "var" then ETIdent else if univ = "prim" & nt = "bigint" then ETBigint else if univ <> "constr" then ETOther (univ,nt) else match nt with - | "constr0" -> ETConstr (0,pos) - | "constr1" -> ETConstr (1,pos) - | "constr2" -> ETConstr (2,pos) - | "constr3" -> ETConstr (3,pos) - | "lassoc_constr4" -> ETConstr (4,pos) - | "constr5" -> ETConstr (5,pos) - | "constr6" -> ETConstr (6,pos) - | "constr7" -> ETConstr (7,pos) - | "constr8" -> ETConstr (8,pos) - | "constr" when !Options.v7 -> ETConstr (8,pos) - | "constr9" -> ETConstr (9,pos) - | "constr10" | "lconstr" -> ETConstr (10,pos) + | "constr0" -> ETConstr (inj 0,pos) + | "constr1" -> ETConstr (inj 1,pos) + | "constr2" -> ETConstr (inj 2,pos) + | "constr3" -> ETConstr (inj 3,pos) + | "lassoc_constr4" -> ETConstr (inj 4,pos) + | "constr5" -> ETConstr (inj 5,pos) + | "constr6" -> ETConstr (inj 6,pos) + | "constr7" -> ETConstr (inj 7,pos) + | "constr8" -> ETConstr (inj 8,pos) + | "constr" when !Options.v7 -> ETConstr (inj 8,pos) + | "constr9" -> ETConstr (inj 9,pos) + | "constr10" | "lconstr" -> ETConstr (inj 10,pos) | "pattern" -> ETPattern | "ident" -> ETIdent | "global" -> ETReference | _ -> ETOther (univ,nt) -let explicitize_entry = explicitize_prod_entry () +let explicitize_entry = explicitize_prod_entry (fun x -> x) () (* Express border sub entries in function of the from level and an assoc *) (* We're cheating: not necessarily the same assoc on right and left *) let clever_explicitize_prod_entry pos univ from en = - let t = explicitize_prod_entry pos univ en in + let t = explicitize_prod_entry (fun x -> NumLevel x) pos univ en in match from with | ETConstr (from,()) -> (match t with - | ETConstr (n,BorderProd (left,None)) when (n=from & left) -> + | ETConstr (n,BorderProd (left,None)) + when (n=NumLevel from & left) -> ETConstr (n,BorderProd (left,Some Gramext.LeftA)) - | ETConstr (n,BorderProd (left,None)) when (n=from-1 & not left) -> - ETConstr (n+1,BorderProd (left,Some Gramext.LeftA)) - | ETConstr (n,BorderProd (left,None)) when (n=from-1 & left) -> - ETConstr (n+1,BorderProd (left,Some Gramext.RightA)) - | ETConstr (n,BorderProd (left,None)) when (n=from & not left) -> + | ETConstr (NumLevel n,BorderProd (left,None)) + when (n=from-1 & not left) -> + ETConstr + (NumLevel (n+1),BorderProd (left,Some Gramext.LeftA)) + | ETConstr (NumLevel n,BorderProd (left,None)) + when (n=from-1 & left) -> + ETConstr + (NumLevel (n+1),BorderProd (left,Some Gramext.RightA)) + | ETConstr (n,BorderProd (left,None)) + when (n=NumLevel from & not left) -> ETConstr (n,BorderProd (left,Some Gramext.RightA)) | t -> t) | _ -> t diff --git a/parsing/extend.mli b/parsing/extend.mli index 808e50158..ef685ffb1 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -25,14 +25,20 @@ type production_position = | BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *) | InternalProd -type 'pos constr_entry_key = +type production_level = + | NextLevel + | NumLevel of int + +type ('lev,'pos) constr_entry_key = | ETIdent | ETReference | ETBigint - | ETConstr of (int * 'pos) + | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string -type constr_production_entry = production_position constr_entry_key -type constr_entry = unit constr_entry_key +type constr_production_entry = + (production_level,production_position) constr_entry_key +type constr_entry = (int,unit) constr_entry_key +type simple_constr_production_entry = (production_level,unit) constr_entry_key type nonterm_prod = | ProdList0 of nonterm_prod @@ -68,10 +74,10 @@ val set_constr_globalizer : (entry_context -> constr_expr -> constr_expr) -> unit type syntax_modifier = - | SetItemLevel of string list * int + | SetItemLevel of string list * production_level | SetLevel of int | SetAssoc of Gramext.g_assoc - | SetEntryType of string * constr_entry + | SetEntryType of string * simple_constr_production_entry | SetOnlyParsing type nonterm = diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 3db24bcd1..13d4a623b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -214,7 +214,7 @@ END (* automatic translation of levels *) let adapt_level n = n*10 let map_modl = function - | SetItemLevel(ids,n) -> SetItemLevel(ids,adapt_level n) + | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n)) | SetLevel n -> SetLevel(adapt_level n) | m -> m @@ -305,11 +305,14 @@ GEXTEND Gram locality: [ [ IDENT "Local" -> true | -> false ] ] ; + level: + [ [ IDENT "level"; n = natural -> NumLevel n + | IDENT "next"; IDENT "level" -> NextLevel ] ] + ; syntax_modifier: - [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> - SetItemLevel ([x],n) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level"; - n = natural -> SetItemLevel (x::l,n) + [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; lev = level -> + SetItemLevel (x::l,lev) | IDENT "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2d1fcdd30..5b88cee39 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -216,8 +216,9 @@ GEXTEND Gram (id,c,lc) ] ] ; oneind: - [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":="; - lc = constructor_list -> (id,indpar,c,lc) ] ] + [ [ ntn = OPT [ ntn = STRING; ":=" -> (ntn,None) ]; + id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":="; + lc = constructor_list -> (id,ntn,indpar,c,lc) ] ] ; simple_binders_list: [ [ bl = ne_simple_binders_list -> bl @@ -298,7 +299,7 @@ GEXTEND Gram gallina_ext: [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token; indl = block_old_style -> - let indl' = List.map (fun (id,ar,c) -> (id,bl,ar,c)) indl in + let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in VernacInductive (f,indl') | record_token; oc = opt_coercion; name = base_ident; ps = simple_binders_list; ":"; @@ -316,7 +317,7 @@ GEXTEND Gram | IDENT "Scheme"; l = schemes -> VernacScheme l | f = finite_token; s = csort; id = base_ident; indpar = simple_binders_list; ":="; lc = constructor_list -> - VernacInductive (f,[id,indpar,s,lc]) ] ] + VernacInductive (f,[id,None,indpar,s,lc]) ] ] ; csort: [ [ s = sort -> CSort (loc,s) ] ] diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 0e9e8dabb..4a6d3ca69 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -103,7 +103,7 @@ GEXTEND Gram test_plurial_form bl; VernacAssumption (stre, bl) (* Gallina inductive declarations *) - | OPT[IDENT "Mutual"]; f = finite_token; + | (* Non porté (?) : OPT[IDENT "Mutual"];*) f = finite_token; indl = LIST1 inductive_definition SEP "with" -> VernacInductive (f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -118,9 +118,11 @@ GEXTEND Gram s = lconstr; ":="; cstr = OPT base_ident; "{"; fs = LIST0 local_decl_expr; "}" -> VernacRecord ((oc,name),ps,s,cstr,fs) +(* Non porté ? | f = finite_token; s = csort; id = base_ident; indpar = LIST0 simple_binder; ":="; lc = constructor_list -> - VernacInductive (f,[id,indpar,s,lc]) + VernacInductive (f,[id,None,indpar,s,lc]) +*) ] ] ; thm_token: @@ -171,17 +173,20 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":="; - lc = constructor_list -> (id,indpar,c,lc) ] ] + [ [ ntn = OPT [ ntn = STRING -> (ntn,None) ]; + id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":="; + lc = constructor_list -> (id,ntn,indpar,c,lc) ] ] ; constructor_list: [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l | l = LIST1 constructor_binder SEP "|" -> l | -> [] ] ] ; +(* csort: [ [ s = sort -> CSort (loc,s) ] ] ; +*) opt_coercion: [ [ ">" -> true | -> false ] ] @@ -699,11 +704,14 @@ GEXTEND Gram [ [ univ = IDENT -> set_default_action_parser (parser_type_from_name univ); univ ] ] ; + level: + [ [ IDENT "level"; n = natural -> NumLevel n + | IDENT "next"; IDENT "level" -> NextLevel ] ] + ; syntax_modifier: - [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> - SetItemLevel ([x],n) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level"; - n = natural -> SetItemLevel (x::l,n) + [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; + lev = level -> SetItemLevel (x::l,lev) | IDENT "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d160734ea..39047e688 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -542,22 +542,27 @@ let camlp4_assoc = function s.t. if [cur] is set then [n] is the same as the [from] level *) let adjust_level assoc from = function (* Associativity is None means force the level *) - | (n,BorderProd (_,None)) -> Some (Some (n,true)) + | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) (* Compute production name on the right side *) (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (n,BorderProd (false,Some (Gramext.NonA|Gramext.LeftA))) -> Some None + | (NumLevel n,BorderProd (false,Some (Gramext.NonA|Gramext.LeftA))) -> + Some None (* If RightA on the right-hand side, set to the explicit (current) level *) - | (n,BorderProd (false,Some Gramext.RightA)) -> Some (Some (n,true)) + | (NumLevel n,BorderProd (false,Some Gramext.RightA)) -> + Some (Some (n,true)) (* Compute production name on the left side *) (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (n,BorderProd (true,Some Gramext.NonA)) -> None + | (NumLevel n,BorderProd (true,Some Gramext.NonA)) -> None (* If the expected assoc is the current one, set to SELF *) - | (n,BorderProd (true,Some a)) when a = camlp4_assoc assoc -> None + | (NumLevel n,BorderProd (true,Some a)) when a = camlp4_assoc assoc -> + None (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (n,BorderProd (true,Some a)) -> + | (NumLevel n,BorderProd (true,Some a)) -> if a = Gramext.LeftA then Some (Some (n,true)) else Some None + (* None means NEXT *) + | (NextLevel,_) -> Some None (* Compute production name elsewhere *) - | (n,InternalProd) -> + | (NumLevel n,InternalProd) -> match from with | ETConstr (p,()) when p = n+1 -> Some None | ETConstr (p,()) -> Some (Some (n,n=p)) @@ -609,7 +614,7 @@ let compute_entry allow_create adjust = function (* This computes the name of the level where to add a new rule *) let get_constr_entry en = match en with - ETConstr(200,_) when not !Options.v7 -> + ETConstr(200,()) when not !Options.v7 -> snd (get_entry (get_univ "constr") "binder_constr"), None, false @@ -620,7 +625,7 @@ let get_constr_entry en = let get_constr_production_entry ass from en = (* first 2 cases to help factorisation *) match en with - | ETConstr (10,q) when !Options.v7 -> + | ETConstr (NumLevel 10,q) when !Options.v7 -> weaken_entry Constr.lconstr, None, false (* | ETConstr (8,q) when !Options.v7 -> @@ -643,9 +648,9 @@ let constr_prod_level assoc cur lev = let is_self from e = match from, e with - ETConstr(n,_), ETConstr(n', + ETConstr(n,()), ETConstr(NumLevel n', BorderProd(false, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false - | ETConstr(n,_), ETConstr(n',BorderProd(true,_)) -> n=n' + | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(true,_)) -> n=n' | (ETIdent,ETIdent | ETReference, ETReference | ETBigint,ETBigint | ETPattern, ETPattern) -> true | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2' @@ -653,7 +658,7 @@ let is_self from e = let is_binder_level from e = match from, e with - ETConstr(200,_), ETConstr(200,_) -> not !Options.v7 + ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7 | _ -> false let symbol_of_production assoc from typ = @@ -667,3 +672,5 @@ let symbol_of_production assoc from typ = | (eobj,Some None,_) -> Gramext.Snext | (eobj,Some (Some (lev,cur)),_) -> Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev) + + diff --git a/toplevel/command.ml b/toplevel/command.ml index ed77973c2..337e321df 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -178,7 +178,7 @@ let corecursive_message v = let interp_mutual lparams lnamearconstrs finite = let allnames = List.fold_left - (fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in + (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in if not (list_distinct allnames) then error "Two inductive objects have the same name"; let nparams = List.length lparams @@ -201,7 +201,7 @@ let interp_mutual lparams lnamearconstrs finite = in let (ind_env,ind_impls,arityl) = List.fold_left - (fun (env, ind_impls, arl) (recname, arityc,_) -> + (fun (env, ind_impls, arl) (recname, _, arityc, _) -> let arity = interp_type sigma env_params arityc in let fullarity = prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in @@ -213,10 +213,19 @@ let interp_mutual lparams lnamearconstrs finite = (env', (recname,impls)::ind_impls, (arity::arl))) (env0, [], []) lnamearconstrs in + let lparnames = List.map (fun (na,_,_) -> na) params in + let fs = States.freeze() in + List.iter2 (fun (recname,ntnopt,_,_) ar -> + option_iter + (fun (df,scope) -> + let larnames = lparnames @ List.map fst (fst (decompose_prod ar)) in + Metasyntax.add_notation_interpretation df + (AVar recname,larnames) scope) ntnopt) + lnamearconstrs arityl; let ind_env_params = push_rel_context params ind_env in let mispecvec = List.map2 - (fun ar (name,_,lname_constr) -> + (fun ar (name,_,_,lname_constr) -> let constrnames, bodies = List.split lname_constr in let constrs = List.map @@ -248,23 +257,23 @@ let extract_coe lc = let extract_coe_la_lc = function | [] -> anomaly "Vernacentries: empty list of inductive types" - | (id,la,ar,lc)::rest -> + | (id,ntn,la,ar,lc)::rest -> let rec check = function | [] -> [],[] - | (id,la',ar,lc)::rest -> + | (id,ntn,la',ar,lc)::rest -> if (List.length la = List.length la') && (List.for_all2 eq_la la la') then let mcoes, mspec = check rest in let coes, lc' = extract_coe lc in - (coes::mcoes,(id,ar,lc')::mspec) + (coes::mcoes,(id,ntn,ar,lc')::mspec) else error ("Parameters should be syntactically the same "^ "for each inductive type") in let mcoes, mspec = check rest in let coes, lc' = extract_coe lc in - (coes,la,(id,ar,lc'):: mspec) + (coes,la,(id,ntn,ar,lc'):: mspec) let build_mutual lind finite = let (coes,lparams,lnamearconstructs) = extract_coe_la_lc lind in diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c5a0c7a92..ece8acb2b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -218,11 +218,12 @@ open Symbols type white_status = Juxtapose | Separate of int | NextIsTerminal -let precedence_of_entry_type = function - | ETConstr (n,BorderProd (_,None)) -> n, Prec n - | ETConstr (n,BorderProd (left,Some a)) -> +let precedence_of_entry_type from = function + | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n + | ETConstr (NumLevel n,BorderProd (left,Some a)) -> n, let (lp,rp) = prec_assoc a in if left then lp else rp - | ETConstr (n,InternalProd) -> n, Prec n + | ETConstr (NumLevel n,InternalProd) -> n, Prec n + | ETConstr (NextLevel,_) -> from, L | ETOther ("constr","annot") -> 10, Prec 10 | _ -> 0, E (* ?? *) @@ -270,7 +271,7 @@ let add_break n l = UNP_BRK (n,1) :: l let make_hunks_ast symbols etyps from = let rec make ws = function | NonTerminal m :: prods -> - let _,lp = precedence_of_entry_type (List.assoc m etyps) in + let _,lp = precedence_of_entry_type from (List.assoc m etyps) in let u = PH (meta_pattern (string_of_id m), None, lp) in if prods <> [] && is_non_terminal (List.hd prods) then u :: add_break 1 (make CanBreak prods) @@ -307,12 +308,12 @@ let make_hunks_ast symbols etyps from = let add_break n l = UnpCut (PpBrk(n,0)) :: l -let make_hunks etyps symbols = +let make_hunks etyps symbols from = let vars,typs = List.split etyps in let rec make ws = function | NonTerminal m :: prods -> let i = list_index m vars in - let _,prec = precedence_of_entry_type (List.nth typs (i-1)) in + let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in let u = UnpMetaVar (i ,prec) in if prods <> [] && is_non_terminal (List.hd prods) then u :: add_break 1 (make CanBreak prods) @@ -363,16 +364,18 @@ let string_of_symbol = function | Terminal s -> [s] | Break _ -> [] -let assoc_of_type (_,typ) = level_rule (precedence_of_entry_type typ) +let assoc_of_type n (_,typ) = level_rule (precedence_of_entry_type n typ) let string_of_assoc = function | Some(Gramext.RightA) -> "RIGHTA" | Some(Gramext.LeftA) | None -> "LEFTA" | Some(Gramext.NonA) -> "NONA" +let make_anon_notation symbols = + String.concat " " (List.flatten (List.map string_of_symbol symbols)) + let make_symbolic n symbols etyps = - (n,List.map assoc_of_type etyps), - (String.concat " " (List.flatten (List.map string_of_symbol symbols))) + ((n,List.map (assoc_of_type n) etyps), make_anon_notation symbols) let rec define_keywords = function NonTerm(_,Some(_,(ETConstr _|ETOther("constr","binder_constr")))) as n1 :: @@ -411,7 +414,31 @@ let quote x = else x -let rec find_symbols c_current c_next c_last vars = function +let rec analyse_tokens = function + | [] -> [], [] + | String x :: sl when Lexer.is_normal_token x -> + Lexer.check_ident x; + let id = Names.id_of_string x in + let (vars,l) = analyse_tokens sl in + if List.mem id vars then + error ("Variable "^x^" occurs more than once"); + (id::vars, NonTerminal id :: l) + | String s :: sl -> + Lexer.check_special_token s; + let (vars,l) = analyse_tokens sl in (vars, Terminal (strip s) :: l) + | WhiteSpace n :: sl -> + let (vars,l) = analyse_tokens sl in (vars, Break n :: l) + +let rec find_symbols c_current c_next c_last = function + | [] -> [] + | NonTerminal id :: sl -> + let prec = if sl <> [] then c_current else c_last in + (id, prec) :: (find_symbols c_next c_next c_last sl) + | Terminal s :: sl -> find_symbols c_next c_next c_last sl + | Break n :: sl -> find_symbols c_current c_next c_last sl + +(* +let rec find_symbols c_current c_next c_last = function | [] -> (vars, []) | String x :: sl when Lexer.is_normal_token x -> Lexer.check_ident x; @@ -419,7 +446,7 @@ let rec find_symbols c_current c_next c_last vars = function if List.mem_assoc id vars then error ("Variable "^x^" occurs more than once"); let prec = if sl <> [] then c_current else c_last in - let (vars,l) = find_symbols c_next c_next c_last vars sl in + let (vars,l) = find_symbols c_next c_next c_last sl in ((id,prec)::vars, NonTerminal id :: l) (* | "_"::sl -> @@ -432,11 +459,12 @@ let rec find_symbols c_current c_next c_last vars = function *) | String s :: sl -> Lexer.check_special_token s; - let (vars,l) = find_symbols c_next c_next c_last vars sl in + let (vars,l) = find_symbols c_next c_next c_last sl in (vars, Terminal (strip s) :: l) | WhiteSpace n :: sl -> - let (vars,l) = find_symbols c_current c_next c_last vars sl in + let (vars,l) = find_symbols c_current c_next c_last sl in (vars, Break n :: l) +*) let make_grammar_rule n assoc typs symbols ntn = let prod = make_production typs symbols in @@ -463,8 +491,8 @@ let make_syntax_rule n name symbols typs ast ntn sc = syn_hunks = [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}] -let make_pp_rule symbols typs = - [UnpBox (PpHOVB 0, make_hunks symbols typs)] +let make_pp_rule symbols typs n = + [UnpBox (PpHOVB 0, make_hunks symbols typs n)] (**************************************************************************) @@ -576,17 +604,18 @@ let recompute_assoc typs = let add_syntax_extension local df modifiers = let (assoc,n,etyps,onlyparse) = interp_notation_modifiers modifiers in - let inner = if !Options.v7 then (10,InternalProd) else - (200,InternalProd) in - let (typs,symbs) = + let inner = if !Options.v7 then (NumLevel 10,InternalProd) else + (NumLevel 200,InternalProd) in + let (vars,symbs) = analyse_tokens (split df) in + let typs = find_symbols - (n,BorderProd(true,assoc)) inner (n,BorderProd(false,assoc)) - [] (split df) in + (NumLevel n,BorderProd(true,assoc)) inner + (NumLevel n,BorderProd(false,assoc)) symbs in let typs = List.map (set_entry_type etyps) typs in let assoc = recompute_assoc typs in let (prec,notation) = make_symbolic n symbs typs in let gram_rule = make_grammar_rule n assoc typs symbs notation in - let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in + let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs n) in Lib.add_anonymous_leaf (inSyntaxExtension(local,prec,notation,gram_rule,pp_rule)) @@ -662,12 +691,13 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks = let onlyparse = onlyparse or !Options.v7_only in let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in let inner = - if !Options.v7 then (10,InternalProd) else (200,InternalProd) in - let (typs,symbols) = + if !Options.v7 then (NumLevel 10,InternalProd) + else (NumLevel 200,InternalProd) in + let (vars,symbols) = analyse_tokens toks in + let typs = find_symbols - (n,BorderProd(true,assoc)) inner (n,BorderProd(false,assoc)) - [] toks in - let vars = List.map fst typs in + (NumLevel n,BorderProd(true,assoc)) inner + (NumLevel n,BorderProd(false,assoc)) symbols in (* To globalize... *) let a = interp_aconstr vars c in let typs = List.map (set_entry_type etyps) typs in @@ -677,11 +707,12 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks = let (ppprec,ppn,pptyps,ppsymbols) = match omodv8 with Some(toks8,(a8,n8,typs8,_)) when Options.do_translate() -> - let (typs,symbols) = + let (_,symbols) = analyse_tokens toks8 in + let typs = find_symbols - (n8,BorderProd(true,a8)) (200,InternalProd) - (n8,BorderProd(false,a8)) - [] toks8 in + (NumLevel n8,BorderProd(true,a8)) (NumLevel 200,InternalProd) + (NumLevel n8,BorderProd(false,a8)) + symbols in let typs = List.map (set_entry_type typs8) typs in let (prec,notation) = make_symbolic n8 symbols typs in (prec, n8, typs, symbols) @@ -689,7 +720,7 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks = let gram_rule = make_grammar_rule n assoc typs symbols notation in let pp_rule = if onlyparse then None - else Some (make_pp_rule pptyps ppsymbols) in + else Some (make_pp_rule pptyps ppsymbols n) in Lib.add_anonymous_leaf (inSyntaxExtension(local,ppprec,notation,gram_rule,pp_rule)); let old_pp_rule = @@ -722,6 +753,24 @@ let add_notation local df a modifiers mv8 sc = (toks8,im8)) mv8) sc toks +let check_occur l id = + if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound") + +let add_notation_interpretation df (c,l) sc = + let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in + let (vars,symbs) = analyse_tokens (split df) in + let notation = make_anon_notation symbs in + let old_pp_rule = None in + let prec = Symbols.find_notation_level notation in + List.iter (check_occur l) vars; + let a = AApp (c,List.map (function Name id when List.mem id vars -> AVar id | +_ -> AHole QuestionMark) l) in + let la = List.map (fun id -> id,[]) vars in + let onlyparse = false in + let local = false in + Lib.add_anonymous_leaf + (inNotation(local,old_pp_rule,prec,notation,scope,(la,a),onlyparse,df)) + (* TODO add boxes information in the expression *) let inject_var x = CRef (Ident (dummy_loc, id_of_string x)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 92f79680e..59e786fe3 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -41,8 +41,10 @@ val add_notation : locality_flag -> string -> constr_expr -> syntax_modifier list -> (string * syntax_modifier list) option -> scope_name option -> unit -val add_syntax_extension : locality_flag -> string -> syntax_modifier list - -> unit +val add_notation_interpretation : string -> (aconstr * Names.name list) + -> scope_name option -> unit + +val add_syntax_extension : locality_flag -> string -> syntax_modifier list -> unit val print_grammar : string -> string -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 99ce8b34e..b2f82854c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -122,11 +122,13 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *) type sort_expr = Rawterm.rawsort +type decl_notation = (string * scope_name option) option type simple_binder = identifier * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binder list * constr_expr * constructor_expr list + identifier * decl_notation * simple_binder list * constr_expr + * constructor_expr list type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 1b2428a9d..1480c765c 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -299,7 +299,10 @@ let pr_require_token = function | None -> str "Closed" let pr_syntax_modifier = function - | SetItemLevel (l,n) -> + | SetItemLevel (l,NextLevel) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ str"at next level" + | SetItemLevel (l,NumLevel n) -> prlist_with_sep sep_v2 str l ++ spc() ++ str"at level" ++ spc() ++ int n | SetLevel n -> str"at level" ++ spc() ++ int n @@ -513,7 +516,7 @@ let rec pr_vernac = function | VernacInductive (f,l) -> (* Copie simplifiée de command.ml pour recalculer les implicites *) - let lparams = match l with [] -> assert false | (_,la,_,_)::_ -> la in + let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in let nparams = List.length lparams and sigma = Evd.empty and env0 = Global.env() in @@ -525,7 +528,7 @@ let rec pr_vernac = function (Name id,None,p)::params)) (env0,[]) lparams in let impls = List.map - (fun (recname, _,arityc,_) -> + (fun (recname,_,_,arityc,_) -> let arity = Constrintern.interp_type sigma env_params arityc in let fullarity = Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) @@ -555,9 +558,13 @@ let rec pr_vernac = function | _ -> fnl() ++ str (if List.length l = 1 then " " else " | ") ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind key (id,indpar,s,lc) = - hov 0 (str key ++ spc() ++ pr_id id ++ spc() ++ - pr_sbinders indpar ++ str":" ++ spc() ++ + let pr_oneind key (id,ntn,indpar,s,lc) = + hov 0 ( + str key ++ spc() ++ + pr_opt (fun (ntn,scopt) -> + str ntn ++ pr_opt (fun sc -> str " :" ++ str sc) scopt ++ spc ()) + ntn ++ + pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++ pr_lconstr s ++ str" :=") ++ pr_constructor_list lc in hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) ++ |