Commits

yoshihiro503  committed eba044c

ワンライナー

  • Participants
  • Parent commits 350c744

Comments (0)

Files changed (8)

File onelinercoq/base/cgi.ml

+open Util
+
+type html = string
+let html_show = id
+
+let url_decode text =
+  let parce_char c = match c with
+  | '0'..'9' -> int_of_char c - int_of_char '0'
+  | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
+  | 'A'..'F' -> 10 + int_of_char c - int_of_char 'A'
+  | _ -> failwith ("decode parce_char: " ^ String.make 1 c)
+  in
+  let rec aux i s =
+    if i < String.length s then
+      match s.[i] with
+      | '+' -> (s.[i] <- ' '; aux (i+1) s)
+      | '%' -> String.sub s 0 i
+          ^ String.make 1 (char_of_int (16 * parce_char s.[i+1] + parce_char s.[i+2]))
+          ^ aux 0 (String.sub s (i+3) (String.length s - i - 3))
+      | _ -> aux (i+1) s
+    else s
+  in aux 0 text
+
+type request = {
+    params: (string * string) list;
+  }
+type response =
+  | HtmlResponse of html
+  | RedirectResponse of string
+  | RowResponse of string
+
+let print_header() =
+  print_endline "Content-type: text/html";
+  print_endline ""
+
+let split2 d s =
+  match Str.split (Str.regexp d) s with
+  | [] -> ("", "")
+  | x::xs -> (x, String.concat d xs)
+
+let get_params () = 
+  try 
+    Sys.getenv "QUERY_STRING"
+    |> Str.split (Str.regexp "&")
+    |> List.map (split2 "=")
+    |> List.map (fun (k,v) -> (k, url_decode v))
+  with e -> failwith "no QUERY_STRING"
+
+let param req s =
+  Some (List.assoc s req.params)
+
+let wrap snippet =
+  try
+    let req = {params=get_params()} in
+    match snippet req with
+    | HtmlResponse html ->
+	print_header();
+	print_string (html_show html)
+    | RedirectResponse url ->
+	()(*TODO*)
+    | RowResponse s ->
+        print_string s
+  with
+  | e ->
+      print_header();
+      print_endline (Printexc.to_string e)
+
+let html_tmpl body =
+  "<html><head>" ^
+  "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />" ^
+"<!-- Google Analytics -->
+<script type=\"text/javascript\">
+
+  var _gaq = _gaq || [];
+  _gaq.push(['_setAccount', 'UA-6143321-8']);
+  _gaq.push(['_trackPageview']);
+
+  (function() {
+    var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
+    ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
+    var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
+  })();
+
+</script>
+<!-- Google Analytics -->" ^
+  "</head><body>" ^ body ^
+"<!-- Google Adsense -->
+<script type=\"text/javascript\"><!--
+google_ad_client = \"ca-pub-4153537904762514\";
+/* ProofServer用バナー */
+google_ad_slot = \"0277579020\";
+google_ad_width = 728;
+google_ad_height = 15;
+//-->
+</script>
+<script type=\"text/javascript\"
+src=\"http://pagead2.googlesyndication.com/pagead/show_ads.js\">
+</script>
+<!-- Google Adsense -->" ^
+  "</body>" ^ "</html>"
+  
+let html_resp html = HtmlResponse html
+  
+	

File onelinercoq/base/llist.ml

+open Lazy
+open Util
+
+type 'a llist = Nil | Cons of 'a * 'a llist Lazy.t
+
+let hd = function | Nil -> failwith "hd" | Cons (x, xs) -> x
+let tl = function | Nil -> failwith "tl" | Cons (x, xs) -> !$xs
+
+let rec map f = function
+  | Nil -> Nil
+  | Cons (x, xs) -> Cons (f x, lazy (map f !$xs))
+
+let rec (++) xs ys =
+  match xs with
+  | Nil -> ys
+  | Cons(x, xs') -> Cons(x, lazy (!$xs' ++ ys))
+
+let rec concat = function
+  | Nil -> Nil
+  | Cons(Nil, tail) -> concat !$tail
+  | Cons(Cons(x,xs), tail) -> Cons(x, lazy(concat(Cons(!$xs, tail))))
+
+let concat_map f xs = concat (map f xs)
+
+(* llist <--> list *)
+let rec of_list = function
+  | [] -> Nil
+  | x::xs -> Cons(x, lazy (of_list xs))
+
+let rec take n l =
+  match n, l with
+  | 0, _ -> []
+  | n, Nil -> []
+  | n, Cons (x, xs) -> x :: take (n-1) !$xs
+
+(* int llist *)
+let rec from n = Cons (n, lazy (from (n+1)))
+
+let rec (--) a b =
+  if b - a < 0 then Nil
+  else Cons(a, lazy ((a+1) -- b))
+
+(* llist <--> stream *)
+let rec of_stream str =
+  try
+    Cons (Stream.next str, lazy (of_stream str))
+  with
+  | Stream.Failure -> Nil
+
+let sllist ?(items:int=20) delim show l =
+  let fin = take items l in
+  if List.length fin <= items then
+    slist delim show fin
+  else
+    slist delim show fin ^ "..."
+
+(* string -> llist *)
+let of_string =
+  of_stream $ Stream.of_string
+
+
+(* llist Monad *)
+
+let return x = Cons(x, lazy Nil)
+let (>>=) m f = concat_map f m
+let guard b = if b then return () else Nil

File onelinercoq/base/parserMonad.ml

+open Util
+open Llist
+
+type ts = char llist
+type state = int * int * (char list * char * char list)
+type error = state * string
+type 'a parser = state -> ts -> ('a * state * ts, error) either
+
+exception ParseError of string
+
+let lt_pos (l1,p1,_) (l2,p2,_) =
+  if l1 < l2 then true
+  else if l1 = l2 then p1 < p2
+  else false
+
+let eplus (st1,msg1) (st2,msg2) =
+  if lt_pos st1 st2 then (st2,msg2) else (st1,msg1)
+
+let showerr ((line,pos,(pre,c,post)),msg) =
+  !%"{\n  line %d, %d: %s\n%s[%c]%s\n}"line pos msg (string_of_chars pre)
+  c (string_of_chars post)
+    
+let return : 'a -> 'a parser =
+    fun x ->
+      fun state code -> Inl (x, state, code)
+
+
+let error msg = fun state _code -> Inr (state, msg)
+
+let (>>=) : 'a parser -> ('a -> 'b parser) -> 'b parser =
+    fun p f ->
+      fun state code ->
+	match p state code with
+	| Inl (x, state', ts) -> f x state' ts
+	| Inr err -> Inr err
+	      
+let (>>) : 'a parser -> 'b parser -> 'b parser =
+    fun p1 p2 ->
+      p1 >>= fun _ -> p2
+
+let (<<) : 'a parser -> 'b parser -> 'a parser =
+    fun p1 p2 ->
+      p1 >>= fun x -> p2 >> return x
+
+let ( ^? ) : 'a parser -> string -> 'a parser =
+    fun p msg ->
+      fun state code ->
+	match p state code with
+	| Inl l -> Inl l
+	| Inr (st,msg0) -> Inr (st,msg ^": "^msg0)
+    
+    (* (<|>) : 'a m -> 'a m -> 'a m *)
+let (<|>) : 'a parser -> 'a parser -> 'a parser =
+    fun p1 p2 ->
+      fun state code ->
+	match p1 state code with
+	| Inl (x1, state', ts) -> Inl (x1, state', ts)
+	| Inr err1 ->
+	    begin match p2 state code with
+	    | Inl (x2, state', ts) -> Inl (x2,state',ts)
+	    | Inr err2 -> Inr (eplus err1 err2)
+	    end
+
+(*
+let (<|?>) p1 p2 = fun state code ->
+  match p1 state code with
+  | Inl (x1, state', ts) -> Inl (x1, state', ts)
+  | Inr err1 ->
+      print_endline err1;
+      begin match p2 state code with
+      | Inl (x2, state', ts) -> Inl (x2,state',ts)
+      | Inr err2 -> Inr (eplus err1 err2)
+      end
+*)	
+
+let rec many : 'a parser -> ('a list) parser =
+    fun p ->
+      (p >>= fun x -> many p >>= fun xs -> return (x::xs))
+	<|> (return [])
+
+let many1 p =
+  p >>= fun x -> many p >>= fun xs -> return (x::xs)
+
+let sep separator p =
+  (p >>= fun x -> many (separator >> p) >>= fun xs -> return (x::xs))
+    <|> (return [])
+
+
+let opt : 'a parser -> ('a option) parser =
+    fun p ->
+      (p >>= fun x -> return (Some x)) <|> (return None)
+
+
+let char1_with_debug state = function
+  | Nil -> Inr (state,"(Nil)")
+  | Cons (x,xs) ->
+      let next (pre,x0, _) =
+	let pre' = if List.length pre < 100 then pre @ [x0]
+	  else List.tl pre @ [x0]
+	in
+	(pre' , x, Llist.take 100 !$xs)
+      in
+      match x, state with
+      | '\n', (line,pos,cs) ->
+	  Inl (x,(line+1,-1, next cs), !$xs)
+      | _, (line,pos,cs) ->
+	  Inl (x,(line, pos+1, next cs),!$xs)
+
+let char1_without_debug state = function
+  | Nil -> Inr (state,"(Nil)")
+  | Cons (x,xs) -> Inl (x, state, !$xs)
+
+let char1 = char1_with_debug
+
+let char_when f = char1 >>= fun c ->
+  if f c then return c
+  else error (!%"(char:'%c')" c)
+
+let char c = char_when ((=) c)
+
+let keyword w =
+  let rec iter i =
+    if i < String.length w then
+      char w.[i] >> iter (i+1)
+    else return w
+  in
+  iter 0
+
+let make_ident f =
+  many1 (char_when f) >>= fun cs ->
+    return (string_of_chars cs)
+
+let int =
+  opt (char '-') >>= fun minus ->
+  make_ident (function '0'..'9' -> true | _ -> false) >>= fun s ->
+  return
+    begin match minus with
+    | None -> int_of_string s
+    | Some _ -> - int_of_string s
+    end
+
+let run p state ts =
+  match p state ts with
+  | Inl (x,state',xs) -> x
+  | Inr err -> 
+      raise (ParseError (showerr err))
+
+let init_state = (1, 0, ([],'_',[]))
+
+let run_ch p ch =
+  run p init_state (Llist.of_stream (Stream.of_channel ch))
+
+let run_stdin p = run_ch p stdin
+
+let run_file p filename =
+  open_in_with filename (fun ch -> run_ch p ch)
+
+let run_string p s =
+  run p init_state (Llist.of_string s)

File onelinercoq/base/util.ml

+let (@@) f x = f x
+let ($) g f = fun x -> g (f x)
+let id x = x
+let p = Printf.printf
+let pr = print_endline
+let tee f x = ignore @@ f x; x
+let (|>) x f = f x
+let const c = fun _ -> c
+
+let (!%) = Printf.sprintf
+let (!$) x = Lazy.force x
+
+let (--) a b =
+  let rec iter store a bi =
+    if a = bi then bi::store
+    else iter (bi::store) a (bi - 1)
+  in
+  if a <= b then iter [] a b
+  else List.rev @@ iter [] b a
+
+let rec repeat n f x =
+  if n > 0 then
+    (f x; repeat (n-1) f x)
+  else ()
+
+let list_concatmap f xs = List.concat (List.map f xs)
+
+let sint   = string_of_int
+let sfloat = string_of_float
+let sbool  = string_of_bool
+
+let string_foldr f s a0 =
+  let rec iter i a =
+    if i >= 0 then
+      iter (i-1) (f s.[i] a)
+    else a
+  in
+  iter (String.length s - 1) a0
+
+let string_iter f s =
+  for i=0 to String.length s - 1 do f s.[i] done
+
+let slist delim show l =
+  String.concat delim @@ List.map show l
+
+let chars_of_string s =
+  let rec iter n =
+    if n >= String.length s then
+      []
+    else 
+      s.[n] :: iter (n+1)
+  in 
+  iter 0
+
+let string_of_chars = slist "" (String.make 1)
+
+let string1 c = String.make 1 c
+
+let mapi f l =
+  List.rev @@ snd @@
+  List.fold_left (fun (i,store) b -> (i+1,f i b::store)) (0,[]) l
+
+let iteri f l =
+  ignore @@ List.fold_left (fun i x -> f i x; (i+1)) 0 l
+
+type ('l, 'r) either = Inl of 'l | Inr of 'r
+
+let list_of_hash t = Hashtbl.fold (fun k v store -> (k,v) :: store) t []
+
+let list_filter_map f xs =
+  List.rev @@ List.fold_left (fun ys x ->
+    match f x with
+    | Some y -> y::ys
+    | None -> ys) [] xs
+
+let maybe f x =
+  try Inl (f x) with e -> Inr e
+let value = function
+    Inl v -> v | Inr e -> raise e
+let value_or default = function
+  | Inl v -> v | Inr _ -> default
+
+module Option = struct
+  type 'a t = 'a option
+  let some x = Some x
+  let none = None
+      
+  let of_either = function
+    | Inl x -> Some x
+    | Inr _ -> None
+
+  let map f = function
+    | Some x -> Some (f x)
+    | None -> None
+
+  let sopt show = function
+    | Some x -> show x
+    | None -> "None"
+
+  let opt_min x y =
+    match x, y with
+    | Some x, Some y -> Some (min x y)
+    | x, None -> x
+    | None, y -> y
+
+  let maybe f x = of_either @@ maybe f x
+  let get_or_else default = function
+    | Some x -> x
+    | None -> default
+end
+
+let open_with (opn, close) filepath f =
+  let ch = opn filepath in
+  value @@ tee (fun _ -> close ch) (maybe f ch)
+let open_in_with filepath f = open_with (open_in, close_in) filepath f
+let open_out_with filepath f = open_with (open_out, close_out) filepath f
+
+let read_all ch =
+  let rec iter store =
+    try iter @@ input_line ch :: store with
+    | End_of_file -> List.rev store
+  in
+  iter []
+
+let read_file filename = slist "\n" id @@ open_in_with filename read_all
+
+let just default = function
+  | Some x -> x
+  | None -> default
+
+let random_int =
+  Random.self_init ();
+  Random.int
+
+let to_hex n =
+  let to_char = function
+    | x when 0<=x && x<=9 -> (string_of_int x).[0]
+    | x when 10<=x && x<=15 -> char_of_int (int_of_char 'A'+(x-10))
+    | _ -> failwith"tohex MNH"
+  in
+  let rec iter store n =
+    if n < 16 then
+      to_char n :: store
+    else
+      let r,q = n / 16, n mod 16 in
+      iter (to_char q :: store) r
+  in
+  if n < 0 then raise (Invalid_argument (!%"to_hex: (%d)" n))
+  else string_of_chars @@ iter [] n
+
+open Unix
+module Date = struct
+  type t = float
+  let make year mon day h m s =
+    fst (mktime { tm_sec=s; tm_min=m; tm_hour=h;
+      tm_mday=day; tm_mon=mon-1; tm_year=year-1900;
+      tm_wday=0; tm_yday=0; tm_isdst=false
+    })
+  let make_from_gmt year mon day h m s =
+    let diff =  fst (mktime (gmtime 0.)) in
+    make year mon day h m s -. diff
+  let now : unit -> t = Unix.time
+  let year t = (localtime t).tm_year + 1900
+  let mon t = (localtime t).tm_mon + 1
+  let day t = (localtime t).tm_mday
+  let hour t = (localtime t).tm_hour
+  let min t = (localtime t).tm_min
+  let sec t = (localtime t).tm_sec
+  let lt d1 d2 = d1 < d2
+  let to_string t = !%"%4d/%02d/%02d %02d:%02d:%02d" (year t) (mon t) (day t)
+      (hour t) (min t) (sec t)
+  let pmonth = function
+    | "Jan" ->  1
+    | "Feb" ->  2
+    | "Mar" ->  3
+    | "Apr" ->  4
+    | "May" ->  5
+    | "Jun" ->  6
+    | "Jul" ->  7
+    | "Aug" ->  8
+    | "Sep" ->  9
+    | "Oct" -> 10
+    | "Nov" -> 11
+    | "Dec" -> 12
+    | unknown ->
+	raise (Invalid_argument ("Date.pmonth: unknown month ["^unknown^"]"))
+  let of_string s =
+    let year = String.sub s 0  4 |> int_of_string in
+    let mon  = String.sub s 5  2 |> int_of_string in
+    let day  = String.sub s 8  2 |> int_of_string in
+    let h    = String.sub s 11 2 |> int_of_string in
+    let m    = String.sub s 14 2 |> int_of_string in
+    let s    = String.sub s 17 2 |> int_of_string in
+    make year mon day h m s
+end

File onelinercoq/base/xml.ml

+open Util
+open ParserMonad
+
+let escape s =
+  let buf = Buffer.create 0 in
+  let f = function
+    | '<' -> "&lt;"
+    | '>' -> "&gt;"
+    | '&' -> "&amp;"
+    | '\"' -> "&quot;"
+    | '\'' -> "&apos;"
+    | c -> String.make 1 c
+  in
+  string_iter (fun c -> Buffer.add_string buf (f c)) s;
+  Buffer.contents buf
+
+let unescape s =
+  let buf = Buffer.create (String.length s) in
+  let next = function
+    | '&'::'l'::'t'::';'::cs -> ('<', cs)
+    | '&'::'g'::'t'::';'::cs -> ('>', cs)
+    | '&'::'a'::'m'::'p'::';'::cs -> ('&', cs)
+    | '&'::'q'::'u'::'o'::'t'::';'::cs -> ('\"', cs)
+    | '&'::'a'::'p'::'o'::'s'::';'::cs -> ('\'', cs)
+    | c::cs -> (c, cs)
+    | [] -> failwith "unescape"
+  in
+  let rec iter = function
+    | [] -> ()
+    | _::_ as cs ->
+        let (c, cs') = next cs in
+        Buffer.add_char buf c;
+        iter cs'
+  in
+  iter (chars_of_string s);
+  Buffer.contents buf
+
+type attr = string * string
+type xml =
+  | Tag of string * attr list * xml list
+  | PCData of string
+
+let show xml =
+  let indent d = String.make (2*d) ' ' in
+  let rec iter d = function
+    | Tag (name,attrs,body) ->
+	indent d ^ "<"^name^" "^slist " " (fun(k,v)->k^"="^v) attrs^">\n"
+	^slist "\n" (iter (d+1)) body
+	^indent d^"</"^name^">"
+    | PCData s -> indent d ^ "PCData("^s^")"
+  in
+  iter 0 xml
+	    
+let whitespace =
+  let whites = [' '; '\t'; '\n'; '\r'] in
+  (many @@ char_when (fun c -> List.mem c whites))
+
+let ident =
+  let igs = ['<'; '>'; '?'; '/'; ' '; '\t'; '\r'; '\n'] in
+  whitespace >>
+  (many1 @@ char_when (fun c -> List.mem c igs = false)) >>=
+  (return $ string_of_chars)
+
+let pattr : attr parser =
+  let k_char c =
+    List.mem c ['='; '<'; '>'; '?'; '/'; ' '; '\t'; '\r'; '\n'] = false
+  in
+  let ident0 = many (char_when ((<>) '\"')) >>= (return $ string_of_chars) in
+    whitespace >> make_ident k_char >>= fun k -> char '=' >> char '\"' >>
+    ident0 << char '\"' >>= fun v -> return (k,unescape(v))
+
+let pcdata =
+  let igs = ['<'; '>'] in
+  whitespace >>
+  (many1 @@ char_when (fun c -> List.mem c igs = false)) >>= fun cs ->
+    return @@ PCData(unescape (string_of_chars cs))
+
+let cdata =
+  keyword "<![CDATA[" >> many (char_when ((<>) ']')) << keyword "]]>" >>=
+  fun cs -> return (PCData (string_of_chars cs))
+    
+let rec parser =
+    let rec iter () =
+      let top = char '<' >> char '?' >> many ident >> whitespace >> char '?' >>
+        char '>' >>= fun _ -> iter()
+      in
+      let tag1 = char '<' >> ident >>= fun name ->
+	many pattr << char '>' >>= fun attrs ->
+	many (iter()) >>= fun children ->
+	whitespace >> char '<' >> char '/' >> ident << char '>' >>= fun name' ->
+	return (Tag(name, attrs, children))
+      in
+      let tag2 = char '<' >> ident >>= fun name ->
+	many pattr << whitespace << char '/' << char '>' >>= fun attrs ->
+	return (Tag(name, attrs, []))
+      in
+      whitespace >> (cdata <|> top <|> tag1^?"tag1" <|> tag2^?"tag2" <|> pcdata)
+    in
+    iter() ^? "xml"
+    
+let parse_ch = run_ch parser
+let parse_file = run_file parser
+let parse_string s = try run_string parser s with e -> prerr_endline ("[[[\n"^s^"\n]]]\n"); raise e
+let getname = function
+  | Tag(name, _, _) -> name
+  | PCData s -> failwith("getname: PCData("^s^")")
+
+let getchild name : xml -> xml = function
+  | Tag(_, _, xmls) ->
+      begin try List.find (fun x -> getname x = name) xmls with
+      | e -> failwith ("getchild: notfound:\""^name^"\":\n"^slist"\n"show xmls)
+      end
+  | PCData s -> failwith("getchild: PCData("^s^")")
+let (%%) xml name = getchild name xml
+let getchildren : xml -> xml list = function
+  | Tag(_, _, xmls) -> xmls
+  | PCData s -> failwith("getchildren: PCData("^s^")")
+
+let pcdata = function
+  | Tag(_, _, _) -> failwith("pcdata:")
+  | PCData s -> s
+let childpc = function
+  | Tag(_, _, PCData s::_) -> s
+  | Tag(_, _, _) -> failwith("childpc: Tag()")
+  | PCData s -> failwith("childpc: PCData("^s^")")
+
+let (%%%) xml name = childpc (xml %% name)
+let (%%<) xml name = getchildren (xml %% name)
+
+let attr name = function
+  | Tag(_, attrs, _) when List.mem_assoc name attrs ->
+      List.assoc name attrs
+  | Tag(_, attrs, _) -> failwith("attr: not member("^name^")")
+  | PCData s -> failwith("attr: PCData("^s^")")

File onelinercoq/comp.sh

+#!/bin/sh
+lib=base
+ocamlc -I $lib unix.cma str.cma $lib/util.ml $lib/cgi.ml \
+    $lib/llist.ml $lib/parserMonad.ml $lib/xml.ml \
+    main.ml -o main.cgi

File onelinercoq/deploy

+#!/bin/sh
+cp index.cgi /usr/lib/cgi-bin/coqtop/

File onelinercoq/main.ml

+open Util
+open Cgi
+
+let cmd s write read =
+  let (in_, out, err) = Unix.open_process_full s [||] in
+  let b = ref "" in
+  try
+    b := "write";
+    write out;
+    b := "read";
+    let y = read in_ in
+    b := "reade";
+    let error = read err in
+    b := "close";
+    ignore @@ Unix.close_process_full (in_, out, err);
+    (y, error)
+  with
+  | e ->
+      let msg = ("cmd: "^s^": "^ !b^": "^Printexc.to_string e) in
+      ignore @@ Unix.close_process_full (in_, out, err);
+      failwith (msg)
+
+    
+let coq s =
+  let outs, errs = cmd "/usr/local/bin/coqtop" 
+    (fun ch ->
+      output_string ch (!%"%s\n" s);
+      flush ch;
+      ignore @@ close_out ch)
+    (fun ch -> read_all ch)
+  in
+  slist "\n" id outs, slist "\n" id errs
+
+let snippet req =
+  let q = param req "s" |> Option.get_or_else "" in
+  let header = "Content-type: text/javascript\n\n" in
+  let stdout,stderr = coq q in
+  let body = !%"callback({\"stdout\":\"%s\"; \"stderr\":\"%s\"})" stdout stderr in
+  RowResponse (header ^ body)
+
+(*
+let snippet req =
+  let q = param req "q" |> Option.get_or_else "" in
+  let (rs,_) = search_pattern q in
+  let body =
+    "<h1>Cochin</h1>"
+    ^ "<form action=\"search.cgi\" method=\"GET\">"
+    ^ "<p><input name=\"q\" size=\"45\"/><input type=\"submit\"/></p>"
+    ^ "</form>"
+    ^ "<pre>"
+    ^ slist "\n" Xml.escape rs
+    ^ "</pre>"
+  in
+  html_tmpl body |> html_resp
+
+let _ =
+  wrap snippet
+*)
+let _ =
+  wrap snippet