From a205eb4442d5b7a0a072a05bdfc525b8b9713c4e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 May 2005 13:07:32 +0000 Subject: [PATCH] snapshot - added parse tree for all levels - implemented parse tree construction for level 1 and 2 --- helm/ocaml/cic_notation/Makefile | 4 +- helm/ocaml/cic_notation/cicNotationParser.ml | 262 ++++++++++++------ helm/ocaml/cic_notation/cicNotationParser.mli | 4 +- helm/ocaml/cic_notation/cicNotationPt.ml | 121 ++++++++ 4 files changed, 296 insertions(+), 95 deletions(-) create mode 100644 helm/ocaml/cic_notation/cicNotationPt.ml diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 9fa417ef5..5c3b09408 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -1,6 +1,7 @@ PACKAGE = cic_notation REQUIRES = \ + helm-cic \ helm-utf8_macros \ ulex NULL = @@ -9,6 +10,7 @@ INTERFACE_FILES = \ cicNotationParser.mli \ $(NULL) IMPLEMENTATION_FILES = \ + cicNotationPt.ml \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(NULL) @@ -18,7 +20,7 @@ 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 +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 diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 08bac32f5..32f0c760f 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -37,12 +37,19 @@ module NotationGrammar = Grammar.GMake (NotationLexer) 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 interpretation = + NotationGrammar.Entry.create "interpretation" (* level2 <-> level 3 *) let return_term loc term = () -(*let fail floc msg =*) -(* let (x, y) = CicAst.loc_of_floc floc in*) -(* failwith (sprintf "Error at characters %d - %d: %s" x y msg)*) +let loc_of_floc = function + | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> + (loc_begin, loc_end) + +let fail floc msg = + let (x, y) = loc_of_floc floc in + failwith (sprintf "Error at characters %d - %d: %s" x y msg) let int_of_string s = try @@ -50,70 +57,89 @@ let int_of_string s = with Failure _ -> failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) +open CicNotationPt + +let boxify = function + | [ a ] -> a + | l -> Layout (Box (H, l)) + +let fold_binder binder pt_names body = + let fold_cluster binder names ty body = + List.fold_right + (fun name body -> Binder (binder, (Cic.Name name, ty), body)) + names body + in + List.fold_right + (fun (names, ty) body -> fold_cluster binder names ty body) + pt_names body + GEXTEND NotationGrammar - GLOBAL: level1_pattern level2_pattern level3_interpretation; + GLOBAL: level1_pattern level2_pattern level3_interpretation notation + interpretation; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) - level1_pattern: [ [ p = l1_pattern -> () ] ]; - l1_pattern: [ [ p = LIST1 l1_simple_pattern -> () ] ]; + level1_pattern: [ [ p = l1_pattern -> boxify p ] ]; + l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ]; literal: [ - [ s = SYMBOL -> () - | k = KEYWORD -> () - ] - ]; - sep: [ [ SYMBOL "\\SEP"; sep = literal -> () ] ]; - row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> () ] ]; - field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ]; - l1_box_pattern: [ - [ SYMBOL "\\HBOX"; p = l1_simple_pattern -> () - | SYMBOL "\\VBOX"; p = l1_simple_pattern -> () - | SYMBOL "\\BREAK" -> () + [ s = SYMBOL -> `Symbol s + | k = KEYWORD -> `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 ] ]; *) l1_magic_pattern: [ - [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> () - | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> () - | SYMBOL "\\OPT"; p = l1_simple_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 ] ]; l1_pattern_variable: [ - [ id = IDENT -> () - | SYMBOL "\\NUM"; id = IDENT -> () - | SYMBOL "\\IDENT"; id = IDENT -> () + [ id = IDENT -> TermVar id + | SYMBOL "\\TERM"; id = IDENT -> TermVar id + | SYMBOL "\\NUM"; id = IDENT -> NumVar id + | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id ] ]; l1_simple_pattern: [ "layout" LEFTA - [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> () - | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> () - | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> () - | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> () + [ 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)) | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern; SYMBOL "]" -> - () + Layout (Frac (boxify p1, boxify p2)) | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern; SYMBOL "]" -> - () - | SYMBOL "\\ARRAY"; p = SELF; fsep = OPT field_sep; rsep = OPT row_sep -> - () - | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> () - | SYMBOL "\\SQRT"; p = SELF -> () - | SYMBOL "\\ROOT"; arg = l1_pattern; SYMBOL "\\OF"; index = SELF -> () + 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) + | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF -> + Layout (Root (arg, Layout (Box (H, index)))) + | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" -> + 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)) + | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" -> + Variable (Ascription (Layout (Box (H, p)), id)) ] | "simple" NONA - [ m = l1_magic_pattern -> () - | v = l1_pattern_variable -> () - | b = l1_box_pattern -> () - | n = NUMBER -> () - | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> () + [ m = l1_magic_pattern -> Magic m + | v = l1_pattern_variable -> Variable v ] ]; (* }}} *) (* {{{ Grammar for ast patterns, notation level 2 *) - level2_pattern: [ [ p = l2_pattern -> () ] ]; + level2_pattern: [ [ p = l2_pattern -> p ] ]; sort: [ - [ SYMBOL "\\PROP" -> () - | SYMBOL "\\SET" -> () - | SYMBOL "\\TYPE" -> () + [ SYMBOL "\\PROP" -> `Prop + | SYMBOL "\\SET" -> `Set + | SYMBOL "\\TYPE" -> `Type ] ]; explicit_subst: [ @@ -125,104 +151,142 @@ GEXTEND NotationGrammar ] ]; possibly_typed_name: [ - [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" -> () - | i = IDENT -> () + [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" -> + Cic.Name id, Some typ + | id = IDENT -> Cic.Name id, None ] ]; match_pattern: [ - [ n = IDENT -> () - | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" -> - () + [ id = IDENT -> id, [] + | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" -> + id, vars ] ]; binder: [ - [ SYMBOL <:unicode> (* Π *) -> () - | SYMBOL <:unicode> (* ∃ *) -> () - | SYMBOL <:unicode> (* ∀ *) -> () - | SYMBOL <:unicode> (* λ *) -> () + [ SYMBOL <:unicode> (* Π *) -> `Pi + | SYMBOL <:unicode> (* ∃ *) -> `Exists + | SYMBOL <:unicode> (* ∀ *) -> `Forall + | SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; bound_names: [ [ vars = LIST1 IDENT SEP SYMBOL ","; - typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ] -> () - | LIST1 [ - SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ","; - typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ]; SYMBOL ")" -> () + ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] -> + [ vars, ty ] + | clusters = LIST1 [ + SYMBOL "("; + vars = LIST1 IDENT SEP SYMBOL ","; + ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ]; + SYMBOL ")" -> + vars, ty ] -> - () + clusters ] ]; induction_kind: [ - [ IDENT "rec" -> () - | IDENT "corec" -> () + [ IDENT "rec" -> `Inductive + | IDENT "corec" -> `CoInductive ] ]; let_defs: [ [ defs = LIST1 [ name = IDENT; args = bound_names; - index_name = OPT [ IDENT "on"; idx = IDENT -> () ]; - ty = OPT [ SYMBOL ":" ; p = l2_pattern -> () ]; + index_name = OPT [ IDENT "on"; id = IDENT -> id ]; + ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ]; SYMBOL <:unicode> (* ≝ *); body = l2_pattern -> - () + let body = fold_binder `Lambda args body in + let ty = + match ty with + | None -> None + | Some ty -> Some (fold_binder `Pi args ty) + in + let rec position_of name p = function + | [] -> None, p + | n :: _ when n = name -> Some p, p + | _ :: tl -> position_of name (p + 1) tl + in + let rec find_arg name n = function + | [] -> fail loc (sprintf "Argument %s not found" name) + | (l,_) :: tl -> + (match position_of name 0 l with + | None, len -> find_arg name (n + len) tl + | Some where, len -> n + where) + in + let index = + match index_name with + | None -> 0 + | Some name -> find_arg name 0 args + in + (Cic.Name name, ty), body, index ] SEP IDENT "and" -> - () + defs ] ]; l2_pattern_variable: [ - [ SYMBOL "\\NUM"; id = IDENT -> () - | SYMBOL "\\IDENT"; id = IDENT -> () - | SYMBOL "\\FRESH"; id = IDENT -> () + [ SYMBOL "\\NUM"; id = IDENT -> NumVar id + | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id + | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id ] ]; l2_magic_pattern: [ - [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ]; - LIST1 IDENT; SYMBOL "."; p1 = l2_pattern; - OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = l2_pattern -> - () - | SYMBOL "\\DEFAULT"; id = IDENT; p1 = l2_pattern; p2 = l2_pattern -> () + [ SYMBOL "\\FOLD"; + kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ]; + base = l2_pattern; + SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern -> + Fold (kind, base, [id], recursive) + | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern -> + Default (some, none) ] ]; l2_pattern: [ "letin" NONA [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = l2_pattern; "in"; p2 = l2_pattern -> - () + LetIn (var, p1, p2) | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in"; body = l2_pattern -> - () + LetRec (k, defs, body) ] | "binder" RIGHTA - [ b = binder; bound_names; SYMBOL "."; body = l2_pattern -> () ] + [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern -> + fold_binder b names body + ] | "extension" [ ] | "apply" LEFTA - [ p1 = l2_pattern; p2 = l2_pattern -> () ] + [ p1 = l2_pattern; p2 = l2_pattern -> + let rec aux = function + | Appl (hd :: tl) -> aux hd @ tl + | term -> [term] + in + Appl (aux p1 @ [p2]) + ] | "simple" NONA - [ i = IDENT -> () - | i = IDENT; s = explicit_subst -> () - | n = NUMBER -> () - | IMPLICIT -> () - | m = META -> () - | m = META; s = meta_subst -> () - | s = sort -> () - | s = SYMBOL -> () - | u = URI -> () - | outtyp = OPT [ SYMBOL "["; typ = l2_pattern; SYMBOL "]" ]; + [ 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) + | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ]; IDENT "match"; t = l2_pattern; - indty_ident = OPT [ SYMBOL ":"; id = IDENT ]; + indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; IDENT "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); rhs = l2_pattern -> - () + lhs, rhs ] SEP SYMBOL "|"; SYMBOL "]" -> - () + Case (t, indty_ident, outtyp, patterns) | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" -> - () - | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> () - | v = l2_pattern_variable -> () - | m = l2_magic_pattern -> () + Appl [ Symbol ("cast", 0); p1; p2 ] + | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p + | v = l2_pattern_variable -> Variable v + | m = l2_magic_pattern -> Magic m ] ]; (* }}} *) @@ -240,6 +304,20 @@ GEXTEND NotationGrammar | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> () ] ]; +(* }}} *) +(* {{{ Notation glues *) + associativity: [ + [ IDENT "left"; IDENT "associative" -> `Left + | IDENT "right"; IDENT "associative" -> `Right + ] + ]; + precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ]; + notation: [ + [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern; + assoc = OPT associativity; prec = OPT precedence -> + () + ] + ]; interpretation: [ [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as"; t = l3_term -> diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 669c8336c..1ce20fe9a 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -28,10 +28,10 @@ exception Parse_error of Token.flocation * string (** {2 Parsing functions} *) (** concrete syntax pattern: notation level 1 *) -val parse_syntax_pattern: char Stream.t -> unit +val parse_syntax_pattern: char Stream.t -> CicNotationPt.term (** AST pattern: notation level 2 *) -val parse_ast_pattern: char Stream.t -> unit +val parse_ast_pattern: char Stream.t -> CicNotationPt.term (** interpretation: notation level 3 *) val parse_interpretation: char Stream.t -> unit diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml new file mode 100644 index 000000000..be082121a --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -0,0 +1,121 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** CIC Notation Parse Tree *) + +type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] +type induction_kind = [ `Inductive | `CoInductive ] +type sort_kind = [ `Prop | `Set | `Type | `CProp ] +type fold_kind = [ `Left | `Right ] + +type location = Lexing.position * Lexing.position + +type term_attribute = + [ `Loc of location (* source file location *) + | `IdRef of string (* ACic pointer *) + ] + +type literal = + [ `Symbol of string + | `Keyword of string + | `Number of string + ] + +type term = + (* CIC AST *) + + | AttributedTerm of term_attribute * term + + | Appl of term list + | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Case of term * string option * term option * (case_pattern * term) list + (* what to match, inductive type, out type, list *) + | LetIn of capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (capture_variable * term * int) list * term + (* (name, body, decreasing argument) list, where *) + | Ident of string * subst list option + (* literal, substitutions. + * Some [] -> user has given an empty explicit substitution list + * None -> user has given no explicit substitution list *) + | Implicit + | Meta of int * meta_subst list + | Num of string * int (* literal, instance *) + | Sort of sort_kind + | Symbol of string * int (* canonical name, instance *) + + | UserInput (* place holder for user input, used by MatitaConsole, not to be + used elsewhere *) + | Uri of string * subst list option (* as Ident, for long names *) + + (* Syntax pattern extensions *) + + | Layout of layout_pattern + | Magic of magic_term + | Variable of pattern_variable + +and capture_variable = Cic.name * term option (* name, type *) +and meta_subst = term option +and subst = string * term +and case_pattern = string * capture_variable list + +and box_kind = H | V + +and layout_pattern = + | Sub of term * term + | Sup of term * term + | Below of term * term + | Above of term * term + | Frac of term * term + | Atop of term * term +(* | Array of term * literal option * literal option + |+ column separator, row separator +| *) + | Sqrt of term + | Root of term * term (* argument, index *) + | Break + | Box of box_kind * term list + +and magic_term = + (* level 1 magics *) + | List0 of term * literal option + | List1 of term * literal option + | Opt of term + + (* level 2 magics *) + | 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 *) + +and pattern_variable = + (* level 1 and 2 variables *) + | NumVar of string + | IdentVar of string + | TermVar of string + + (* level 1 variables *) + | Ascription of term * string + + (* level 2 variables *) + | FreshVar of string + -- 2.39.2