1(* ======================================================================== *) 2(* FILE : tttInfix.sml *) 3(* DESCRIPTION : Transforming a prefix operator into an infix one *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================= *) 7 8structure tttInfix :> tttInfix = 9struct 10 11infix 0 ttt_infixl0_open ttt_infixl0_close 12infix 1 ttt_infixl1_open ttt_infixl1_close 13infix 2 ttt_infixl2_open ttt_infixl2_close 14infix 3 ttt_infixl3_open ttt_infixl3_close 15infix 4 ttt_infixl4_open ttt_infixl4_close 16infix 5 ttt_infixl5_open ttt_infixl5_close 17infix 6 ttt_infixl6_open ttt_infixl6_close 18infix 7 ttt_infixl7_open ttt_infixl7_close 19infix 8 ttt_infixl8_open ttt_infixl8_close 20infix 9 ttt_infixl9_open ttt_infixl9_close 21 22infixr 0 ttt_infixr0_open ttt_infixr0_close 23infixr 1 ttt_infixr1_open ttt_infixr1_close 24infixr 2 ttt_infixr2_open ttt_infixr2_close 25infixr 3 ttt_infixr3_open ttt_infixr3_close 26infixr 4 ttt_infixr4_open ttt_infixr4_close 27infixr 5 ttt_infixr5_open ttt_infixr5_close 28infixr 6 ttt_infixr6_open ttt_infixr6_close 29infixr 7 ttt_infixr7_open ttt_infixr7_close 30infixr 8 ttt_infixr8_open ttt_infixr8_close 31infixr 9 ttt_infixr9_open ttt_infixr9_close 32 33fun a ttt_infixl0_open f = fn x => f (a,x) 34fun g ttt_infixl0_close b = g b 35 36fun f ttt_infixr0_close b = fn x => f (x,b) 37fun a ttt_infixr0_open g = g a 38 39val op ttt_infixl1_open = op ttt_infixl0_open 40val op ttt_infixl2_open = op ttt_infixl0_open 41val op ttt_infixl3_open = op ttt_infixl0_open 42val op ttt_infixl4_open = op ttt_infixl0_open 43val op ttt_infixl5_open = op ttt_infixl0_open 44val op ttt_infixl6_open = op ttt_infixl0_open 45val op ttt_infixl7_open = op ttt_infixl0_open 46val op ttt_infixl8_open = op ttt_infixl0_open 47val op ttt_infixl9_open = op ttt_infixl0_open 48 49val op ttt_infixl1_close = op ttt_infixl0_close 50val op ttt_infixl2_close = op ttt_infixl0_close 51val op ttt_infixl3_close = op ttt_infixl0_close 52val op ttt_infixl4_close = op ttt_infixl0_close 53val op ttt_infixl5_close = op ttt_infixl0_close 54val op ttt_infixl6_close = op ttt_infixl0_close 55val op ttt_infixl7_close = op ttt_infixl0_close 56val op ttt_infixl8_close = op ttt_infixl0_close 57val op ttt_infixl9_close = op ttt_infixl0_close 58 59val op ttt_infixr1_open = op ttt_infixr0_open 60val op ttt_infixr2_open = op ttt_infixr0_open 61val op ttt_infixr3_open = op ttt_infixr0_open 62val op ttt_infixr4_open = op ttt_infixr0_open 63val op ttt_infixr5_open = op ttt_infixr0_open 64val op ttt_infixr6_open = op ttt_infixr0_open 65val op ttt_infixr7_open = op ttt_infixr0_open 66val op ttt_infixr8_open = op ttt_infixr0_open 67val op ttt_infixr9_open = op ttt_infixr0_open 68 69val op ttt_infixr1_close = op ttt_infixr0_close 70val op ttt_infixr2_close = op ttt_infixr0_close 71val op ttt_infixr3_close = op ttt_infixr0_close 72val op ttt_infixr4_close = op ttt_infixr0_close 73val op ttt_infixr5_close = op ttt_infixr0_close 74val op ttt_infixr6_close = op ttt_infixr0_close 75val op ttt_infixr7_close = op ttt_infixr0_close 76val op ttt_infixr8_close = op ttt_infixr0_close 77val op ttt_infixr9_close = op ttt_infixr0_close 78 79datatype infixity_t = Inf_left of int | Inf_right of int 80 81fun infix_pair infixity = case infixity of 82 Inf_left n => 83 ("ttt_infixl" ^ Int.toString n ^ "_open", 84 "ttt_infixl" ^ Int.toString n ^ "_close") 85 | Inf_right n => 86 ("ttt_infixr" ^ Int.toString n ^ "_open", 87 "ttt_infixr" ^ Int.toString n ^ "_close") 88 89(*--------------------------------------------------------------------------- 90 Infixity from src/thm/Overlay.sml. 91 ---------------------------------------------------------------------------*) 92 93val l0 = String.tokens Char.isSpace 94 ( 95 String.concatWith " " 96 [ 97 "++ && |-> THEN THEN1 THENL THEN_LT THENC ORELSE ORELSE_LT ORELSEC", 98 "THEN_TCL ORELSE_TCL ?> |> |>> ||> ||->", 99 ">> >- >| \\\\ >>> >>- ??", 100 "~~ !~ Un Isct -- IN -*" 101 ] 102 ) 103val l1 = String.tokens Char.isSpace "## $ ?" 104val l2 = String.tokens Char.isSpace "via by suffices_by" 105 106val overlay_infixity = 107 map (fn x => (x,Inf_left 0)) l0 @ 108 map (fn x => (x,Inf_right 0)) l1 @ 109 map (fn x => (x,Inf_right 3)) ["-->"] @ 110 map (fn x => (x,Inf_left 8)) l2 111 112 113 114 115end 116