From: Stefano Zacchiroli Date: Mon, 23 May 2005 15:18:20 +0000 (+0000) Subject: snapshot X-Git-Tag: single_binding~23 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7433c53083f5e6f28ce02c7ad53d26f064f31a5c;p=helm.git snapshot --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index e69de29bb..8d107d761 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -0,0 +1,7 @@ +cicNotationParser.cmi: cicNotationPt.cmo +cicNotationLexer.cmo: cicNotationLexer.cmi +cicNotationLexer.cmx: cicNotationLexer.cmi +cicNotationParser.cmo: cicNotationPt.cmo cicNotationLexer.cmi \ + cicNotationParser.cmi +cicNotationParser.cmx: cicNotationPt.cmx cicNotationLexer.cmx \ + cicNotationParser.cmi diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 5c3b09408..6a43c4890 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -1,10 +1,12 @@ PACKAGE = cic_notation -REQUIRES = \ - helm-cic \ - helm-utf8_macros \ - ulex NULL = +REQUIRES = \ + helm-cic \ + helm-utf8_macros \ + camlp4.gramlib \ + ulex \ + $(NULL) INTERFACE_FILES = \ cicNotationLexer.mli \ cicNotationParser.mli \ @@ -16,17 +18,6 @@ IMPLEMENTATION_FILES = \ all: -cicNotationLexer.cmo: cicNotationLexer.ml cicNotationLexer.cmi - $(OCAMLC_P4) -c $< -cicNotationLexer.cmx: cicNotationLexer.ml cicNotationLexer.cmi - $(OCAMLOPT_P4) -c $< -cicNotationParser.cmo: REQUIRES = helm-utf8_macros camlp4.gramlib helm-cic -cicNotationParser.cmo: cicNotationParser.ml cicNotationParser.cmi cicNotationLexer.cmi - $(OCAMLC_P4) -c $< -cicNotationParser.cmx: REQUIRES = helm-utf8_macros camlp4.gramlib -cicNotationParser.cmx: cicNotationParser.ml cicNotationParser.cmi cicNotationLexer.cmi - $(OCAMLOPT_P4) -c $< - LOCAL_LINKOPTS = -package helm-cic_notation -linkpkg test: test_lexer test_parser test_lexer: test_lexer.ml $(PACKAGE).cma @@ -34,6 +25,11 @@ test_lexer: test_lexer.ml $(PACKAGE).cma test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) +cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) +cicNotationLexer.cmx: OCAMLC = $(OCAMLC_P4) +cicNotationParser.cmx: OCAMLC = $(OCAMLC_P4) + clean: extra_clean distclean: extra_clean rm -f macro_table.dump diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 32f0c760f..7186ccf14 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -27,19 +27,14 @@ open Printf exception Parse_error of Token.flocation * string -module NotationLexer = -struct - type te = string * string - let lexer = CicNotationLexer.notation_lexer -end -module NotationGrammar = Grammar.GMake (NotationLexer) +let grammar = Grammar.gcreate CicNotationLexer.notation_lexer -let level1_pattern = NotationGrammar.Entry.create "level1_pattern" -let level2_pattern = NotationGrammar.Entry.create "level2_pattern" -let level3_interpretation = NotationGrammar.Entry.create "level3_interpretation" -let notation = NotationGrammar.Entry.create "notation" (* level1 <-> level 2 *) +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 notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *) let interpretation = - NotationGrammar.Entry.create "interpretation" (* level2 <-> level 3 *) + Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *) let return_term loc term = () @@ -73,11 +68,13 @@ let fold_binder binder pt_names body = (fun (names, ty) body -> fold_cluster binder names ty body) pt_names body -GEXTEND NotationGrammar - GLOBAL: level1_pattern level2_pattern level3_interpretation notation - interpretation; +let return_term loc term = AttributedTerm (`Loc loc, term) + +EXTEND + GLOBAL: level1_pattern level2_pattern level3_term + notation interpretation; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) - level1_pattern: [ [ p = l1_pattern -> boxify p ] ]; + level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ]; l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ]; literal: [ [ s = SYMBOL -> `Symbol s @@ -103,34 +100,41 @@ GEXTEND NotationGrammar ]; l1_simple_pattern: [ "layout" LEFTA - [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> Layout (Sub (p1, p2)) - | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> Layout (Sup (p1, p2)) - | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> Layout (Below (p1, p2)) - | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> Layout (Above (p1, p2)) + [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> + return_term loc (Layout (Sub (p1, p2))) + | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> + return_term loc (Layout (Sup (p1, p2))) + | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> + 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 "]" -> - Layout (Frac (boxify p1, boxify p2)) + return_term loc (Layout (Frac (boxify p1, boxify p2))) | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern; SYMBOL "]" -> - Layout (Atop (boxify p1, boxify p2)) + return_term loc (Layout (Atop (boxify p1, boxify p2))) (* | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep -> - Array (p, csep, rsep) *) - | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> Layout (Frac (p1, p2)) - | SYMBOL "\\SQRT"; p = SELF -> Layout (Sqrt p) + 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 -> - Layout (Root (arg, Layout (Box (H, index)))) + return_term loc (Layout (Root (arg, Layout (Box (H, index))))) | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" -> - Layout (Box (H, p)) + return_term loc (Layout (Box (H, p))) | SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" -> - Layout (Box (V, p)) - | SYMBOL "\\BREAK" -> Layout Break - | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> Layout (Box (H, p)) + 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))) | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" -> - Variable (Ascription (Layout (Box (H, p)), id)) + return_term loc (Variable (Ascription (Layout (Box (H, p)), id))) ] | "simple" NONA - [ m = l1_magic_pattern -> Magic m - | v = l1_pattern_variable -> Variable v + [ 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) ] ]; (* }}} *) @@ -242,35 +246,37 @@ GEXTEND NotationGrammar [ "letin" NONA [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = l2_pattern; "in"; p2 = l2_pattern -> - LetIn (var, p1, p2) + return_term loc (LetIn (var, p1, p2)) | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in"; body = l2_pattern -> - LetRec (k, defs, body) + return_term loc (LetRec (k, defs, body)) ] | "binder" RIGHTA [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern -> - fold_binder b names body + return_term loc (fold_binder b names body) ] | "extension" [ ] | "apply" LEFTA [ p1 = l2_pattern; p2 = l2_pattern -> let rec aux = function - | Appl (hd :: tl) -> aux hd @ tl + | Appl (hd :: tl) + | AttributedTerm (_, Appl (hd :: tl)) -> + aux hd @ tl | term -> [term] in - Appl (aux p1 @ [p2]) + return_term loc (Appl (aux p1 @ [p2])) ] | "simple" NONA - [ id = IDENT -> Ident (id, None) - | id = IDENT; s = explicit_subst -> Ident (id, Some s) - | u = URI -> Uri (u, None) - | n = NUMBER -> Num (n, 0) - | IMPLICIT -> Implicit - | m = META -> Meta (int_of_string m, []) - | m = META; s = meta_subst -> Meta (int_of_string m, s) - | s = sort -> Sort s - | s = SYMBOL -> Symbol (s, 0) + [ 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)) + | 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 ]; @@ -281,27 +287,31 @@ GEXTEND NotationGrammar lhs, rhs ] SEP SYMBOL "|"; SYMBOL "]" -> - Case (t, indty_ident, outtyp, patterns) + return_term loc (Case (t, indty_ident, outtyp, patterns)) | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" -> - Appl [ Symbol ("cast", 0); p1; p2 ] + return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ]) | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p - | v = l2_pattern_variable -> Variable v - | m = l2_magic_pattern -> Magic m + | v = l2_pattern_variable -> return_term loc (Variable v) + | m = l2_magic_pattern -> return_term loc (Magic m) ] ]; (* }}} *) (* {{{ Grammar for interpretation, notation level 3 *) - level3_interpretation: [ [ i = interpretation -> () ] ]; argument: [ - [ i = IDENT -> () - | SYMBOL <:unicode> (* η *); SYMBOL "."; a = SELF -> () - | SYMBOL <:unicode> (* η *); i = IDENT; SYMBOL "."; a = SELF -> () + [ id = IDENT -> IdentArg id + | SYMBOL <:unicode> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a) + | SYMBOL <:unicode> (* η *); id = IDENT; SYMBOL "."; a = SELF -> + EtaArg (Some id, a) ] ]; - l3_term: [ - [ u = URI -> () - | a = argument -> () - | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> () + level3_term: [ + [ u = URI -> UriPattern u + | a = argument -> ArgPattern a + | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> + (match terms with + | [] -> assert false + | [term] -> term + | terms -> ApplPattern terms) ] ]; (* }}} *) @@ -320,7 +330,7 @@ GEXTEND NotationGrammar ]; interpretation: [ [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as"; - t = l3_term -> + t = level3_term -> () ] ]; @@ -337,21 +347,12 @@ let exc_located_wrapper f = raise (Parse_error (floc, (Printexc.to_string exn))) let parse_syntax_pattern stream = - exc_located_wrapper - (fun () -> - (NotationGrammar.Entry.parse level1_pattern - (NotationGrammar.parsable stream))) + exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream) let parse_ast_pattern stream = - exc_located_wrapper - (fun () -> - (NotationGrammar.Entry.parse level2_pattern - (NotationGrammar.parsable stream))) + exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream) let parse_interpretation stream = - exc_located_wrapper - (fun () -> - (NotationGrammar.Entry.parse level3_interpretation - (NotationGrammar.parsable stream))) + exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream) (* vim:set encoding=utf8 foldmethod=marker: *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 1ce20fe9a..5112f6dbd 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -34,5 +34,5 @@ val parse_syntax_pattern: char Stream.t -> CicNotationPt.term val parse_ast_pattern: char Stream.t -> CicNotationPt.term (** interpretation: notation level 3 *) -val parse_interpretation: char Stream.t -> unit +val parse_interpretation: char Stream.t -> CicNotationPt.cic_appl_pattern diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index be082121a..6987937d5 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -71,6 +71,7 @@ type term = (* Syntax pattern extensions *) + | Literal of literal | Layout of layout_pattern | Magic of magic_term | Variable of pattern_variable @@ -119,3 +120,12 @@ and pattern_variable = (* level 2 variables *) | FreshVar of string +type argument_pattern = + | IdentArg of string + | EtaArg of string option * argument_pattern (* eta abstraction *) + +type cic_appl_pattern = + | UriPattern of string + | ArgPattern of argument_pattern + | ApplPattern of cic_appl_pattern list + diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 53ee4f8eb..99e7371fc 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -35,11 +35,11 @@ let _ = 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 parse_fun = + let parse_fun s = match !level with - | 1 -> CicNotationParser.parse_syntax_pattern - | 2 -> CicNotationParser.parse_ast_pattern - | 3 -> CicNotationParser.parse_interpretation + | 1 -> ignore (CicNotationParser.parse_syntax_pattern s) + | 2 -> ignore (CicNotationParser.parse_ast_pattern s) + | 3 -> ignore (CicNotationParser.parse_interpretation s) | _ -> Arg.usage arg_spec usage; exit 1 in let ic = stdin in @@ -49,7 +49,7 @@ let _ = let line = input_line ic in let istream = Stream.of_string line in try - let _ = parse_fun istream in + parse_fun istream; print_endline "ok" with CicNotationParser.Parse_error (floc, msg) -> let (x, y) = loc_of_floc floc in