let min_precedence = 0
let max_precedence = 100
-type ('a,'b,'c,'d) grammars = {
+type ('a,'b,'c,'d,'e) grammars = {
level1_pattern: 'a Grammar.Entry.e;
level2_ast: 'b Grammar.Entry.e;
level2_ast_grammar : Grammar.g;
term: 'b Grammar.Entry.e;
+ ident: 'e Grammar.Entry.e;
let_defs: 'c Grammar.Entry.e;
+ let_codefs: 'c Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
}
type checked_l1_pattern = CL1P of NotationPt.term * int
+let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term
+ ~refresh_uri_in_reference (CL1P (t,n))
+=
+ CL1P (NotationUtil.refresh_uri_in_term ~refresh_uri_in_term
+ ~refresh_uri_in_reference t, n)
+
+type binding =
+ | NoBinding
+ | Binding of string * Env.value_type
+ | Env of (string * Env.value_type) list
+
type db = {
grammars:
(int -> NotationPt.term,
Ast.term,
(Ast.term Ast.capture_variable list *
Ast.term Ast.capture_variable * Ast.term * int) list,
- Ast.term list * Ast.term option) grammars;
- items: (checked_l1_pattern * int * Gramext.g_assoc * NotationPt.term) list
+ Ast.term list * Ast.term option, Env.ident_or_var) grammars;
+ keywords: string list;
+ items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list
}
let int_of_string s =
string_of_int precedence
let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
-let gram_ident s = Gramext.Stoken ("IDENT", s)
+let gram_ident status =
+ Gramext.Snterm (Grammar.Entry.obj
+ (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
+ (*Gramext.Stoken ("IDENT", s)*)
let gram_number s = Gramext.Stoken ("NUMBER", s)
let gram_keyword s = Gramext.Stoken ("", s)
let gram_term status = function
| Ast.Level precedence ->
Gramext.Snterml
(Grammar.Entry.obj
- (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e),
+ (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
level_of precedence)
;;
| `Keyword s -> gram_keyword s
| `Number s -> gram_number s
-type binding =
- | NoBinding
- | Binding of string * Env.value_type
- | Env of (string * Env.value_type) list
-
let make_action action bindings =
let rec aux (vl : NotationEnv.t) =
function
aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
| Binding (name, Env.StringType) :: tl ->
Gramext.action
- (fun (v:string) ->
+ (fun (v:Env.ident_or_var) ->
aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
| Binding (name, Env.NumType) :: tl ->
Gramext.action
| Ast.Magic m -> aux_magic m
| Ast.Variable v -> aux_variable v
| t ->
- prerr_endline (NotationPp.pp_term t);
+ prerr_endline (NotationPp.pp_term status t);
assert false
and aux_literal =
function
and aux_magic magic =
match magic with
| Ast.Opt p ->
- let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
- let action (env_opt : NotationEnv.t option) (loc : Ast.location) =
+ let _p_bindings, p_atoms, p_names, p_action = inner_pattern p in
+ let action (env_opt : NotationEnv.t option) (_loc : Ast.location) =
match env_opt with
| Some env -> List.map Env.opt_binding_some env
| None -> List.map Env.opt_binding_of_name p_names
match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
| Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) ->
[Binding (s, Env.TermType level), gram_term status lv]
- | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
+ | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident status]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
and inner_pattern p =
CL1P (cp,level)
;;
-let extend status (CL1P (level1_pattern,precedence)) action =
- assert false
-(*
- CicNotationParser.new_parser ();
- let create_cb_old (l1, precedence, associativity, l2) =
- ignore(
- CicNotationParser.extend l1
- (fun env loc ->
- NotationPt.AttributedTerm
- (`Loc loc,TermContentPres.instantiate_level2 env l2)))
- in
- RefCounter.iter create_cb_old !parser_ref_counter;
-*)
-(*
- let p_bindings, p_atoms =
- List.split (extract_term_production status level1_pattern)
- in
- let level = level_of precedence in
- let () =
- Grammar.extend
- [ Grammar.Entry.obj
- (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e),
- Some (Gramext.Level level),
- [ None,
- Some (*Gramext.NonA*) Gramext.NonA,
- [ p_atoms,
- (make_action
- (fun (env: NotationEnv.t) (loc: Ast.location) ->
- (action env loc))
- p_bindings) ]]]
- in
- let keywords = NotationUtil.keywords_of_term level1_pattern in
- let rule_id = p_atoms in
- List.iter CicNotationLexer.add_level2_ast_keyword keywords;
- rule_id
-*)
-
(** {2 Grammar} *)
let fold_cluster binder terms ty body =
try
f ()
with
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc, Parse_error msg))
- | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
let parse_level1_pattern grammars precedence lexbuf =
exc_located_wrapper
(fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
-let parse_term grammars lexbuf =
- exc_located_wrapper
- (fun () -> (Grammar.Entry.parse grammars.term (Obj.magic lexbuf)))
-
(* create empty precedence level for "term" *)
let initialize_grammars grammars =
let dummy_action =
let level2_ast = grammars.level2_ast in
let term = grammars.term in
let let_defs = grammars.let_defs in
+ let let_codefs = grammars.let_codefs in
+ let ident = grammars.ident in
let protected_binder_vars = grammars.protected_binder_vars in
EXTEND
- GLOBAL: level2_ast term let_defs protected_binder_vars;
+ GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
];
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
- SYMBOL ":"; ty = term; RPAREN ->
+ typ = OPT [ SYMBOL ":"; typ = term -> typ] ; RPAREN -> (* FG: now type is optional *)
+ let ty = match typ with Some ty -> ty | None -> Ast.Implicit `JustOne in
List.map (fun n -> Ast.Ident (n, None)) names, Some ty
| name = IDENT -> [Ast.Ident (name, None)], None
| blob = UNPARSED_META ->
| _ -> failwith "Invalid index name."
]
];
+ ident: [
+ [ name = IDENT -> Env.Ident name
+ | blob = UNPARSED_META ->
+ let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
+ match meta with
+ | Ast.Variable (Ast.FreshVar _) ->
+ (* it makes sense: extend Env.ident_or_var *)
+ assert false
+ | Ast.Variable (Ast.IdentVar name) -> Env.Var name
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Env.Var "_"
+ | _ -> failwith ("Invalid index name: " ^ blob)
+ ]
+ ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
args = LIST1 arg;
index_name = OPT [ "on"; id = single_arg -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
let rec position_of name p = function
| [] -> None, p
| n :: _ when n = name -> Some p, p
in
let rec find_arg name n = function
| [] ->
+ (* CSC: new NCicPp.status is the best I can do here
+ without changing the return type *)
Ast.fail loc (sprintf "Argument %s not found"
- (NotationPp.pp_term name))
+ (NotationPp.pp_term (new NCicPp.status) name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
defs
]
];
+ let_codefs: [
+ [ defs = LIST1 [
+ name = single_arg;
+ args = LIST0 arg;
+ ty = OPT [ SYMBOL ":" ; p = term -> p ];
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
+ let args =
+ List.concat
+ (List.map
+ (function (names,ty) -> List.map (function x -> x,ty) names
+ ) args)
+ in
+ args, (name, ty), body, 0
+ ] SEP "and" ->
+ defs
+ ]
+ ];
binder_vars: [
[ vars = [ l =
[ l = LIST1 single_arg SEP SYMBOL "," -> l
SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
- | LETCOREC; defs = let_defs; "in";
- body = term ->
- return_term loc (Ast.LetRec (`CoInductive, defs, body))
- | LETREC; defs = let_defs; "in";
- body = term ->
- return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
term: LEVEL "20"
grammars
;;
-let initial_grammars =
- let lexers = CicNotationLexer.mk_lexers [] in
+let initial_grammars keywords =
+ let lexers = CicNotationLexer.mk_lexers keywords in
let level1_pattern_grammar =
Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in
let level2_ast_grammar =
Grammar.Entry.create level1_pattern_grammar "level1_pattern" in
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 let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+ let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
let protected_binder_vars =
Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
initialize_grammars { level1_pattern=level1_pattern;
level2_ast=level2_ast;
term=term;
+ ident=ident;
let_defs=let_defs;
+ let_codefs=let_codefs;
protected_binder_vars=protected_binder_vars;
level2_meta=level2_meta;
level2_ast_grammar=level2_ast_grammar;
method notation_parser_db: db
end
-class status =
- object(self)
- val db = { grammars = initial_grammars ; items = [] }
+class status0 ~keywords:kwds =
+ object
+ val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
method notation_parser_db = db
method set_notation_parser_db v = {< db = v >}
method set_notation_parser_status
= fun o -> {< db = o#notation_parser_db >}
end
+class virtual status ~keywords:kwds =
+ object
+ inherit NCic.status
+ inherit status0 kwds
+ end
+
+let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
+ (* move inside constructor XXX *)
+ let add1item status (level, level1_pattern, action) =
+ let p_bindings, p_atoms =
+ List.split (extract_term_production status level1_pattern) in
+ Grammar.extend
+ [ Grammar.Entry.obj
+ (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
+ Some (Gramext.Level level),
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ p_atoms,
+ (make_action
+ (fun (env: NotationEnv.t) (loc: Ast.location) ->
+ (action env loc))
+ p_bindings) ]]];
+ status
+ in
+ let current_item =
+ let level = level_of precedence in
+ level, level1_pattern, action in
+ let keywords = NotationUtil.keywords_of_term level1_pattern @
+ status#notation_parser_db.keywords in
+ let items = current_item :: status#notation_parser_db.items in
+ let status = status#set_notation_parser_status (new status0 ~keywords) in
+ let status = status#set_notation_parser_db
+ {status#notation_parser_db with items = items} in
+ List.fold_left add1item status items
+;;
+
+
let parse_level1_pattern status =
parse_level1_pattern status#notation_parser_db.grammars
let parse_level2_ast status =
parse_level2_ast status#notation_parser_db.grammars
let parse_level2_meta status =
parse_level2_meta status#notation_parser_db.grammars
-let parse_term status =
- parse_term status#notation_parser_db.grammars
let level2_ast_grammar status =
status#notation_parser_db.grammars.level2_ast_grammar
let term status = status#notation_parser_db.grammars.term
let let_defs status = status#notation_parser_db.grammars.let_defs
+let let_codefs status = status#notation_parser_db.grammars.let_codefs
let protected_binder_vars status =
status#notation_parser_db.grammars.protected_binder_vars
projects / helm.git / blobdiff