7 let mk_app x y = App(x, y);;
\r
8 let mk_lam x = Lam x;;
\r
9 let mk_var x = Var x;;
\r
11 exception ParsingError of string;;
\r
13 let isAlphaNum c = let n = Char.code c in 48 <= n && n <= 122 ;;
\r
14 let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;
\r
16 let rec index_of x =
\r
18 | [] -> raise (Failure "index_of: Not Found")
\r
19 | h::t -> if x = h then 0 else 1 + index_of x t
\r
22 let mk_var' (bound, free) x =
\r
24 then free, mk_var (index_of x bound)
\r
25 else if List.mem x free
\r
26 then free, mk_var (List.length bound + index_of x free)
\r
27 else (free @ [x]), mk_var (List.length bound + List.length free)
\r
30 let mk_app' = function
\r
31 | [] -> raise (ParsingError "bug")
\r
32 | t :: ts -> List.fold_left mk_app t ts
\r
37 if i < 0 then l else aux (i - 1) (s.[i] :: l)
\r
38 in aux (String.length s - 1) []
\r
42 let res = String.create (List.length l) in
\r
43 let rec aux i = function
\r
45 | c :: l -> res.[i] <- c; aux (i + 1) l in
\r
49 let rec strip_spaces = function
\r
50 | c::cs when isSpace c -> strip_spaces cs
\r
55 let rec aux = function
\r
57 | c::cs as x -> if isAlphaNum c
\r
58 then match aux cs with
\r
59 | (Some x), cs' -> Some (c :: x), cs'
\r
60 | None, cs' -> (Some [c]), cs'
\r
63 | None, y -> None, y
\r
64 | Some x, y -> Some (implode x), y
\r
67 let read_var' (bound, free as vars) s =
\r
68 match read_var s with
\r
69 | Some varname, cs ->
\r
70 let free, v = mk_var' vars varname in
\r
71 Some [v], cs, (bound, free)
\r
72 | _, _ -> raise (ParsingError ("Can't read variable"))
\r
75 let rec read_smt vars =
\r
76 let check_if_lambda cs = match read_var cs with
\r
78 | Some x, cs -> match strip_spaces cs with
\r
81 in let read_lambda (bound, free) cs = (
\r
82 match read_var (strip_spaces cs) with
\r
83 | Some varname, cs ->
\r
84 let vars' = (varname::bound, free) in
\r
85 (match strip_spaces cs with
\r
86 | [] -> raise (ParsingError "manca dopo variabile lambda")
\r
87 | c::cs -> (if c = '.' then (match read_smt vars' cs with
\r
88 | None, _, _ -> raise (ParsingError "manca corpo lambda")
\r
89 | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)
\r
90 | Some _, _, _ -> raise (ParsingError "???")
\r
91 ) else raise (ParsingError "manca . nel lambda")
\r
93 | _, _ -> assert false
\r
94 ) in let rec aux vars cs =
\r
95 match strip_spaces cs with
\r
96 | [] -> None, [], vars
\r
98 let tms, cs, vars = (
\r
99 if c = '(' then read_pars vars x
\r
100 else if c = ')' then (None, x, vars)
\r
101 else if check_if_lambda x then read_lambda vars x
\r
102 else read_var' vars x) in
\r
105 match aux vars cs with
\r
106 | None, cs, vars -> Some [tm], cs, vars
\r
107 | Some ts, cs, vars -> Some (tm :: ts), cs, vars
\r
109 | Some _ -> raise (ParsingError "bug")
\r
110 | None -> None, x, vars
\r
111 in fun cs -> match aux vars cs with
\r
112 | None, cs, vars -> None, cs, vars
\r
113 | Some ts, cs, vars -> Some [mk_app' ts], cs, vars
\r
114 and read_pars vars = function
\r
115 | [] -> None, [], vars
\r
116 | c::cs -> if c = '(' then (
\r
117 let tm, cs, vars = read_smt vars cs in
\r
118 let cs = strip_spaces cs in
\r
120 | [] -> None, [], vars
\r
121 | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError ") mancante")
\r
122 ) else raise (ParsingError "???")
\r
126 match read_smt ([],[]) (explode x) with
\r
127 | Some [y], [], _ -> y
\r
128 | _, _, _ -> raise (ParsingError "???")
\r
131 let var_zero = "ω";; (* w is an invalid variable name *)
\r
133 let parse_many strs =
\r
134 let f (x, y) z = match read_smt y (explode z) with
\r
135 | Some[tm], [], vars -> (tm :: x, vars)
\r
136 | _, _, _ -> raise (ParsingError "???")
\r
137 in let aux = List.fold_left f ([], ([], [var_zero])) (* index zero is reserved *)
\r
138 in let (tms, (_, free)) = aux strs
\r
139 in (List.rev tms, free)
\r
142 (**********************************************************************
\r
144 let rec string_of_term = function
\r
145 | Tvar n -> string_of_int n
\r
146 | Tapp(t1, t2) -> "(" ^ string_of_term t1 ^ " " ^ string_of_term t2 ^ ")"
\r
147 | Tlam(t1) -> "(\\" ^ string_of_term t1 ^ ")"
\r
150 let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j"));;
\r
153 **********************************************************************)
\r