src/Tools/Metis/src/Parser.sml
changeset 39353 7f11d833d65b
parent 39313 41ce0b56d858
parent 39352 7d850b17a7a6
child 39354 cd20519eb9d0
equal deleted inserted replaced
39313:41ce0b56d858 39353:7f11d833d65b
     1 (* ========================================================================= *)
       
     2 (* PARSER COMBINATORS                                                        *)
       
     3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
       
     4 (* ========================================================================= *)
       
     5 
       
     6 structure Parser :> Parser =
       
     7 struct
       
     8 
       
     9 infixr 9 >>++
       
    10 infixr 8 ++
       
    11 infixr 7 >>
       
    12 infixr 6 ||
       
    13 
       
    14 (* ------------------------------------------------------------------------- *)
       
    15 (* Helper functions.                                                         *)
       
    16 (* ------------------------------------------------------------------------- *)
       
    17 
       
    18 exception Bug = Useful.Bug;
       
    19 
       
    20 val trace = Useful.trace
       
    21 and equal = Useful.equal
       
    22 and I = Useful.I
       
    23 and K = Useful.K
       
    24 and C = Useful.C
       
    25 and fst = Useful.fst
       
    26 and snd = Useful.snd
       
    27 and pair = Useful.pair
       
    28 and curry = Useful.curry
       
    29 and funpow = Useful.funpow
       
    30 and mem = Useful.mem
       
    31 and sortMap = Useful.sortMap;
       
    32 
       
    33 (* ------------------------------------------------------------------------- *)
       
    34 (* Pretty printing for built-in types                                        *)
       
    35 (* ------------------------------------------------------------------------- *)
       
    36 
       
    37 type ppstream = PP.ppstream
       
    38 
       
    39 datatype breakStyle = Consistent | Inconsistent
       
    40 
       
    41 type 'a pp = PP.ppstream -> 'a -> unit;
       
    42 
       
    43 val lineLength = ref 75;
       
    44 
       
    45 fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT
       
    46   | beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT;
       
    47 
       
    48 val endBlock = PP.end_block
       
    49 and addString = PP.add_string
       
    50 and addBreak = PP.add_break
       
    51 and addNewline = PP.add_newline;
       
    52 
       
    53 fun ppMap f ppA (ppstrm : PP.ppstream) x : unit = ppA ppstrm (f x);
       
    54 
       
    55 fun ppBracket l r ppA pp a =
       
    56     let
       
    57       val ln = size l
       
    58     in
       
    59       beginBlock pp Inconsistent ln;
       
    60       if ln = 0 then () else addString pp l;
       
    61       ppA pp a;
       
    62       if r = "" then () else addString pp r;
       
    63       endBlock pp
       
    64     end;
       
    65 
       
    66 fun ppSequence sep ppA pp =
       
    67     let
       
    68       fun ppX x = (addString pp sep; addBreak pp (1,0); ppA pp x)
       
    69     in
       
    70       fn [] => ()
       
    71        | h :: t =>
       
    72          (beginBlock pp Inconsistent 0;
       
    73           ppA pp h;
       
    74           app ppX t;
       
    75           endBlock pp)
       
    76     end;
       
    77 
       
    78 fun ppBinop s ppA ppB pp (a,b) =
       
    79     (beginBlock pp Inconsistent 0;
       
    80       ppA pp a;
       
    81       if s = "" then () else addString pp s;
       
    82       addBreak pp (1,0);
       
    83       ppB pp b;
       
    84       endBlock pp);
       
    85 
       
    86 fun ppTrinop ab bc ppA ppB ppC pp (a,b,c) =
       
    87     (beginBlock pp Inconsistent 0;
       
    88      ppA pp a;
       
    89      if ab = "" then () else addString pp ab;
       
    90      addBreak pp (1,0);
       
    91      ppB pp b;
       
    92      if bc = "" then () else addString pp bc;
       
    93      addBreak pp (1,0);
       
    94      ppC pp c;
       
    95      endBlock pp);
       
    96 
       
    97 (* Pretty-printers for common types *)
       
    98 
       
    99 fun ppString pp s =
       
   100     (beginBlock pp Inconsistent 0;
       
   101      addString pp s;
       
   102      endBlock pp);
       
   103 
       
   104 val ppUnit = ppMap (fn () => "()") ppString;
       
   105 
       
   106 val ppChar = ppMap str ppString;
       
   107 
       
   108 val ppBool = ppMap (fn true => "true" | false => "false") ppString;
       
   109 
       
   110 val ppInt = ppMap Int.toString ppString;
       
   111 
       
   112 val ppReal = ppMap Real.toString ppString;
       
   113 
       
   114 val ppOrder =
       
   115     let
       
   116       fun f LESS = "Less"
       
   117         | f EQUAL = "Equal"
       
   118         | f GREATER = "Greater"
       
   119     in
       
   120       ppMap f ppString
       
   121     end;
       
   122 
       
   123 fun ppList ppA = ppBracket "[" "]" (ppSequence "," ppA);
       
   124 
       
   125 fun ppOption _ pp NONE = ppString pp "-"
       
   126   | ppOption ppA pp (SOME a) = ppA pp a;
       
   127 
       
   128 fun ppPair ppA ppB = ppBracket "(" ")" (ppBinop "," ppA ppB);
       
   129 
       
   130 fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppTrinop "," "," ppA ppB ppC);
       
   131 
       
   132 (* Keep eta expanded to evaluate lineLength when supplied with a *)
       
   133 fun toString ppA a = PP.pp_to_string (!lineLength) ppA a;
       
   134 
       
   135 fun fromString toS = ppMap toS ppString;
       
   136 
       
   137 fun ppTrace ppX nameX x =
       
   138     trace (toString (ppBinop " =" ppString ppX) (nameX,x) ^ "\n");
       
   139 
       
   140 (* ------------------------------------------------------------------------- *)
       
   141 (* Generic.                                                                  *)
       
   142 (* ------------------------------------------------------------------------- *)
       
   143 
       
   144 exception NoParse;
       
   145 
       
   146 val error : 'a -> 'b * 'a = fn _ => raise NoParse;
       
   147 
       
   148 fun op ++ (parser1,parser2) input =
       
   149     let
       
   150       val (result1,input) = parser1 input
       
   151       val (result2,input) = parser2 input
       
   152     in
       
   153       ((result1,result2),input)
       
   154     end;
       
   155 
       
   156 fun op >> (parser : 'a -> 'b * 'a, treatment) input =
       
   157     let
       
   158       val (result,input) = parser input
       
   159     in
       
   160       (treatment result, input)
       
   161     end;
       
   162 
       
   163 fun op >>++ (parser,treatment) input =
       
   164     let
       
   165       val (result,input) = parser input
       
   166     in
       
   167       treatment result input
       
   168     end;
       
   169 
       
   170 fun op || (parser1,parser2) input =
       
   171     parser1 input handle NoParse => parser2 input;
       
   172 
       
   173 fun first [] _ = raise NoParse
       
   174   | first (parser :: parsers) input = (parser || first parsers) input;
       
   175 
       
   176 fun mmany parser state input =
       
   177     let
       
   178       val (state,input) = parser state input
       
   179     in
       
   180       mmany parser state input
       
   181     end
       
   182     handle NoParse => (state,input);
       
   183 
       
   184 fun many parser =
       
   185     let
       
   186       fun sparser l = parser >> (fn x => x :: l)
       
   187     in
       
   188       mmany sparser [] >> rev      
       
   189     end;
       
   190 
       
   191 fun atLeastOne p = (p ++ many p) >> op::;
       
   192 
       
   193 fun nothing input = ((),input);
       
   194 
       
   195 fun optional p = (p >> SOME) || (nothing >> K NONE);
       
   196 
       
   197 (* ------------------------------------------------------------------------- *)
       
   198 (* Stream-based.                                                             *)
       
   199 (* ------------------------------------------------------------------------- *)
       
   200 
       
   201 type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
       
   202 
       
   203 fun everything parser =
       
   204     let
       
   205       fun f input =
       
   206           let
       
   207             val (result,input) = parser input
       
   208           in
       
   209             Stream.append (Stream.fromList result) (fn () => f input)
       
   210           end
       
   211           handle NoParse =>
       
   212             if Stream.null input then Stream.NIL else raise NoParse
       
   213     in
       
   214       f
       
   215     end;
       
   216 
       
   217 fun maybe p Stream.NIL = raise NoParse
       
   218   | maybe p (Stream.CONS (h,t)) =
       
   219     case p h of SOME r => (r, t ()) | NONE => raise NoParse;
       
   220 
       
   221 fun finished Stream.NIL = ((), Stream.NIL)
       
   222   | finished (Stream.CONS _) = raise NoParse;
       
   223 
       
   224 fun some p = maybe (fn x => if p x then SOME x else NONE);
       
   225 
       
   226 fun any input = some (K true) input;
       
   227 
       
   228 fun exact tok = some (fn item => item = tok);
       
   229 
       
   230 (* ------------------------------------------------------------------------- *)
       
   231 (* Parsing and pretty-printing for infix operators.                          *)
       
   232 (* ------------------------------------------------------------------------- *)
       
   233 
       
   234 type infixities = {token : string, precedence : int, leftAssoc : bool} list;
       
   235 
       
   236 local
       
   237   fun unflatten ({token,precedence,leftAssoc}, ([],_)) =
       
   238       ([(leftAssoc, [token])], precedence)
       
   239     | unflatten ({token,precedence,leftAssoc}, ((a,l) :: dealt, p)) =
       
   240       if p = precedence then
       
   241         let
       
   242           val _ = leftAssoc = a orelse
       
   243                   raise Bug "infix parser/printer: mixed assocs"
       
   244         in
       
   245           ((a, token :: l) :: dealt, p)
       
   246         end
       
   247       else
       
   248         ((leftAssoc,[token]) :: (a,l) :: dealt, precedence);
       
   249 in
       
   250   fun layerOps infixes =
       
   251       let
       
   252         val infixes = sortMap #precedence Int.compare infixes
       
   253         val (parsers,_) = foldl unflatten ([],0) infixes
       
   254       in
       
   255         parsers
       
   256       end;
       
   257 end;
       
   258 
       
   259 local
       
   260   fun chop (#" " :: chs) = let val (n,l) = chop chs in (n + 1, l) end
       
   261     | chop chs = (0,chs);
       
   262 
       
   263   fun nspaces n = funpow n (curry op^ " ") "";
       
   264 
       
   265   fun spacify tok =
       
   266       let
       
   267         val chs = explode tok
       
   268         val (r,chs) = chop (rev chs)
       
   269         val (l,chs) = chop (rev chs)
       
   270       in
       
   271         ((l,r), implode chs)
       
   272       end;
       
   273 
       
   274   fun lrspaces (l,r) =
       
   275       (if l = 0 then K () else C addString (nspaces l),
       
   276        if r = 0 then K () else C addBreak (r, 0));
       
   277 in
       
   278   fun opSpaces s = let val (l_r,s) = spacify s in (lrspaces l_r, s) end;
       
   279 
       
   280   val opClean = snd o spacify;
       
   281 end;
       
   282 
       
   283 val infixTokens : infixities -> string list =
       
   284     List.map (fn {token,...} => opClean token);
       
   285 
       
   286 fun parseGenInfix update sof toks parse inp =
       
   287     let
       
   288       val (e, rest) = parse inp
       
   289                       
       
   290       val continue =
       
   291           case rest of
       
   292             Stream.NIL => NONE
       
   293           | Stream.CONS (h, t) => if mem h toks then SOME (h, t) else NONE
       
   294     in
       
   295       case continue of
       
   296         NONE => (sof e, rest)
       
   297       | SOME (h,t) => parseGenInfix update (update sof h e) toks parse (t ())
       
   298     end;
       
   299 
       
   300 fun parseLeftInfix toks con =
       
   301     parseGenInfix (fn f => fn t => fn a => fn b => con (t, f a, b)) I toks;
       
   302 
       
   303 fun parseRightInfix toks con =
       
   304     parseGenInfix (fn f => fn t => fn a => fn b => f (con (t, a, b))) I toks;
       
   305 
       
   306 fun parseInfixes ops =
       
   307     let
       
   308       fun layeredOp (x,y) = (x, List.map opClean y)
       
   309 
       
   310       val layeredOps = List.map layeredOp (layerOps ops)
       
   311 
       
   312       fun iparser (a,t) = (if a then parseLeftInfix else parseRightInfix) t
       
   313 
       
   314       val iparsers = List.map iparser layeredOps
       
   315     in
       
   316       fn con => fn subparser => foldl (fn (p,sp) => p con sp) subparser iparsers
       
   317     end;
       
   318 
       
   319 fun ppGenInfix left toks =
       
   320     let
       
   321       val spc = List.map opSpaces toks
       
   322     in
       
   323       fn dest => fn ppSub =>
       
   324       let
       
   325         fun dest' tm =
       
   326             case dest tm of
       
   327               NONE => NONE
       
   328             | SOME (t, a, b) =>
       
   329               Option.map (pair (a,b)) (List.find (equal t o snd) spc)
       
   330 
       
   331         open PP
       
   332 
       
   333         fun ppGo pp (tmr as (tm,r)) =
       
   334             case dest' tm of
       
   335               NONE => ppSub pp tmr
       
   336             | SOME ((a,b),((lspc,rspc),tok)) =>
       
   337               ((if left then ppGo else ppSub) pp (a,true);
       
   338                lspc pp; addString pp tok; rspc pp;
       
   339                (if left then ppSub else ppGo) pp (b,r))
       
   340       in
       
   341         fn pp => fn tmr as (tm,_) =>
       
   342         case dest' tm of
       
   343           NONE => ppSub pp tmr
       
   344         | SOME _ => (beginBlock pp Inconsistent 0; ppGo pp tmr; endBlock pp)
       
   345       end
       
   346     end;
       
   347 
       
   348 fun ppLeftInfix toks = ppGenInfix true toks;
       
   349 
       
   350 fun ppRightInfix toks = ppGenInfix false toks;
       
   351 
       
   352 fun ppInfixes ops =
       
   353     let
       
   354       val layeredOps = layerOps ops
       
   355                        
       
   356       val toks = List.concat (List.map (List.map opClean o snd) layeredOps)
       
   357                  
       
   358       fun iprinter (a,t) = (if a then ppLeftInfix else ppRightInfix) t
       
   359                            
       
   360       val iprinters = List.map iprinter layeredOps
       
   361     in
       
   362       fn dest => fn ppSub =>
       
   363       let
       
   364         fun printer sub = foldl (fn (ip,p) => ip dest p) sub iprinters
       
   365 
       
   366         fun isOp t = case dest t of SOME (x,_,_) => mem x toks | _ => false
       
   367 
       
   368         open PP
       
   369 
       
   370         fun subpr pp (tmr as (tm,_)) =
       
   371             if isOp tm then
       
   372               (beginBlock pp Inconsistent 1; addString pp "(";
       
   373                printer subpr pp (tm, false); addString pp ")"; endBlock pp)
       
   374             else ppSub pp tmr
       
   375       in
       
   376         fn pp => fn tmr =>
       
   377         (beginBlock pp Inconsistent 0; printer subpr pp tmr; endBlock pp)
       
   378       end
       
   379     end;
       
   380 
       
   381 (* ------------------------------------------------------------------------- *)
       
   382 (* Quotations                                                                *)
       
   383 (* ------------------------------------------------------------------------- *)
       
   384 
       
   385 type 'a quotation = 'a frag list;
       
   386 
       
   387 fun parseQuotation printer parser quote =
       
   388   let
       
   389     fun expand (QUOTE q, s) = s ^ q
       
   390       | expand (ANTIQUOTE a, s) = s ^ printer a
       
   391 
       
   392     val string = foldl expand "" quote
       
   393   in
       
   394     parser string
       
   395   end;
       
   396 
       
   397 end