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