X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=09fd55b0d4bae7c890c6eb98599fbf6d3e9aa034;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=7186ccf149a556817bd213250127f9fd1dcaac36;hpb=7433c53083f5e6f28ce02c7ad53d26f064f31a5c;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 7186ccf14..09fd55b0d 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -26,12 +26,14 @@ open Printf exception Parse_error of Token.flocation * string +exception Level_not_found of int 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 *) @@ -72,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 ] ]; @@ -110,7 +113,7 @@ EXTEND return_term loc (Layout (Above (p1, p2))) | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern; SYMBOL "]" -> - return_term loc (Layout (Frac (boxify p1, boxify p2))) + 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))) @@ -127,7 +130,7 @@ EXTEND return_term loc (Layout (Box (V, p))) | SYMBOL "\\BREAK" -> return_term loc (Layout Break) | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> - return_term loc (Layout (Box (H, p))) + return_term loc (boxify p) | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" -> return_term loc (Variable (Ascription (Layout (Box (H, p)), id))) ] @@ -139,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 @@ -243,7 +246,8 @@ EXTEND ] ]; l2_pattern: - [ "letin" NONA + [ "0" [ ] + | "10" NONA (* let in *) [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = l2_pattern; "in"; p2 = l2_pattern -> return_term loc (LetIn (var, p1, p2)) @@ -251,13 +255,15 @@ EXTEND body = l2_pattern -> return_term loc (LetRec (k, defs, body)) ] - | "binder" RIGHTA + | "20" RIGHTA (* binder *) [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern -> return_term loc (fold_binder b names body) ] - | "extension" - [ ] - | "apply" LEFTA + | "30" [ ] + | "40" [ ] + | "50" [ ] + | "60" [ ] + | "70" LEFTA (* apply *) [ p1 = l2_pattern; p2 = l2_pattern -> let rec aux = function | Appl (hd :: tl) @@ -267,16 +273,16 @@ EXTEND in return_term loc (Appl (aux p1 @ [p2])) ] - | "simple" NONA + | "80" [ ] + | "90" NONA (* simple *) [ 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 ]; @@ -294,6 +300,7 @@ 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 *) @@ -355,4 +362,184 @@ 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 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 + [] -> + 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 [] (List.rev bindings) + +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) -> + 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))) + 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 (* TODO *) + | FreshVar _ -> assert false + 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 + +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: *)