From 9230a8085102cd39258c047949e87001be6ffcf0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 27 May 2005 13:20:05 +0000 Subject: [PATCH] snapshot - first version with working DEFAULT magic --- helm/ocaml/cic_notation/.depend | 16 +- helm/ocaml/cic_notation/Makefile | 2 + helm/ocaml/cic_notation/cicNotationEnv.ml | 236 ++++++ helm/ocaml/cic_notation/cicNotationEnv.mli | 59 ++ helm/ocaml/cic_notation/cicNotationLexer.ml | 5 + .../cicNotationParser.expanded.ml | 699 +++++++++++------- helm/ocaml/cic_notation/cicNotationParser.ml | 608 +++++++-------- helm/ocaml/cic_notation/cicNotationParser.mli | 11 +- helm/ocaml/cic_notation/cicNotationPp.ml | 173 +++++ helm/ocaml/cic_notation/cicNotationPp.mli | 31 + helm/ocaml/cic_notation/cicNotationPt.ml | 28 +- helm/ocaml/cic_notation/test_parser.ml | 49 +- 12 files changed, 1293 insertions(+), 624 deletions(-) create mode 100644 helm/ocaml/cic_notation/cicNotationEnv.ml create mode 100644 helm/ocaml/cic_notation/cicNotationEnv.mli create mode 100644 helm/ocaml/cic_notation/cicNotationPp.ml create mode 100644 helm/ocaml/cic_notation/cicNotationPp.mli diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 8d107d761..d75b3fe64 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,7 +1,13 @@ -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 diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 9f8a0cb38..53c39ee5e 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -9,6 +9,8 @@ REQUIRES = \ $(NULL) INTERFACE_FILES = \ cicNotationLexer.mli \ + cicNotationEnv.mli \ + cicNotationPp.mli \ cicNotationParser.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml new file mode 100644 index 000000000..8d3149b98 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -0,0 +1,236 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli new file mode 100644 index 000000000..4ba9f2487 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -0,0 +1,59 @@ +(* 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 *) + diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index dfbedef73..8ad805c8d 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -35,6 +35,9 @@ let regexp ident = xml_letter ident_cont* ident_decoration* let regexp tex_token = '\\' ident +let regexp delim_begin = "\\[" +let regexp delim_end = "\\]" + let regexp keyword = '"' ident '"' let regexp implicit = '?' @@ -106,6 +109,8 @@ let rec token = lexer | 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", "") diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index 69b51c398..fcbc081a7 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -24,14 +24,14 @@ *) 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) @@ -39,27 +39,232 @@ llet int_of_string s = 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 @@ -78,11 +283,15 @@ Elet _ = 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 = @@ -104,15 +313,15 @@ Elet _ = 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)))], @@ -189,30 +398,22 @@ Elet _ = [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) -> @@ -221,30 +422,28 @@ Elet _ = 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 @@ -256,30 +455,16 @@ Elet _ = (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) @@ -321,7 +506,11 @@ Elet _ = 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, @@ -344,26 +533,68 @@ Elet _ = (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, @@ -400,13 +631,25 @@ Elet _ = 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 @@ -417,18 +660,20 @@ Elet _ = 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", ":"); @@ -438,9 +683,9 @@ Elet _ = 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), @@ -458,18 +703,22 @@ Elet _ = [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", ":"); @@ -479,15 +728,15 @@ Elet _ = 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 = @@ -503,7 +752,10 @@ Elet _ = 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 @@ -514,11 +766,11 @@ Elet _ = 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 @@ -542,12 +794,15 @@ Elet _ = 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"); @@ -555,23 +810,28 @@ Elet _ = [[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 @@ -593,8 +853,10 @@ Elet _ = (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 @@ -603,10 +865,10 @@ Elet _ = 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) @@ -618,9 +880,10 @@ Elet _ = | 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))], @@ -659,7 +922,7 @@ Elet _ = 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 @@ -667,7 +930,7 @@ Elet _ = 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 @@ -681,28 +944,24 @@ Elet _ = 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", "")], @@ -733,8 +992,7 @@ Elet _ = [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", ""); @@ -777,47 +1035,51 @@ Elet _ = 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, @@ -832,7 +1094,27 @@ Elet _ = 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 @@ -843,153 +1125,14 @@ let exc_located_wrapper 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 - -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); diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index ede5b6e66..c7cc77be0 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -25,11 +25,18 @@ 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" @@ -37,13 +44,10 @@ let l2_pattern = Grammar.Entry.create grammar "l2_pattern" 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) @@ -54,17 +58,213 @@ let int_of_string s = 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) @@ -72,13 +272,27 @@ let fold_binder binder pt_names 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 @@ -95,8 +309,7 @@ EXTEND ] ]; 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 ] @@ -111,38 +324,37 @@ EXTEND 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 @@ -150,17 +362,26 @@ EXTEND ] ]; explicit_subst: [ - [ (* TODO explicit substitution *) + [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + SYMBOL "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); 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: [ @@ -176,13 +397,18 @@ EXTEND | SYMBOL <:unicode> (* λ *) -> `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 @@ -197,8 +423,8 @@ EXTEND ]; 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> (* ≝ *); body = l2_pattern -> let body = fold_binder `Lambda args body in @@ -213,7 +439,9 @@ EXTEND | _ :: 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 @@ -224,13 +452,14 @@ EXTEND | 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 ] @@ -238,16 +467,18 @@ EXTEND 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> (* ≝ *); p1 = l2_pattern; "in"; p2 = l2_pattern -> return_term loc (LetIn (var, p1, p2)) @@ -255,15 +486,15 @@ EXTEND 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) @@ -273,15 +504,16 @@ EXTEND 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; @@ -300,7 +532,6 @@ EXTEND | 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 *) @@ -324,15 +555,20 @@ EXTEND (* }}} *) (* {{{ 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: [ @@ -342,8 +578,18 @@ EXTEND ] ]; (* }}} *) +(* {{{ 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 () @@ -355,244 +601,14 @@ let exc_located_wrapper 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); diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index ef6aa482c..b619606d0 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -37,9 +37,10 @@ val parse_ast_pattern: char Stream.t -> CicNotationPt.term (** 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 @@ -47,17 +48,13 @@ val extend: 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 diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml new file mode 100644 index 000000000..5befd8ed2 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -0,0 +1,173 @@ +(* 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) + diff --git a/helm/ocaml/cic_notation/cicNotationPp.mli b/helm/ocaml/cic_notation/cicNotationPp.mli new file mode 100644 index 000000000..77f65bf5f --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationPp.mli @@ -0,0 +1,31 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 3d6242e96..e9683521e 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -31,6 +31,11 @@ type sort_kind = [ `Prop | `Set | `Type | `CProp ] 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 *) @@ -76,7 +81,9 @@ type term = | 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 @@ -130,19 +137,8 @@ type cic_appl_pattern = | 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 *) diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 6cbb0ef2d..e4db4d503 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -25,11 +25,6 @@ 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 @@ -42,7 +37,7 @@ let _ = (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"); @@ -65,23 +60,11 @@ let _ = ]))) (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; @@ -89,10 +72,32 @@ let _ = 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 -- 2.39.2