From: Luca Padovani Date: Tue, 12 Jul 2005 15:07:10 +0000 (+0000) Subject: snapshot X-Git-Tag: pre_notation~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;p=helm.git snapshot - revised concrete syntax - split parsers and lexers - removed IF and THEN magics in favour of IF/THEN/ELSE and FAIL --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 808549afc..6eae806d5 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -4,8 +4,8 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationMatcher.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi -cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationRew.cmi: cicNotationPt.cmo cicNotationPres.cmi: cicNotationPt.cmo cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi @@ -27,15 +27,19 @@ cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ cicNotationFwd.cmi cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ cicNotationFwd.cmi -cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ - cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi -cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ - cicNotationMatcher.cmx cicNotationEnv.cmx cicNotationRew.cmi cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationPp.cmi cicNotationLexer.cmi cicNotationEnv.cmi \ cicNotationParser.cmi cicNotationParser.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ cicNotationPp.cmx cicNotationLexer.cmx cicNotationEnv.cmx \ cicNotationParser.cmi -cicNotationPres.cmo: cicNotationPt.cmo cicNotationPres.cmi -cicNotationPres.cmx: cicNotationPt.cmx cicNotationPres.cmi +cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ + cicNotationParser.cmi cicNotationMatcher.cmi cicNotationEnv.cmi \ + cicNotationRew.cmi +cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + cicNotationParser.cmx cicNotationMatcher.cmx cicNotationEnv.cmx \ + cicNotationRew.cmi +cicNotationPres.cmo: cicNotationPt.cmo cicNotationPres.cmi cicNotationPp.cmi \ + cicNotationPres.cmi +cicNotationPres.cmx: cicNotationPt.cmx cicNotationPres.cmx cicNotationPp.cmx \ + cicNotationPres.cmi diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index f2e2c7164..8e955c0b1 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -211,7 +211,6 @@ let instantiate_level2 env term = | [] -> assert false (* as above *) | (name :: _) as names -> let rec instantiate_fold_left acc env' = - prerr_endline "instantiate_fold_left"; match lookup_value env' name with | ListValue (_ :: _) -> instantiate_fold_left @@ -232,7 +231,6 @@ let instantiate_level2 env term = | [] -> assert false (* as above *) | (name :: _) as names -> let rec instantiate_fold_right env' = - prerr_endline "instantiate_fold_right"; match lookup_value env' name with | ListValue (_ :: _) -> let acc = instantiate_fold_right (tail_names names env') in @@ -242,8 +240,8 @@ let instantiate_level2 env term = | _ -> assert false in instantiate_fold_right env) - | If (_, body) - | Unless (_, body) -> aux env body + | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t)) + | Fail -> assert false | _ -> assert false in aux env term diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 3c262ceec..26dc5aaca 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -39,12 +39,45 @@ let regexp delim_begin = "\\[" let regexp delim_end = "\\]" let regexp keyword = '"' ident '"' +let regexp qkeyword = "'" ident "'" let regexp implicit = '?' let regexp meta = implicit number let regexp csymbol = '\'' ident +let regexp begin_group = "@{" | "${" +let regexp end_group = '}' +let regexp wildcard = "$_" +let regexp ast_ident = "@" ident +let regexp ast_csymbol = "@" csymbol +let regexp meta_ident = "$" ident +let regexp meta_anonymous = "$_" +let regexp qstring = '"' [^ '"']* '"' + +let level1_layouts = + [ "sub"; "sup"; + "below"; "above"; + "over"; "atop"; "frac"; + "sqrt"; "root" + ] + +let level2_meta_keywords = + [ "if"; "then"; "else"; + "fold"; "left"; "right"; "rec"; + "fail"; + "default"; + "anonymous"; "ident"; "number"; "term"; "fresh" + ] + +let level1_keywords = + [ "hbox"; "hvbox"; "hovbox"; "vbox"; + "break"; + "list0"; "list1"; "sep"; + "opt"; + "term"; "ident"; "number" + ] + let regexp uri = ("cic:/" | "theory:/") (* schema *) ident ('/' ident)* (* path *) @@ -58,8 +91,7 @@ let error_at_end lexbuf msg = let begin_cnum, end_cnum = Ulexing.loc lexbuf in raise (Error (begin_cnum, end_cnum, msg)) -let return lexbuf token = - let begin_cnum, end_cnum = Ulexing.loc lexbuf in +let return_with_loc token begin_cnum end_cnum = (* TODO handle line/column numbers *) let flocation_begin = { Lexing.pos_fname = ""; @@ -69,6 +101,10 @@ let return lexbuf token = let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in (token, (flocation_begin, flocation_end)) +let return lexbuf token = + let begin_cnum, end_cnum = Ulexing.loc lexbuf in + return_with_loc token begin_cnum end_cnum + let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf) let remove_quotes s = String.sub s 1 (String.length s - 2) @@ -104,22 +140,84 @@ let expand_macro lexbuf = let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf) -let rec token = lexer - | xml_blank+ -> token lexbuf +let remove_quotes s = String.sub s 1 (String.length s - 2) +let remove_left_quote s = String.sub s 1 (String.length s - 1) + +let rec level2_pattern_token_group counter buffer = lexer + | end_group -> + if (counter > 0) then + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + snd (Ulexing.loc lexbuf) + | begin_group -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + | _ -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + +let read_unparsed_group token_name lexbuf = + let buffer = Buffer.create 16 in + let begin_cnum, _ = Ulexing.loc lexbuf in + let end_cnum = level2_pattern_token_group 0 buffer lexbuf in + return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum + +let rec level2_meta_token = lexer + | xml_blank+ -> level2_meta_token lexbuf + | ident -> + let s = Ulexing.utf8_lexeme lexbuf in + begin + if List.mem s level2_meta_keywords then + return lexbuf ("", s) + else + return lexbuf ("IDENT", s) + end + | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf + | ast_ident -> return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | ast_csymbol -> return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | eof -> return lexbuf ("EOI", "") + +let rec level2_ast_token = lexer + | xml_blank+ -> level2_ast_token lexbuf | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) | 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", "") + | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf) + | "${" -> read_unparsed_group "UNPARSED_META" lexbuf + | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf + | '(' -> return lexbuf ("LPAREN", "") + | ')' -> return lexbuf ("RPAREN", "") + | meta_ident -> return lexbuf ("UNPARSED_META", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous") + | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) + | eof -> return lexbuf ("EOI", "") + +let rec level1_pattern_token = lexer + | xml_blank+ -> level1_pattern_token lexbuf + | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) + | ident -> + let s = Ulexing.utf8_lexeme lexbuf in + begin + if List.mem s level1_keywords then + return lexbuf ("", s) + else + return lexbuf ("IDENT", s) + end + | tex_token -> return lexbuf (expand_macro lexbuf) + | qkeyword -> return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)) + | '(' -> return lexbuf ("LPAREN", "") + | ')' -> return lexbuf ("RPAREN", "") + | eof -> return lexbuf ("EOI", "") | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) (* API implementation *) -let notation_lexer = mk_lexer token +let level1_pattern_lexer = mk_lexer level1_pattern_token +let level2_ast_lexer = mk_lexer level2_ast_token +let level2_meta_lexer = mk_lexer level2_meta_token diff --git a/helm/ocaml/cic_notation/cicNotationLexer.mli b/helm/ocaml/cic_notation/cicNotationLexer.mli index dd1561be2..33ba97e2b 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.mli +++ b/helm/ocaml/cic_notation/cicNotationLexer.mli @@ -28,5 +28,7 @@ * error message *) exception Error of int * int * string -val notation_lexer: (string * string) Token.glexer +val level1_pattern_lexer: (string * string) Token.glexer +val level2_ast_lexer: (string * string) Token.glexer +val level2_meta_lexer: (string * string) Token.glexer diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 39c82b7da..9d879db5e 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -122,6 +122,20 @@ struct | hd :: tl -> k (hd :: matched_terms) tl | _ -> assert false) + let success_closure ks k = + (fun matched_terms terms -> + match ks matched_terms with + None -> + begin + (* the match has failed, we rollback the last matched term + * into the unmatched ones and call the failure continuation + *) + match matched_terms with + hd :: tl -> k tl (hd :: terms) + | _ -> assert false + end + | Some v -> Some v) + let constructor_closure ks k = (fun matched_terms terms -> match terms with @@ -138,19 +152,7 @@ struct if t = [] then k else if are_empty t then - let res = match_cb (matched t) in - (fun matched_terms terms -> - match res matched_terms with - None -> - begin - (* the match has failed, we rollback the last matched term - * into the unmatched ones and call the failure continuation - *) - match matched_terms with - hd :: tl -> k tl (hd :: terms) - | _ -> assert false - end - | Some v -> Some v) + success_closure (match_cb (matched t)) k else match horizontal_split t with | _, [], _ -> assert false @@ -248,29 +250,23 @@ struct let magichecker map = List.fold_left (fun f (name, m) -> - prerr_endline ("compiling magichecker for " ^ name) ; let m_checker = compile_magic m in (fun env -> match m_checker (Env.lookup_term env name) env with | None -> None | Some env' -> f env')) - (fun env -> - prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ; - Some env) + (fun env -> Some env) map in let magichooser candidates = List.fold_left (fun f (pid, pl, checker) -> - List.iter (fun p -> prerr_endline ("P = " ^ Pp.pp_term p)) pl ; (fun matched_terms -> let env = env_of_matched pl matched_terms in match checker env with | None -> f matched_terms | Some env -> - prerr_endline (String.concat " / " (List.map Pp.pp_term pl)) ; - prerr_endline ("magichoose found a match for " ^ Pp.pp_env env ^ " " ^ string_of_int pid) ; let magic_map = try List.assoc pid magic_maps with Not_found -> assert false in @@ -334,33 +330,21 @@ struct | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) | _ -> assert false) - | Pt.If (guard, p) -> - let compiled_guard = compiler [guard, 0] - and compiled_p = compiler [p, 0] in - (fun term env -> - match compiled_guard term with - | None -> None - | Some _ -> - begin - match compiled_p term with - | None -> None - | Some (env', _) -> - Some (env' @ env) - end) - - | Pt.Unless (guard, p) -> - let compiled_guard = compiler [guard, 0] - and compiled_p = compiler [p, 0] in + | Pt.If (p_test, p_true, p_false) -> + let compiled_test = compiler [p_test, 0] + and compiled_true = compiler [p_true, 0] + and compiled_false = compiler [p_false, 0] in (fun term env -> - match compiled_guard term with - | None -> - begin - match compiled_p term with - | None -> None - | Some (env', _) -> - Some (env' @ env) - end - | Some _ -> None) + let branch = + match compiled_test term with + | None -> compiled_false + | Some _ -> compiled_true + in + match branch term with + | None -> None + | Some (env', _) -> Some (env' @ env)) + + | Pt.Fail -> (fun _ _ -> None) | _ -> assert false end diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index 0adf84723..5d103bdaa 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -134,7 +134,6 @@ let extract_term_production pattern = 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 -> @@ -143,12 +142,11 @@ let extract_term_production pattern = 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 + List.fold_right grow_env env_list env0 in let g_symbol s = match magic with @@ -173,14 +171,9 @@ let extract_term_production pattern = 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) + (fun (env : env_type) (loc : location) -> env) p_bindings in p_bindings, p_atoms, p_names, action @@ -202,7 +195,6 @@ let extend level1_pattern ?(precedence = default_precedence) = 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), diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index f3a6035d4..b64fdb5ee 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -31,7 +31,10 @@ open CicNotationPt exception Parse_error of Token.flocation * string exception Level_not_found of int -let grammar = Grammar.gcreate CicNotationLexer.notation_lexer +let level1_pattern_grammar = + Grammar.gcreate CicNotationLexer.level1_pattern_lexer +let level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexer +let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer let min_precedence = 0 let max_precedence = 100 @@ -47,14 +50,18 @@ let binder_assoc = Gramext.RightA let apply_assoc = Gramext.LeftA let simple_assoc = Gramext.NonA -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 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 level1_pattern = + Grammar.Entry.create level1_pattern_grammar "level1_pattern" +let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" +let term = Grammar.Entry.create level2_ast_grammar "term" +let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" + +let level3_term = Grammar.Entry.create level2_ast_grammar "level3_term" +let notation = (* level1 <-> level 2 *) + Grammar.Entry.create level2_ast_grammar "notation" +let interpretation = (* level2 <-> level 3 *) + Grammar.Entry.create level2_ast_grammar "interpretation" +let phrase = Grammar.Entry.create level2_ast_grammar "phrase" let return_term loc term = () @@ -73,7 +80,6 @@ let int_of_string s = 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 @@ -143,18 +149,18 @@ let extract_term_production pattern = | `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 + | 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"] + [NoBinding, symbol "\\root"] @ aux p2 @ [NoBinding, symbol "\\of"] @ aux p1 - | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p -(* | Break -> [] *) + | Sqrt p -> [NoBinding, symbol "\\sqrt"] @ aux p + | Break -> [] | Box (_, pl) -> List.flatten (List.map aux pl) and aux_magic magic = match magic with @@ -205,14 +211,13 @@ let extract_term_production pattern = and aux_variable = function | NumVar s -> [Binding (s, NumType), number ""] - | TermVar s -> [Binding (s, TermType), term] + | TermVar s -> [Binding (s, TermType), Gramext.Sself] | 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 : CicNotationEnv.t) (loc : location) -> env) p_bindings @@ -237,9 +242,8 @@ let extend level1_pattern ?(precedence = default_precedence) 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), + [ Grammar.Entry.obj (term: 'a Grammar.Entry.e), Some (Gramext.Level level), [ None, associativity, @@ -250,10 +254,14 @@ let extend level1_pattern ?(precedence = default_precedence) in p_atoms -let delete atoms = Grammar.delete_rule l2_pattern atoms +let delete atoms = Grammar.delete_rule term atoms (** {2 Grammar} *) +let parse_level1_pattern_ref = ref (fun _ -> assert false) +let parse_level2_ast_ref = ref (fun _ -> assert false) +let parse_level2_meta_ref = ref (fun _ -> assert false) + let fold_binder binder pt_names body = let fold_cluster binder terms ty body = List.fold_right @@ -266,7 +274,7 @@ 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 _ = (* create empty precedence level for "term" *) let mk_level_list first last = let rec aux acc = function | i when i < first -> acc @@ -275,96 +283,131 @@ let _ = (* create empty precedence level for "l2_pattern" *) aux [] last in Grammar.extend - [ Grammar.Entry.obj (l2_pattern: 'a Grammar.Entry.e), + [ Grammar.Entry.obj (term: 'a Grammar.Entry.e), None, mk_level_list min_precedence max_precedence ] -EXTEND - GLOBAL: level1_pattern level2_pattern level3_term - l2_pattern - notation interpretation - phrase; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) - level1_pattern: [ [ p = l1_simple_pattern -> p ] ]; +EXTEND + GLOBAL: level1_pattern; + + level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ]; l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ]; literal: [ [ s = SYMBOL -> `Symbol s - | k = KEYWORD -> `Keyword k + | k = QKEYWORD -> `Keyword k | n = NUMBER -> `Number n ] ]; - sep: [ [ SYMBOL "\\SEP"; sep = literal -> sep ] ]; -(* row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> sep ] ]; - field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> sep ] ]; *) + sep: [ [ "sep"; sep = literal -> sep ] ]; +(* row_sep: [ [ "rowsep"; sep = literal -> sep ] ]; + field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *) l1_magic_pattern: [ - [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep) - | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep) - | SYMBOL "\\OPT"; p = l1_simple_pattern -> Opt p + [ "list0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep) + | "list1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep) + | "opt"; p = l1_simple_pattern -> Opt p ] ]; l1_pattern_variable: [ - [ SYMBOL "\\TERM"; id = IDENT -> TermVar id - | SYMBOL "\\NUM"; id = IDENT -> NumVar id - | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id + [ "term"; id = IDENT -> TermVar id + | "number"; id = IDENT -> NumVar id + | "ident"; id = IDENT -> IdentVar id ] ]; l1_simple_pattern: [ "layout" LEFTA - [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> + [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF -> return_term loc (Layout (Sub (p1, p2))) - | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\sup"; p2 = SELF -> return_term loc (Layout (Sup (p1, p2))) - | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\below"; p2 = SELF -> return_term loc (Layout (Below (p1, p2))) - | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\above"; p2 = SELF -> return_term loc (Layout (Above (p1, p2))) - | p1 = SELF; SYMBOL "\\OVER"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\over"; p2 = SELF -> return_term loc (Layout (Over (p1, p2))) - | p1 = SELF; SYMBOL "\\ATOP"; p2 = SELF -> + | 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 -> +(* | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep -> return_term loc (Array (p, csep, rsep)) *) - | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> + | 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 = 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, false, false), p))) - | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box ((V, false, false), p))) - | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box ((HV, false, false), p))) - | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box ((HOV, false, false), p))) -(* | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *) + | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Layout (Sqrt p)) + | SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF -> + return_term loc (Layout (Root (arg, index))) + | "hbox"; LPAREN; p = l1_pattern; RPAREN -> + return_term loc (CicNotationUtil.boxify p) + | "vbox"; LPAREN; p = l1_pattern; RPAREN -> + return_term loc (CicNotationUtil.boxify p) + | "hvbox"; LPAREN; p = l1_pattern; RPAREN -> + return_term loc (CicNotationUtil.boxify p) + | "hovbox"; LPAREN; p = l1_pattern; RPAREN -> + return_term loc (CicNotationUtil.boxify p) + | "break" -> return_term loc (Layout Break) (* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *) - | DELIM "\\["; p = l1_pattern; DELIM "\\]" -> + | "LPAREN"; p = l1_pattern; "RPAREN" -> return_term loc (CicNotationUtil.boxify p) - | p = SELF; SYMBOL "\\AS"; id = IDENT -> - return_term loc (Variable (Ascription (p, id))) ] | "simple" NONA - [ i = IDENT -> return_term loc (Ident (i, None)) + [ i = IDENT -> return_term loc (Variable (TermVar i)) | 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) ] ]; + END (* }}} *) + + +EXTEND + GLOBAL: level2_meta; + l2_variable: [ + [ "term"; id = IDENT -> TermVar id + | "number"; id = IDENT -> NumVar id + | "ident"; id = IDENT -> IdentVar id + | "fresh"; id = IDENT -> FreshVar id + | "anonymous" -> TermVar "_" + | id = IDENT -> TermVar id + ] + ]; + l2_magic: [ + [ "fold"; kind = [ "left" -> `Left | "right" -> `Right ]; + base = level2_meta; "rec"; id = IDENT; recursive = level2_meta -> + Fold (kind, base, [id], recursive) + | "default"; some = level2_meta; none = level2_meta -> Default (some, none) + | "if"; p_test = level2_meta; + "then"; p_true = level2_meta; + "else"; p_false = level2_meta -> + If (p_test, p_true, p_false) + | "fail" -> Fail + ] + ]; + level2_meta: [ + [ magic = l2_magic -> Magic magic + | var = l2_variable -> Variable var + | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob) + ] + ]; +END + +EXTEND + GLOBAL: level2_ast term + level3_term + notation interpretation + phrase; (* {{{ Grammar for ast patterns, notation level 2 *) - level2_pattern: [ [ p = l2_pattern -> p ] ]; + level2_ast: [ [ p = term -> p ] ]; sort: [ - [ SYMBOL "\\PROP" -> `Prop - | SYMBOL "\\SET" -> `Set - | SYMBOL "\\TYPE" -> `Type + [ IDENT "Prop" -> `Prop + | IDENT "Set" -> `Set + | IDENT "Type" -> `Type ] ]; explicit_subst: [ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) SYMBOL "["; substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = l2_pattern -> (i, t) + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) ] SEP SYMBOL ";"; SYMBOL "]" -> substs @@ -372,20 +415,20 @@ EXTEND ]; meta_subst: [ [ s = SYMBOL "_" -> None - | p = l2_pattern -> Some p ] + | p = term -> Some p ] ]; meta_substs: [ [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ] ]; possibly_typed_name: [ - [ SYMBOL "("; id = bound_name; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" -> + [ LPAREN; id = bound_name; SYMBOL ":"; typ = term; RPAREN -> id, Some typ | id = bound_name -> id, None ] ]; match_pattern: [ [ id = IDENT -> id, [] - | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" -> + | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> id, vars ] ]; @@ -403,13 +446,13 @@ EXTEND ]; bound_names: [ [ vars = LIST1 bound_name SEP SYMBOL ","; - ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] -> + ty = OPT [ SYMBOL ":"; p = term -> p ] -> [ vars, ty ] | clusters = LIST1 [ - SYMBOL "("; + LPAREN; vars = LIST1 bound_name SEP SYMBOL ","; - ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ]; - SYMBOL ")" -> + ty = OPT [ SYMBOL ":"; p = term -> p ]; + RPAREN -> vars, ty ] -> clusters @@ -424,8 +467,8 @@ EXTEND [ defs = LIST1 [ 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 -> + ty = OPT [ SYMBOL ":" ; p = term -> p ]; + SYMBOL <:unicode> (* ≝ *); body = term -> let body = fold_binder `Lambda args body in let ty = match ty with @@ -456,53 +499,25 @@ EXTEND defs ] ]; - l2_pattern_variable: [ - [ 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 ]; - DELIM "\\["; base = l2_pattern; DELIM "\\]"; - SYMBOL "\\LAMBDA"; id = IDENT; - DELIM "\\["; recursive = l2_pattern; DELIM "\\]" -> - Fold (kind, base, [id], recursive) - | SYMBOL "\\DEFAULT"; - DELIM "\\["; some = l2_pattern; DELIM "\\]"; - DELIM "\\["; none = l2_pattern; DELIM "\\]" -> - Default (some, none) - | SYMBOL "\\IF"; - DELIM "\\["; guard = l2_pattern; DELIM "\\]"; - DELIM "\\["; p = l2_pattern; DELIM "\\]" -> - If (guard, p) - | SYMBOL "\\UNLESS"; - DELIM "\\["; guard = l2_pattern; DELIM "\\]"; - DELIM "\\["; p = l2_pattern; DELIM "\\]" -> - Unless (guard, p) - ] - ]; - l2_pattern: LEVEL "10" (* let in *) + term: LEVEL "10" (* let in *) [ "10" NONA [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); - p1 = l2_pattern; "in"; p2 = l2_pattern -> + p1 = term; "in"; p2 = term -> return_term loc (LetIn (var, p1, p2)) | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in"; - body = l2_pattern -> + body = term -> return_term loc (LetRec (k, defs, body)) ] ]; - l2_pattern: LEVEL "20" (* binder *) + term: LEVEL "20" (* binder *) [ "20" RIGHTA - [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern -> + [ b = binder; names = bound_names; SYMBOL "."; body = term -> return_term loc (fold_binder b names body) ] ]; - l2_pattern: LEVEL "70" (* apply *) + term: LEVEL "70" (* apply *) [ "70" LEFTA - [ p1 = l2_pattern; p2 = l2_pattern -> + [ p1 = term; p2 = term -> let rec aux = function | Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) -> @@ -512,7 +527,7 @@ EXTEND return_term loc (Appl (aux p1 @ [p2])) ] ]; - l2_pattern: LEVEL "90" (* simple *) + term: 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)) @@ -523,22 +538,21 @@ EXTEND | m = META -> return_term loc (Meta (int_of_string m, [])) | 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; + | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ]; + IDENT "match"; t = term; indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; IDENT "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); - rhs = l2_pattern -> + rhs = term -> lhs, rhs ] SEP SYMBOL "|"; SYMBOL "]" -> return_term loc (Case (t, indty_ident, outtyp, patterns)) - | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" -> + | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN -> return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ]) - | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p - | v = l2_pattern_variable -> return_term loc (Variable v) - | m = l2_magic_pattern -> return_term loc (Magic m) + | LPAREN; p = term; RPAREN -> p + | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob) ] ]; (* }}} *) @@ -553,7 +567,7 @@ EXTEND level3_term: [ [ u = URI -> UriPattern (UriManager.uri_of_string u) | id = IDENT -> VarPattern id - | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> + | LPAREN; terms = LIST1 SELF; RPAREN -> (match terms with | [] -> assert false | [term] -> term @@ -572,10 +586,15 @@ EXTEND [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ - [ p1 = level1_pattern; + [ s = QSTRING; assoc = OPT associativity; prec = OPT precedence; - IDENT "for"; p2 = level2_pattern -> - (p1, assoc, prec, p2) + IDENT "for"; + p2 = + [ blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob) + | blob = UNPARSED_META -> + !parse_level2_meta_ref (Stream.of_string blob) ] + -> + (!parse_level1_pattern_ref (Stream.of_string s), assoc, prec, p2) ] ]; interpretation: [ @@ -586,7 +605,7 @@ EXTEND (* }}} *) (* {{{ Top-level phrases *) phrase: [ - [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2 + [ IDENT "print"; t = term; SYMBOL "." -> Print t | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." -> Notation (l1, assoc, prec, l2) | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." -> @@ -608,19 +627,26 @@ let exc_located_wrapper f = | Stdpp.Exc_located (floc, exn) -> raise (Parse_error (floc, (Printexc.to_string exn))) -let parse_syntax_pattern stream = +let parse_level1_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_level2_ast stream = + exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream) +let parse_level2_meta stream = + exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta 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) +let _ = + parse_level1_pattern_ref := parse_level1_pattern; + parse_level2_ast_ref := parse_level2_ast; + parse_level2_meta_ref := parse_level2_meta + (** {2 Debugging} *) let print_l2_pattern () = - Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern); + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term); Format.pp_print_flush Format.std_formatter (); flush stdout diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 22dffd4bf..73627cd0a 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -29,10 +29,10 @@ exception Level_not_found of int (** {2 Parsing functions} *) (** concrete syntax pattern: notation level 1 *) -val parse_syntax_pattern: char Stream.t -> CicNotationPt.term +val parse_level1_pattern: char Stream.t -> CicNotationPt.term (** AST pattern: notation level 2 *) -val parse_ast_pattern: char Stream.t -> CicNotationPt.term +val parse_level2_ast: char Stream.t -> CicNotationPt.term (** interpretation: notation level 3 *) val parse_interpretation: char Stream.t -> CicNotationPt.cic_appl_pattern diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index c3185d6a2..f8b8acba0 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -138,7 +138,7 @@ and pp_layout = function | Sqrt t -> sprintf "\\SQRT %s" (pp_term t) | Root (arg, index) -> sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) -(* | Break -> "\\BREAK" *) + | Break -> "\\BREAK" (* | Space -> "\\SPACE" *) | Box (box_spec, terms) -> sprintf "\\%s [%s]" (pp_box_spec box_spec) @@ -156,10 +156,10 @@ and pp_magic = function (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec) | Default (p_some, p_none) -> sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none) - | If (p_guard, p) -> - sprintf "\\IF \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p) - | Unless (p_guard, p) -> - sprintf "\\UNLESS \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p) + | If (p_test, p_true, p_false) -> + sprintf "\\IF \\[%s\\] \\[%s\\] \\[%s\\]" + (pp_term p_test) (pp_term p_true) (pp_term p_false) + | Fail -> "\\FAIL" and pp_fold_kind = function | `Left -> "left" diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 790bb3785..83bb10878 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -142,8 +142,8 @@ let is_atomic t = aux_mpres t let add_parens child_prec child_assoc child_pos curr_prec t = - prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec - (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); +(* prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec + (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); *) if is_atomic t then t else if child_prec < curr_prec || (child_prec = curr_prec && @@ -211,7 +211,6 @@ let render ids_to_uris = add_parens child_prec child_assoc pos prec t' | `IdRef xref -> aux mathonly (Some xref) pos prec uris t | `Href uris' -> aux mathonly xref pos prec uris' t - | _ -> assert false and aux_literal xref prec uris l = let attrs = make_href xref uris in match l with diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 56bf85474..9c5257e07 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -79,6 +79,7 @@ type term = | Literal of literal | Layout of layout_pattern + | Magic of magic_term | Variable of pattern_variable @@ -104,7 +105,7 @@ and layout_pattern = |+ column separator, row separator +| *) | Sqrt of term | Root of term * term (* argument, index *) -(* | Break *) + | Break | Box of box_spec * term list and magic_term = @@ -117,8 +118,8 @@ and magic_term = | Fold of fold_kind * term * string list * term (* base case pattern, recursive case bound names, recursive case pattern *) | Default of term * term (* "some" case pattern, "none" case pattern *) - | If of term * term (* guard, body *) - | Unless of term * term (* guard, body *) + | Fail + | If of term * term * term (* test, pattern if true, pattern if false *) and pattern_variable = (* level 1 and 2 variables *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 180a8c912..f3f6cac2a 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -118,7 +118,6 @@ let pp_ast0 t k = aux t let ast_of_acic0 term_info acic k = -(* prerr_endline "ast_of_acic0"; *) let k = k term_info in let register_uri id uri = Hashtbl.add term_info.uri id uri in let sort_of_id id = @@ -265,7 +264,6 @@ let instantiate21 env (* precedence associativity *) l1 = | Ast.AttributedTerm (_, t) -> subst env t | Ast.Variable var -> let name, expected_ty = CicNotationEnv.declaration_of_var var in - prerr_endline ("searching for " ^ name); let ty, value = try List.assoc name env @@ -357,15 +355,9 @@ let rec pp_ast1 term = Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - prerr_endline ("IN " ^ CicNotationPp.pp_term term); - (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *) - let res = Ast.AttributedTerm (`Level (precedence, associativity), - (instantiate21 (ast_env_of_env env) l1)) - in - prerr_endline "OUT"; - res + Ast.AttributedTerm (`Level (precedence, associativity), + (instantiate21 (ast_env_of_env env) l1)) end - let instantiate32 term_info env symbol args = let rec instantiate_arg = function diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index f10efa754..24b4af1d9 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -161,7 +161,7 @@ let visit_layout k = function | Frac (t1, t2) -> Frac (k t1, k t2) | Sqrt t -> Sqrt (k t) | Root (arg, index) -> Root (k arg, k index) -(* | Break -> Break *) + | Break -> Break | Box (kind, terms) -> Box (kind, List.map k terms) let visit_magic k = function @@ -170,8 +170,8 @@ let visit_magic k = function | Opt t -> Opt (k t) | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2) | Default (t1, t2) -> Default (k t1, k t2) - | If (t1, t2) -> If (k t1, k t2) - | Unless (t1, t2) -> Unless (k t1, k t2) + | If (t1, t2, t3) -> If (k t1, k t2, k t3) + | Fail -> Fail let variables_of_term t = let rec vars = ref [] in @@ -277,6 +277,11 @@ let meta_names_of_term term = | Fold (_, t1, _, t2) -> aux t1 ; aux t2 + | If (t1, t2, t3) -> + aux t1 ; + aux t2 ; + aux t3 + | Fail -> () | _ -> assert false in aux term ; @@ -326,3 +331,8 @@ let find_appl_pattern_uris ap = in aux [] ap +let rec find_branch = + function + Magic (If (_, Magic Fail, t)) -> find_branch t + | Magic (If (_, t, _)) -> find_branch t + | t -> t diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 1a7d7d6f4..a03c415d2 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -51,3 +51,5 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term val find_appl_pattern_uris: CicNotationPt.cic_appl_pattern -> UriManager.uri list +val find_branch: + CicNotationPt.term -> CicNotationPt.term diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index d724ac4eb..f1f6ac939 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -1,3 +1,83 @@ + +notation + "\langle a , b \rangle" +for + @{ 'pair $a $b }. +print \langle 1, \langle 2, 3 \rangle \rangle. +print 'pair 1 ('pair 2 ('pair 3 4)). + +notation + "a :: b" +for + @{ 'cons $a $b }. +print 1 :: 2 :: 'ugo. + +notation + "[ hovbox (list0 a sep ; ) ]" +for ${ + fold right + @'nil + rec acc + @{ 'cons $a $acc } +}. +print [1;2;3;4]. + +notation + "[ list1 a sep ; | b ]" +for ${ + if @{ 'cons $_ $_ } then + fold right + if @'nil then + fail + else if @{ 'cons $_ $_ } then + fail + else + b + rec acc + @{ 'cons $a $acc } + else + fail +}. +print 'cons 1 ('cons 2 ('cons 3 'ugo)). +print 'cons 1 ('cons 2 ('cons 3 'nil)). +print [1;2;3;4]. +print [1;2;3;4|5]. + +notation "a + b" left associative for @{ 'plus $a $b }. +print 1 + 2 + 3. +print 1 + (2 + 3). + +notation + "'if' a 'then' b 'else' c" +for + @{ 'ifthenelse $a $b $c }. + +TODO collezionare le keyword e aggiungerle al lexer nonche' ricordarsele per quando si rimuove la notazione. + +notation + "a \vee b" +for + @{ if $a > $b then $a else $b } + +notation + "'fun' ident x \to a" + right associative at precedence ... +for + @{ 'lambda ${ident x} $a } + +NOTES + +@a e' un'abbreviazione per @{term a} +"x" e' un'abbreviazione per @{keyword x} +@_ e' un'abbreviazione per @{anonymous} + +\x simbolo della sintassi concreta +'x simbolo della sintassi astratta + +\lbrace \rbrace per le parentesi graffe al livello 1 + +OLD SAMPLES + # sample mappings level 1 <--> level 2 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]). @@ -6,7 +86,7 @@ print 1 ++ 2. notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \]. print + 1 2 3 4. -notation \[ [ \LIST0 \TERM a \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \]. +notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \]. print []. print [1;2;3;4]. diff --git a/helm/ocaml/cic_notation/test_lexer.ml b/helm/ocaml/cic_notation/test_lexer.ml index 386c0f1b9..c3569cda4 100644 --- a/helm/ocaml/cic_notation/test_lexer.ml +++ b/helm/ocaml/cic_notation/test_lexer.ml @@ -24,18 +24,26 @@ *) let _ = - let level = ref ~-1 in + let level = ref "2@" in let ic = ref stdin in - let arg_spec = [] in - let usage = "test_lexer [ file ]" in + let arg_spec = [ "-level", Arg.Set_string level, "set the notation level" ] in + let usage = "test_lexer [ -level level ] [ file ]" in let open_file fname = if !ic <> stdin then close_in !ic; ic := open_in fname in Arg.parse arg_spec open_file usage; - let lexer = CicNotationLexer.notation_lexer in + let lexer = + match !level with + "1" -> CicNotationLexer.level1_pattern_lexer + | "2@" -> CicNotationLexer.level2_ast_lexer + | "2$" -> CicNotationLexer.level2_meta_lexer + | l -> + prerr_endline (Printf.sprintf "Unsupported level %s" l); + exit 2 + in let token_stream = fst (lexer.Token.tok_func (Stream.of_channel !ic)) in - Printf.printf "Lexing notation level %d\n" !level; flush stdout; + Printf.printf "Lexing notation level %s\n" !level; flush stdout; let rec dump () = let (a,b) = Stream.next token_stream in if a = "EOI" then raise Stream.Failure; diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index ce87368bf..522baaccc 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -38,7 +38,7 @@ let xml_stream_of_markup = print_mpres let dump_xml t id_to_uri fname = - print_endline (sprintf "dumping MathML to %s ..." fname); + prerr_endline (sprintf "dumping MathML to %s ..." fname); flush stdout; let oc = open_out fname in Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; @@ -46,95 +46,78 @@ let dump_xml t id_to_uri fname = let _ = let module P = CicNotationPt in - let level = ref ~-1 in - let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in - let usage = "test_parser -level { 1 | 2 | 3 }" in - Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; - let ic = stdin in - try - printf "Parsing notation level %d\n" !level; flush stdout; - while true do - let line = input_line ic in - let istream = Stream.of_string line in - try - (match !level with - | -1 -> - (match CicNotationParser.parse_phrase istream with - | P.Print t -> + let arg_spec = [ ] in + let usage = "" in + Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + try + let istream = Stream.of_channel stdin in + while Stream.peek istream <> None do + match CicNotationParser.parse_phrase istream with + | P.Print t -> prerr_endline "===="; - print_endline (CicNotationPp.pp_term t); flush stdout; + prerr_endline (CicNotationPp.pp_term t); flush stdout; let t' = CicNotationRew.pp_ast t in - print_endline (CicNotationPp.pp_term t'); flush stdout; - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" - | P.Notation (l1, associativity, precedence, l2) -> - print_endline "Extending parser ..."; flush stdout; + prerr_endline (CicNotationPp.pp_term t'); flush stdout; + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | P.Notation (l1, associativity, precedence, l2) -> + prerr_endline "Extending parser ..."; flush stdout; + prerr_endline (CicNotationPp.pp_term l1) ; let time1 = Unix.gettimeofday () in - ignore - (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); - let time2 = Unix.gettimeofday () in - print_endline "Extending pretty printer ..."; flush stdout; - let time3 = Unix.gettimeofday () in - ignore - (CicNotationRew.add_pretty_printer ?precedence ?associativity - l2 l1); - let time4 = Unix.gettimeofday () in - printf "done (extending parser took %f, extending pretty printer took %f)\n" - (time2 -. time1) (time4 -. time3); - flush stdout - | P.Interpretation (l2, l3) -> - print_endline "Adding interpretation ..."; flush stdout; + ignore + (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); + let time2 = Unix.gettimeofday () in + prerr_endline "Extending pretty printer ..."; flush stdout; + let time3 = Unix.gettimeofday () in + ignore + (CicNotationRew.add_pretty_printer ?precedence ?associativity + l2 l1); + let time4 = Unix.gettimeofday () in + printf "done (extending parser took %f, extending pretty printer took %f)\n" + (time2 -. time1) (time4 -. time3); + flush stdout + | P.Interpretation (l2, l3) -> + prerr_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation l2 l3); - let time2 = Unix.gettimeofday () in - printf "done (patterns compilation took %f seconds)\n" - (time2 -. time1); - flush stdout - | P.Render uri -> + ignore (CicNotationRew.add_interpretation l2 l3); + let time2 = Unix.gettimeofday () in + printf "done (patterns compilation took %f seconds)\n" + (time2 -. time1); + flush stdout + | P.Render uri -> let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let annobj, _, _, id_to_sort, _, _, _ = Cic2acic.acic_object_of_cic_object obj in let annterm = match annobj with - | Cic.AConstant (_, _, _, _, ty, _, _) - | Cic.AVariable (_, _, _, ty, _, _) -> ty - | _ -> assert false + | Cic.AConstant (_, _, _, _, ty, _, _) + | Cic.AVariable (_, _, _, ty, _, _) -> ty + | _ -> assert false in let time1 = Unix.gettimeofday () in let t, id_to_uri = CicNotationRew.ast_of_acic id_to_sort annterm in let time2 = Unix.gettimeofday () in - prerr_endline (sprintf "ast creation took %f seconds\n" (time2 -. time1)); - prerr_endline "AST"; - prerr_endline (CicNotationPp.pp_term t); - flush stdout; - let time3 = Unix.gettimeofday () in - let t' = CicNotationRew.pp_ast t in - let time4 = Unix.gettimeofday () in - prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3)); - prerr_endline (CicNotationPp.pp_term t'); - dump_xml t' id_to_uri "out.xml") -(* 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) = 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 - eprintf "%s%s%s\n" before error after; - prerr_endline (sprintf "at character %d-%d: %s" x y msg) - done - with End_of_file -> - close_in ic - + prerr_endline (sprintf "ast creation took %f seconds\n" (time2 -. time1)); + prerr_endline "AST"; + prerr_endline (CicNotationPp.pp_term t); + flush stdout; + let time3 = Unix.gettimeofday () in + let t' = CicNotationRew.pp_ast t in + let time4 = Unix.gettimeofday () in + prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3)); + prerr_endline (CicNotationPp.pp_term t'); + dump_xml t' id_to_uri "out.xml" +(* CicNotationParser.print_l2_pattern () *) + (* 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 *) + (* eprintf "%s%s%s\n" before error after; *) + (* prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) + done + with End_of_file -> + ()