-cicNotationParser.cmi: cicNotationPt.cmo
+cicNotationEnv.cmi: cicNotationPt.cmo
+cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
+cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationLexer.cmx: cicNotationLexer.cmi
-cicNotationParser.cmo: cicNotationPt.cmo cicNotationLexer.cmi \
- cicNotationParser.cmi
-cicNotationParser.cmx: cicNotationPt.cmx cicNotationLexer.cmx \
- cicNotationParser.cmi
+cicNotationEnv.cmo: cicNotationPt.cmo cicNotationEnv.cmi
+cicNotationEnv.cmx: cicNotationPt.cmx cicNotationEnv.cmi
+cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi
+cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi
+cicNotationParser.cmo: cicNotationPt.cmo cicNotationPp.cmi \
+ cicNotationLexer.cmi cicNotationEnv.cmi cicNotationParser.cmi
+cicNotationParser.cmx: cicNotationPt.cmx cicNotationPp.cmx \
+ cicNotationLexer.cmx cicNotationEnv.cmx cicNotationParser.cmi
$(NULL)
INTERFACE_FILES = \
cicNotationLexer.mli \
+ cicNotationEnv.mli \
+ cicNotationPp.mli \
cicNotationParser.mli \
$(NULL)
IMPLEMENTATION_FILES = \
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open CicNotationPt
+
+exception Value_not_found of string
+
+type value =
+ | TermValue of term
+ | StringValue of string
+ | NumValue of string
+ | OptValue of value option
+ | ListValue of value list
+
+type value_type =
+ | TermType
+ | StringType
+ | NumType
+ | OptType of value_type
+ | ListType of value_type
+
+type declaration = string * value_type
+type binding = string * (value_type * value)
+type env_type = (string * (value_type * value)) list
+
+let lookup_value ~env name =
+ try
+ snd (List.assoc name env)
+ with Not_found -> raise (Value_not_found name)
+
+let lookup_term ~env name =
+ match lookup_value ~env name with
+ | TermValue x -> x
+ | _ -> raise (Value_not_found name)
+
+let lookup_num ~env name =
+ match lookup_value ~env name with
+ | NumValue x -> x
+ | _ -> raise (Value_not_found name)
+
+let lookup_string ~env name =
+ match lookup_value ~env name with
+ | StringValue x -> x
+ | _ -> raise (Value_not_found name)
+
+let unopt_names names env =
+ let rec aux acc = function
+ | (name, (ty, v)) :: tl when List.mem name names ->
+ (match ty, v with
+ | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl
+ | _ -> assert false)
+ | _ :: tl -> aux acc tl
+ | [] -> acc
+ in
+ aux [] env
+
+let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
+let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
+let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
+let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
+let opt_declaration (n, ty) = (n, OptType ty)
+let list_declaration (n, ty) = (n, ListType ty)
+
+ (* TODO ensure that names generated by fresh_var do not clash with user's *)
+let fresh_var =
+ let index = ref ~-1 in
+ fun () ->
+ incr index;
+ "fresh" ^ string_of_int !index
+
+let meta_names_of term =
+ let rec names = ref [] in
+ let add_name n =
+ if List.mem n !names then ()
+ else names := n :: !names
+ in
+ let rec aux = function
+ | AttributedTerm (_, term) -> aux term
+ | Appl terms -> List.iter aux terms
+ | Binder (_, _, body) -> aux body
+ | Case (term, indty, outty_opt, patterns) ->
+ aux term ;
+ aux_opt outty_opt ;
+ List.iter aux_branch patterns
+ | LetIn (_, t1, t2) ->
+ aux t1 ;
+ aux t2
+ | LetRec (_, definitions, body) ->
+ List.iter aux_definition definitions ;
+ aux body
+ | Uri (_, Some substs) -> aux_substs substs
+ | Ident (_, Some substs) -> aux_substs substs
+ | Meta (_, substs) -> aux_meta_substs substs
+
+ | Implicit
+ | Ident _
+ | Num _
+ | Sort _
+ | Symbol _
+ | Uri _
+ | UserInput -> ()
+
+ | Magic magic -> aux_magic magic
+ | Variable var -> aux_variable var
+
+ | _ -> assert false
+ and aux_opt = function
+ | Some term -> aux term
+ | None -> ()
+ and aux_capture_var (_, ty_opt) = aux_opt ty_opt
+ and aux_branch (pattern, term) =
+ aux_pattern pattern ;
+ aux term
+ and aux_pattern (head, vars) =
+ List.iter aux_capture_var vars
+ and aux_definition (var, term, i) =
+ aux_capture_var var ;
+ aux term
+ and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
+ and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
+ and aux_variable = function
+ | NumVar name -> add_name name
+ | IdentVar name -> add_name name
+ | TermVar name -> add_name name
+ | FreshVar _ -> ()
+ | Ascription _ -> assert false
+ and aux_magic = function
+ | Fold (_, t1, _, t2) ->
+ aux t1 ;
+ aux t2
+ | Default (t1, t2) ->
+ aux t1 ;
+ aux t2
+ | _ -> assert false
+ in
+ aux term ;
+ !names
+
+let instantiate ~env term =
+ let fresh_env = ref [] in
+ let lookup_fresh_name n =
+ try
+ List.assoc n !fresh_env
+ with Not_found ->
+ let new_name = fresh_var () in
+ fresh_env := (n, new_name) :: !fresh_env;
+ new_name
+ in
+ let rec aux env term =
+ match term with
+ | AttributedTerm (_, term) -> aux env term
+ | Appl terms -> Appl (List.map (aux env) terms)
+ | Binder (binder, var, body) ->
+ Binder (binder, aux_capture_var env var, aux env body)
+ | Case (term, indty, outty_opt, patterns) ->
+ Case (aux env term, indty, aux_opt env outty_opt,
+ List.map (aux_branch env) patterns)
+ | LetIn (var, t1, t2) ->
+ LetIn (aux_capture_var env var, aux env t1, aux env t2)
+ | LetRec (kind, definitions, body) ->
+ LetRec (kind, List.map (aux_definition env) definitions, aux env body)
+ | Uri (name, None) -> Uri (name, None)
+ | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs))
+ | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs))
+ | Meta (index, substs) -> Meta (index, aux_meta_substs env substs)
+
+ | Implicit
+ | Ident _
+ | Num _
+ | Sort _
+ | Symbol _
+ | UserInput -> term
+
+ | Magic magic -> aux_magic env magic
+ | Variable var -> aux_variable env var
+
+ | _ -> assert false
+ and aux_opt env = function
+ | Some term -> Some (aux env term)
+ | None -> None
+ and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
+ and aux_branch env (pattern, term) =
+ (aux_pattern env pattern, aux env term)
+ and aux_pattern env (head, vars) =
+ (head, List.map (aux_capture_var env) vars)
+ and aux_definition env (var, term, i) =
+ (aux_capture_var env var, aux env term, i)
+ and aux_substs env substs =
+ List.map (fun (name, term) -> (name, aux env term)) substs
+ and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
+ and aux_variable env = function
+ | NumVar name -> Num (lookup_num ~env name, 0)
+ | IdentVar name -> Ident (lookup_string ~env name, None)
+ | TermVar name -> lookup_term ~env name
+ | FreshVar name -> Ident (lookup_fresh_name name, None)
+ | Ascription (term, name) -> assert false
+ and aux_magic env = function
+ | Default (some_pattern, none_pattern) ->
+ (match meta_names_of some_pattern with
+ | [] -> assert false (* some pattern must contain at least 1 name *)
+ | (name :: _) as names ->
+ (match lookup_value ~env name with
+ | OptValue (Some _) ->
+ (* assumption: if "name" above is bound to Some _, then all
+ * names returned by "meta_names_of" are bound to Some _ as well
+ *)
+ aux (unopt_names names env) some_pattern
+ | OptValue None -> aux env none_pattern
+ | _ -> assert false))
+ | Fold _ -> failwith "not yet implemented" (* TODO Fold *)
+ | _ -> assert false
+ in
+ aux env term
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception Value_not_found of string
+
+type value =
+ | TermValue of CicNotationPt.term
+ | StringValue of string
+ | NumValue of string
+ | OptValue of value option
+ | ListValue of value list
+
+type value_type =
+ | TermType
+ | StringType
+ | NumType
+ | OptType of value_type
+ | ListType of value_type
+
+type declaration = string * value_type
+type binding = string * (value_type * value)
+type env_type = binding list
+
+ (** fills a term pattern instantiating variable magics *)
+val instantiate: env:env_type -> CicNotationPt.term -> CicNotationPt.term
+
+(** {2 Bindings mangling} *)
+
+val opt_binding_some: binding -> binding (* v -> Some v *)
+val opt_binding_none: binding -> binding (* v -> None *)
+
+val opt_binding_of_name: declaration -> binding (* None binding *)
+val list_binding_of_name: declaration -> binding (* [] binding *)
+
+val opt_declaration: declaration -> declaration (* t -> OptType t *)
+val list_declaration: declaration -> declaration (* t -> ListType t *)
+
let regexp tex_token = '\\' ident
+let regexp delim_begin = "\\["
+let regexp delim_end = "\\]"
+
let regexp keyword = '"' ident '"'
let regexp implicit = '?'
| ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| keyword -> return lexbuf (keyword lexbuf)
+ | delim_begin -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
+ | delim_end -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| eof -> return lexbuf ("EOI", "")
*)
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);
open Printf
+open CicNotationEnv
+open CicNotationPt
+
exception Parse_error of Token.flocation * string
exception Level_not_found of int
let grammar = Grammar.gcreate CicNotationLexer.notation_lexer
+let min_precedence = 0
+let max_precedence = 100
+let default_precedence = 50
+
let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
let level3_term = Grammar.Entry.create grammar "level3_term"
let notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *)
let interpretation =
Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *)
+let phrase = Grammar.Entry.create grammar "phrase"
let return_term loc term = ()
-let loc_of_floc = function
- | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
- (loc_begin, loc_end)
-
let fail floc msg =
let (x, y) = loc_of_floc floc in
failwith (sprintf "Error at characters %d - %d: %s" x y msg)
with Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
-open CicNotationPt
+(** {2 Grammar extension} *)
+
+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
+
+let g_symbol_of_literal =
+ function
+ | `Symbol s -> symbol s
+ | `Keyword s -> ident s
+ | `Number s -> number s
+
+type binding =
+ | NoBinding
+ | Binding of string * value_type
+ | Env of (string * value_type) list
+
+let 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)
+ (* LUCA: DEFCON 2 BEGIN *)
+ | 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)
+ (* LUCA: DEFCON 2 END *)
+ in
+ aux [] (List.rev bindings)
+
+let 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 (* TODO *)
+ | 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)
+ ?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))
let fold_binder binder pt_names body =
- let fold_cluster binder names ty body =
+ let fold_cluster binder terms ty body =
List.fold_right
- (fun name body -> Binder (binder, (Cic.Name name, ty), body))
- names body
+ (fun term body -> Binder (binder, (term, ty), body))
+ terms body (* terms are names: either Ident or FreshVar *)
in
List.fold_right
(fun (names, ty) body -> fold_cluster binder names ty body)
let return_term loc term = AttributedTerm (`Loc loc, term)
+let _ = (* create empty precedence level for "l2_pattern" *)
+ 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 ]
+
EXTEND
GLOBAL: level1_pattern level2_pattern level3_term
l2_pattern
- notation interpretation;
+ notation interpretation
+ phrase;
(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
- level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ];
- l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
+ level1_pattern: [ [ p = l1_simple_pattern -> p ] ];
+ l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
literal: [
[ s = SYMBOL -> `Symbol s
| k = KEYWORD -> `Keyword k
]
];
l1_pattern_variable: [
- [ id = IDENT -> TermVar id
- | SYMBOL "\\TERM"; id = IDENT -> TermVar id
+ [ SYMBOL "\\TERM"; id = IDENT -> TermVar id
| SYMBOL "\\NUM"; id = IDENT -> NumVar id
| SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
]
return_term loc (Layout (Below (p1, p2)))
| p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF ->
return_term loc (Layout (Above (p1, p2)))
- | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
- SYMBOL "]" ->
- return_term loc (Layout (Over (boxify p1, boxify p2)))
- | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
- SYMBOL "]" ->
- return_term loc (Layout (Atop (boxify p1, boxify p2)))
+ | p1 = SELF; SYMBOL "\\OVER"; p2 = SELF ->
+ return_term loc (Layout (Over (p1, p2)))
+ | p1 = SELF; SYMBOL "\\ATOP"; p2 = SELF ->
+ return_term loc (Layout (Atop (p1, p2)))
(* | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
return_term loc (Array (p, csep, rsep)) *)
| SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF ->
return_term loc (Layout (Frac (p1, p2)))
| SYMBOL "\\SQRT"; p = SELF -> return_term loc (Layout (Sqrt p))
- | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
- return_term loc (Layout (Root (arg, Layout (Box (H, index)))))
- | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
+ | SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
+ return_term loc (Layout (Root (arg, index)));
+ | SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
return_term loc (Layout (Box (H, p)))
- | SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
+ | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
return_term loc (Layout (Box (V, p)))
| SYMBOL "\\BREAK" -> return_term loc (Layout Break)
- | SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
+ | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
return_term loc (boxify p)
- | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
- return_term loc (Variable (Ascription (Layout (Box (H, p)), id)))
+ | p = SELF; SYMBOL "\\AS"; id = IDENT ->
+ return_term loc (Variable (Ascription (p, id)))
]
| "simple" NONA
- [ m = l1_magic_pattern -> return_term loc (Magic m)
+ [ i = IDENT -> return_term loc (Ident (i, None))
+ | m = l1_magic_pattern -> return_term loc (Magic m)
| v = l1_pattern_variable -> return_term loc (Variable v)
| l = literal -> return_term loc (Literal l)
]
];
(* }}} *)
(* {{{ Grammar for ast patterns, notation level 2 *)
- level2_pattern: [ [ p = l2_pattern; EOI -> p ] ];
+ level2_pattern: [ [ p = l2_pattern -> p ] ];
sort: [
[ SYMBOL "\\PROP" -> `Prop
| SYMBOL "\\SET" -> `Set
]
];
explicit_subst: [
- [ (* TODO explicit substitution *)
+ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
+ SYMBOL "[";
+ substs = LIST1 [
+ i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = l2_pattern -> (i, t)
+ ] SEP SYMBOL ";";
+ SYMBOL "]" ->
+ substs
]
];
meta_subst: [
- [ (* TODO meta substitution *)
- ]
+ [ s = SYMBOL "_" -> None
+ | p = l2_pattern -> Some p ]
+ ];
+ meta_substs: [
+ [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ]
];
possibly_typed_name: [
- [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
- Cic.Name id, Some typ
- | id = IDENT -> Cic.Name id, None
+ [ SYMBOL "("; id = bound_name; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
+ id, Some typ
+ | id = bound_name -> id, None
]
];
match_pattern: [
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
];
+ bound_name: [
+ [ i = IDENT -> Ident (i, None)
+ | SYMBOL "\\FRESH"; i = IDENT -> Variable (FreshVar i)
+ ]
+ ];
bound_names: [
- [ vars = LIST1 IDENT SEP SYMBOL ",";
+ [ vars = LIST1 bound_name SEP SYMBOL ",";
ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
[ vars, ty ]
| clusters = LIST1 [
SYMBOL "(";
- vars = LIST1 IDENT SEP SYMBOL ",";
+ vars = LIST1 bound_name SEP SYMBOL ",";
ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
SYMBOL ")" ->
vars, ty
];
let_defs: [
[ defs = LIST1 [
- name = IDENT; args = bound_names;
- index_name = OPT [ IDENT "on"; id = IDENT -> id ];
+ name = bound_name; args = bound_names;
+ index_name = OPT [ IDENT "on"; id = bound_name -> id ];
ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
let body = fold_binder `Lambda args body in
| _ :: tl -> position_of name (p + 1) tl
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
+ (name, ty), body, index
] SEP IDENT "and" ->
defs
]
];
l2_pattern_variable: [
- [ SYMBOL "\\NUM"; id = IDENT -> NumVar id
+ [ SYMBOL "\\TERM"; id = IDENT -> TermVar id
+ | SYMBOL "\\NUM"; id = IDENT -> NumVar id
| SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
| SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
]
l2_magic_pattern: [
[ SYMBOL "\\FOLD";
kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
- base = l2_pattern;
- SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern ->
+ DELIM "\\["; base = l2_pattern; DELIM "\\]";
+ SYMBOL "\\LAMBDA"; id = IDENT;
+ DELIM "\\["; recursive = l2_pattern; DELIM "\\]" ->
Fold (kind, base, [id], recursive)
- | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern ->
+ | SYMBOL "\\DEFAULT";
+ DELIM "\\["; some = l2_pattern; DELIM "\\]";
+ DELIM "\\["; none = l2_pattern; DELIM "\\]" ->
Default (some, none)
]
];
- l2_pattern:
- [ "0" [ ]
- | "10" NONA (* let in *)
+ l2_pattern: LEVEL "10" (* let in *)
+ [ "10" NONA
[ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = l2_pattern; "in"; p2 = l2_pattern ->
return_term loc (LetIn (var, p1, p2))
body = l2_pattern ->
return_term loc (LetRec (k, defs, body))
]
- | "20" RIGHTA (* binder *)
+ ];
+ l2_pattern: LEVEL "20" (* binder *)
+ [ "20" RIGHTA
[ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
return_term loc (fold_binder b names body)
]
- | "30" [ ]
- | "40" [ ]
- | "50" [ ]
- | "60" [ ]
- | "70" LEFTA (* apply *)
+ ];
+ l2_pattern: LEVEL "70" (* apply *)
+ [ "70" LEFTA
[ p1 = l2_pattern; p2 = l2_pattern ->
let rec aux = function
| Appl (hd :: tl)
in
return_term loc (Appl (aux p1 @ [p2]))
]
- | "80" [ ]
- | "90" NONA (* simple *)
+ ];
+ l2_pattern: LEVEL "90" (* simple *)
+ [ "90" NONA
[ id = IDENT -> return_term loc (Ident (id, None))
| id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
| u = URI -> return_term loc (Uri (u, None))
| n = NUMBER -> prerr_endline "number"; return_term loc (Num (n, 0))
| IMPLICIT -> return_term loc (Implicit)
| m = META -> return_term loc (Meta (int_of_string m, []))
- | m = META; s = meta_subst -> return_term loc (Meta (int_of_string m, s))
+ | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
| s = sort -> return_term loc (Sort s)
| outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
IDENT "match"; t = l2_pattern;
| v = l2_pattern_variable -> return_term loc (Variable v)
| m = l2_magic_pattern -> return_term loc (Magic m)
]
- | "100" [ ]
];
(* }}} *)
(* {{{ Grammar for interpretation, notation level 3 *)
(* }}} *)
(* {{{ Notation glues *)
associativity: [
- [ IDENT "left"; IDENT "associative" -> `Left
- | IDENT "right"; IDENT "associative" -> `Right
+ [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
+ | IDENT "right"; IDENT "associative" -> Gramext.RightA
+ | IDENT "non"; IDENT "associative" -> Gramext.NonA
]
];
- precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ];
+ precedence: [
+ [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+ ];
notation: [
- [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern;
- assoc = OPT associativity; prec = OPT precedence ->
- ()
+ [ IDENT "notation";
+ p1 = level1_pattern;
+ assoc = OPT associativity; prec = OPT precedence;
+ IDENT "for"; p2 = level2_pattern ->
+ (p1, assoc, prec, p2)
]
];
interpretation: [
]
];
(* }}} *)
+(* {{{ Top-level phrases *)
+ phrase: [
+ [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2
+ | (l1, assoc, prec, l2) = notation; SYMBOL "." ->
+ Notation (l1, assoc, prec, l2)
+ ]
+ ];
+(* }}} *)
END
+(** {2 API implementation} *)
+
let exc_located_wrapper f =
try
f ()
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
-
-let g_symbol_of_literal =
- function
- | `Symbol s -> symbol s
- | `Keyword s -> ident s
- | `Number s -> number s
-
-type env_type = (string * (value_type * value)) list
-
-type binding =
- | NoBinding
- | Binding of string * value_type
- | Env of (string * value_type) list
-
-let rec pp_value =
- function
-(* | TermValue (CicNotationPt.AttributedTerm (_, CicNotationPt.Num (s, _)))
- | TermValue (CicNotationPt.Num (s, _)) ->
- sprintf "@TERM[%s]@" s *)
- | TermValue _ -> "@TERM@"
- | StringValue s -> sprintf "\"%s\"" s
- | NumValue n -> n
- | OptValue (Some v) -> "Some " ^ pp_value v
- | OptValue None -> "None"
- | ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
-
-let rec pp_value_type =
- function
- | TermType -> "Term"
- | StringType -> "String"
- | NumType -> "Number"
- | OptType t -> "Maybe " ^ pp_value_type t
- | ListType l -> "List " ^ pp_value_type l
-
-let pp_env env =
- String.concat "; "
- (List.map
- (fun (name, (ty, value)) ->
- sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
- env)
-
-let 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)
- (* LUCA: DEFCON 2 BEGIN *)
- | 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)
- (* LUCA: DEFCON 2 END *)
- in
- aux [] (List.rev bindings)
-
-let 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 []
-
-let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
-let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
-
-let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
-let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
-
-let opt_name (n, ty) = (n, OptType ty)
-let list_name (n, ty) = (n, ListType ty)
-
- (* 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 -> [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_name 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_name 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 (* TODO *)
- | 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 =
- (* TODO "mod" test to be removed as soon as we add all 100 levels *)
- 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) ?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, (* TODO should we put None here? *)
- 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);
(** interpretation: notation level 3 *)
val parse_interpretation: char Stream.t -> CicNotationPt.cic_appl_pattern
-(** {2 Grammar extension} *)
+ (** top level phrases *)
+val parse_phrase: char Stream.t -> CicNotationPt.phrase
-type env_type = (string * (CicNotationPt.value_type * CicNotationPt.value)) list
+(** {2 Grammar extension} *)
type rule_id
CicNotationPt.term ->
?precedence:int ->
?associativity:Gramext.g_assoc ->
- (env_type -> CicNotationPt.location -> CicNotationPt.term) ->
+ (CicNotationEnv.env_type -> CicNotationPt.location -> CicNotationPt.term) ->
rule_id
val delete: rule_id -> unit
(** {2 Debugging} *)
-val pp_env: env_type -> string
-val pp_value: CicNotationPt.value -> string
-val pp_value_type: CicNotationPt.value_type -> string
-
(** print "level2_pattern" entry on stdout, flushing afterwards *)
val print_l2_pattern: unit -> unit
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open CicNotationEnv
+open CicNotationPt
+
+let pp_binder = function
+ | `Lambda -> "lambda"
+ | `Pi -> "Pi"
+ | `Exists -> "exists"
+ | `Forall -> "forall"
+
+let pp_literal l =
+ sprintf "literal(%s)"
+ (match l with
+ | `Symbol s
+ | `Keyword s
+ | `Number s -> s)
+
+let rec pp_term = function
+ | AttributedTerm (_, term) -> pp_term term
+
+ | Appl terms ->
+ sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+ | Binder (`Forall, (Ident ("_", None), typ), body)
+ | Binder (`Pi, (Ident ("_", None), typ), body) ->
+ sprintf "(%s \\to %s)"
+ (match typ with None -> "?" | Some typ -> pp_term typ)
+ (pp_term body)
+ | Binder (kind, var, body) ->
+ sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
+ (pp_term body)
+ | Case (term, indtype, typ, patterns) ->
+ sprintf "%smatch %s with %s"
+ (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
+ (pp_term term) (pp_patterns patterns)
+ | LetIn (var, t1, t2) ->
+ sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
+ (pp_term t2)
+ | LetRec (kind, definitions, term) ->
+ sprintf "let %s %s in %s"
+ (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (String.concat " and "
+ (List.map
+ (fun (var, body, _) ->
+ sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
+ definitions))
+ (pp_term term)
+ | Ident (name, Some []) | Ident (name, None)
+ | Uri (name, Some []) | Uri (name, None) ->
+ name
+ | Ident (name, Some substs)
+ | Uri (name, Some substs) ->
+ sprintf "%s \\subst [%s]" name (pp_substs substs)
+ | Implicit -> "?"
+ | Meta (index, substs) ->
+ sprintf "%d[%s]" index
+ (String.concat "; "
+ (List.map (function None -> "_" | Some term -> pp_term term) substs))
+ | Num (num, _) -> num
+ | Sort `Set -> "Set"
+ | Sort `Prop -> "Prop"
+ | Sort `Type -> "Type"
+ | Sort `CProp -> "CProp"
+ | Symbol (name, _) -> name
+
+ | UserInput -> ""
+
+ | Literal l -> pp_literal l
+ | Layout l -> pp_layout l
+ | Magic m -> pp_magic m
+ | Variable v -> pp_variable v
+
+and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
+and pp_substs substs = String.concat "; " (List.map pp_subst substs)
+
+and pp_pattern ((head, vars), term) =
+ sprintf "%s \\Rightarrow %s"
+ (match vars with
+ | [] -> head
+ | _ ->
+ sprintf "(%s %s)" head
+ (String.concat " " (List.map pp_capture_variable vars)))
+ (pp_term term)
+
+and pp_patterns patterns =
+ sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
+
+and pp_capture_variable = function
+ | term, None -> pp_term term
+ | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
+
+and pp_layout = function
+ | Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
+ | Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
+ | Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
+ | Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2)
+ | Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
+ | Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
+ | Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
+ | Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
+ | Root (arg, index) ->
+ sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
+ | Break -> "\\BREAK"
+ | Box (H, terms) ->
+ sprintf "\\HBOX [%s]" (String.concat " " (List.map pp_term terms))
+ | Box (V, terms) ->
+ sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
+
+and pp_magic = function
+ | List0 (t, sep_opt) -> sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | List1 (t, sep_opt) -> sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | Opt t -> sprintf "\\OPT %s" (pp_term t)
+ | _ -> failwith "magic not implemented"
+
+and pp_sep_opt = function
+ | None -> ""
+ | Some sep -> sprintf "\\SEP %s" (pp_literal sep)
+
+and pp_variable = function
+ | NumVar s -> "\\NUM " ^ s
+ | IdentVar s -> "\\IDENT " ^ s
+ | TermVar s -> "\\TERM " ^ s
+ | Ascription (t, n) -> sprintf "[%s \\AS %s]" (pp_term t) n
+ | FreshVar n -> "\\FRESH " ^ n
+
+let rec pp_value = function
+ | TermValue t -> sprintf "$%s$" (pp_term t)
+ | StringValue s -> sprintf "\"%s\"" s
+ | NumValue n -> n
+ | OptValue (Some v) -> "Some " ^ pp_value v
+ | OptValue None -> "None"
+ | ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
+
+let rec pp_value_type =
+ function
+ | TermType -> "Term"
+ | StringType -> "String"
+ | NumType -> "Number"
+ | OptType t -> "Maybe " ^ pp_value_type t
+ | ListType l -> "List " ^ pp_value_type l
+
+let pp_env env =
+ String.concat "; "
+ (List.map
+ (fun (name, (ty, value)) ->
+ sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
+ env)
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val pp_term: CicNotationPt.term -> string
+
+val pp_env: CicNotationEnv.env_type -> string
+val pp_value: CicNotationEnv.value -> string
+val pp_value_type: CicNotationEnv.value_type -> string
+
type fold_kind = [ `Left | `Right ]
type location = Lexing.position * Lexing.position
+(* cut and past from CicAst.loc_of_floc *)
+let loc_of_floc = function
+ | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+ (loc_begin, loc_end)
+
type term_attribute =
[ `Loc of location (* source file location *)
| Magic of magic_term
| Variable of pattern_variable
-and capture_variable = Cic.name * term option (* name, type *)
+ (* name, type. First component must be Ident or Variable (FreshVar _) *)
+and capture_variable = term * term option
+
and meta_subst = term option
and subst = string * term
and case_pattern = string * capture_variable list
| ArgPattern of argument_pattern
| ApplPattern of cic_appl_pattern list
-type value =
- | TermValue of term
- | StringValue of string
- | NumValue of string
- | OptValue of value option
- | ListValue of value list
-
-type value_type =
- | TermType
- | StringType
- | NumType
- | OptType of value_type
- | ListType of value_type
-
-type declaration = string * value_type
+type phrase = (* TODO hackish: replace with TacticAst.statement or similar *)
+ | Print of term
+ | Notation of term * Gramext.g_assoc option * int option * term
+ (* level 1 pattern, associativity, precedence, level 2 pattern *)
open Printf
-(* cut and past from CicAst.loc_of_floc *)
-let loc_of_floc = function
- | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
- (loc_begin, loc_end)
-
let _ =
let module P = CicNotationPt in
let level = ref ~-1 in
(P.Layout (P.Box (P.H,
[
P.Magic
- (P.List0
+ (P.List1
(P.Layout (P.Box (P.H,
[ P.Literal (`Symbol "|");
P.Variable (P.TermVar "ugo");
])))
(fun env _ ->
prerr_endline "reducing rule" ;
- prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env));
+ prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env));
P.Sort `Prop)
in
CicNotationParser.print_l2_pattern ()
end;
- let parse_fun s =
- match !level with
- | 1 -> ignore (CicNotationParser.parse_syntax_pattern s)
- | 2 ->
- let ast = CicNotationParser.parse_ast_pattern s in
- if ast = P.Sort `Prop then
- prerr_endline "eureka (ma sono cazzi)"
- else
- prerr_endline ":-("
- | 3 -> ignore (CicNotationParser.parse_interpretation s)
- | _ -> Arg.usage arg_spec usage; exit 1
- in
let ic = stdin in
try
printf "Parsing notation level %d\n" !level; flush stdout;
let line = input_line ic in
let istream = Stream.of_string line in
try
- parse_fun istream;
- print_endline ">"
+ (match !level with
+ | -1 ->
+ (match CicNotationParser.parse_phrase istream with
+ | P.Print t ->
+ print_endline (CicNotationPp.pp_term t); flush stdout
+ | P.Notation (l1, associativity, precedence, l2) ->
+ prerr_endline "foo";
+ print_endline "Extending notation ..."; flush stdout;
+ ignore
+ (CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc ->
+ prerr_endline "ENV";
+ prerr_endline (CicNotationPp.pp_env env);
+ CicNotationEnv.instantiate env l2));
+ CicNotationParser.print_l2_pattern ())
+ | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
+ | 2 ->
+ let ast = CicNotationParser.parse_ast_pattern istream in
+ if ast = P.Sort `Prop then
+ prerr_endline "eureka"
+ else
+ prerr_endline ":-("
+ | 3 -> ignore (CicNotationParser.parse_interpretation istream)
+ | _ -> Arg.usage arg_spec usage; exit 1);
with CicNotationParser.Parse_error (floc, msg) ->
- let (x, y) = loc_of_floc floc in
+ let (x, y) = P.loc_of_floc floc in
let before = String.sub line 0 x in
let error = String.sub line x (y - x) in
let after = String.sub line y (String.length line - y) in
projects / helm.git / commitdiff