1structure parse_type :> parse_type =
2struct
3
4open type_tokens type_grammar HOLgrammars Feedback
5
6open qbuf
7
8type term = Term.term
9
10exception InternalFailure of locn.locn
11
12type ('a,'b) tyconstructors =
13     {vartype : string locn.located -> 'a,
14      tyop : (string locn.located * 'a list) -> 'a,
15      qtyop : {Thy:string, Tyop:string, Locn:locn.locn, Args: 'a list} -> 'a,
16      antiq : 'b -> 'a}
17
18(* antiquoting types into terms *)
19fun ty_antiq ty = Term.mk_var("ty_antiq",ty)
20
21fun dest_ty_antiq tm =
22  case Lib.with_exn Term.dest_var tm
23                (mk_HOL_ERR "Parse" "dest_ty_antiq" "not a type antiquotation")
24   of ("ty_antiq",Ty) => Ty
25    |  _ => raise mk_HOL_ERR "Parse" "dest_ty_antiq" "not a type antiquotation";
26
27val is_ty_antiq = Lib.can dest_ty_antiq
28
29val ERR = Feedback.mk_HOL_ERR "Parse" "parse_type"
30val ERRloc = Feedback.mk_HOL_ERRloc "Parse" "parse_type"
31
32fun totalify f x = SOME (f x) handle InternalFailure _ => NONE
33
34fun parse_type_fns tyfns allow_unknown_suffixes G = let
35  val G = rules G and abbrevs = parse_map G
36  and privabbs = privileged_abbrevs G
37  val {vartype = pVartype, tyop = pType, antiq = pAQ, qtyop} = tyfns
38  fun structure_to_value0 (s,locn) args st =
39      case st of
40        TYOP {Args, Thy, Tyop} =>
41        qtyop {Args = map (structure_to_value0 (s,locn) args) Args,
42               Thy = Thy, Tyop = Tyop, Locn = locn}
43      | PARAM n => List.nth(args, n)
44
45  fun structure_to_value (s,locn) args st =
46      if num_params st <> length args then
47        raise ERRloc
48                  locn
49                  ("Incorrect number of arguments to abbreviated operator "^s^
50                   " (expects "^Int.toString (num_params st)^")")
51      else structure_to_value0 (s,locn) args st
52
53  (* extra fails on next two definitions will effectively make the stream
54     push back the unwanted token *)
55  (* can't use item for these, because this would require the token type
56     to be an equality type, which is icky *)
57  fun is_LParen t = case t of LParen => true | _ => false
58  fun is_RParen t = case t of RParen => true | _ => false
59  fun is_LBracket t = case t of LBracket => true | _ => false
60  fun is_RBracket t = case t of RBracket => true | _ => false
61  fun is_Comma t = case t of Comma => true | _ => false
62  fun itemP P fb = let
63    val (adv, (t,locn)) = typetok_of fb (* TODO:KSW: use locn *)
64  in
65    if P t then (locn,adv()) else raise InternalFailure locn
66  end
67
68  fun many f fb = let
69    fun recurse acc =
70        case totalify f fb of
71          NONE => List.rev acc
72        | SOME i => recurse (i::acc)
73  in
74    recurse []
75  end
76
77  fun many1 f fb = let
78    val i1 = f fb
79    fun recurse acc =
80        case totalify f fb of
81          NONE => List.rev acc
82        | SOME i => recurse (i::acc)
83  in
84    recurse [i1]
85  end
86
87  fun is_numeric s = let
88    val lim = size s
89    fun recurse n =
90        n >= lim orelse (Char.isDigit (String.sub(s,n)) andalso
91                         recurse (n + 1))
92  in
93    recurse 0
94  end
95
96  fun generate_fcpbit ((s,locn), args) = let
97    val _ = null args orelse raise ERRloc locn "Number types take no arguments"
98    val n = Arbnum.fromString s
99    val _ = n <> Arbnum.zero orelse
100            raise ERRloc locn "Zero is not a valid number type"
101    fun recurse acc m =
102        if m = Arbnum.one then acc
103        else let
104            val (q,r) = Arbnum.divmod(m,Arbnum.two)
105          in
106            recurse ((r = Arbnum.one) :: acc) q
107          end
108    fun bit b arg = qtyop {Thy = "fcp", Tyop = if b then "bit1" else "bit0",
109                           Locn = locn, Args = [arg]}
110    fun build acc bits =
111        case bits of
112          [] => acc
113        | b :: rest => build (bit b acc) rest
114    val one = qtyop {Thy = "one", Tyop = "one", Locn = locn, Args = []}
115  in
116    build one (recurse [] n)
117  end
118
119  fun apply_tyop (t,locn) args =
120    case t of
121      TypeIdent s => let
122      in
123        if is_numeric s then generate_fcpbit((s,locn), args)
124        else
125          case Binarymap.peek(privabbs, s) of
126            NONE => pType((s,locn), args)
127          | SOME thy => let
128            in
129              case Binarymap.peek(abbrevs, {Name = s, Thy = thy}) of
130                  NONE => raise Fail
131                            "parse_tyop.apply_tyop: probably shouldn't happen"
132                | SOME st => structure_to_value (s,locn) args st
133            end
134      end
135    | QTypeIdent(thy,ty) =>
136        (case Binarymap.peek(abbrevs, {Name = ty, Thy = thy}) of
137             NONE => qtyop{Thy=thy,Tyop=ty,Locn=locn,Args=args}
138         |   SOME st => structure_to_value (ty,locn) args st)
139    | _ => raise Fail "parse_type.apply_tyop: can't happen"
140
141  fun apply_asfx locn (base,index) =
142      qtyop{Thy = "fcp", Tyop = "cart",Locn=locn,Args = [base, index]}
143
144  fun parse_op slist fb = let
145    val (adv, (t,locn)) = typetok_of fb
146  in
147    case t of
148      TypeIdent s => if allow_unknown_suffixes orelse Lib.mem s slist then
149                       (adv(); (t,locn))
150                     else raise InternalFailure locn
151    | QTypeIdent _ => (adv(); (t,locn))
152    | _ => raise InternalFailure locn
153  end
154
155  fun parse_binop (stlist:{parse_string:string,opname:string}list) fb = let
156    val (adv, (t,locn)) = typetok_of fb
157    fun doit (t,locn) =
158      case List.find (fn r => (#parse_string r = token_string t)) stlist of
159        NONE => raise InternalFailure locn
160      | SOME r => (adv(); (TypeIdent (#opname r),locn))
161  in
162    case t of
163      TypeIdent s => doit (t,locn)
164    | TypeSymbol s => doit (t,locn)
165    | _ => raise InternalFailure locn
166  end
167
168  fun parse_asfx prse fb = let
169    val (llocn, _) = itemP is_LBracket fb
170    val ty = prse fb
171    val (rlocn, _) = itemP is_RBracket fb
172  in
173    ty
174  end
175
176  fun parse_tuple prse fb = let
177    val (llocn,_) = itemP is_LParen fb
178    val ty1 = prse fb
179    fun recurse acc = let
180      val (adv,(t,locn)) = typetok_of fb
181    in
182      case t of
183        RParen => (adv(); (List.rev acc,locn.between llocn locn))
184      | Comma => (adv(); recurse (prse fb :: acc))
185      | _ => raise InternalFailure locn
186    end
187  in
188    recurse [ty1]
189  end
190
191  fun uniconvert c = let
192    val ((s,i), s') = valOf (UTF8.getChar c)
193  in
194    if s' = "" andalso 0x3B1 <= i andalso i <= 0x3C9 then
195      "'" ^ str (Char.chr (i - 0x3B1 + Char.ord #"a"))
196    else c
197  end
198
199  fun parse_atom fb = let
200    val (adv, (t,locn)) = typetok_of fb
201  in
202    case t of
203      TypeVar s => (adv(); pVartype (uniconvert s, locn))
204    | AQ x => (adv(); pAQ x)
205    | TypeIdent s => (adv(); apply_tyop(t,locn) [])
206                     (* should only be a number *)
207    | _ => raise InternalFailure locn
208  end
209
210  val {suffixes,infixes = rules} = G
211
212  datatype ('op,'array) OPARRAY = NormalSfx of 'op
213                                | ArraySfx of 'array * locn.locn
214  fun parse_oparray p strm = let
215    val (adv, (t,locn)) = typetok_of strm
216  in
217    case t of
218      LBracket => ArraySfx (parse_asfx p strm, locn)
219    | _ => NormalSfx (parse_op suffixes strm)
220  end
221  fun apply_oparrays ops base =
222      case ops of
223        [] => base
224      | NormalSfx sfx :: rest => apply_oparrays rest (apply_tyop sfx [base])
225      | ArraySfx (index,l) :: rest =>
226          apply_oparrays rest (apply_asfx l (base, index))
227
228  fun tuple_oparrays first rest tuple =
229      case first of
230        ArraySfx (i,l) => let
231        in
232          if length tuple <> 1 then
233            raise ERRloc l "array type can't take tuple as first argument"
234          else
235            apply_oparrays rest (apply_asfx l (hd tuple, i))
236        end
237      | NormalSfx s => apply_oparrays rest (apply_tyop s tuple)
238
239  fun parse_atomsuffixes p strm = let
240  in
241    case totalify (parse_tuple p) strm of
242      NONE => let
243        val ty1 = let
244          val op1 = parse_op suffixes strm
245        in
246          apply_tyop op1 []
247        end handle InternalFailure l => parse_atom strm
248        val ops = many (parse_oparray p) strm
249      in
250        apply_oparrays ops ty1
251      end
252    | SOME (tyl,locn) => let
253      in
254        case (many (parse_oparray p) strm) of
255          [] => if length tyl <> 1 then
256                  raise ERRloc locn "tuple with no suffix"
257                else
258                  hd tyl
259        | h::t => tuple_oparrays h t tyl
260      end
261  end
262
263  fun parse_term current strm =
264      case current of
265        [] => parse_atomsuffixes (parse_term rules) strm
266      | (x::xs) => parse_rule x xs strm
267  and parse_rule (rule as (_, r)) rs strm = let
268    val next_level = parse_term rs
269    val same_level = parse_rule rule rs
270  in
271    case r of
272      INFIX (stlist, NONASSOC) => let
273        val ty1 = next_level strm
274      in
275        case totalify (parse_binop stlist) strm of
276          NONE => ty1
277        | SOME opn => apply_tyop opn [ty1, next_level strm]
278      end
279    | INFIX (stlist, LEFT) => let
280        val ty1 = next_level strm
281        fun recurse acc =
282            case totalify (parse_binop stlist) strm of
283              NONE => acc
284            | SOME opn => recurse (apply_tyop opn [acc, next_level strm])
285      in
286        recurse ty1
287      end
288    | INFIX (stlist, RIGHT) => let
289        val ty1 = next_level strm
290      in
291        case totalify (parse_binop stlist) strm of
292          NONE => ty1
293        | SOME opn => apply_tyop opn [ty1, same_level strm]
294      end
295  end
296in
297  ((fn qb => parse_term rules qb
298     handle InternalFailure locn =>
299            raise ERRloc locn
300                  ("Type parsing failure with remaining input: "^
301                   qbuf.toString qb)),
302   (fn qb =>
303       case totalify (parse_op suffixes) qb of
304           NONE => (parse_atom qb
305                    handle InternalFailure locn =>
306                           raise ERRloc locn
307                            ("Type-atom parsing failure with remaining input: "^
308                             qbuf.toString qb)
309                   )
310         | SOME tloc => apply_tyop tloc []))
311
312end
313
314fun parse_type tyfns allow_unknown_suffixes G qb =
315  #1 (parse_type_fns tyfns allow_unknown_suffixes G) qb
316
317fun parse_atom tyfns allow_unknown_suffixes G qb =
318  #2 (parse_type_fns tyfns allow_unknown_suffixes G) qb
319
320end; (* struct *)
321