*)
oopen Printf
+oopen CicNotationEnvoopen CicNotationPt
eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
+llet min_precedence = 0llet max_precedence = 100llet default_precedence = 50
llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet l2_pattern = Grammar.Entry.create grammar "l2_pattern"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
-
+llet phrase = Grammar.Entry.create grammar "phrase"
llet return_term loc term = ()
-llet loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) =
- loc_begin, loc_end
llet fail floc msg =
let (x, y) = loc_of_floc floc in
failwith (sprintf "Error at characters %d - %d: %s" x y msg)
try Pervasives.int_of_string s with
Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
-oopen CicNotationPt
-llet boxify =
+(** {2 Grammar extension} *)
+
+llet symbol s = Gramext.Stoken ("SYMBOL", s)llet ident s = Gramext.Stoken ("IDENT", s)llet number s = Gramext.Stoken ("NUMBER", s)llet term = Gramext.Sself
+llet g_symbol_of_literal =
+ function
+ `Symbol s -> symbol s
+ | `Keyword s -> ident s
+ | `Number s -> number s
+ttype binding =
+ NoBinding
+ | Binding of string * value_type
+ | Env of (string * value_type) list
+llet make_action action bindings =
+ let rec aux (vl : env_type) =
+ function
+ [] ->
+ prerr_endline "aux: make_action";
+ Gramext.action (fun (loc : location) -> action vl loc)
+ | NoBinding :: tl ->
+ prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl)
+ | Binding (name, TermType) :: tl ->
+ prerr_endline "aux: term";
+ Gramext.action
+ (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
+ | Binding (name, StringType) :: tl ->
+ prerr_endline "aux: string";
+ Gramext.action
+ (fun (v : string) ->
+ aux ((name, (StringType, StringValue v)) :: vl) tl)
+ | Binding (name, NumType) :: tl ->
+ prerr_endline "aux: num";
+ Gramext.action
+ (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
+ | Binding (name, OptType t) :: tl ->
+ prerr_endline "aux: opt";
+ Gramext.action
+ (fun (v : 'a option) ->
+ aux ((name, (OptType t, OptValue v)) :: vl) tl)
+ | Binding (name, ListType t) :: tl ->
+ prerr_endline "aux: list";
+ Gramext.action
+ (fun (v : 'a list) ->
+ aux ((name, (ListType t, ListValue v)) :: vl) tl)
+ | Env _ :: tl ->
+ prerr_endline "aux: env";
+ Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
+ in
+ aux [] (List.rev bindings)
+llet flatten_opt =
+ let rec aux acc =
+ function
+ [] -> List.rev acc
+ | NoBinding :: tl -> aux acc tl
+ | Env names :: tl -> aux (List.rev names @ acc) tl
+ | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
+ in
+ aux []
+
+ (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
+let extract_term_production pattern =
+ let rec aux =
+ function
+ AttributedTerm (_, t) -> aux t
+ | Literal l -> aux_literal l
+ | Layout l -> aux_layout l
+ | Magic m -> aux_magic m
+ | Variable v -> aux_variable v
+ | t -> prerr_endline (CicNotationPp.pp_term t); assert false
+ and aux_literal =
+ function
+ `Symbol s -> [NoBinding, symbol s]
+ | `Keyword s -> [NoBinding, ident s]
+ | `Number s -> [NoBinding, number s]
+ and aux_layout =
+ function
+ Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
+ | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
+ | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
+ | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
+ | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
+ | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
+ | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
+ | Root (p1, p2) ->
+ [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @
+ aux p1
+ | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
+ | Break -> []
+ | Box (_, pl) -> List.flatten (List.map aux pl)
+ and aux_magic magic =
+ match magic with
+ Opt p ->
+ let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
+ let action (env_opt : env_type option) (loc : location) =
+ match env_opt with
+ Some env -> List.map opt_binding_some env
+ | None -> List.map opt_binding_of_name p_names
+ in
+ [Env (List.map opt_declaration p_names),
+ Gramext.srules
+ [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
+ Gramext.action action]]
+ | List0 (p, _) | List1 (p, _) ->
+ let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
+ let env0 = List.map list_binding_of_name p_names in
+ let grow_env_entry env n v =
+ prerr_endline "grow_env_entry";
+ List.map
+ (function
+ n', (ty, ListValue vl) as entry ->
+ if n' = n then n', (ty, ListValue (v :: vl)) else entry
+ | _ -> assert false)
+ env
+ in
+ let grow_env env_i env =
+ prerr_endline "grow_env";
+ List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env
+ env_i
+ in
+ let action (env_list : env_type list) (loc : location) =
+ prerr_endline "list action"; List.fold_right grow_env env_list env0
+ in
+ let g_symbol s =
+ match magic with
+ List0 (_, None) -> Gramext.Slist0 s
+ | List1 (_, None) -> Gramext.Slist1 s
+ | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l)
+ | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l)
+ | _ -> assert false
+ in
+ [Env (List.map list_declaration p_names),
+ Gramext.srules
+ [[g_symbol (Gramext.srules [p_atoms, p_action])],
+ Gramext.action action]]
+ | _ -> assert false
+ and aux_variable =
+ function
+ NumVar s -> [Binding (s, NumType), number ""]
+ | TermVar s -> [Binding (s, TermType), term]
+ | IdentVar s -> [Binding (s, StringType), ident ""]
+ | Ascription (p, s) -> assert false
+ | FreshVar _ -> assert false
+ and inner_pattern p =
+ let (p_bindings, p_atoms) = List.split (aux p) in
+ let p_names = flatten_opt p_bindings in
+ let _ =
+ prerr_endline
+ ("inner names: " ^ String.concat " " (List.map fst p_names))
+ in
+ let action =
+ make_action
+ (fun (env : env_type) (loc : location) ->
+ prerr_endline "inner action"; env)
+ p_bindings
+ in
+ p_bindings, p_atoms, p_names, action
+ in
+ aux pattern
+
+let level_of_int precedence =
+ if precedence < min_precedence || precedence > max_precedence then
+ raise (Level_not_found precedence);
+ string_of_int precedence
+
+type rule_id = Token.t Gramext.g_symbol list
+
+let extend level1_pattern ?(precedence = default_precedence) =
+ fun ?associativity action ->
+ let (p_bindings, p_atoms) =
+ List.split (extract_term_production level1_pattern)
+ in
+ let level = level_of_int precedence in
+ let p_names = flatten_opt p_bindings in
+ let _ =
+ prerr_endline (string_of_int (List.length p_bindings));
+ Grammar.extend
+ [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e),
+ Some (Gramext.Level level),
+ [None, associativity,
+ [p_atoms,
+ make_action
+ (fun (env : env_type) (loc : location) -> action env loc)
+ p_bindings]]]
+ in
+ p_atoms
+
+let delete atoms = Grammar.delete_rule l2_pattern atoms
+
+(** {2 Grammar} *)
+
+let boxify =
function
[a] -> a
| l -> Layout (Box (H, l))
-llet fold_binder binder pt_names body =
- let fold_cluster binder names ty body =
- List.fold_right
- (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body
+
+let fold_binder binder pt_names body =
+ let fold_cluster binder terms ty body =
+ List.fold_right (fun term body -> Binder (binder, (term, ty), body)) terms
+ body
in
List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
pt_names body
-llet return_term loc term = AttributedTerm (`Loc loc, term)
-Elet _ =
+
+let return_term loc term = AttributedTerm (`Loc loc, term)
+
+let _ =
+ let mk_level_list first last =
+ let rec aux acc =
+ function
+ i when i < first -> acc
+ | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
+ in
+ aux [] last
+ in
+ Grammar.extend
+ [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e), None,
+ mk_level_list min_precedence max_precedence]
+
+let _ =
Grammar.extend
(let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
and _ = (level3_term : 'level3_term Grammar.Entry.e)
and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e)
and _ = (notation : 'notation Grammar.Entry.e)
- and _ = (interpretation : 'interpretation Grammar.Entry.e) in
+ and _ = (interpretation : 'interpretation Grammar.Entry.e)
+ and _ = (phrase : 'phrase Grammar.Entry.e) in
let grammar_entry_create s =
Grammar.Entry.create (Grammar.of_entry level1_pattern) s
in
grammar_entry_create "explicit_subst"
and meta_subst : 'meta_subst Grammar.Entry.e =
grammar_entry_create "meta_subst"
+ and meta_substs : 'meta_substs Grammar.Entry.e =
+ grammar_entry_create "meta_substs"
and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
grammar_entry_create "possibly_typed_name"
and match_pattern : 'match_pattern Grammar.Entry.e =
grammar_entry_create "match_pattern"
and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
+ and bound_name : 'bound_name Grammar.Entry.e =
+ grammar_entry_create "bound_name"
and bound_names : 'bound_names Grammar.Entry.e =
grammar_entry_create "bound_names"
and induction_kind : 'induction_kind Grammar.Entry.e =
None,
[None, None,
[[Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("EOI", "")],
+ (Grammar.Entry.obj
+ (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
Gramext.action
- (fun _ (p : 'l1_pattern)
+ (fun (p : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (boxify p : 'level1_pattern))]];
+ (p : 'level1_pattern))]];
Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
[None, None,
- [[Gramext.Slist0
+ [[Gramext.Slist1
(Gramext.Snterm
(Grammar.Entry.obj
(l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
[Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")],
Gramext.action
(fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
- (TermVar id : 'l1_pattern_variable));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
(TermVar id : 'l1_pattern_variable))]];
Grammar.Entry.obj
(l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
None,
[Some "layout", Some Gramext.LeftA,
- [[Gramext.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", "");
- Gramext.Stoken ("SYMBOL", "]")],
+ [[Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\AS");
+ Gramext.Stoken ("IDENT", "")],
Gramext.action
- (fun _ (id : string) _ (p : 'l1_pattern) _
+ (fun (id : string) _ (p : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc
- (Variable (Ascription (Layout (Box (H, p)), id))) :
+ (return_term loc (Variable (Ascription (p, id))) :
'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "[");
+ [Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
(Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.Stoken ("DELIM", "\\]")],
Gramext.action
(fun _ (p : 'l1_pattern) _
(loc : Lexing.position * Lexing.position) ->
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
(return_term loc (Layout Break) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
+ [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
(Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.Stoken ("DELIM", "\\]")],
Gramext.action
(fun _ (p : 'l1_pattern) _ _
(loc : Lexing.position * Lexing.position) ->
(return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("SYMBOL", "[");
+ [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
(Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.Stoken ("DELIM", "\\]")],
Gramext.action
(fun _ (p : 'l1_pattern) _ _
(loc : Lexing.position * Lexing.position) ->
(return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "\\ROOT");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
+ [Gramext.Stoken ("SYMBOL", "\\ROOT"); Gramext.Sself;
Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
Gramext.action
- (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
+ (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
+ (return_term loc (Layout (Root (arg, index))) :
'l1_simple_pattern));
[Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
Gramext.action
(fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
(loc : Lexing.position * Lexing.position) ->
(return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\ATOP");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ATOP"); Gramext.Sself],
Gramext.action
- (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
+ (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Atop (boxify p1, boxify p2))) :
- 'l1_simple_pattern));
- [Gramext.Stoken ("SYMBOL", "[");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "\\OVER");
- Gramext.Snterm
- (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", "]")],
+ (return_term loc (Layout (Atop (p1, p2))) : 'l1_simple_pattern));
+ [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\OVER"); Gramext.Sself],
Gramext.action
- (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
+ (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Layout (Over (boxify p1, boxify p2))) :
- 'l1_simple_pattern));
+ (return_term loc (Layout (Over (p1, p2))) : 'l1_simple_pattern));
[Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
Gramext.action
(fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
Gramext.action
(fun (m : 'l1_magic_pattern)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (Magic m) : 'l1_simple_pattern))]];
+ (return_term loc (Magic m) : 'l1_simple_pattern));
+ [Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (i : string) (loc : Lexing.position * Lexing.position) ->
+ (return_term loc (Ident (i, None)) : 'l1_simple_pattern))]];
Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
None,
[None, None,
(fun _ (loc : Lexing.position * Lexing.position) ->
(`Prop : 'sort))]];
Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
- None, [None, None, []];
+ None,
+ [None, None,
+ [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
+ Gramext.Slist1sep
+ (Gramext.srules
+ [[Gramext.Stoken ("IDENT", "");
+ Gramext.Stoken ("SYMBOL", "≔");
+ Gramext.Snterm
+ (Grammar.Entry.obj
+ (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+ Gramext.action
+ (fun (t : 'l2_pattern) _ (i : string)
+ (loc : Lexing.position * Lexing.position) ->
+ (i, t : 'e__1))],
+ Gramext.Stoken ("SYMBOL", ";"));
+ Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.action
+ (fun _ (substs : 'e__1 list) _ _
+ (loc : Lexing.position * Lexing.position) ->
+ (substs : 'explicit_subst))]];
Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
- [None, None, []];
+ [None, None,
+ [[Gramext.Snterm
+ (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+ Gramext.action
+ (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
+ (Some p : 'meta_subst));
+ [Gramext.Stoken ("SYMBOL", "_")],
+ Gramext.action
+ (fun (s : string) (loc : Lexing.position * Lexing.position) ->
+ (None : 'meta_subst))]];
+ Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Stoken ("SYMBOL", "[");
+ Gramext.Slist0
+ (Gramext.Snterm
+ (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
+ Gramext.Stoken ("SYMBOL", "]")],
+ Gramext.action
+ (fun _ (substs : 'meta_subst list) _
+ (loc : Lexing.position * Lexing.position) ->
+ (substs : 'meta_substs))]];
Grammar.Entry.obj
(possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
None,
[None, None,
- [[Gramext.Stoken ("IDENT", "")],
+ [[Gramext.Snterm
+ (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e))],
Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (Cic.Name id, None : 'possibly_typed_name));
- [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
+ (fun (id : 'bound_name) (loc : Lexing.position * Lexing.position) ->
+ (id, None : 'possibly_typed_name));
+ [Gramext.Stoken ("SYMBOL", "(");
+ Gramext.Snterm
+ (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e));
Gramext.Stoken ("SYMBOL", ":");
Gramext.Snterm
(Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
Gramext.Stoken ("SYMBOL", ")")],
Gramext.action
- (fun _ (typ : 'l2_pattern) _ (id : string) _
+ (fun _ (typ : 'l2_pattern) _ (id : 'bound_name) _
(loc : Lexing.position * Lexing.position) ->
- (Cic.Name id, Some typ : 'possibly_typed_name))]];
+ (id, Some typ : 'possibly_typed_name))]];
Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
None,
[None, None,
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
(`Pi : 'binder))]];
+ Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (i : string) _ (loc : Lexing.position * Lexing.position) ->
+ (Variable (FreshVar i) : 'bound_name));
+ [Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (i : string) (loc : Lexing.position * Lexing.position) ->
+ (Ident (i, None) : 'bound_name))]];
Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
[None, None,
[[Gramext.Slist1
(Gramext.srules
[[Gramext.Stoken ("SYMBOL", "(");
Gramext.Slist1sep
- (Gramext.Stoken ("IDENT", ""),
+ (Gramext.Snterm
+ (Grammar.Entry.obj
+ (bound_name : 'bound_name Grammar.Entry.e)),
Gramext.Stoken ("SYMBOL", ","));
Gramext.Sopt
(Gramext.srules
Gramext.action
(fun (p : 'l2_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (p : 'e__2))]);
+ (p : 'e__3))]);
Gramext.Stoken ("SYMBOL", ")")],
Gramext.action
- (fun _ (ty : 'e__2 option) (vars : string list) _
+ (fun _ (ty : 'e__3 option) (vars : 'bound_name list) _
(loc : Lexing.position * Lexing.position) ->
- (vars, ty : 'e__3))])],
+ (vars, ty : 'e__4))])],
Gramext.action
- (fun (clusters : 'e__3 list)
+ (fun (clusters : 'e__4 list)
(loc : Lexing.position * Lexing.position) ->
(clusters : 'bound_names));
[Gramext.Slist1sep
- (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
+ (Gramext.Snterm
+ (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)),
+ Gramext.Stoken ("SYMBOL", ","));
Gramext.Sopt
(Gramext.srules
[[Gramext.Stoken ("SYMBOL", ":");
Gramext.action
(fun (p : 'l2_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (p : 'e__1))])],
+ (p : 'e__2))])],
Gramext.action
- (fun (ty : 'e__1 option) (vars : string list)
+ (fun (ty : 'e__2 option) (vars : 'bound_name list)
(loc : Lexing.position * Lexing.position) ->
([vars, ty] : 'bound_names))]];
Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
[None, None,
[[Gramext.Slist1sep
(Gramext.srules
- [[Gramext.Stoken ("IDENT", "");
+ [[Gramext.Snterm
+ (Grammar.Entry.obj
+ (bound_name : 'bound_name Grammar.Entry.e));
Gramext.Snterm
(Grammar.Entry.obj
(bound_names : 'bound_names Grammar.Entry.e));
Gramext.Sopt
(Gramext.srules
[[Gramext.Stoken ("IDENT", "on");
- Gramext.Stoken ("IDENT", "")],
+ Gramext.Snterm
+ (Grammar.Entry.obj
+ (bound_name : 'bound_name Grammar.Entry.e))],
Gramext.action
- (fun (id : string) _
+ (fun (id : 'bound_name) _
(loc : Lexing.position * Lexing.position) ->
- (id : 'e__4))]);
+ (id : 'e__5))]);
Gramext.Sopt
(Gramext.srules
[[Gramext.Stoken ("SYMBOL", ":");
Gramext.action
(fun (p : 'l2_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (p : 'e__5))]);
+ (p : 'e__6))]);
Gramext.Stoken ("SYMBOL", "≝");
Gramext.Snterm
(Grammar.Entry.obj
(l2_pattern : 'l2_pattern Grammar.Entry.e))],
Gramext.action
- (fun (body : 'l2_pattern) _ (ty : 'e__5 option)
- (index_name : 'e__4 option) (args : 'bound_names)
- (name : string)
+ (fun (body : 'l2_pattern) _ (ty : 'e__6 option)
+ (index_name : 'e__5 option) (args : 'bound_names)
+ (name : 'bound_name)
(loc : Lexing.position * Lexing.position) ->
(let body = fold_binder `Lambda args body in
let ty =
in
let rec find_arg name n =
function
- [] -> fail loc (sprintf "Argument %s not found" name)
+ [] ->
+ fail loc
+ (sprintf "Argument %s not found"
+ (CicNotationPp.pp_term name))
| (l, _) :: tl ->
match position_of name 0 l with
None, len -> find_arg name (n + len) tl
None -> 0
| Some name -> find_arg name 0 args
in
- (Cic.Name name, ty), body, index :
- 'e__6))],
+ (name, ty), body, index :
+ 'e__7))],
Gramext.Stoken ("IDENT", "and"))],
Gramext.action
- (fun (defs : 'e__6 list)
+ (fun (defs : 'e__7 list)
(loc : Lexing.position * Lexing.position) ->
(defs : 'let_defs))]];
Grammar.Entry.obj
None,
[None, None,
[[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
+ Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
(Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+ Gramext.Stoken ("DELIM", "\\]"); Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+ (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+ Gramext.Stoken ("DELIM", "\\]")],
Gramext.action
- (fun (none : 'l2_pattern) (some : 'l2_pattern) _
+ (fun _ (none : 'l2_pattern) _ _ (some : 'l2_pattern) _ _
(loc : Lexing.position * Lexing.position) ->
(Default (some, none) : 'l2_magic_pattern));
[Gramext.Stoken ("SYMBOL", "\\FOLD");
[[Gramext.Stoken ("IDENT", "right")],
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
- (`Right : 'e__7));
+ (`Right : 'e__8));
[Gramext.Stoken ("IDENT", "left")],
Gramext.action
(fun _ (loc : Lexing.position * Lexing.position) ->
- (`Left : 'e__7))];
+ (`Left : 'e__8))];
+ Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
(Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+ Gramext.Stoken ("DELIM", "\\]");
Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
+ Gramext.Stoken ("DELIM", "\\[");
Gramext.Snterm
- (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+ (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+ Gramext.Stoken ("DELIM", "\\]")],
Gramext.action
- (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
- (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
+ (fun _ (recursive : 'l2_pattern) _ (id : string) _ _
+ (base : 'l2_pattern) _ (kind : 'e__8) _
+ (loc : Lexing.position * Lexing.position) ->
(Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
- Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
- [Some "0", None, [];
- Some "10", Some Gramext.NonA,
+ Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
+ Some (Gramext.Level "10"),
+ [Some "10", Some Gramext.NonA,
[[Gramext.Stoken ("IDENT", "let");
Gramext.Snterm
(Grammar.Entry.obj
(fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
(var : 'possibly_typed_name) _
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))];
- Some "20", Some Gramext.RightA,
+ (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]];
+ Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
+ Some (Gramext.Level "20"),
+ [Some "20", Some Gramext.RightA,
[[Gramext.Snterm
(Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
Gramext.Snterm
Gramext.action
(fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
(loc : Lexing.position * Lexing.position) ->
- (return_term loc (fold_binder b names body) : 'l2_pattern))];
- Some "30", None, []; Some "40", None, []; Some "50", None, [];
- Some "60", None, [];
- Some "70", Some Gramext.LeftA,
+ (return_term loc (fold_binder b names body) : 'l2_pattern))]];
+ Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
+ Some (Gramext.Level "70"),
+ [Some "70", Some Gramext.LeftA,
[[Gramext.Sself; Gramext.Sself],
Gramext.action
(fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
| term -> [term]
in
return_term loc (Appl (aux p1 @ [p2])) :
- 'l2_pattern))];
- Some "80", None, [];
- Some "90", Some Gramext.NonA,
+ 'l2_pattern))]];
+ Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
+ Some (Gramext.Level "90"),
+ [Some "90", Some Gramext.NonA,
[[Gramext.Snterm
(Grammar.Entry.obj
(l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
Gramext.action
(fun _ (ty : 'l2_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (ty : 'e__8))]);
+ (ty : 'e__9))]);
Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
Gramext.Sopt
(Gramext.srules
Gramext.action
(fun (id : string) _
(loc : Lexing.position * Lexing.position) ->
- (id : 'e__9))]);
+ (id : 'e__10))]);
Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
Gramext.Slist0sep
(Gramext.srules
Gramext.action
(fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
(loc : Lexing.position * Lexing.position) ->
- (lhs, rhs : 'e__10))],
+ (lhs, rhs : 'e__11))],
Gramext.Stoken ("SYMBOL", "|"));
Gramext.Stoken ("SYMBOL", "]")],
Gramext.action
- (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option)
- (t : 'l2_pattern) _ (outtyp : 'e__8 option)
+ (fun _ (patterns : 'e__11 list) _ _ (indty_ident : 'e__10 option)
+ (t : 'l2_pattern) _ (outtyp : 'e__9 option)
(loc : Lexing.position * Lexing.position) ->
(return_term loc (Case (t, indty_ident, outtyp, patterns)) :
'l2_pattern));
- [Gramext.Stoken ("SYMBOL", "")],
- Gramext.action
- (fun (s : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Symbol (s, 0)) : 'l2_pattern));
[Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
Gramext.action
(fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
(return_term loc (Sort s) : 'l2_pattern));
[Gramext.Stoken ("META", "");
Gramext.Snterm
- (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e))],
+ (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
Gramext.action
- (fun (s : 'meta_subst) (m : string)
+ (fun (s : 'meta_substs) (m : string)
(loc : Lexing.position * Lexing.position) ->
(return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
[Gramext.Stoken ("META", "")],
[Gramext.Stoken ("IDENT", "")],
Gramext.action
(fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (return_term loc (Ident (id, None)) : 'l2_pattern))];
- Some "100", None, []];
+ (return_term loc (Ident (id, None)) : 'l2_pattern))]];
Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
[None, None,
[[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
None,
[None, None,
- [[Gramext.Stoken ("IDENT", "right");
+ [[Gramext.Stoken ("IDENT", "non");
+ Gramext.Stoken ("IDENT", "associative")],
+ Gramext.action
+ (fun _ _ (loc : Lexing.position * Lexing.position) ->
+ (Gramext.NonA : 'associativity));
+ [Gramext.Stoken ("IDENT", "right");
Gramext.Stoken ("IDENT", "associative")],
Gramext.action
(fun _ _ (loc : Lexing.position * Lexing.position) ->
- (`Right : 'associativity));
+ (Gramext.RightA : 'associativity));
[Gramext.Stoken ("IDENT", "left");
Gramext.Stoken ("IDENT", "associative")],
Gramext.action
(fun _ _ (loc : Lexing.position * Lexing.position) ->
- (`Left : 'associativity))]];
+ (Gramext.LeftA : 'associativity))]];
Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
[None, None,
- [[Gramext.Stoken ("IDENT", "at");
+ [[Gramext.Stoken ("IDENT", "with");
Gramext.Stoken ("IDENT", "precedence");
Gramext.Stoken ("NUMBER", "")],
Gramext.action
(fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
- (n : 'precedence))]];
+ (int_of_string n : 'precedence))]];
Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
[None, None,
[[Gramext.Stoken ("IDENT", "notation");
Gramext.Snterm
(Grammar.Entry.obj
(level1_pattern : 'level1_pattern Grammar.Entry.e));
- Gramext.Stoken ("IDENT", "for");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level2_pattern : 'level2_pattern Grammar.Entry.e));
Gramext.Sopt
(Gramext.Snterm
(Grammar.Entry.obj
(associativity : 'associativity Grammar.Entry.e)));
Gramext.Sopt
(Gramext.Snterm
- (Grammar.Entry.obj
- (precedence : 'precedence Grammar.Entry.e)))],
+ (Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e)));
+ Gramext.Stoken ("IDENT", "for");
+ Gramext.Snterm
+ (Grammar.Entry.obj
+ (level2_pattern : 'level2_pattern Grammar.Entry.e))],
Gramext.action
- (fun (prec : 'precedence option) (assoc : 'associativity option)
- (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
+ (fun (p2 : 'level2_pattern) _ (prec : 'precedence option)
+ (assoc : 'associativity option) (p1 : 'level1_pattern) _
(loc : Lexing.position * Lexing.position) ->
- (() : 'notation))]];
+ (p1, assoc, prec, p2 : 'notation))]];
Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
None,
[None, None,
Gramext.action
(fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
(loc : Lexing.position * Lexing.position) ->
- (() : 'interpretation))]]])
+ (() : 'interpretation))]];
+ Grammar.Entry.obj (phrase : 'phrase Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Snterm
+ (Grammar.Entry.obj (notation : 'notation Grammar.Entry.e));
+ Gramext.Stoken ("SYMBOL", ".")],
+ Gramext.action
+ (fun _ (l1, assoc, prec, l2 : 'notation)
+ (loc : Lexing.position * Lexing.position) ->
+ (Notation (l1, assoc, prec, l2) : 'phrase));
+ [Gramext.Stoken ("IDENT", "print");
+ Gramext.Snterm
+ (Grammar.Entry.obj
+ (level2_pattern : 'level2_pattern Grammar.Entry.e));
+ Gramext.Stoken ("SYMBOL", ".")],
+ Gramext.action
+ (fun _ (p2 : 'level2_pattern) _
+ (loc : Lexing.position * Lexing.position) ->
+ (Print p2 : 'phrase))]]])
+
+(** {2 API implementation} *)
let exc_located_wrapper f =
try f () with
let parse_syntax_pattern stream =
exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
-
let parse_ast_pattern stream =
exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
-
let parse_interpretation stream =
exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
+let parse_phrase stream =
+ exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream)
-(** {2 Grammar extension} *)
-
-type associativity_kind = [ `Left | `Right | `None ]
-
-let symbol s = Gramext.Stoken ("SYMBOL", s)
-let ident s = Gramext.Stoken ("IDENT", s)
-let number s = Gramext.Stoken ("NUMBER", s)
-let term = Gramext.Sself
-
-type env_type = (string * (value_type * value)) list
-
-let make_action action =
- let rec aux (vl : env_type) =
- prerr_endline "aux";
- function
- [] ->
- prerr_endline "make_action";
- Gramext.action (fun (loc : location) -> action vl loc)
- | None :: tl -> Gramext.action (fun _ -> aux vl tl)
- | Some (name, TermType) :: tl ->
- Gramext.action
- (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
- | Some (name, StringType) :: tl ->
- Gramext.action
- (fun (v : string) ->
- aux ((name, (StringType, StringValue v)) :: vl) tl)
- | Some (name, NumType) :: tl ->
- Gramext.action
- (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
- | Some (name, OptType t) :: tl ->
- Gramext.action
- (fun (v : 'a option) ->
- aux ((name, (OptType t, OptValue v)) :: vl) tl)
- | Some (name, ListType t) :: tl ->
- Gramext.action
- (fun (v : 'a list) ->
- aux ((name, (ListType t, ListValue v)) :: vl) tl)
- in
- aux []
-
-let flatten_opt =
- let rec aux acc =
- function
- [] -> List.rev acc
- | None :: tl -> aux acc tl
- | Some hd :: tl -> aux (hd :: acc) tl
- in
- aux []
-
- (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
-let extract_term_production pattern =
- let rec aux =
- function
- Literal l -> aux_literal l
- | Layout l -> aux_layout l
- | Magic m -> aux_magic m
- | Variable v -> aux_variable v
- | _ -> assert false
- and aux_literal =
- function
- `Symbol s -> [None, symbol s]
- | `Keyword s -> [None, ident s]
- | `Number s -> [None, number s]
- and aux_layout =
- function
- Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
- | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
- | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
- | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
- | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
- | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
- | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
- | Root (p1, p2) ->
- [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
- | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
- | Break -> []
- | Box (_, pl) -> List.flatten (List.map aux pl)
- and aux_magic =
- function
- Opt p ->
- let (p_bindings, p_atoms) = List.split (aux p) in
- let p_names = flatten_opt p_bindings in
- [None,
- Gramext.srules
- [[Gramext.Sopt
- (Gramext.srules
- [p_atoms,
- make_action (fun (env : env_type) (loc : location) -> env)
- p_bindings])],
- Gramext.action
- (fun (env_opt : env_type option) (loc : location) ->
- match env_opt with
- Some env ->
- List.map
- (fun (name, (typ, v)) ->
- name, (OptType typ, OptValue (Some v)))
- env
- | None ->
- List.map
- (fun (name, typ) -> name, (OptType typ, OptValue None))
- p_names)]]
- | _ -> assert false
- and aux_variable =
- function
- NumVar s -> [Some (s, NumType), number ""]
- | TermVar s -> [Some (s, TermType), term]
- | IdentVar s -> [Some (s, StringType), ident ""]
- | Ascription (p, s) -> assert false
- | FreshVar _ -> assert false
- in
- aux pattern
-
-let level_of_int precedence =
- if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
- raise (Level_not_found precedence);
- string_of_int precedence
-
-type rule_id = Token.t Gramext.g_symbol list
-
-let extend level1_pattern ?(precedence = 0) =
- fun ?associativity action ->
- let (p_bindings, p_atoms) =
- List.split (extract_term_production level1_pattern)
- in
- let level = level_of_int precedence in
- let p_names = flatten_opt p_bindings in
- let entry = Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e) in
- let _ =
- prerr_endline (string_of_int (List.length p_bindings));
- Grammar.extend
- [entry, Some (Gramext.Level level),
- [Some level, associativity,
- [p_atoms,
- make_action
- (fun (env : env_type) (loc : location) -> action env loc)
- p_bindings]]]
- in
- p_atoms
-
-let delete atoms = Grammar.delete_rule l2_pattern atoms
+(** {2 Debugging} *)
let print_l2_pattern () =
Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
projects / helm.git / blobdiff