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