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 =
[ 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: [
arg: [
[ LPAREN; names = LIST1 IDENT 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 -> Ast.Ident (n, `Ambiguous)) names, Some ty
+ | name = IDENT -> [Ast.Ident (name, `Ambiguous)], 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 = IDENT -> Ast.Ident (name, `Ambiguous)
| 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."
]
];
[ 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)
]
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
| id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
- Ast.Ident(id,None), ty ];
+ Ast.Ident(id,`Ambiguous), 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 = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
+ | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
+ assert false
+ (* return_term loc (Ast.Ident (id, Some s))*)
+ | 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