let min_precedence = 0
let max_precedence = 100
+let hash_expr e =
+ e
+ |> Hashtbl.hash
+ |> Printf.sprintf "%08x"
+
type ('a,'b,'c,'d,'e) grammars = {
level1_pattern: 'a Grammar.Entry.e;
level2_ast: 'b Grammar.Entry.e;
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;
}
let int_of_string s =
try
- Pervasives.int_of_string s
+ Stdlib.int_of_string s
with Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
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
in
[ Env (List.map Env.opt_declaration p_names),
Gramext.srules
- [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
+ [ [ Gramext.Sopt (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+ hash_expr action,
Gramext.action action ] ]
| Ast.List0 (p, _)
| Ast.List1 (p, _) ->
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,false)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)
+ | 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),
Gramext.srules
- [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
+ [ [ gram_of_list (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+ hash_expr action,
Gramext.action action ] ]
| _ -> assert false
and aux_variable =
| _,[] -> 1
| ((s1::tl1) as x),((s2::tl2) as y) ->
if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
- else Pervasives.compare x y
+ else Stdlib.compare x y
in
aux (x,y)
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 =
in
(* Needed since campl4 on "delete_rule" remove the precedence level if it gets
* empty after the deletion. The lexer never generate the Stoken below. *)
- let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
+ let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], "DUMMY", dummy_action ] in
let mk_level_list first last =
let rec aux acc = function
| i when i < first -> acc
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 ident;
+ 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 ->
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
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"
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
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;
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
[ p_atoms,
+ hash_expr "(make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings)",
(make_action
(fun (env: NotationEnv.t) (loc: Ast.location) ->
(action env loc))
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