From: Stefano Zacchiroli Date: Wed, 25 May 2005 14:32:40 +0000 (+0000) Subject: snapshot (first version in which some extensions work, e.g. infix +) X-Git-Tag: single_binding~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aca103d3c3d740efcc0bcc2932922cff77facb49;p=helm.git snapshot (first version in which some extensions work, e.g. infix +) ueeeeeehh! --- diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index bd42ea9cb..69b51c398 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -24,9 +24,9 @@ *) oopen Printf -eexception Parse_error of Token.flocation * string +eexception Parse_error of Token.flocation * stringeexception Level_not_found of int llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer -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 notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *) +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 return_term loc term = () @@ -57,6 +57,7 @@ Elet _ = (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 let grammar_entry_create s = @@ -92,8 +93,6 @@ Elet _ = grammar_entry_create "l2_pattern_variable" and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e = grammar_entry_create "l2_magic_pattern" - and l2_pattern : 'l2_pattern Grammar.Entry.e = - grammar_entry_create "l2_pattern" and argument : 'argument Grammar.Entry.e = grammar_entry_create "argument" and associativity : 'associativity Grammar.Entry.e = @@ -217,7 +216,7 @@ Elet _ = Gramext.action (fun _ (p : 'l1_pattern) _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern)); + (return_term loc (boxify p) : 'l1_simple_pattern)); [Gramext.Stoken ("SYMBOL", "\\BREAK")], Gramext.action (fun _ (loc : Lexing.position * Lexing.position) -> @@ -279,7 +278,7 @@ Elet _ = Gramext.action (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _ (loc : Lexing.position * Lexing.position) -> - (return_term loc (Layout (Frac (boxify p1, boxify p2))) : + (return_term loc (Layout (Over (boxify p1, boxify p2))) : 'l1_simple_pattern)); [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself], Gramext.action @@ -571,7 +570,8 @@ Elet _ = (kind : 'e__7) _ (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 "letin", Some Gramext.NonA, + [Some "0", None, []; + Some "10", Some Gramext.NonA, [[Gramext.Stoken ("IDENT", "let"); Gramext.Snterm (Grammar.Entry.obj @@ -594,7 +594,7 @@ Elet _ = (var : 'possibly_typed_name) _ (loc : Lexing.position * Lexing.position) -> (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]; - Some "binder", Some Gramext.RightA, + Some "20", Some Gramext.RightA, [[Gramext.Snterm (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e)); Gramext.Snterm @@ -604,8 +604,9 @@ Elet _ = (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 "extension", None, []; - Some "apply", Some Gramext.LeftA, + Some "30", None, []; Some "40", None, []; Some "50", None, []; + Some "60", None, []; + Some "70", Some Gramext.LeftA, [[Gramext.Sself; Gramext.Sself], Gramext.action (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern) @@ -618,7 +619,8 @@ Elet _ = in return_term loc (Appl (aux p1 @ [p2])) : 'l2_pattern))]; - Some "simple", Some Gramext.NonA, + Some "80", None, []; + Some "90", Some Gramext.NonA, [[Gramext.Snterm (Grammar.Entry.obj (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))], @@ -714,7 +716,8 @@ Elet _ = [Gramext.Stoken ("NUMBER", "")], Gramext.action (fun (n : string) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Num (n, 0)) : 'l2_pattern)); + (prerr_endline "number"; return_term loc (Num (n, 0)) : + 'l2_pattern)); [Gramext.Stoken ("URI", "")], Gramext.action (fun (u : string) (loc : Lexing.position * Lexing.position) -> @@ -730,7 +733,8 @@ Elet _ = [Gramext.Stoken ("IDENT", "")], Gramext.action (fun (id : string) (loc : Lexing.position * Lexing.position) -> - (return_term loc (Ident (id, None)) : 'l2_pattern))]]; + (return_term loc (Ident (id, None)) : 'l2_pattern))]; + Some "100", None, []]; Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None, [None, None, [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", ""); @@ -846,4 +850,150 @@ let parse_ast_pattern stream = let parse_interpretation stream = exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term 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 + +let print_l2_pattern () = + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern); + Format.pp_print_flush Format.std_formatter (); + flush stdout + (* vim:set encoding=utf8 foldmethod=marker: *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index b0529dd7a..09fd55b0d 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -33,6 +33,7 @@ let grammar = Grammar.gcreate CicNotationLexer.notation_lexer 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 *) @@ -73,6 +74,7 @@ let return_term loc term = AttributedTerm (`Loc loc, term) EXTEND GLOBAL: level1_pattern level2_pattern level3_term + l2_pattern notation interpretation; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ]; @@ -140,7 +142,7 @@ EXTEND ]; (* }}} *) (* {{{ Grammar for ast patterns, notation level 2 *) - level2_pattern: [ [ p = l2_pattern -> p ] ]; + level2_pattern: [ [ p = l2_pattern; EOI -> p ] ]; sort: [ [ SYMBOL "\\PROP" -> `Prop | SYMBOL "\\SET" -> `Set @@ -276,12 +278,11 @@ EXTEND [ 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 -> return_term loc (Num (n, 0)) + | 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)) | s = sort -> return_term loc (Sort s) - | s = SYMBOL -> return_term loc (Symbol (s, 0)) | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ]; IDENT "match"; t = l2_pattern; indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; @@ -372,18 +373,66 @@ let term = Gramext.Sself type env_type = (string * (value_type * value)) list -let make_action action = +let rec pp_value = + function + | 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 - [] -> Gramext.action (fun (loc: location) -> action vl loc) - | None :: tl -> Gramext.action (fun _ -> aux vl tl) - | Some (name, typ) :: tl -> - (* i tipi servono? Magari servono solo quando si verifica la - * correttezza della notazione? - *) - Gramext.action (fun (v: value) -> aux ((name, (typ, v))::vl) tl) + [] -> + prerr_endline "aux: make_action"; + Gramext.action (fun (loc: location) -> action vl loc) + | None :: tl -> + prerr_endline "aux: none"; + Gramext.action (fun _ -> aux vl tl) + (* LUCA: DEFCON 3 BEGIN *) + | Some (name, TermType) :: tl -> + prerr_endline "aux: term"; + Gramext.action + (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl) + | Some (name, StringType) :: tl -> + prerr_endline "aux: string"; + Gramext.action + (fun (v:string) -> + aux ((name, (StringType, (StringValue v))) :: vl) tl) + | Some (name, NumType) :: tl -> + prerr_endline "aux: num"; + Gramext.action + (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl) + | Some (name, OptType t) :: tl -> + prerr_endline "aux: opt"; + Gramext.action + (fun (v:'a option) -> + aux ((name, (OptType t, (OptValue v))) :: vl) tl) + | Some (name, ListType t) :: tl -> + prerr_endline "aux: list"; + Gramext.action + (fun (v:'a list) -> + aux ((name, (ListType t, (ListValue v))) :: vl) tl) + (* LUCA: DEFCON 3 END *) in - aux [] + aux [] (List.rev bindings) let flatten_opt = let rec aux acc = @@ -429,17 +478,21 @@ let extract_term_production pattern = (Gramext.srules [ p_atoms, (make_action - (fun (env : env_type) (loc : location) -> env) + (fun (env : env_type) (loc : location) -> + prerr_endline "inner opt action"; + env) p_bindings)])], Gramext.action (fun (env_opt : env_type option) (loc : location) -> match env_opt with Some env -> + prerr_endline "opt action (Some _)"; List.map (fun (name, (typ, v)) -> (name, (OptType typ, OptValue (Some v)))) env | None -> + prerr_endline "opt action (None)"; List.map (fun (name, typ) -> (name, (OptType typ, OptValue None))) @@ -460,7 +513,7 @@ let level_of_int precedence = raise (Level_not_found precedence); string_of_int precedence -type rule_id = term Grammar.Entry.e * Token.t Gramext.g_symbol list +type rule_id = Token.t Gramext.g_symbol list let extend level1_pattern ?(precedence = 0) ?associativity action = let p_bindings, p_atoms = @@ -468,23 +521,25 @@ let extend level1_pattern ?(precedence = 0) ?associativity action = in let level = level_of_int precedence in let p_names = flatten_opt p_bindings in - let entry = Grammar.Entry.obj (level2_pattern: 'a Grammar.Entry.e) 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) -> TermValue (action env loc)) + (fun (env: env_type) (loc: location) -> (action env loc)) p_bindings) ]]] in - (level2_pattern, p_atoms) + p_atoms -let delete (entry, atoms) = Grammar.delete_rule entry atoms +let delete atoms = Grammar.delete_rule l2_pattern atoms -let print_level2_pattern () = - Grammar.print_entry Format.std_formatter (Grammar.Entry.obj level2_pattern); - Format.pp_print_flush Format.std_formatter () +let print_l2_pattern () = + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern); + Format.pp_print_flush Format.std_formatter (); + flush stdout (* vim:set encoding=utf8 foldmethod=marker: *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 1dd81ef9f..32ba0a318 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -54,6 +54,8 @@ val delete: rule_id -> unit (** {2 Debugging} *) +val pp_env: env_type -> string + (** print "level2_pattern" entry on stdout, flushing afterwards *) -val print_level2_pattern: unit -> unit +val print_l2_pattern: unit -> unit diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 99e7371fc..c068491a3 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -31,14 +31,48 @@ let loc_of_floc = function (loc_begin, loc_end) 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; + if !level = 2 then begin + let id = + CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA + (P.Layout (P.Box (P.H, + [ P.Literal (`Symbol "+"); + P.Magic (P.Opt (P.Variable (P.TermVar "ugo"))) ] +(* [ P.Variable (P.TermVar "a"); + P.Literal (`Symbol "+"); + P.Variable (P.TermVar "b"); + ] *) + ))) + (fun env _ -> + begin + prerr_endline "reducing rule" ; + prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env)); +(* match env with + [(x, (_, P.OptValue v))] -> + begin + match v with + Some _ -> Printf.printf "Ugo c'e'? %s\n" x; flush stdout + | None -> prerr_endline "nooooo" + end + | _ -> assert false *) + end ; + P.Sort `Prop) + in + CicNotationParser.print_l2_pattern () + end; let parse_fun s = match !level with | 1 -> ignore (CicNotationParser.parse_syntax_pattern s) - | 2 -> ignore (CicNotationParser.parse_ast_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 @@ -50,7 +84,7 @@ let _ = let istream = Stream.of_string line in try parse_fun istream; - print_endline "ok" + print_endline ">" with CicNotationParser.Parse_error (floc, msg) -> let (x, y) = loc_of_floc floc in let before = String.sub line 0 x in