(* ========================================================================= *) (* Lexical analyzer, type and preterm parsers. *) (* *) (* John Harrison, University of Cambridge Computer Laboratory *) (* *) (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) (* ========================================================================= *) needs "preterm.ml";; (* ------------------------------------------------------------------------- *) (* Need to have this now for set enums, since "," isn't a reserved word. *) (* ------------------------------------------------------------------------- *) parse_as_infix (",",(14,"right"));; (* ------------------------------------------------------------------------- *) (* Basic parser combinators. *) (* ------------------------------------------------------------------------- *) exception Noparse;; let (||) parser1 parser2 input = try parser1 input with Noparse -> parser2 input;; let (++) parser1 parser2 input = let result1,rest1 = parser1 input in let result2,rest2 = parser2 rest1 in (result1,result2),rest2;; let rec many prs input = try let result,next = prs input in let results,rest = many prs next in (result::results),rest with Noparse -> [],input;; let (>>) prs treatment input = let result,rest = prs input in treatment(result),rest;; let fix err prs input = try prs input with Noparse -> failwith (err ^ " expected");; let rec listof prs sep err = prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);; let nothing input = [],input;; let elistof prs sep err = listof prs sep err || nothing;; let leftbin prs sep cons err = prs ++ many (sep ++ fix err prs) >> (fun (x,opxs) -> let ops,xs = unzip opxs in itlist2 (fun op y x -> cons op x y) (rev ops) (rev xs) x);; let rightbin prs sep cons err = prs ++ many (sep ++ fix err prs) >> (fun (x,opxs) -> if opxs = [] then x else let ops,xs = unzip opxs in itlist2 cons ops (x::butlast xs) (last xs));; let possibly prs input = try let x,rest = prs input in [x],rest with Noparse -> [],input;; let some p = function [] -> raise Noparse | (h::t) -> if p h then (h,t) else raise Noparse;; let a tok = some (fun item -> item = tok);; let rec atleast n prs i = (if n <= 0 then many prs else prs ++ atleast (n - 1) prs >> (fun (h,t) -> h::t)) i;; let finished input = if input = [] then 0,input else failwith "Unparsed input";; (* ------------------------------------------------------------------------- *) (* The basic lexical classes: identifiers, strings and reserved words. *) (* ------------------------------------------------------------------------- *) type lexcode = Ident of string | Resword of string;; (* ------------------------------------------------------------------------- *) (* Lexical analyzer. Apart from some special bracket symbols, each *) (* identifier is made up of the longest string of alphanumerics or *) (* the longest string of symbolics. *) (* ------------------------------------------------------------------------- *) reserve_words ["//"];; let comment_token = ref (Resword "//");; let lex = let collect (h,t) = end_itlist (^) (h::t) in let reserve = function (Ident n as tok) -> if is_reserved_word n then Resword(n) else tok | t -> t in let stringof p = atleast 1 p >> end_itlist (^) in let simple_ident = stringof(some isalnum) || stringof(some issymb) in let undertail = stringof (a "_") ++ possibly simple_ident >> collect in let ident = (undertail || simple_ident) ++ many undertail >> collect in let septok = stringof(some issep) in let escapecode i = match i with "\\"::rst -> "\\",rst | "\""::rst -> "\"",rst | "\'"::rst -> "\'",rst | "n"::rst -> "\n",rst | "r"::rst -> "\r",rst | "t"::rst -> "\t",rst | "b"::rst -> "\b",rst | " "::rst -> " ",rst | "x"::h::l::rst -> String.make 1 (Char.chr(int_of_string("0x"^h^l))),rst | a::b::c::rst when forall isnum [a;b;c] -> String.make 1 (Char.chr(int_of_string(a^b^c))),rst | _ -> failwith "lex:unrecognized OCaml-style escape in string" in let stringchar = some (fun i -> i <> "\\" & i <> "\"") || (a "\\" ++ escapecode >> snd) in let string = a "\"" ++ many stringchar ++ a "\"" >> (fun ((_,s),_) -> "\""^implode s^"\"") in let rawtoken = (string || some isbra || septok || ident) >> (fun x -> Ident x) in let simptoken = many (some isspace) ++ rawtoken >> (reserve o snd) in let rec tokens i = try let (t,rst) = simptoken i in if t = !comment_token then (many (fun i -> if i <> [] & hd i <> "\n" then 1,tl i else raise Noparse) ++ tokens >> snd) rst else let toks,rst1 = tokens rst in t::toks,rst1 with Noparse -> [],i in fst o (tokens ++ many (some isspace) ++ finished >> (fst o fst));; (* ------------------------------------------------------------------------- *) (* Parser for pretypes. Concrete syntax: *) (* *) (* TYPE :: SUMTYPE -> TYPE *) (* | SUMTYPE *) (* *) (* SUMTYPE :: PRODTYPE + SUMTYPE *) (* | PRODTYPE *) (* *) (* PRODTYPE :: POWTYPE # PRODTYPE *) (* | POWTYPE *) (* *) (* POWTYPE :: APPTYPE ^ POWTYPE *) (* | APPTYPE *) (* *) (* APPTYPE :: ATOMICTYPES type-constructor [Provided arity matches] *) (* | ATOMICTYPES [Provided only 1 ATOMICTYPE] *) (* *) (* ATOMICTYPES :: type-constructor [Provided arity zero] *) (* | type-variable *) (* | ( TYPE ) *) (* | ( TYPE LIST ) *) (* *) (* TYPELIST :: TYPE , TYPELIST *) (* | TYPE *) (* *) (* Two features make this different from previous HOL type syntax: *) (* *) (* o Any identifier not in use as a type constant will be parsed as a *) (* type variable; a ' is not needed and a * is not allowed. *) (* *) (* o Antiquotation is not supported. *) (* ------------------------------------------------------------------------- *) let parse_pretype = let btyop n n' x y = Ptycon(n,[x;y]) and mk_apptype = function ([s],[]) -> s | (tys,[c]) -> Ptycon(c,tys) | _ -> failwith "Bad type construction" and type_atom input = match input with (Ident s)::rest -> (try pretype_of_type(assoc s (type_abbrevs())) with Failure _ -> if try get_type_arity s = 0 with Failure _ -> false then Ptycon(s,[]) else Utv(s)),rest | _ -> raise Noparse and type_constructor input = match input with (Ident s)::rest -> if try get_type_arity s > 0 with Failure _ -> false then s,rest else raise Noparse | _ -> raise Noparse in let rec pretype i = rightbin sumtype (a (Resword "->")) (btyop "fun") "type" i and sumtype i = rightbin prodtype (a (Ident "+")) (btyop "sum") "type" i and prodtype i = rightbin carttype (a (Ident "#")) (btyop "prod") "type" i and carttype i = leftbin apptype (a (Ident "^")) (btyop "cart") "type" i and apptype i = (atomictypes ++ (type_constructor >> (fun x -> [x]) || nothing) >> mk_apptype) i and atomictypes i = (((a (Resword "(")) ++ typelist ++ a (Resword ")") >> (snd o fst)) || type_atom >> (fun x -> [x])) i and typelist i = listof pretype (a (Ident ",")) "type" i in pretype;; (* ------------------------------------------------------------------------- *) (* Hook to allow installation of user parsers. *) (* ------------------------------------------------------------------------- *) let install_parser,delete_parser,installed_parsers,try_user_parser = let rec try_parsers ps i = if ps = [] then raise Noparse else try snd(hd ps) i with Noparse -> try_parsers (tl ps) i in let parser_list = ref([]:(string*(lexcode list -> preterm * lexcode list))list) in (fun dat -> parser_list := dat::(!parser_list)), (fun key -> try parser_list := snd (remove (fun (key',_) -> key = key') (!parser_list)) with Failure _ -> ()), (fun () -> !parser_list), (fun i -> try_parsers (!parser_list) i);; (* ------------------------------------------------------------------------- *) (* Initial preterm parsing. This uses binder and precedence/associativity/ *) (* prefix status to guide parsing and preterm construction, but treats all *) (* identifiers as variables. *) (* *) (* PRETERM :: APPL_PRETERM binop APPL_PRETERM *) (* | APPL_PRETERM *) (* *) (* APPL_PRETERM :: APPL_PRETERM : type *) (* | APPL_PRETERM BINDER_PRETERM *) (* | BINDER_PRETERM *) (* *) (* BINDER_PRETERM :: binder VARSTRUCT_PRETERMS . PRETERM *) (* | let PRETERM and ... and PRETERM in PRETERM *) (* | ATOMIC_PRETERM *) (* *) (* VARSTRUCT_PRETERMS :: TYPED_PRETERM VARSTRUCT_PRETERMS *) (* | TYPED_PRETERM *) (* *) (* TYPED_PRETERM :: TYPED_PRETERM : type *) (* | ATOMIC_PRETERM *) (* *) (* ATOMIC_PRETERM :: ( PRETERM ) *) (* | if PRETERM then PRETERM else PRETERM *) (* | [ PRETERM; .. ; PRETERM ] *) (* | { PRETERM, .. , PRETERM } *) (* | { PRETERM | PRETERM } *) (* | identifier *) (* *) (* Note that arbitrary preterms are allowed as varstructs. This allows *) (* more general forms of matching and considerably regularizes the syntax. *) (* ------------------------------------------------------------------------- *) let parse_preterm = let rec pairwise r l = match l with [] -> true | h::t -> forall (r h) t & pairwise r t in let rec pfrees ptm acc = match ptm with Varp(v,pty) -> if v = "" & pty = dpty then acc else if can get_const_type v or can num_of_string v or exists (fun (w,_) -> v = w) (!the_interface) then acc else insert ptm acc | Constp(_,_) -> acc | Combp(p1,p2) -> pfrees p1 (pfrees p2 acc) | Absp(p1,p2) -> subtract (pfrees p2 acc) (pfrees p1 []) | Typing(p,_) -> pfrees p acc in let pdest_eq (Combp(Combp(Varp(("="|"<=>"),_),l),r)) = l,r in let pmk_let (letbindings,body) = let vars,tms = unzip (map pdest_eq letbindings) in let _ = warn(not (pairwise (fun s t -> intersect(pfrees s []) (pfrees t []) = []) vars)) "duplicate names on left of let-binding: latest is used" in let lend = Combp(Varp("LET_END",dpty),body) in let abs = itlist (fun v t -> Absp(v,t)) vars lend in let labs = Combp(Varp("LET",dpty),abs) in rev_itlist (fun x f -> Combp(f,x)) tms labs in let pmk_vbinder(n,v,bod) = if n = "\\" then Absp(v,bod) else Combp(Varp(n,dpty),Absp(v,bod)) in let pmk_binder(n,vs,bod) = itlist (fun v b -> pmk_vbinder(n,v,b)) vs bod in let pmk_set_enum ptms = itlist (fun x t -> Combp(Combp(Varp("INSERT",dpty),x),t)) ptms (Varp("EMPTY",dpty)) in let pgenvar = let gcounter = ref 0 in fun () -> let count = !gcounter in (gcounter := count + 1; Varp("GEN%PVAR%"^(string_of_int count),dpty)) in let pmk_exists(v,ptm) = Combp(Varp("?",dpty),Absp(v,ptm)) in let pmk_list els = itlist (fun x y -> Combp(Combp(Varp("CONS",dpty),x),y)) els (Varp("NIL",dpty)) in let pmk_bool = let tt = Varp("T",dpty) and ff = Varp("F",dpty) in fun b -> if b then tt else ff in let pmk_char c = let lis = map (fun i -> pmk_bool((c / (1 lsl i)) mod 2 = 1)) (0--7) in itlist (fun x y -> Combp(y,x)) lis (Varp("ASCII",dpty)) in let pmk_string s = let ns = map (fun i -> Char.code(String.get s i)) (0--(String.length s - 1)) in pmk_list(map pmk_char ns) in let pmk_setcompr (fabs,bvs,babs) = let v = pgenvar() in let bod = itlist (curry pmk_exists) bvs (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in Combp(Varp("GSPEC",dpty),Absp(v,bod)) in let pmk_setabs (fabs,babs) = let evs = let fvs = pfrees fabs [] and bvs = pfrees babs [] in if length fvs <= 1 or bvs = [] then fvs else intersect fvs bvs in pmk_setcompr (fabs,evs,babs) in let rec mk_precedence infxs prs inp = match infxs with (s,(p,at))::_ -> let topins,rest = partition (fun (s',pat') -> pat' = (p,at)) infxs in (if at = "right" then rightbin else leftbin) (mk_precedence rest prs) (end_itlist (||) (map (fun (s,_) -> a (Ident s)) topins)) (fun (Ident op) x y -> Combp(Combp(Varp(op,dpty),x),y)) ("term after binary operator") inp | _ -> prs inp in let pmk_geq s t = Combp(Combp(Varp("GEQ",dpty),s),t) in let pmk_pattern ((pat,guards),res) = let x = pgenvar() and y = pgenvar() in let vs = pfrees pat [] and bod = if guards = [] then Combp(Combp(Varp("_UNGUARDED_PATTERN",dpty),pmk_geq pat x), pmk_geq res y) else Combp(Combp(Combp(Varp("_GUARDED_PATTERN",dpty),pmk_geq pat x), hd guards), pmk_geq res y) in Absp(x,Absp(y,itlist (curry pmk_exists) vs bod)) in let pretype = parse_pretype and string inp = match inp with Ident s::rst when String.length s >= 2 & String.sub s 0 1 = "\"" & String.sub s (String.length s - 1) 1 = "\"" -> String.sub s 1 (String.length s - 2),rst | _ -> raise Noparse and singleton1 x = [x] and lmk_ite (((((_,b),_),l),_),r) = Combp(Combp(Combp(Varp("COND",dpty),b),l),r) and lmk_typed = function (p,[]) -> p | (p,[ty]) -> Typing(p,ty) | _ -> fail() and lmk_let (((_,bnds),_),ptm) = pmk_let (bnds,ptm) and lmk_binder ((((s,h),t),_),p) = pmk_binder(s,h::t,p) and lmk_setenum(l,_) = pmk_set_enum l and lmk_setabs(((l,_),r),_) = pmk_setabs(l,r) and lmk_setcompr(((((f,_),vs),_),b),_) = pmk_setcompr(f,pfrees vs [],b) and lmk_decimal ((_,l0),ropt) = let l,r = if ropt = [] then l0,"1" else let r0 = hd ropt in let n_l = num_of_string l0 and n_r = num_of_string r0 in let n_d = power_num (Int 10) (Int (String.length r0)) in let n_n = n_l */ n_d +/ n_r in string_of_num n_n,string_of_num n_d in Combp(Combp(Varp("DECIMAL",dpty),Varp(l,dpty)),Varp(r,dpty)) and lmk_univ((_,pty),_) = Typing(Varp("UNIV",dpty),Ptycon("fun",[pty;Ptycon("bool",[])])) and any_identifier = function ((Ident s):: rest) -> s,rest | _ -> raise Noparse and identifier = function ((Ident s):: rest) -> if can get_infix_status s or is_prefix s or parses_as_binder s then raise Noparse else s,rest | _ -> raise Noparse and binder = function ((Ident s):: rest) -> if parses_as_binder s then s,rest else raise Noparse | _ -> raise Noparse and pre_fix = function ((Ident s):: rest) -> if is_prefix s then s,rest else raise Noparse | _ -> raise Noparse in let rec preterm i = mk_precedence (infixes()) typed_appl_preterm i and nocommapreterm i = let infs = filter (fun (s,_) -> s <> ",") (infixes()) in mk_precedence infs typed_appl_preterm i and typed_appl_preterm i = (appl_preterm ++ possibly (a (Resword ":") ++ pretype >> snd) >> lmk_typed) i and appl_preterm i = (pre_fix ++ appl_preterm >> (fun (x,y) -> Combp(Varp(x,dpty),y)) || binder_preterm ++ many binder_preterm >> (fun (h,t) -> itlist (fun x y -> Combp(y,x)) (rev t) h)) i and binder_preterm i = (a (Resword "let") ++ leftbin (preterm >> singleton1) (a (Resword "and")) (K (@)) "binding" ++ a (Resword "in") ++ preterm >> lmk_let || binder ++ typed_apreterm ++ many typed_apreterm ++ a (Resword ".") ++ preterm >> lmk_binder || atomic_preterm) i and typed_apreterm i = (atomic_preterm ++ possibly (a (Resword ":") ++ pretype >> snd) >> lmk_typed) i and atomic_preterm i = (try_user_parser || (a (Resword "(") ++ a (Resword ":")) ++ pretype ++ a (Resword ")") >> lmk_univ || string >> pmk_string || a (Resword "(") ++ (any_identifier >> (fun s -> Varp(s,dpty))) ++ a (Resword ")") >> (snd o fst) || a (Resword "(") ++ preterm ++ a (Resword ")") >> (snd o fst) || a (Resword "if") ++ preterm ++ a (Resword "then") ++ preterm ++ a (Resword "else") ++ preterm >> lmk_ite || a (Resword "[") ++ elistof preterm (a (Resword ";")) "term" ++ a (Resword "]") >> (pmk_list o snd o fst) || a (Resword "{") ++ (elistof nocommapreterm (a (Ident ",")) "term" ++ a (Resword "}") >> lmk_setenum || preterm ++ a (Resword "|") ++ preterm ++ a (Resword "}") >> lmk_setabs || preterm ++ a (Resword "|") ++ preterm ++ a (Resword "|") ++ preterm ++ a (Resword "}") >> lmk_setcompr) >> snd || a (Resword "match") ++ preterm ++ a (Resword "with") ++ clauses >> (fun (((_,e),_),c) -> Combp(Combp(Varp("_MATCH",dpty),e),c)) || a (Resword "function") ++ clauses >> (fun (_,c) -> Combp(Varp("_FUNCTION",dpty),c)) || a (Ident "#") ++ identifier ++ possibly (a (Resword ".") ++ identifier >> snd) >> lmk_decimal || identifier >> (fun s -> Varp(s,dpty))) i and pattern i = (preterm ++ possibly (a (Resword "when") ++ preterm >> snd)) i and clause i = ((pattern ++ (a (Resword "->") ++ preterm >> snd)) >> pmk_pattern) i and clauses i = ((possibly (a (Resword "|")) ++ listof clause (a (Resword "|")) "pattern-match clause" >> snd) >> end_itlist (fun s t -> Combp(Combp(Varp("_SEQPATTERN",dpty),s),t))) i in (fun inp -> match inp with [Ident s] -> Varp(s,dpty),[] | _ -> preterm inp);; (* ------------------------------------------------------------------------- *) (* Type and term parsers. *) (* ------------------------------------------------------------------------- *) let parse_type s = let pty,l = (parse_pretype o lex o explode) s in if l = [] then type_of_pretype pty else failwith "Unparsed input following type";; let parse_term s = let ptm,l = (parse_preterm o lex o explode) s in if l = [] then (term_of_preterm o (retypecheck [])) ptm else failwith "Unparsed input following term";; let retyvar_funny tm = let tvs = type_vars_in_term tm in let (tvsgood, tvsbad) = List.partition (fun ty -> try (dest_vartype ty).[0] <> '?' with _ -> false) tvs in let tyvno = ref (-1) in let rec nexttv () = incr tyvno; let ret = mk_vartype ("?" ^ string_of_int !tyvno) in if List.mem ret tvsgood then nexttv () else ret in let ins = List.map (fun x -> (nexttv (),x)) tvsbad in inst ins tm ;; let parse_term s = let tm = parse_term s in if type_of tm = bool_ty then retyvar_funny tm else tm ;;