1(* ========================================================================== *)
2(* FILE          : tttNumber.sml                                              *)
3(* DESCRIPTION   : Tagging each SML token with a number                       *)
4(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck             *)
5(* DATE          : 2017                                                       *)
6(* ========================================================================== *)
7
8
9structure tttNumber :> tttNumber =
10struct
11
12open HolKernel boolLib tttTools tttLexer
13
14val ERR = mk_HOL_ERR "tttNumber"
15
16(*---------------------------------------------------------------------------
17 *  Tokens
18 *---------------------------------------------------------------------------*)
19
20(* either real numbers or already prefixed *)
21fun contain_dot s = mem #"." (explode s)
22
23(*---------------------------------------------------------------------------
24 * Number tokens of a string
25 *---------------------------------------------------------------------------*)
26
27val ttt_fst = fst
28
29fun number_token n s =
30  ttt_lex ("(tttNumber.ttt_fst ( " ^ s ^ "," ^ int_to_string n ^ "))")
31
32fun number_tokenl n sl =
33  if sl = [] then [] else
34  let val (a,m) = (hd sl,tl sl) in
35    if mem a ["|","of","handle","fn"] then
36      let val (head,cont) = split_level "=>" m in
37        (a :: head) @ ["=>"] @ number_tokenl n cont
38      end
39    else if mem a ["val","fun","structure"] then
40      let val (head,cont) = split_level "=" m in
41        (a :: head) @ ["="] @ number_tokenl n cont
42      end
43    else if contain_dot a
44      then (number_token n a) @ number_tokenl (n + 1) m
45    else a :: number_tokenl n m
46  end
47
48fun number_stac s =
49  String.concatWith " " (number_tokenl 0 (ttt_lex s))
50
51(*---------------------------------------------------------------------------
52 * Drop numbering
53 *---------------------------------------------------------------------------*)
54
55fun drop_numbering sl = case sl of
56   "(" :: "tttNumber.ttt_fst" :: "(" :: v :: "," :: n :: ")" :: ")" :: m =>
57    v :: drop_numbering m
58  | "tttNumber.ttt_fst" :: "(" :: v :: "," :: n :: ")" :: m =>
59    v :: drop_numbering m
60  | a :: m => a :: drop_numbering m
61  | []  => []
62
63(*---------------------------------------------------------------------------
64 * Use the numbering for replacing at a certain point in a string list
65 *---------------------------------------------------------------------------*)
66
67fun prefix l1 l2 = case (l1,l2) of
68    ([],r) => r
69  | (_,[]) => raise ERR "prefix" ""
70  | (a1 :: m1, a2 :: m2) =>
71    if a1 = a2
72    then prefix m1 m2
73    else raise ERR "prefix" ""
74
75fun replace_at (l1,lrep) l2 = case l2 of
76    []       => raise ERR "replace_at" (String.concatWith " " l1)
77  | a2 :: m2 =>
78    (
79    let val r = prefix l1 l2 in lrep @ r end
80    handle _ => (a2 :: replace_at (l1,lrep) m2)
81    )
82
83end (* struct *)
84