From 5ec963822874008c725ec11968ce453e80f252e2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 13:47:46 +0000 Subject: [PATCH] Syntactic change: [ ... ] match t in t with ==> match t in t return ... with --- helm/ocaml/cic_notation/cicNotationLexer.ml | 2 +- helm/ocaml/cic_notation/cicNotationParser.ml | 4 ++-- helm/ocaml/cic_notation/cicNotationRew.ml | 22 +++++++++++++------- 3 files changed, 17 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 5d2dae341..3d9d6be25 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -107,7 +107,7 @@ let level2_ast_keywords = Hashtbl.create 23 let _ = List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; - "with"; "in"; "and"; "to"; "as"; "on" ] + "with"; "in"; "and"; "to"; "as"; "on"; "return" ] 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 578a9d6f0..32b6b0a90 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -586,9 +586,9 @@ EXTEND | m = META; s = meta_substs -> return_term loc (Ast.Meta (int_of_string m, s)) | s = sort -> return_term loc (Ast.Sort s) - | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ]; - "match"; t = term; + | "match"; t = term; indty_ident = OPT [ "in"; id = IDENT -> id, None ]; + outtyp = OPT [ "return"; ty = term -> ty ]; "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index aa171c55c..27040d5ae 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -158,19 +158,25 @@ let pp_ast0 t k = match outty_opt with | None -> [] | Some outty -> - [ builtin_symbol "["; remove_level_info (k outty); - builtin_symbol "]"; break ] + [ keyword "return"; break; remove_level_info (k outty)] in let indty_box = match indty_opt with | None -> [] - | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ] + | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ] in let match_box = - hvbox false true [ - keyword "match"; break; - hvbox false false ([ top_pos (k what) ] @ indty_box); break; - keyword "with" ] + hvbox false false [ + hvbox false true [ + hvbox false true [ keyword "match"; break; top_pos (k what) ]; + break; + hvbox false true indty_box; + break; + hvbox false true outty_box + ]; + break; + keyword "with" + ] in let mk_case_pattern (head, href, vars) = hbox true false (ident_w_href href head :: List.map aux_var vars) @@ -209,7 +215,7 @@ let pp_ast0 t k = in add_level_info Ast.simple_prec Ast.simple_assoc (hvbox false false [ - hvbox false false (outty_box @ [ match_box ]); break; + hvbox false false ([match_box]); break; hbox false false [ hvbox false false patterns'' ] ]) | Ast.Cast (bo, ty) -> add_level_info Ast.simple_prec Ast.simple_assoc -- 2.39.2