From: Stefano Zacchiroli Date: Wed, 25 May 2005 09:49:50 +0000 (+0000) Subject: snapshot X-Git-Tag: single_binding~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2e41c32bf536719437749de627c7e034f5852f83;p=helm.git snapshot - implemented first draft of extensible parser ... brrrrrr --- diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index fcf53edd5..9f8a0cb38 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -29,6 +29,8 @@ cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) +cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) +cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) clean: extra_clean distclean: extra_clean @@ -39,12 +41,6 @@ extra_clean: include ../Makefile.common OCAMLARCHIVEOPTIONS += -linkall -disambiguateTypes.cmi: disambiguateTypes.mli - $(OCAMLC) -c -rectypes $< -disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi - $(OCAMLC) -c -rectypes $< -disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi - $(OCAMLOPT) -c -rectypes $< - cicNotationParser.expanded.ml: cicNotationParser.ml camlp4 -nolib '-I' '/usr/lib/ocaml/3.08.3/' '-I' '/home/zack/helm/ocaml/urimanager' '-I' '/usr/lib/ocaml/3.08.3/pcre' '-I' '/usr/lib/ocaml/3.08.3/' '-I' '/usr/lib/ocaml/3.08.3/netstring' '-I' '/usr/lib/ocaml/3.08.3/pxp-engine' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-utf8' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-iso88591' '-I' '/usr/lib/ocaml/3.08.3/pxp-lex-iso885915' '-I' '/usr/lib/ocaml/3.08.3/http' '-I' '/home/zacchiro/helm/ocaml/pxp' '-I' '/usr/lib/ocaml/3.08.3/zip' '-I' '/usr/lib/ocaml/3.08.3/expat' '-I' '/home/zacchiro/helm/ocaml/xml' '-I' '/home/zack/helm/ocaml/cic' '-I' '/usr/lib/ocaml/3.08.3/camlp4' '-I' '/home/zack/helm/ocaml/utf8_macros' '-I' '/usr/lib/ocaml/3.08.3/camlp4' '-I' '/usr/lib/ocaml/3.08.3/ulex' 'pa_o.cmo' 'pa_op.cmo' 'pr_o.cmo' 'pa_extend.cmo' 'pa_unicode_macro.cma' 'pa_ulex.cma' $< > $@ + diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 7186ccf14..b0529dd7a 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -26,6 +26,7 @@ open Printf exception Parse_error of Token.flocation * string +exception Level_not_found of int let grammar = Grammar.gcreate CicNotationLexer.notation_lexer @@ -110,7 +111,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 +128,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))) ] @@ -243,7 +244,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 +253,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,7 +271,8 @@ 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)) @@ -294,6 +299,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 +361,130 @@ 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) = + 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) + 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 (* 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 = term Grammar.Entry.e * 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 (level2_pattern: 'a Grammar.Entry.e) in + let _ = + 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)) + p_bindings) ]]] + in + (level2_pattern, p_atoms) + +let delete (entry, atoms) = Grammar.delete_rule entry atoms + +let print_level2_pattern () = + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj level2_pattern); + Format.pp_print_flush Format.std_formatter () + (* vim:set encoding=utf8 foldmethod=marker: *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 5112f6dbd..1dd81ef9f 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -24,6 +24,7 @@ *) exception Parse_error of Token.flocation * string +exception Level_not_found of int (** {2 Parsing functions} *) @@ -36,3 +37,23 @@ 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} *) + +type env_type = (string * (CicNotationPt.value_type * CicNotationPt.value)) list + +type rule_id + +val extend: + CicNotationPt.term -> + ?precedence:int -> + ?associativity:Gramext.g_assoc -> + (env_type -> CicNotationPt.location -> CicNotationPt.term) -> + rule_id + +val delete: rule_id -> unit + +(** {2 Debugging} *) + + (** print "level2_pattern" entry on stdout, flushing afterwards *) +val print_level2_pattern: unit -> unit + diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 6987937d5..3d6242e96 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -89,8 +89,9 @@ and layout_pattern = | Below of term * term | Above of term * term | Frac of term * term + | Over of term * term | Atop of term * term -(* | Array of term * literal option * literal option +(* | array of term * literal option * literal option |+ column separator, row separator +| *) | Sqrt of term | Root of term * term (* argument, index *) @@ -129,3 +130,19 @@ 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 +