text_formalization/general/parser_verbose.hl

   1 (* ========================================================================= *)
   2 (* Lexical analyzer, type and preterm parsers.                               *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 (*
  11 Slightly more verbose error messages added by thales, July 2010
  12 *)
  13
  14
  15
  16 module Parser_verbose = struct
  17
  18 let string_of_lexcode = function
  19    Ident s -> s
  20    |Resword s -> s;;
  21
  22  let string_of_lexcodel r = itlist (fun a b -> string_of_lexcode a^"   "^b) r "";;
  23
  24 let err_lex_rest prs i =
  25     try prs i with
  26       Failure s -> failwith (s^ "\n unread tokens:\n"^string_of_lexcodel i);;
  27
  28 let parse_pretype_verbose =
  29   let btyop n n' x y = Ptycon(n,[x;y])
  30   and mk_apptype =
  31     function
  32         ([s],[]) -> s
  33       | (tys,[c]) -> Ptycon(c,tys)
  34       | _ -> failwith "Bad type construction"
  35   and type_atom input =
  36     match input with
  37       (Ident s)::rest ->
  38           (try pretype_of_type(assoc s (type_abbrevs())) with Failure _ ->
  39            if try get_type_arity s = 0 with Failure _ -> false
  40            then Ptycon(s,[]) else Utv(s)),rest
  41     | _ -> raise Noparse
  42   and type_constructor input =
  43     match input with
  44       (Ident s)::rest -> if try get_type_arity s > 0 with Failure _ -> false
  45                          then s,rest else raise Noparse
  46     | _ -> raise Noparse in
  47   let rec pretype i = rightbin sumtype (a (Resword "->")) (btyop "fun") "proper use of type operator (->)" i
  48   and sumtype i = rightbin prodtype (a (Ident "+")) (btyop "sum") "proper use of type operator (+)" i
  49   and prodtype i = rightbin carttype (a (Ident "#")) (btyop "prod") "proper use of type operator (#)" i
  50   and carttype i = leftbin apptype (a (Ident "^")) (btyop "cart") " proper use of type operator (^) " i
  51   and apptype i = (atomictypes ++ (type_constructor >> (fun x -> [x])
  52                                 || nothing) >> mk_apptype) i
  53   and atomictypes i =
  54         (((a (Resword "(")) ++ typelist ++ a (Resword ")") >> (snd o fst))
  55       || type_atom >> (fun x -> [x])) i
  56   and typelist i = listof pretype (a (Ident ",")) "comma separated list for type constructor" i in
  57   pretype;;
  58
  59 let parse_preterm_verbose =
  60   let rec pfrees ptm acc =
  61     match ptm with
  62       Varp(v,pty) ->
  63         if v = "" & pty = dpty then acc
  64         else if can get_const_type v or can num_of_string v
  65                 or exists (fun (w,_) -> v = w) (!the_interface) then acc
  66         else insert ptm acc
  67     | Constp(_,_) -> acc
  68     | Combp(p1,p2) -> pfrees p1 (pfrees p2 acc)
  69     | Absp(p1,p2) -> subtract (pfrees p2 acc) (pfrees p1 [])
  70     | Typing(p,_) -> pfrees p acc in
  71   let pdest_eq (Combp(Combp(Varp(("="|"<=>"),_),l),r)) = l,r in
  72   let pmk_let (letbindings,body) =
  73     let vars,tms = unzip (map pdest_eq letbindings) in
  74     let lend = Combp(Varp("LET_END",dpty),body) in
  75     let abs = itlist (fun v t -> Absp(v,t)) vars lend in
  76     let labs = Combp(Varp("LET",dpty),abs) in
  77     rev_itlist (fun x f -> Combp(f,x)) tms labs in
  78   let pmk_vbinder(n,v,bod) =
  79     if n = "\\" then Absp(v,bod)
  80     else Combp(Varp(n,dpty),Absp(v,bod)) in
  81   let pmk_binder(n,vs,bod) =
  82     itlist (fun v b -> pmk_vbinder(n,v,b)) vs bod in
  83   let pmk_set_enum ptms =
  84     itlist (fun x t -> Combp(Combp(Varp("INSERT",dpty),x),t)) ptms
  85            (Varp("EMPTY",dpty)) in
  86   let pgenvar =
  87     let gcounter = ref 0 in
  88     fun () -> let count = !gcounter in
  89               (gcounter := count + 1;
  90                Varp("GEN%PVAR%"^(string_of_int count),dpty)) in
  91   let pmk_exists(v,ptm) = Combp(Varp("?",dpty),Absp(v,ptm)) in
  92   let pmk_list els =
  93     itlist (fun x y -> Combp(Combp(Varp("CONS",dpty),x),y))
  94            els (Varp("NIL",dpty)) in
  95   let pmk_bool =
  96     let tt = Varp("T",dpty) and ff = Varp("F",dpty) in
  97     fun b -> if b then tt else ff in
  98   let pmk_char c =
  99     let lis = map (fun i -> pmk_bool((c / (1 lsl i)) mod 2 = 1)) (0--7) in
 100     itlist (fun x y -> Combp(y,x)) lis (Varp("ASCII",dpty)) in
 101   let pmk_string s =
 102     let ns = map (fun i -> Char.code(String.get s i))
 103                  (0--(String.length s - 1)) in
 104     pmk_list(map pmk_char ns) in
 105   let pmk_setcompr (fabs,bvs,babs) =
 106     let v = pgenvar() in
 107     let bod = itlist (curry pmk_exists) bvs
 108                      (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
 109     Combp(Varp("GSPEC",dpty),Absp(v,bod)) in
 110   let pmk_setabs (fabs,babs) =
 111     let evs =
 112       let fvs = pfrees fabs []
 113       and bvs = pfrees babs [] in
 114       if length fvs <= 1 or bvs = [] then fvs
 115       else intersect fvs bvs in
 116     pmk_setcompr (fabs,evs,babs) in
 117   let rec mk_precedence infxs prs inp =
 118     match infxs with
 119       (s,(p,at))::_ ->
 120           let topins,rest = partition (fun (s',pat') -> pat' = (p,at)) infxs in
 121           (if at = "right" then rightbin else leftbin)
 122           (mk_precedence rest prs)
 123           (end_itlist (||) (map (fun (s,_) -> a (Ident s)) topins))
 124           (fun (Ident op) x y -> Combp(Combp(Varp(op,dpty),x),y))
 125           ("preterm after binary operator ("^s^")")
 126           inp
 127     | _ -> prs inp in
 128   let pmk_geq s t = Combp(Combp(Varp("GEQ",dpty),s),t) in
 129   let pmk_pattern ((pat,guards),res) =
 130     let x = pgenvar() and y = pgenvar() in
 131     let vs = pfrees pat []
 132     and bod =
 133      if guards = [] then
 134        Combp(Combp(Varp("_UNGUARDED_PATTERN",dpty),pmk_geq pat x),
 135              pmk_geq res y)
 136      else
 137        Combp(Combp(Combp(Varp("_GUARDED_PATTERN",dpty),pmk_geq pat x),
 138                    hd guards),
 139              pmk_geq res y) in
 140     Absp(x,Absp(y,itlist (curry pmk_exists) vs bod)) in
 141   let pretype = parse_pretype_verbose
 142   and string inp =
 143     match inp with
 144       Ident s::rst when String.length s >= 2 &
 145                         String.sub s 0 1 = "\"" &
 146                         String.sub s (String.length s - 1) 1 = "\""
 147        -> String.sub s 1 (String.length s - 2),rst
 148     | _ -> raise Noparse
 149   and singleton1 x = [x]
 150   and lmk_ite (((((_,b),_),l),_),r) =
 151           Combp(Combp(Combp(Varp("COND",dpty),b),l),r)
 152   and lmk_typed =
 153     function (p,[]) -> p | (p,[ty]) -> Typing(p,ty) | _ -> fail()
 154   and lmk_let (((_,bnds),_),ptm) = pmk_let (bnds,ptm)
 155   and lmk_binder ((((s,h),t),_),p) = pmk_binder(s,h::t,p)
 156   and lmk_setenum(l,_) = pmk_set_enum l
 157   and lmk_setabs(((l,_),r),_) = pmk_setabs(l,r)
 158   and lmk_setcompr(((((f,_),vs),_),b),_) =
 159      pmk_setcompr(f,pfrees vs [],b)
 160   and lmk_decimal ((_,l0),ropt) =
 161     let l,r = if ropt = [] then l0,"1" else
 162               let r0 = hd ropt in
 163               let n_l = num_of_string l0
 164               and n_r = num_of_string r0 in
 165               let n_d = power_num (Int 10) (Int (String.length r0)) in
 166               let n_n = n_l */ n_d +/ n_r in
 167               string_of_num n_n,string_of_num n_d in
 168      Combp(Combp(Varp("DECIMAL",dpty),Varp(l,dpty)),Varp(r,dpty))
 169   and lmk_univ((_,pty),_) =
 170     Typing(Varp("UNIV",dpty),Ptycon("fun",[pty;Ptycon("bool",[])]))
 171   and any_identifier =
 172     function
 173         ((Ident s):: rest) -> s,rest
 174       | _ -> raise Noparse
 175   and identifier =
 176     function
 177        ((Ident s):: rest) ->
 178         if can get_infix_status s or is_prefix s or parses_as_binder s
 179         then raise Noparse else s,rest
 180       | _ -> raise Noparse
 181   and binder =
 182     function
 183         ((Ident s):: rest) ->
 184         if parses_as_binder s then s,rest else raise Noparse
 185       | _ -> raise Noparse
 186   and pre_fix =
 187     function
 188         ((Ident s):: rest) ->
 189         if is_prefix s then s,rest else raise Noparse
 190       | _ -> raise Noparse in
 191   let rec preterm i =
 192     mk_precedence (infixes()) (typed_appl_preterm) i
 193   and nocommapreterm i =
 194     let infs = filter (fun (s,_) -> s <> ",") (infixes()) in
 195     mk_precedence infs typed_appl_preterm i
 196   and typed_appl_preterm i =
 197     (appl_preterm ++
 198      possibly (a (Resword ":") ++ pretype >> snd)
 199     >> lmk_typed) i
 200   and appl_preterm i =
 201     (pre_fix ++ appl_preterm
 202     >> (fun (x,y) -> Combp(Varp(x,dpty),y))
 203   || binder_preterm ++ many binder_preterm >>
 204         (fun (h,t) -> itlist (fun x y -> Combp(y,x)) (rev t) h)) i
 205   and binder_preterm i =
 206     (a (Resword "let") ++
 207      leftbin (preterm >> singleton1) (a (Resword "and")) (K (@)) "binding" ++
 208      a (Resword "in") ++
 209      preterm
 210     >> lmk_let
 211   || binder ++
 212      typed_apreterm ++
 213      many typed_apreterm ++
 214      a (Resword ".") ++
 215      preterm
 216     >> lmk_binder
 217   || atomic_preterm) i
 218   and typed_apreterm i =
 219     (atomic_preterm ++
 220      possibly (a (Resword ":") ++ pretype >> snd)
 221     >> lmk_typed) i
 222   and atomic_preterm i =
 223     (try_user_parser
 224   || (a (Resword "(") ++ a (Resword ":")) ++ pretype ++ a (Resword ")")
 225     >> lmk_univ
 226   || (a (Resword "(") ++ a (Resword ":")) ++ pretype
 227     >>(fun _ -> failwith "closing right parenthesis on universe expected")
 228   || (a (Resword "(") ++ a (Resword ":"))
 229     >>(fun _ -> failwith "pretype in universe construction expected")
 230   || string
 231      >> pmk_string
 232   || a (Resword "(") ++
 233      (any_identifier >> (fun s -> Varp(s,dpty))) ++
 234      a (Resword ")")
 235     >> (snd o fst)
 236   || a (Resword "(") ++
 237      preterm ++
 238      a (Resword ")")
 239     >> (snd o fst)
 240 (*    || a (Resword "(") ++
 241      preterm >> (fun _ -> failwith "closing right parenthesis expected")
 242    || a (Resword "(") >> (fun _ -> failwith "preterm following left parenthesis expected") *)
 243  || a (Resword "if") ++
 244      preterm ++
 245      a (Resword "then") ++
 246      preterm ++
 247      a (Resword "else") ++
 248      preterm
 249      >> lmk_ite
 250     ||  (a (Resword "if") ) ++ preterm ++ a (Resword "then") ++ preterm ++ a (Resword "else") >> (fun _ -> failwith "malformed else clause")
 251     ||  (a (Resword "if") ) ++ preterm ++ a (Resword "then") ++ preterm  >> (fun _ -> failwith "missing else following then clause")
 252     ||  (a (Resword "if") ) ++ preterm ++ a (Resword "then")   >> (fun _ -> failwith "malformed then clause in if-then-else statement")
 253     ||  (a (Resword "if") ) ++ preterm    >> (fun _ -> failwith "missing 'then' reserved word if-then-else statement")
 254     ||  (a (Resword "if") ) >> (fun _ -> failwith "malformed if-then-else")
 255   || a (Resword "[") ++
 256      elistof preterm (a (Resword ";")) "semicolon separated list of preterms" ++
 257      a (Resword "]")
 258     >> (pmk_list o snd o fst)
 259   || a (Resword "[") ++
 260      elistof preterm (a (Resword ";")) "semicolon separated list of preterms"
 261       >> (fun _ -> failwith "closing square bracket on list expected")
 262   || a (Resword "{") ++
 263      (elistof nocommapreterm (a (Ident ",")) "comma separated list of preterms" ++  a (Resword "}")
 264             >> lmk_setenum
 265       || preterm ++ a (Resword "|") ++ preterm ++ a (Resword "}")
 266             >> lmk_setabs
 267       || preterm ++ a (Resword "|") ++ preterm ++
 268          a (Resword "|") ++ preterm ++ a (Resword "}")
 269             >> lmk_setcompr)
 270     >> snd
 271     || a (Resword "{") >> (fun _ -> failwith "malformed set {}")
 272   || a (Resword "match") ++ preterm ++ a (Resword "with") ++ clauses
 273      >> (fun (((_,e),_),c) -> Combp(Combp(Varp("_MATCH",dpty),e),c))
 274  || a (Resword "match")  >> (fun _ -> failwith "malformed match-with statement")
 275   || a (Resword "function") ++ clauses
 276      >> (fun (_,c) -> Combp(Varp("_FUNCTION",dpty),c))
 277  || a (Resword "function")  >> (fun _ -> failwith "malformed function and pattern clauses")
 278   || a (Ident "#") ++ identifier ++
 279      possibly (a (Resword ".") ++ identifier >> snd)
 280     >> lmk_decimal
 281   || a (Ident "#")  >> (fun _ -> failwith "malformed numerical # identifier")
 282   || identifier
 283     >> (fun s -> Varp(s,dpty))) i
 284   and pattern i =
 285     (preterm ++ possibly (a (Resword "when") ++ preterm >> snd)) i
 286   and clause i =
 287    ((pattern ++ (a (Resword "->") ++ preterm >> snd)) >> pmk_pattern) i
 288   and clauses i =
 289    ((possibly (a (Resword "|")) ++
 290      listof clause (a (Resword "|")) "pattern-match clause" >> snd)
 291     >> end_itlist (fun s t -> Combp(Combp(Varp("_SEQPATTERN",dpty),s),t))) i in
 292   (fun inp ->
 293     match inp with
 294       [Ident s] -> Varp(s,dpty),[]
 295     | _ -> preterm inp);;
 296
 297 end;;