Excerpts from echinuz echinuz's message of Sat Dec 15 20:32:55 +0100 2007:
> Allow me to clarify what I meant by type errors and antiquotations.  Here is a
> very simple program that contains the parser, type checker, and quotation
> generator:

Ok,  I  understand your problem and will try to help you using Camlp4 examples
based on your original code.

In  first  I  attach  alg1.ml that is some minimum translation of your code in
order to use Camlp4 and to have locations.

I also attach a _tags file that helps ocamlbuild to build them.

Let's try this first example using alg1_test.ml.

$ mkdir algtest
$ cd algtest
$ cp <attachments> .
$ ocamlbuild alg1.cmo
$ cat alg1_test.ml
open Alg1;;
let x = <:exp< add(21, 21) >>;;
let y = <:exp< add(31, 11.0) >>;;
$ camlp4of ./_build/alg1.cmo alg1_test.ml
open Alg1
let x = App ("add", [ Int 21; Int 21 ])
let y = App ("add", [ Int 31; Flo 11.0 ])

Then  let's add antiquotations (alg1_ant.ml), basically one adds a Ant case to
the  alg type that will hold the antiquoted expression/pattern plus it's type.
We  embed  the  type  to  simplify the dynamic typing and don't involving some
type  inference.  One also embed the type of an expression at runtime in order
to check it against the type of the hole.

In  order to show some useful examples of typing errors one add strings values
to the language (alg1_ant_str.ml).

Here is the kind of program that we want accept:

$ cat alg1_ant_test.ml
open Alg1_ant;;
let x = <:exp< add(21, 21) >> in
let y = <:exp< add(31, 11.0) >> in
<:exp< add(add($Int: x$, $Real: y$), 42) >>

And the kind of programs that we want to dynamically reject:

$ cat alg1_ant_test_bad.ml
open Alg1_ant_str;;
let x = <:exp< "FOO" >> in
<:exp< add(42, $Int:x$) >>

Let's try the two new extensions:

# Compilation
$ ocamlbuild alg1_ant.cmo alg1_ant_str.cmo

# Let's look at the result
$ camlp4of ./_build/alg1_ant.cmo alg1_ant_test.ml
open Alg1_ant
let x = ((App ("add", [ Int 21; Int 21 ])), `Int) in
let y = ((App ("add", [ Int 31; Flo 11.0 ])), `Real)
in
  ((App ("add",
      [ App ("add",
          [ type_check
              (Loc.of_tuple
                 ("alg1_ant_test.ml", 4, 84, 100, 4, 84, 107, false))
              x `Int;
            type_check
              (Loc.of_tuple
                 ("alg1_ant_test.ml", 4, 84, 110, 4, 84, 118, false))
              y `Real ]);
        Int 42 ])),
   `Real)

# Let's compile and run the example
$ ocamlbuild alg1_ant_test.byte --

# Let's try the bad example to see that there is no static error.
$ camlp4of ./_build/alg1_ant_str.cmo alg1_ant_test_bad.ml
open Alg1_ant_str
let x = ((Str "FOO"), `Str)
in
  ((App ("add",
      [ Int 42;
        type_check
          (Loc.of_tuple
             ("alg1_ant_test_bad.ml", 3, 47, 63, 3, 47, 69, false))
          x `Int ])),
   `Int)

# Finally let's run it to show the runtime check failure.
$ ocamlbuild alg1_ant_test_bad.byte --
Dynamic Typing Error at File "alg1_ant_test_bad.ml", line 3, characters 16-22
Fatal error: exception Alg1_ant_str.TypeError

Hope that helps

Best regards,

> ---------------------------------------
> #load "pa_extend.cmo";;
> #load "q_MLast.cmo";;
> 
> (* Parser *)
> type palg=
> | PApp of string*palg list
> | PInt of string
> | PFlo of string;;
> 
> 
> let g=Grammar.gcreate (Plexer.gmake ());;
> let exp_eoi = Grammar.Entry.create g "exp_eoi";;
> 
> EXTEND
>     GLOBAL: exp_eoi;
>     exp_eoi:
>         [[ x = exp; EOI -> x ]] ;
>     exp:
>         [[x=INT -> PInt x
>         | x=FLOAT -> PFlo x
>         | f = LIDENT; "("; xs=LIST1 SELF SEP ","; ")"-> PApp (f,xs)]];
> END;;
> 
> let parse s = Grammar.Entry.parse exp_eoi (Stream.of_string s);;
> 
> (* Type Checker *)
> exception TypeError;;
> type integer=[`Int];;
> type real=[integer | `Real];;
> let rec type_expr=function
>     | PApp (f,args) ->
>         (match f with
>         | "add" ->
>             if List.length args != 2 then
>                 raise TypeError
>             else
>                 let args=List.map type_expr args in
>                 (match (List.nth args 0,List.nth args 1) with
>                 | #integer,#integer -> `Int
>                 | #real,#real -> `Real)
>         | _ -> raise TypeError)
>     | PInt _ -> `Int
>     | PFlo _ -> `Real
> ;;
> 
> 
> (* Quotations *)
> type alg=
> | App of string*alg list
> | Int of int
> | Flo of float;;
> 
> let loc=Ploc.dummy;;
> let rec to_expr=function
>     | PInt x-> <:expr< Int $int:x$ >>
>     | PFlo x-> <:expr< Flo $flo:x$ >>
>     | PApp (f,el)->
>         let rec make_el=function
>             | x::xs -> <:expr< [$x$::$make_el xs$] >>
>             | [] -> <:expr< [] >>
>         in
>         let el=List.map to_expr el in
>         let el=make_el el in
>         <:expr< App ($str:f$,$el$) >>
> ;;
> let rec to_patt=function
>     | PInt x-> <:patt< Int $int:x$ >>
>     | PFlo x-> <:patt< Flo $flo:x$ >>
>     | PApp (f,el)->
>         let rec make_el=function
>             | x::xs -> <:patt< [$x$::$make_el xs$] >>
>             | [] -> <:patt< [] >>
>         in
>         let el=List.map to_patt el in
>         let el=make_el el in
>         <:patt< App ($str:f$,$el$) >>
> ;;
> 
> let expand_expr s=
>     let p=parse s in
>     let t=type_expr p in
>     to_expr p
> ;;
> let expand_patt s=
>     let p=parse s in
>     let t=type_expr p in
>     to_patt p
> ;;
> Quotation.add "exp" (Quotation.ExAst (expand_expr,expand_patt));;
>  ---------------------------------------
> 
> Thus, by type check, I mean actually verifying the typing rules of the DSL.  In
> this case, it means that the only function allowed is "add" and that this
> function requires two arguments.  Now, imagine the above language where
> antiquotations are allowed.  The parsed AST would have datatype
> 
> type palg=
> | PApp of string*palg list
> | PInt of string
> | PFlo of string
> | PQuote of Ploc.t*string
> 
> and it becomes impossible to type check in the above sense since we can not
> ascertain the type of PQuote.  Now, we can still type check the resulting AST
> of type alg (not palg).  But, this must occur at runtime rather than during the
> preprocessing step at compile time.  Therein lies the problem.
> 
> If we discover a type error during runtime, it would be nice to give the user
> some indication of where the error occurs short of saying, "Add expects two
> arguments."  Since the location information provided is relative to the quote,
> it can still be challenging to determine exactly where the type error occurs. 
> Thus, I'm either trying to obtain better location information or perhaps learn
> that there's a better place or method to type check than what I'm using.
> 

-- 
Nicolas Pouillard aka Ertai