1(* ========================================================================= *) 2(* FILE : smlParser.sml *) 3(* DESCRIPTION : Parse SML using the Poly/ML compiler *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================= *) 7 8structure smlParser :> smlParser = 9struct 10 11open HolKernel boolLib aiLib smlLexer smlExecute 12 13val ERR = mk_HOL_ERR "smlExtract" 14 15(* ------------------------------------------------------------------------- 16 Property tests 17 ------------------------------------------------------------------------- *) 18 19fun is_print p = case p of PolyML.PTprint _ => true | _ => false 20fun is_type p = case p of PolyML.PTtype _ => true | _ => false 21fun is_firstchild p = case p of PolyML.PTfirstChild _ => true | _ => false 22fun is_nextsibling p = case p of PolyML.PTnextSibling _ => true | _ => false 23 24(* ------------------------------------------------------------------------- 25 Property destructors 26 ------------------------------------------------------------------------- *) 27 28fun dest_firstchild p = case p of 29 PolyML.PTfirstChild f => snd (f ()) 30 | _ => raise ERR "dest_firstchild" "" 31 32fun dest_print p = case p of 33 PolyML.PTprint f => f 34 | _ => raise ERR "dest_print" "" 35 36fun dest_type p = case p of 37 PolyML.PTtype ty => ty 38 | _ => raise ERR "dest_type" "" 39 40fun dest_firstchild p = case p of 41 PolyML.PTfirstChild g => snd (g ()) 42 | _ => raise ERR "dest_firstchild" "" 43 44fun dest_nextsibling p = case p of 45 PolyML.PTnextSibling g => snd (g ()) 46 | _ => raise ERR "dest_nextsibling" "" 47 48(* ------------------------------------------------------------------------- 49 Printing functions 50 ------------------------------------------------------------------------- *) 51 52fun respace s = String.concatWith " " (partial_sml_lexer s) 53 54fun string_of_pretty pretty = 55 let 56 val acc = ref [] 57 fun f s = acc := s :: !acc 58 in 59 PolyML.prettyPrint (f,80) pretty; 60 respace (String.concatWith " " (rev (!acc))) 61 end 62 63fun string_of_print p = string_of_pretty ((dest_print p) 80) 64 65fun string_of_type ty = 66 let 67 val pretty = PolyML.NameSpace.Values.printType 68 (ty, 80, SOME PolyML.globalNameSpace) 69 in 70 respace (string_of_pretty pretty) 71 end 72 73fun string_of_propl pl = case List.find is_print pl of 74 SOME p => SOME (string_of_print p) 75 | NONE => NONE 76 77fun stype_of_propl pl = case List.find is_type pl of 78 SOME (PolyML.PTtype ty) => SOME (string_of_type ty) 79 | _ => NONE 80 81(* ------------------------------------------------------------------------- 82 Calling the PolyML compiler 83 ------------------------------------------------------------------------- *) 84 85fun parse s = 86 let 87 val stream = TextIO.openString s 88 val resultTrees : PolyML.parseTree list ref = ref [] 89 fun compilerResultFun (parsetree, codeOpt) = 90 let 91 val _ = 92 case parsetree of 93 SOME pt => resultTrees := !resultTrees @ [pt] 94 | NONE => () 95 in 96 fn () => raise ERR "parse" "" 97 end 98 val _ = PolyML.compiler (fn () => 99 TextIO.input1 stream, 100 [PolyML.Compiler.CPCompilerResultFun compilerResultFun, 101 PolyML.Compiler.CPNameSpace PolyML.globalNameSpace]) 102 in 103 dest_firstchild 104 (singleton_of_list (snd (singleton_of_list (!resultTrees)))) 105 end 106 107(* ------------------------------------------------------------------------- 108 Simplified parsed tree with type information 109 ------------------------------------------------------------------------- *) 110 111datatype smlexp = 112 SmlExp of (string option * string option) * smlexp list 113 | SmlUnit of (string option * string option) 114 115fun dest_smlexp e = case e of 116 SmlExp x => x 117 | _ => raise ERR "dest_smlexp" "" 118 119fun string_of_smlexp e = case e of 120 SmlExp ((SOME s,_),_) => s 121 | SmlUnit (SOME s,_) => s 122 | _ => raise ERR "string_of_smlexp" "" 123 124fun extract_smlexp_aux propl = 125 let 126 val s = string_of_propl propl 127 val sty = stype_of_propl propl 128 val l1 = List.filter is_firstchild propl 129 val l2 = List.filter is_nextsibling propl 130 in 131 case (l1,l2) of 132 ([],[]) => [SmlUnit (s,sty)] 133 | ([fprop],[]) => 134 let val ftreel = extract_smlexp_aux (dest_firstchild fprop) in 135 [SmlExp ((s,sty),ftreel)] 136 end 137 | ([],[nprop]) => 138 let val ntreel = extract_smlexp_aux (dest_nextsibling nprop) in 139 SmlUnit (s,sty) :: ntreel 140 end 141 | ([fprop],[nprop]) => 142 let 143 val ftreel = extract_smlexp_aux (dest_firstchild fprop) 144 val ntreel = extract_smlexp_aux (dest_nextsibling nprop) 145 in 146 SmlExp ((s,sty),ftreel) :: ntreel 147 end 148 | _ => raise ERR "extract_smlexp_aux" "" 149 end 150 151fun extract_smlexp s = singleton_of_list (extract_smlexp_aux (parse s)) 152 153(* ------------------------------------------------------------------------- 154 Proof tree separated into tactic units 155 ------------------------------------------------------------------------- *) 156 157datatype proofexp = 158 ProofInfix of string * (proofexp * proofexp) 159 | ProofTactical of string 160 | ProofTactic of string 161 | ProofOther of string 162 163fun size_of_proofexp proofexp = case proofexp of 164 ProofInfix (_,(e1,e2)) => size_of_proofexp e1 + size_of_proofexp e2 165 | ProofTactical _ => 0 166 | ProofTactic _ => 1 167 | ProofOther _ => 0 168 169fun is_infixr s = 170 let val sl = partial_sml_lexer s in 171 String.isPrefix "sml_infixr" (singleton_of_list sl) 172 end 173 174fun is_infixl s = 175 let val sl = partial_sml_lexer s in 176 String.isPrefix "sml_infixl" (singleton_of_list sl) 177 end 178 179fun is_infix s = 180 let val sl = partial_sml_lexer s in 181 String.isPrefix "sml_infix" (singleton_of_list sl) 182 end 183 184fun dest_infix e = case e of 185 SmlExp (_,[a,b,c]) => 186 if not (is_infix (string_of_smlexp b)) 187 then raise ERR "dest_infix" "unexpected" 188 else (a,b,c) 189 | _ => raise ERR "dest_infix" "unexpected" 190 191fun extract_proofexp smlexp = case smlexp of 192 SmlExp ((SOME s,_),[a,inf,b]) => 193 if is_infixl (string_of_smlexp inf) then 194 let 195 val (a0,ainf,a1) = dest_infix a 196 val infs = string_of_smlexp inf 197 val ainfs = string_of_smlexp ainf 198 val a1s = string_of_smlexp a1 199 in 200 ProofInfix (infs, 201 ( 202 ProofInfix (ainfs, (extract_proofexp a0, ProofTactical a1s)), 203 extract_proofexp b 204 ) 205 ) 206 end 207 else if is_infixr (string_of_smlexp inf) then 208 let 209 val (b0,binf,b1) = dest_infix b 210 val infs = string_of_smlexp inf 211 val binfs = string_of_smlexp binf 212 val b0s = string_of_smlexp b0 213 in 214 ProofInfix (infs, 215 ( 216 extract_proofexp a, 217 ProofInfix (binfs, (ProofTactical b0s, extract_proofexp b1)) 218 ) 219 ) 220 end 221 else (if is_tactic s then ProofTactic s else ProofOther s) 222 | SmlExp ((SOME s,_),_) => 223 if is_tactic s then ProofTactic s else ProofOther s 224 | SmlUnit (SOME s,_) => 225 if is_tactic s then ProofTactic s else ProofOther s 226 | _ => raise ERR "extract_tacticl_aux" "option" 227 228fun safe_par s = 229 if mem #" " (explode s) 230 then String.concatWith " " ["(",s,")"] 231 else s 232 233fun string_of_proofexp e = case e of 234 ProofInfix (s,(e1,e2)) => String.concatWith " " 235 ["(",string_of_proofexp e1,s,string_of_proofexp e2,")"] 236 | ProofTactic s => safe_par s 237 | ProofOther s => safe_par s 238 | ProofTactical s => safe_par s 239 240(* ------------------------------------------------------------------------- 241 Tactic sketch. Break a sml expression into applications. 242 ------------------------------------------------------------------------- *) 243 244fun drop_all_sig stac = 245 String.concatWith " " (map drop_sig (partial_sml_lexer stac)); 246 247datatype applyexp = 248 ApplyExp of applyexp * applyexp 249 | ApplyUnit of (string * string option) 250 251fun is_app s (s1,s2) = 252 let 253 val s1par = "( " ^ s1 ^ " )" 254 val s2par = "( " ^ s2 ^ " )" 255 val s1parpar = "( " ^ s1par ^ " )" 256 val s2parpar = "( " ^ s2par ^ " )" 257 258 val l = cartesian_product [s1,s1par,s1parpar] [s2,s2par,s2parpar] 259 fun f (a,b) = a ^ " " ^ b 260 in 261 mem s (map f l) 262 end 263 264fun extract_applyexp smlexp = case smlexp of 265 SmlExp ((SOME a, SOME b),[e1,e2]) => 266 if is_app a (string_of_smlexp e1, string_of_smlexp e2) 267 then ApplyExp (extract_applyexp e1, extract_applyexp e2) 268 else ApplyUnit (a, SOME (drop_all_sig b)) 269 | SmlExp ((SOME a, b), _) => ApplyUnit (a, Option.map drop_all_sig b) 270 | SmlUnit (SOME a, b) => ApplyUnit (a, Option.map drop_all_sig b) 271 | _ => raise ERR "extract_applyexp" "" 272 273end (* struct *) 274