term: 'b Grammar.Entry.e;
ident: 'e Grammar.Entry.e;
let_defs: 'c Grammar.Entry.e;
+ located: Stdpp.location Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
}
raise (Level_not_found precedence);
string_of_int precedence
-let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
+let gram_symbol s =
+ Gramext.srules
+ [ [ Gramext.Stoken ("SYMBOL",s) ], Gramext.action (fun _ loc -> loc) ]
+
let gram_ident status =
Gramext.Snterm (Grammar.Entry.obj
(status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+ | NoBinding :: tl -> Gramext.action
+ (fun (loc: Ast.location) ->
+ aux (("",(Env.NoType,Env.LocValue loc))::vl) tl)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
| Env _ :: tl ->
Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl)
+ | _ (* Binding (_,NoType) *) -> assert false
(* LUCA: DEFCON 3 END *)
in
aux [] (List.rev bindings)
List.fold_right
(fun term body ->
let lambda = Ast.Binder (`Lambda, (term, ty), body) in
- Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+ Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
terms body
let fold_binder binder pt_names body =
| "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
]
];
- explicit_subst: [
- [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *)
- SYMBOL "[";
- substs = LIST1 [
- i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
- ] SEP SYMBOL ";";
- SYMBOL "]" ->
- substs
- ]
- ];
meta_subst: [
[ s = SYMBOL "_" -> None
| p = term -> Some p ]
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
| arg = single_arg -> arg, None
- | id = PIDENT -> Ast.Ident (id, None), None
- | SYMBOL "_" -> Ast.Ident ("_", None), None
+ | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
+ | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
| LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
- Ast.Ident (id, None), Some typ
+ Ast.Ident (id, `Ambiguous), Some typ
| LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
- Ast.Ident ("_", None), Some typ
+ Ast.Ident ("_", `Ambiguous), Some typ
]
];
match_pattern: [
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
];
+ tident: [
+ [ uri = HREF;
+ id = IDENT;
+ HREFEND -> (id, `Uri uri) ]];
+ gident: [
+ [ fullident = tident -> fullident;
+ | id = IDENT -> (id, `Ambiguous) ]];
arg: [
- [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
+ [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
- List.map (fun n -> Ast.Ident (n, None)) names, Some ty
- | name = IDENT -> [Ast.Ident (name, None)], None
+ List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty
+ | (name,uri) = gident -> [Ast.Ident (name,uri)], None
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
+ | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
| _ -> failwith "Invalid bound name."
]
];
single_arg: [
- [ name = IDENT -> Ast.Ident (name, None)
+ [ (name,uri) = gident -> Ast.Ident (name,uri)
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _)
| Ast.Variable (Ast.IdentVar _) -> meta
- | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
| _ -> failwith "Invalid index name."
]
];
| _ -> failwith ("Invalid index name: " ^ blob)
]
];
+ located: [
+ [ s = SYMBOL -> loc ]
+ ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
[ vars = [ l =
[ l = LIST1 single_arg SEP SYMBOL "," -> l
| l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," ->
- List.map (fun x -> Ast.Ident(x,None)) l
+ List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
] -> l ];
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
]
var =
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
- | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
- Ast.Ident(id,None), ty ];
+ | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+ Ast.Ident (id,uri), ty ];
SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
];
term: LEVEL "90"
[
- [ id = IDENT -> return_term loc (Ast.Ident (id, None))
- | id = IDENT; s = explicit_subst ->
- return_term loc (Ast.Ident (id, Some s))
- | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
- | u = URI -> return_term loc (Ast.Uri (u, None))
+ [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri))
+ | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
+ | u = URI -> return_term loc (Ast.Ident
+ (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
| r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
- | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+ | n = NUMBER -> return_term loc (Ast.Num (n, None))
| IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
| SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
let term = Grammar.Entry.create level2_ast_grammar "term" in
let ident = Grammar.Entry.create level2_ast_grammar "ident" in
+ let located = Grammar.Entry.create level2_ast_grammar "located" in
let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
let protected_binder_vars =
Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
term=term;
ident=ident;
let_defs=let_defs;
+ located=located;
protected_binder_vars=protected_binder_vars;
level2_meta=level2_meta;
level2_ast_grammar=level2_ast_grammar;
Some (Gramext.Level level),
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
- [ p_atoms,
+ [ p_atoms, (* concrete l1 syntax *)
(make_action
(fun (env: NotationEnv.t) (loc: Ast.location) ->
(action env loc))