* Two Different Exception Behaviors in camlp4 on the toplevel
@ 2010-05-24 3:46 Joseph Young
2010-05-24 7:35 ` [Caml-list] " blue storm
0 siblings, 1 reply; 4+ messages in thread
From: Joseph Young @ 2010-05-24 3:46 UTC (permalink / raw)
To: caml-list
Hi,
At the moment, I'm receiving two different exception behaviors in
camlp4 on the toplevel and I would like to unify them. As some
background, I would like to implement a small DSL where I insert OCaml
code using quotations. This causes some difficulty with type checking
since it may or may not be possible to type check an expression when it
contains a quotation. For example, we can immediately determine
that expressions such as "1+true" are ill-typed whereas the expression
"1+$x$" may or may not be ill-typed. It depends on the value of x. Since
I would like to return an error to the user as soon as possible, I can
partially type check expressions at compile time and then check the rest
at run time. Normally, camlp4 provides a nice exception handling
function:
Loc.raise loc Some_exception
which will underline the offending piece of code when executed at the
toplevel. However, this function only seems to work when called during
macro expansion. In the case of type checking above, this works function
works well when a type error can be determined at compile time, but does
not work well when a type error is discovered at runtime.
More concretely, I have the following behavior (code follows
below):
---------------------------------------
$ rlwrap ocaml -rectypes dynlink.cma camlp4o.cma calc.cmo
Objective Caml version 3.11.2
Camlp4 Parsing version 3.11.2
# open Calc;;
# open CamlSyntax;;
# let x= <:calc< 1+2 >>;;
val x : Calc.calc =
Nonterm (<abstr>, `Add, [Term (<abstr>, `Int 1); Term (<abstr>, `Int
2)])
# let y= <:calc< true or 1 + 2 >>;;
Error: While expanding quotation "calc" in a position of "expr":
Camlp4: Uncaught exception: Calc.Type_error
# let z= <:calc< true or $"x"$ >>;;
Exception: Loc.Exc_located (<abstr>, Calc.Type_error).
---------------------------------------
Although it doesn't show up in an ascii email, the definition of y
underlines the string "true or 1" as the exception is thrown. The
definition of z does not hilight any text.
The code that generates this behavior is below:
---------------------------------------
$ cat calc.ml
open Camlp4.PreCast;;
module CamlSyntax=
Camlp4OCamlParser.Make(
Camlp4OCamlRevisedParser.Make(
Camlp4.PreCast.Syntax));;
(* The AST for the small calculator *)
type loc=CamlSyntax.Loc.t
type nonterminal=[`Add | `Sub | `Or | `And ];;
type terminal=[`Int of int | `Bool of bool | `Ocaml of (loc*string)];;
type calc=
| Nonterm of loc*nonterminal*(calc list)
| Term of loc*terminal;;
(* Grammar for a simple calculator *)
module CalcGram = Camlp4.PreCast.MakeGram(Camlp4.PreCast.Lexer);;
let (term:calc CalcGram.Entry.t)= CalcGram.Entry.mk "term";;
let term_eoi = CalcGram.Entry.mk "Simple calculator quotation";;
EXTEND CalcGram
GLOBAL: term term_eoi;
term:
[ "alg"
[ e1 = SELF; "+"; e2 = SELF -> Nonterm(_loc,`Add,[e1;e2])
| e1 = SELF; "-"; e2 = SELF -> Nonterm(_loc,`Sub,[e1;e2])]
| "bool"
[ e1 = SELF; "or"; e2 = SELF -> Nonterm(_loc,`Or,[e1;e2])
| e1 = SELF; "and"; e2 = SELF -> Nonterm(_loc,`And,[e1;e2])]
| "simple"
[ "$"; `STRING (e,_); "$" -> Term(_loc,`Ocaml (_loc,e))
| `INT (i, _) -> Term(_loc,`Int i)
| "true" -> Term(_loc,`Bool true)
| "false" -> Term(_loc,`Bool false)
| "("; e = term; ")" -> e ]
];
term_eoi:
[[ t = term; `EOI -> t ]];
END;;
(* Generates an expression with the location information *)
let expr_of_loc _loc=
let (a, b, c, d, e, f, g, h) = CamlSyntax.Loc.to_tuple _loc in
<:expr< Loc.of_tuple ($`str:a$, $`int:b$, $`int:c$, $`int:d$,
$`int:e$, $`int:f$, $`int:g$, $`bool:h$) >>
;;
(* Generates an expression with the nonterminal information *)
let expr_of_nonterm _loc e=
match e with
| `Add -> <:expr< `Add >>
| `Sub -> <:expr< `Sub >>
| `Or -> <:expr< `Or >>
| `And -> <:expr< `And >>
;;
(* Generates an expression with the terminal information *)
let expr_of_term _loc e=
match e with
| `Int i -> <:expr< `Int($`int:i$) >>
| `Bool b -> <:expr< `Bool($`bool:b$) >>
| `Ocaml(l,e) -> CamlSyntax.Gram.parse_string CamlSyntax.expr_eoi l e
;;
(* Generates an expression list from a list of expressions *)
let rec expr_of_list _loc es=
match es with
| e :: es -> <:expr< $e$ :: $expr_of_list _loc es$ >>
| [] -> <:expr< [] >>
;;
(* Strips out the location information *)
let loc_of_ast e=
match e with
| Nonterm (loc,_,_) | Term (loc,_) -> loc
;;
(* Program types. Need types to deal with quotations *)
type wild=[`Wild];;
type myint=[wild | `Int];;
type mybool=[wild | `Bool];;
type typ=[wild | myint | mybool];;
exception Type_error;;
(* Type check the AST *)
let rec type_ast e : typ=
let same_type t es=
let ts=List.map type_ast es in
if List.for_all (fun x-> x=t or x=`Wild) ts then
t
else
let loc=loc_of_ast e in
CamlSyntax.Loc.raise loc Type_error
in
match e with
| Nonterm (_,`Add,es) | Nonterm (_,`Sub,es) -> same_type `Int es
| Nonterm (_,`Or,es) | Nonterm (_,`And,es) -> same_type `Bool es
| Term(_,`Int _) -> `Int
| Term(_,`Bool _) -> `Bool
| Term(_,`Ocaml _ ) -> `Wild
;;
(* Converts a calculator AST into an OCaml AST *)
let to_expr base_loc prog=
let e=CalcGram.parse_string term_eoi base_loc prog in
let _= type_ast e in
let rec to_expr e=
let _loc=loc_of_ast e in
let expr_loc=expr_of_loc _loc in
match e with
| Nonterm (_,name,nodes) ->
let name= expr_of_nonterm _loc name in
let nodes= expr_of_list _loc (List.map to_expr nodes) in
<:expr< Nonterm ($expr_loc$,$name$,$nodes$) >>
| Term(_,`Ocaml e) ->
let e=expr_of_term _loc (`Ocaml e) in
<:expr< $e$ >>
| Term (_,data) ->
let data= expr_of_term _loc data in
<:expr< Term ($expr_loc$,$data$) >>
in
let e= to_expr e in
let _loc=base_loc in
<:expr< let _ = type_ast $e$ in $e$ >>
;;
let expand_calc_quot loc lopt e= to_expr loc e;;
Syntax.Quotation.add "calc" Syntax.Quotation.DynAst.expr_tag
expand_calc_quot;;
---------------------------------------
$ cat Makefile
all:
ocamlc -c -I +camlp4 -I +camlp4/Camlp4Parsers -pp camlp4of -o
calc.cmo calc.ml
---------------------------------------
If possible, I would like to have the offending, ill-typed code
hilighted in both cases. Thanks for the help.
Joe
^ permalink raw reply [flat|nested] 4+ messages in thread* Re: [Caml-list] Two Different Exception Behaviors in camlp4 on the toplevel
2010-05-24 3:46 Two Different Exception Behaviors in camlp4 on the toplevel Joseph Young
@ 2010-05-24 7:35 ` blue storm
2010-05-25 6:44 ` Joseph Young
0 siblings, 1 reply; 4+ messages in thread
From: blue storm @ 2010-05-24 7:35 UTC (permalink / raw)
To: Joseph Young; +Cc: caml-list
The reason you have two different kinds of error is that you use
type_ast in two different places :
(* Converts a calculator AST into an OCaml AST *)
let to_expr base_loc prog=
let e=CalcGram.parse_string term_eoi base_loc prog in
let _= type_ast e in
let rec to_expr e= ... in
let e= to_expr e in ...
<:expr< let _ = type_ast $e$ in $e$ >>
;;
The first occurence of "type_ast" in that code is executed at
parsing-time. The second occurence, inside <:expr< ... >>, is executed
at runtime, like a classical OCaml exception, and the toplevel does no
special error reporting on Camlp4-related exceptions.
You could fix this by inserting (at runtime) a call to the Camlp4
exception printer :
<:expr< let _ =
try type_ast $e$ with exn ->
Format.eprintf "%a@." Camlp4.ErrorHandler.print exn;
raise exn in
$e$ >>
Unfortunately, I'm not sure it will work in the toplevel (wich has a
special location handling as there is no "file" associated to
locations). It will work however if you #use a file containing an
erroneous code.
$ cat foo.ml
open Camlp4.PreCast
open Calc
let _ = <:calc< 1 + (2 + $"<:calc< true >>"$) >>
$ ocamlc -pp 'camlp4o calc.cmo' -I +camlp4 dynlink.cma camlp4lib.cma
calc.cmo foo.ml -o foo
$ ./foo
File "foo.ml", line 3, characters 21-45:
Camlp4: Uncaught exception: Calc.Type_error
Fatal error: exception Loc.Exc_located(_, _)
$ ocaml dynlink.cma camlp4o.cma calc.cmo
# #use "foo.ml";;
File "foo.ml", line 3, characters 21-45:
Camlp4: Uncaught exception: Calc.Type_error
Exception: Loc.Exc_located (<abstr>, Calc.Type_error).
You are actually doing unecessary work. The OCaml type system being
quite powerful, it is easy to have it doing the work, instead of
coding your own limited typechecker. The idea is that you should only
generate OCaml terms that are typed exactly when you want them to be
typed.
(** We use a RuntimeCalc module with a typed interface to enforce correct types
for calc values *)
module RuntimeCalc : sig
type calc =
[ `Nonterm of [ `Add | `Sub | `Or | `And ] * calc list
| `Term of [ `Int of int | `Bool of bool ] ]
type 'a t
val add : int t list -> int t
val sub : int t list -> int t
val or_ : bool t list -> bool t
val and_ : bool t list -> bool t
val int : int -> int t
val bool : bool -> bool t
val expose : 'a t -> calc
end = struct
type calc =
[ `Nonterm of [ `Add | `Sub | `Or | `And ] * calc list
| `Term of [ `Int of int | `Bool of bool ] ]
type 'a t = calc
let expose calc = calc
let op name li = `Nonterm (name, li)
let add li = op `Add li
let sub li = op `Sub li
let and_ li = op `And li
let or_ li = op `Or li
let int n = `Term (`Int n)
let bool b = `Term (`Bool b)
let expose t = t
end
(* Generates an expression with the nonterminal information *)
let expr_of_nonterm _loc e=
match e with
| `Add -> <:expr< RuntimeCalc.add >>
| `Sub -> <:expr< RuntimeCalc.sub >>
| `Or -> <:expr< RuntimeCalc.or_ >>
| `And -> <:expr< RuntimeCalc.and_ >>
;;
(* Generates an expression with the terminal information *)
let expr_of_term _loc e=
match e with
| `Int i -> <:expr< RuntimeCalc.int $`int:i$ >>
| `Bool b -> <:expr< RuntimeCalc.bool $`bool:b$ >>
| `Ocaml(l,e) -> Gram.parse_string Syntax.expr_eoi l e
;;
(* Converts a calculator AST into an OCaml AST *)
let to_expr _loc prog =
let rec to_expr : calc -> Ast.expr = function
| `Nonterm (_loc, name, nodes) ->
let nodes= expr_of_list _loc (List.map to_expr nodes) in
let name = expr_of_nonterm _loc name in
<:expr< $name$ $nodes$ >>
| `Term(_loc, term) ->
expr_of_term _loc term in
let e = to_expr (CalcGram.parse_string term_eoi _loc prog) in
<:expr< $e$ >>
;;
In that example, I put RuntimeCalc inside the Calc module for
convenience (and similarity with your code). You should really put it
outside, in a separated module, and keep a strong separation between
camlp4-time code and runtime code.
^ permalink raw reply [flat|nested] 4+ messages in thread* Re: [Caml-list] Two Different Exception Behaviors in camlp4 on the toplevel
2010-05-24 7:35 ` [Caml-list] " blue storm
@ 2010-05-25 6:44 ` Joseph Young
2010-05-25 7:28 ` blue storm
0 siblings, 1 reply; 4+ messages in thread
From: Joseph Young @ 2010-05-25 6:44 UTC (permalink / raw)
To: caml-list
The type checking using phantom types worked great. Thanks. In
case it helps anyone else, I'm attaching complete working code below.
Joe
----------------------------
$ cat calc.ml
open Camlp4.PreCast;;
module CamlSyntax=
Camlp4OCamlParser.Make(
Camlp4OCamlRevisedParser.Make(
Camlp4.PreCast.Syntax));;
(* The AST for the small calculator *)
type loc=CamlSyntax.Loc.t
type nonterminal=[`Add | `Sub | `Or | `And | `MixedFn];;
type terminal=[`Int of int | `Bool of bool | `Ocaml of (loc*string)];;
type calc=
| Nonterm of loc*nonterminal*(calc list)
| Term of loc*terminal;;
module TypeChecker : sig
type 'a t
val add : loc->int t->int t->int t
val sub : loc->int t->int t->int t
val or_: loc->bool t->bool t->bool t
val and_: loc->bool t->bool t->bool t
val mixed: loc->bool t->int t->int t
val int_: loc->int -> int t
val bool_: loc->bool -> bool t
val expose : 'a t->calc
end = struct
type 'a t=calc
let add loc e1 e2 = Nonterm (loc,`Add,[e1;e2])
let sub loc e1 e2 = Nonterm (loc,`Sub,[e1;e2])
let or_ loc e1 e2 = Nonterm (loc,`Or,[e1;e2])
let and_ loc e1 e2 = Nonterm (loc,`And,[e1;e2])
let mixed loc e1 e2 = Nonterm (loc,`MixedFn,[e1;e2])
let int_ loc i = Term (loc,`Int i)
let bool_ loc b = Term (loc,`Bool b)
let expose e=e
end;;
open TypeChecker;;
(* Grammar for a simple calculator *)
module CalcGram = Camlp4.PreCast.MakeGram(Camlp4.PreCast.Lexer);;
let (term:calc CalcGram.Entry.t)= CalcGram.Entry.mk "term";;
let term_eoi = CalcGram.Entry.mk "Simple calculator quotation";;
EXTEND CalcGram
GLOBAL: term term_eoi;
term:
[ "alg"
[ e1 = SELF; "+"; e2 = SELF -> Nonterm(_loc,`Add,[e1;e2])
| e1 = SELF; "-"; e2 = SELF -> Nonterm(_loc,`Sub,[e1;e2])]
| "bool"
[ e1 = SELF; "or"; e2 = SELF -> Nonterm(_loc,`Or,[e1;e2])
| e1 = SELF; "and"; e2 = SELF -> Nonterm(_loc,`And,[e1;e2])]
| "other"
[ e1 = SELF; "mix"; e2= SELF -> Nonterm(_loc,`MixedFn,[e1;e2])]
| "simple"
[ "$"; `STRING (e,_); "$" -> Term(_loc,`Ocaml (_loc,e))
| `INT (i, _) -> Term(_loc,`Int i)
| "true" -> Term(_loc,`Bool true)
| "false" -> Term(_loc,`Bool false)
| "("; e = term; ")" -> e ]
];
term_eoi:
[[ t = term; `EOI -> t ]];
END;;
(* Generates an expression with the location information *)
let expr_of_loc _loc=
let (a, b, c, d, e, f, g, h) = CamlSyntax.Loc.to_tuple _loc in
<:expr< Loc.of_tuple ($`str:a$, $`int:b$, $`int:c$, $`int:d$,
$`int:e$, $`int:f$, $`int:g$, $`bool:h$) >>
;;
(* Generates an expression with the nonterminal information *)
let expr_of_nonterm _loc name=
match name with
| `Add -> <:expr< add >>
| `Sub -> <:expr< sub >>
| `Or -> <:expr< or_ >>
| `And -> <:expr< and_ >>
| `MixedFn -> <:expr< mixed >>
;;
(* Generates an expression with the terminal information *)
let expr_of_term _loc e=
let expr_loc=expr_of_loc _loc in
match e with
| `Int i -> <:expr< int_ $expr_loc$ $`int:i$ >>
| `Bool b -> <:expr< bool_ $expr_loc$ $`bool:b$ >>
| `Ocaml(l,e) -> CamlSyntax.Gram.parse_string CamlSyntax.expr_eoi l e
;;
(* Converts a calculator AST into an OCaml AST *)
let to_expr base_loc prog=
let e=CalcGram.parse_string term_eoi base_loc prog in
let rec to_expr e=
match e with
| Nonterm (_loc,name,[e1;e2]) ->
let constr= expr_of_nonterm _loc name in
let e1=to_expr e1 in
let e2=to_expr e2 in
<:expr< $constr$ $expr_of_loc _loc$ $e1$ $e2$>>
| Term (_loc,data) ->
let data= expr_of_term _loc data in
<:expr< $data$ >>
| _ -> failwith ("Wrong number of arguments.")
in
to_expr e
;;
let expand_calc_quot loc lopt e= to_expr loc e;;
Syntax.Quotation.add "calc" Syntax.Quotation.DynAst.expr_tag
expand_calc_quot;;
----------------------------
$ cat Makefile
all:
ocamlc -c -I +camlp4 -I +camlp4/Camlp4Parsers -pp camlp4of -o
calc.cmo calc.ml
----------------------------
^ permalink raw reply [flat|nested] 4+ messages in thread* Re: [Caml-list] Two Different Exception Behaviors in camlp4 on the toplevel
2010-05-25 6:44 ` Joseph Young
@ 2010-05-25 7:28 ` blue storm
0 siblings, 0 replies; 4+ messages in thread
From: blue storm @ 2010-05-25 7:28 UTC (permalink / raw)
To: Joseph Young; +Cc: caml-list
In case you're interested in more sophisticated examples of the DSL +
phantom types combination, I've worked on [Macaque] wich is a SQL DSL
for Caml using essentially the same technique. We were able to encode
useful properties of the SQL values, such as nullability, in the OCaml
type system.
The translation from the DSL to the caml code is not always direct,
because in some case you want to generate elaborate source terms wich
use the type system to enforce static guarantees (eg. correcteness of
the GROUP BY clauses).
[Macaque] http://macaque.forge.ocamlcore.org/
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2010-05-25 7:28 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-05-24 3:46 Two Different Exception Behaviors in camlp4 on the toplevel Joseph Young
2010-05-24 7:35 ` [Caml-list] " blue storm
2010-05-25 6:44 ` Joseph Young
2010-05-25 7:28 ` blue storm
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).