From cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 18 Jul 2005 16:27:25 +0000 Subject: [PATCH] - synced notation pretty printing with parsing syntax - added pretty printing of notation patterns via `Raw attribute --- helm/ocaml/cic_notation/.depend | 6 +- helm/ocaml/cic_notation/cicNotationLexer.ml | 4 +- helm/ocaml/cic_notation/cicNotationParser.ml | 1 + helm/ocaml/cic_notation/cicNotationPp.ml | 169 ++++++++++--------- helm/ocaml/cic_notation/cicNotationPres.ml | 3 +- helm/ocaml/cic_notation/cicNotationPt.ml | 3 + helm/ocaml/cic_notation/cicNotationUtil.ml | 4 + helm/ocaml/cic_notation/grafiteAst.ml | 6 +- helm/ocaml/cic_notation/grafiteAstPp.ml | 54 +++++- helm/ocaml/cic_notation/grafiteParser.ml | 15 +- helm/ocaml/cic_notation/test_parser.conf.xml | 2 +- helm/ocaml/cic_notation/test_parser.ml | 1 + 12 files changed, 173 insertions(+), 95 deletions(-) diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index c08c2bf91..27f186e2f 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -22,8 +22,10 @@ cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -grafiteAstPp.cmo: grafiteAst.cmo cicNotationPp.cmi grafiteAstPp.cmi -grafiteAstPp.cmx: grafiteAst.cmx cicNotationPp.cmx grafiteAstPp.cmi +grafiteAstPp.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationPp.cmi \ + grafiteAstPp.cmi +grafiteAstPp.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationPp.cmx \ + grafiteAstPp.cmi cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \ cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \ cicNotationMatcher.cmi diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 9897412b9..3dc82ae42 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -94,8 +94,8 @@ let _ = (* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to * be reviewed *) List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) - [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; "with"; - "in"; "and"; "to"; "as"; "on"; "names" ] + [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; + "with"; "in"; "and"; "to"; "as"; "on"; "names" ] let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index c9a5fbafb..041010649 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -396,6 +396,7 @@ EXTEND [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type + | "CProp" -> `CProp ] ]; explicit_subst: [ diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index f98b51067..3118753f6 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -36,69 +36,82 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -let pp_literal = function +(* let pp_literal = function (* debugging version *) | `Symbol s -> sprintf "symbol(%s)" s | `Keyword s -> sprintf "keyword(%s)" s - | `Number s -> sprintf "number(%s)" s - -let rec pp_term = function - | AttributedTerm (`Href _, term) when print_attributes -> - sprintf "#[%s]" (pp_term term) - | AttributedTerm (_, term) when print_attributes -> - sprintf "@[%s]" (pp_term term) - | AttributedTerm (_, term) -> pp_term term - - | Appl terms -> - sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | Binder (`Forall, (Ident ("_", None), typ), body) - | Binder (`Pi, (Ident ("_", None), typ), body) -> - sprintf "(%s \\to %s)" - (match typ with None -> "?" | Some typ -> pp_term typ) - (pp_term body) - | Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) - | Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" - (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) - (pp_term term) (pp_patterns patterns) - | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) - | LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) - | LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " - (List.map - (fun (var, body, _) -> - sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) - definitions)) - (pp_term term) - | Ident (name, Some []) | Ident (name, None) - | Uri (name, Some []) | Uri (name, None) -> - name - | Ident (name, Some substs) - | Uri (name, Some substs) -> - sprintf "%s \\subst [%s]" name (pp_substs substs) - | Implicit -> "?" - | Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Num (num, _) -> num - | Sort `Set -> "Set" - | Sort `Prop -> "Prop" - | Sort `Type -> "Type" - | Sort `CProp -> "CProp" - | Symbol (name, _) -> name - - | UserInput -> "" - - | Literal l -> pp_literal l - | Layout l -> pp_layout l - | Magic m -> pp_magic m - | Variable v -> pp_variable v + | `Number s -> sprintf "number(%s)" s *) + +let pp_literal = function + | `Symbol s + | `Keyword s + | `Number s -> s + +let rec pp_term ?(pp_parens = true) t = + let t_pp = + match t with +(* | AttributedTerm (`Href _, term) when print_attributes -> + sprintf "#[%s]" (pp_term term) + | AttributedTerm (_, term) when print_attributes -> + sprintf "@[%s]" (pp_term term) *) + | AttributedTerm (`Raw (text, None), _) -> text + | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text + | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text + | AttributedTerm (_, term) -> pp_term ~pp_parens:false term + + | Appl terms -> + sprintf "%s" (String.concat " " (List.map pp_term terms)) + | Binder (`Forall, (Ident ("_", None), typ), body) + | Binder (`Pi, (Ident ("_", None), typ), body) -> + sprintf "%s \\to %s" + (match typ with None -> "?" | Some typ -> pp_term typ) + (pp_term body) + | Binder (kind, var, body) -> + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) + (pp_term body) + | Case (term, indtype, typ, patterns) -> + sprintf "%smatch %s with %s" + (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) + (pp_term term) (pp_patterns patterns) + | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) + | LetIn (var, t1, t2) -> + sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) + (pp_term t2) + | LetRec (kind, definitions, term) -> + sprintf "let %s %s in %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (String.concat " and " + (List.map + (fun (var, body, _) -> + sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) + definitions)) + (pp_term term) + | Ident (name, Some []) | Ident (name, None) + | Uri (name, Some []) | Uri (name, None) -> + name + | Ident (name, Some substs) + | Uri (name, Some substs) -> + sprintf "%s \\subst [%s]" name (pp_substs substs) + | Implicit -> "?" + | Meta (index, substs) -> + sprintf "%d[%s]" index + (String.concat "; " + (List.map (function None -> "_" | Some t -> pp_term t) substs)) + | Num (num, _) -> num + | Sort `Set -> "Set" + | Sort `Prop -> "Prop" + | Sort `Type -> "Type" + | Sort `CProp -> "CProp" + | Symbol (name, _) -> name + + | UserInput -> "" + + | Literal l -> pp_literal l + | Layout l -> pp_layout l + | Magic m -> pp_magic m + | Variable v -> pp_variable v + in + if pp_parens then sprintf "(%s)" t_pp + else t_pp and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) @@ -146,21 +159,19 @@ and pp_layout = function sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) and pp_magic = function - | List0 (t, sep_opt) -> - sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | List1 (t, sep_opt) -> - sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | Opt t -> sprintf "\\OPT %s" (pp_term t) - | Fold (k, p_base, names, p_rec) -> + | List0 (t, sep_opt) -> sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | List1 (t, sep_opt) -> sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Opt t -> sprintf "opt %s" (pp_term t) + | Fold (kind, p_base, names, p_rec) -> let acc = match names with acc :: _ -> acc | _ -> assert false in - sprintf "\\FOLD %s \\[%s\\] \\LAMBDA %s \\[%s\\]" - (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec) + sprintf "fold %s %s rec %s %s" + (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec) | Default (p_some, p_none) -> - sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none) + sprintf "default %s %s" (pp_term p_some) (pp_term p_none) | If (p_test, p_true, p_false) -> - sprintf "\\IF \\[%s\\] \\[%s\\] \\[%s\\]" + sprintf "if %s then %s else %s" (pp_term p_test) (pp_term p_true) (pp_term p_false) - | Fail -> "\\FAIL" + | Fail -> "fail" and pp_fold_kind = function | `Left -> "left" @@ -168,14 +179,16 @@ and pp_fold_kind = function and pp_sep_opt = function | None -> "" - | Some sep -> sprintf "\\SEP %s" (pp_literal sep) + | Some sep -> sprintf " sep %s" (pp_literal sep) and pp_variable = function - | NumVar s -> "\\NUM " ^ s - | IdentVar s -> "\\IDENT " ^ s - | TermVar s -> "\\TERM " ^ s - | Ascription (t, n) -> sprintf "[%s \\AS %s]" (pp_term t) n - | FreshVar n -> "\\FRESH " ^ n + | NumVar s -> "number " ^ s + | IdentVar s -> "ident " ^ s + | TermVar s -> "term " ^ s + | Ascription (t, n) -> assert false + | FreshVar n -> "fresh " ^ n + +let pp_term t = pp_term ~pp_parens:false t let rec pp_value = function | TermValue t -> sprintf "$%s$" (pp_term t) diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index c6b006f42..395cab6c2 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -208,7 +208,8 @@ let render ids_to_uris = assert false and aux_attribute xmlattrs mathonly xref pos prec uris t = function - | `Loc _ -> aux xmlattrs mathonly xref pos prec uris t + | `Loc _ + | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t | `Level (child_prec, child_assoc) -> let t' = aux xmlattrs mathonly xref pos child_prec uris t in add_parens child_prec child_assoc pos prec t' diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index ba31a3705..4ea310ee5 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -39,6 +39,8 @@ let fail floc msg = let (x, y) = loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) +type blob_context = [ `Ast | `Meta ] + type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) @@ -46,6 +48,7 @@ type term_attribute = | `Level of int * Gramext.g_assoc (* precedence, associativity *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) + | `Raw of string * blob_context option (* unparsed version *) ] type literal = diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 4489344f5..f2c2539cd 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -319,6 +319,10 @@ let boxify = function | [ a ] -> a | l -> Layout (Box ((H, false, false), l)) +let unboxify = function + | Layout (Box ((H, false, false), [ a ])) -> a + | l -> l + let group = function | [ a ] -> a | l -> Layout (Group l) diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index e845e5755..7d09e2d6a 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -109,15 +109,15 @@ type obj = | Inductive of (string * CicNotationPt.term) list * CicNotationPt.term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of thm_flavour * string * CicNotationPt.term * CicNotationPt.term option + | Theorem of thm_flavour * string * CicNotationPt.term * + CicNotationPt.term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) - | Record of - (string * CicNotationPt.term) list * string * CicNotationPt.term * + | Record of (string * CicNotationPt.term) list * string * CicNotationPt.term * (string * CicNotationPt.term) list type ('term,'obj) command = diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index db7a7253e..b7a62476c 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -229,6 +229,34 @@ let pp_obj = function "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ pp_fields fields ^ "}" +let pp_argument_pattern = function + | CicNotationPt.IdentArg (eta_depth, name) -> + let eta_buf = Buffer.create 5 in + for i = 1 to eta_depth do + Buffer.add_string eta_buf "\\eta." + done; + sprintf "%s%s" (Buffer.contents eta_buf) name + +let rec pp_cic_appl_pattern = function + | CicNotationPt.UriPattern uri -> UriManager.string_of_uri uri + | CicNotationPt.VarPattern name -> name + | CicNotationPt.ImplicitPattern -> "_" + | CicNotationPt.ApplPattern aps -> + sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps)) + +let pp_l1_pattern = CicNotationPp.pp_term +let pp_l2_pattern = CicNotationPp.pp_term + +let pp_associativity = function + | Some Gramext.LeftA -> "left associative " + | Some Gramext.RightA -> "right associative " + | Some Gramext.NonA -> "non associative " + | None -> "" + +let pp_precedence = function + | Some i -> sprintf "with precedence %d " i + | None -> "" + let pp_command = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" @@ -240,6 +268,19 @@ let pp_command = function | Default (_,what,uris) -> sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) + | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> + sprintf "interpretation \"%s\" '%s %s = %s" + dsc symbol + (String.concat " " (List.map pp_argument_pattern arg_patterns)) + (pp_cic_appl_pattern cic_appl_pattern) + | Notation (_, l1_pattern, assoc, prec, l2_pattern) -> + sprintf "notation \"%s\" %s%sfor %s" + (pp_l1_pattern l1_pattern) + (pp_associativity assoc) + (pp_precedence prec) + (pp_l2_pattern l2_pattern) + | Render _ + | Dump _ -> assert false (* ZACK: debugging *) let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac @@ -277,7 +318,12 @@ let pp_cic_command = function | Qed _ -> "qed" | Drop _ -> "drop" | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term) - | Set (_, _, _) - | Alias (_,_) - | Default (_,_,_) - | Obj (_,_) -> assert false (* not implemented *) + | Set _ + | Alias _ + | Default _ + | Render _ + | Dump _ + | Interpretation _ + | Notation _ + | Obj _ -> assert false (* not implemented *) + diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 8bd5cc04e..984635ec6 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -30,6 +30,9 @@ let grammar = CicNotationParser.level2_ast_grammar let term = CicNotationParser.term let statement = Grammar.Entry.create grammar "statement" +let add_raw_attribute ?context ~text term = + CicNotationPt.AttributedTerm (`Raw (text, context), term) + EXTEND GLOBAL: term statement; arg: [ @@ -358,11 +361,15 @@ EXTEND IDENT "for"; p2 = [ blob = UNPARSED_AST -> - CicNotationParser.parse_level2_ast (Stream.of_string blob) + add_raw_attribute ~context:`Ast ~text:blob + (CicNotationParser.parse_level2_ast (Stream.of_string blob)) | blob = UNPARSED_META -> - CicNotationParser.parse_level2_meta (Stream.of_string blob) ] - -> - (CicNotationParser.parse_level1_pattern (Stream.of_string s), assoc, prec, p2) + add_raw_attribute ~context:`Meta ~text:blob + (CicNotationParser.parse_level2_meta (Stream.of_string blob)) + ] -> + (add_raw_attribute ~text:s + (CicNotationParser.parse_level1_pattern (Stream.of_string s)), + assoc, prec, p2) ] ]; level3_term: [ diff --git a/helm/ocaml/cic_notation/test_parser.conf.xml b/helm/ocaml/cic_notation/test_parser.conf.xml index eca4f2d8c..9864ac1dc 100644 --- a/helm/ocaml/cic_notation/test_parser.conf.xml +++ b/helm/ocaml/cic_notation/test_parser.conf.xml @@ -6,6 +6,6 @@
- doc/core_notation.ma + ../../matita/core_notation.ma
diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index df94eaa6f..62b0ae32b 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -76,6 +76,7 @@ let process_stream ?(ignore_exn = false) istream = G.Notation (_, l1, associativity, precedence, l2))) -> prerr_endline "Extending parser ..."; flush stdout; prerr_endline (CicNotationPp.pp_term l1) ; + prerr_endline (CicNotationPp.pp_term l2) ; prerr_endline (sprintf "Found keywords: %s" (String.concat " " (CicNotationUtil.keywords_of_term l1))); let time1 = Unix.gettimeofday () in -- 2.39.2