Commit 154fac89 authored by Pietro Abate's avatar Pietro Abate

[r2002-10-31 16:59:46 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-31 17:00:08+00:00
parent adc618c3
......@@ -13,6 +13,8 @@ let (source,input_channel) =
| 2 -> let s = Sys.argv.(1) in (s, open_in s)
| _ -> raise Usage
let () = Location.set_source source
let input = Stream.of_channel input_channel
let ppf = Format.std_formatter
......@@ -25,20 +27,8 @@ let print_norm ppf d =
Types.Print.print_descr ppf (Types.normalize d)
let rec print_exn ppf = function
| Location ((i,j), exn) ->
if source = "" then
Format.fprintf ppf "Error at chars %i-%i@\n" i j
else (
let (l1,c1) = Location.get_line_number source i
and (l2,c2) = Location.get_line_number source j in
if l1 = l2 then
Format.fprintf ppf "Error at line %i (chars %i-%i)@\n"
l1 c1 c2
else
Format.fprintf ppf "Error at lines %i (char %i) - %i (char %i)@\n"
l1 c1 l2 c2
);
print_exn ppf exn
| Location (loc, exn) ->
Format.fprintf ppf "Error %a:@\n%a" Location.print_loc loc print_exn exn
| Value.CDuceExn v ->
Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n"
Value.print v
......@@ -96,28 +86,62 @@ let debug = function
(Patterns.descr p)) pl) in
Patterns.Compile.show ppf (Types.descr t) pl
| _ -> Format.fprintf ppf "Unknown or ill-formed debugging directive !! @\n"
let typing_env = ref Typer.Env.empty
let eval_env = ref Value.Env.empty
let insert_type_bindings =
List.iter (fun (x,t) ->
typing_env := Typer.Env.add x t !typing_env;
Format.fprintf ppf "|- %s : %a@\n" x print_norm t)
let type_decl decl =
insert_type_bindings (Typer.type_let_decl !typing_env decl)
let eval_decl decl =
let bindings = Value.eval_let_decl !eval_env decl in
List.iter
(fun (x,v) ->
eval_env := Value.Env.add x v !eval_env;
Format.fprintf ppf "=> %s : @[%a@]@\n" x Value.print v
) bindings
let phrase ph =
match ph.descr with
| Ast.EvalStatement e ->
let (fv,e) = Typer.expr e in
let t = Typer.type_check Typer.Env.empty e Types.any true in
let t = Typer.type_check !typing_env e Types.any true in
Format.fprintf ppf "|- %a@\n" print_norm t;
let v = Value.eval Value.empty_env e in
let v = Value.eval !eval_env e in
Format.fprintf ppf "=> @[%a@]@\n" Value.print v
| Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> ()
| Ast.LetDecl (p,e) ->
let decl = Typer.let_decl p e in
type_decl decl;
eval_decl decl
| Ast.TypeDecl _ -> ()
| Ast.Debug l -> debug l
| _ -> assert false
let do_fun_decls decls =
let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
insert_type_bindings (Typer.type_rec_funs !typing_env decls);
List.iter eval_decl decls
let () =
try
let p = prog () in
let type_decls =
let (type_decls,fun_decls) =
List.fold_left
(fun accu ph -> match ph.descr with
| Ast.TypeDecl (x,t) -> (x,t) :: accu
(fun ((typs,funs) as accu) ph -> match ph.descr with
| Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs)
| Ast.LetDecl (p,({descr=Ast.Abstraction _} as e)) ->
(typs, (p,e)::funs)
| _ -> accu
) [] p in
) ([],[]) p in
Typer.register_global_types type_decls;
do_fun_decls fun_decls;
List.iter phrase p
with
| (Failure _ | Not_found | Invalid_argument _) as e ->
......
......@@ -3,6 +3,9 @@ exception Location of loc * exn
let noloc = (-1,-1)
let source = ref ""
let set_source s = source := s
let get_line_number src i =
let ic = open_in_bin src in
let rec aux pos line start =
......@@ -17,7 +20,20 @@ let get_line_number src i =
let r = aux 0 1 0 in
close_in ic;
r
let print_loc ppf (i,j) =
if !source = "" then
Format.fprintf ppf "at chars %i-%i" i j
else (
let (l1,c1) = get_line_number !source i
and (l2,c2) = get_line_number !source j in
if l1 = l2 then
Format.fprintf ppf "at line %i (chars %i-%i)"
l1 c1 c2
else
Format.fprintf ppf "at lines %i (char %i) - %i (char %i)"
l1 c1 l2 c2
)
type 'a located = { loc : loc; descr : 'a }
......
type loc = int * int
exception Location of loc * exn
val set_source: string -> unit
val noloc:loc
val get_line_number: string -> int -> int * int
val print_loc: Format.formatter -> loc -> unit
type 'a located = { loc : loc; descr : 'a }
val recurs: (('a located -> 'b) -> loc -> 'a -> 'b) -> ('a located -> 'b)
......
......@@ -20,18 +20,22 @@ let rec tuple loc = function
| [] -> assert false
let char = mk noloc (Internal (Types.char Chars.any))
let string = Star (Elem char)
let string_regexp = Star (Elem char)
let cst_nil = mk noloc (Cst (Types.Atom Sequence.nil_atom))
let seq_of_string s =
let rec aux accu i = if (i = 0) then accu else aux (s.[i-1]::accu) (i-1) in
let seq_of_string pos s =
let (pos,_) = pos in
let rec aux accu i =
if (i = 0)
then accu
else aux (((pos+i,pos+i+1),s.[i-1])::accu) (i-1) in
aux [] (String.length s)
let char_list loc s =
let s = seq_of_string (Token.eval_string s) in
List.map (fun c -> mk loc (Cst (Types.Char (Chars.Unichar.from_char c)))) s
let char_list pos s =
let s = seq_of_string pos (Token.eval_string s) in
List.map (fun (loc,c) -> mk loc (Cst (Types.Char (Chars.Unichar.from_char c)))) s
EXTEND
......@@ -42,9 +46,13 @@ EXTEND
];
phrase: [
[ e = expr -> EvalStatement e
[ (p,e) = let_binding -> LetDecl (p,e)
| (p,e1) = let_binding; "in"; e2 = expr LEVEL "top"->
EvalStatement (mk loc (Match (e1,[p,e2])))
| "type"; x = UIDENT; "="; t = pat -> TypeDecl (x,t)
| "debug"; d = debug_directive -> Debug d
] |
[ e = expr -> EvalStatement e
]
];
......@@ -86,9 +94,12 @@ EXTEND
]
|
[ LIDENT "flatten"; e = expr -> mk loc (Op ("flatten",[e]))
| LIDENT "load_xml"; e = expr -> mk loc (Op ("load_xml",[e]))
| LIDENT "raise"; e = expr -> mk loc (Op ("raise",[e]))
[ op = [ LIDENT "flatten"
| LIDENT "load_xml"
| LIDENT "raise"
| LIDENT "int_of"
];
e = expr -> mk loc (Op (op,[e]))
| e1 = expr; e2 = expr -> mk loc (Apply (e1,e2))
]
......@@ -165,16 +176,20 @@ EXTEND
| x = regexp; "?" -> Alt (x, Epsilon)
| x = regexp; "??" -> Alt (Epsilon, x) ]
| [ "("; x = regexp; ")" -> x
| UIDENT "String" -> string
| s = CHAR ->
let s = seq_of_string (Token.eval_string s) in
| UIDENT "PCDATA" -> string_regexp
| i = CHAR ; "--"; j = CHAR ->
let i = Chars.Unichar.from_char (Token.eval_char i)
and j = Chars.Unichar.from_char (Token.eval_char j) in
Elem (mk loc (Internal (Types.char (Chars.char_class i j))))
| s = CHAR ->
let s = seq_of_string loc (Token.eval_string s) in
List.fold_right
(fun c accu ->
(fun (loc,c) accu ->
let c = Chars.Unichar.from_char c in
let c = Chars.atom c in
Seq (Elem (mk loc (Internal (Types.char c))), accu))
s
Epsilon
Epsilon
| e = pat LEVEL "simple" -> Elem e
]
];
......@@ -220,9 +235,9 @@ EXTEND
| "<"; t = tag_spec; a = attrib_spec; ">"; c = pat ->
multi_prod loc [t;a;c]
| s = STRING ->
let s = seq_of_string (Token.eval_string s) in
let s = seq_of_string loc (Token.eval_string s) in
let s = List.map
(fun c ->
(fun (loc,c) ->
mk loc (Internal
(Types.char
(Chars.atom
......
module Env = Map.Make (struct type t = string let compare = compare end)
let empty_env = Env.empty
type t =
| Pair of t * t
......@@ -19,9 +17,15 @@ and abstr = {
exception CDuceExn of t
let nil = Atom Sequence.nil_atom
let string s = String (0,String.length s, s, nil)
let exn_int_of = CDuceExn (Pair (Atom (Types.mk_atom "Invalid_argument"),
string "int_of"))
let rec is_seq = function
| Pair (_, y) when is_seq y -> true
| Atom a when a = Sequence.nil_atom -> true
| String (_,_,_,y) when is_seq y -> true
| _ -> false
let is_xml = function
......@@ -54,6 +58,9 @@ and print_quoted_str ppf = function
and print_seq ppf = function
| Pair (Char _, _) as s -> Format.fprintf ppf "'%a" print_str s
| Pair (x,y) -> Format.fprintf ppf "@[%a@]@ %a" print x print_seq y
| String (i,j,s,y) ->
Format.fprintf ppf "'%s' %a" (String.escaped (String.sub s i (j-i)))
print_seq y
| _ -> ()
and print_str ppf = function
| Pair (Char c,y) ->
......@@ -331,6 +338,7 @@ let rec eval env e0 =
| Typed.Op ("-", [e1; e2]) -> eval_sub (eval env e1) (eval env e2)
| Typed.Op ("/", [e1; e2]) -> eval_div (eval env e1) (eval env e2)
| Typed.Op ("load_xml", [e]) -> eval_load_xml (eval env e)
| Typed.Op ("int_of", [e]) -> eval_int_of (eval env e)
| Typed.Dot (e, l) -> eval_dot l (eval env e)
| Typed.DebugTyper t -> failwith "Evaluating a ! expression"
| Typed.Op (o,_) -> failwith ("Unknown operator " ^ o)
......@@ -350,6 +358,12 @@ and eval_branches env brs arg =
else Env.add x bindings.(i) env) env bind in
eval env e
and eval_let_decl env l =
let v = eval env l.Typed.let_body in
let (disp,bind) = Typed.dispatcher_let_decl l in
let (_,bindings) = run_dispatcher disp v in
List.map (fun (x,i) -> (x, if (i = -1) then v else bindings.(i))) bind
and eval_map env brs = function
| Pair (x,y) -> Pair (eval_branches env brs x, eval_map env brs y)
| String (_,_,_,_) as v -> eval_map env brs (normalize v)
......@@ -387,11 +401,20 @@ and eval_div x y = match (x,y) with
and eval_load_xml e =
Load_xml.run (get_string e)
and eval_int_of e =
let s = get_string e in
try Integer (Big_int.big_int_of_string s)
with Failure _ -> raise exn_int_of
and get_string e =
let rec compute_len accu = function
| Pair (_,y) -> compute_len (accu + 1) y
| String (i,j,_,y) -> compute_len (accu + j - i) y
| _ -> accu in
let rec fill pos s = function
| Pair (Char x,y) -> s.[pos] <- Chars.Unichar.to_char x; fill (pos + 1) s y
| String (i,j,src,y) ->
String.blit src i s pos (j - i); fill (pos + j - i) s y
| _ -> s in
fill 0 (String.create (compute_len 0 e)) e
type t
and abstr
and env
exception CDuceExn of t
module Env : Map.S with type key = string
type env = t Env.t
val empty_env : env
exception CDuceExn of t
val print: Format.formatter -> t -> unit
val run_dispatcher: Patterns.Compile.dispatcher -> t -> int * t array
val eval: env -> Typed.texpr -> t
val eval_let_decl: env -> Typed.let_decl -> (string * t) list
type Content = [(Name Addr Tel?)*];;
type Addrbook = <addrbook>Content;;
type Name = <name>[String];;
type Addr = <addr>[String];;
type Tel = <tel>[String];;
type Name = <name>[ PCDATA ];;
type Addr = <addr>[ PCDATA ];;
type Tel = <tel>[ PCDATA ];;
<addrbook>[
......
type Biblio = <bibliography>[Heading Paper*];;
type Heading = <heading>[String];;
type Heading = <heading>[ PCDATA ];;
type Paper = <paper>[Author+ Title Conference File];;
type Author = <author>[String];;
type Title = <title>[String];;
type Conference = <conference>[String];;
type File = <file>[String];;
type Author = <author>[ PCDATA ];;
type Title = <title>[ PCDATA ];;
type Conference = <conference>[ PCDATA ];;
type File = <file>[ PCDATA ];;
type Html = <html>[Head? Body];;
type Head = <head>[ <title>[String] ];;
type Head = <head>[ <title>[ PCDATA ] ];;
type Body = <body>[Mix*];;
type Mix = <h1>[Mix*]
| <a href=[String]>[Mix*]
| <a href=String>[Mix*]
| <p>[Mix*]
| <em>[Mix*]
| <ul>[ <li>[Mix*] +]
......
......@@ -2,7 +2,7 @@ type Person = FPerson | MPerson;;
type FPerson = <person gender = ['F'] >[ Name Children ];;
type MPerson = <person gender="M">[ Name Children];;
type Children = <children>[Person*];;
type Name = <name>[String];;
type Name = <name>[ PCDATA ];;
type Man = <man>[ Name Sons Daughters ];;
type Woman = <woman>[ Name Sons Daughters ];;
......
type Str = [String];;
type Bool = `True | `False;;
let fun check (Str -> Bool)
let fun check (String -> Bool)
| [ _* 'Castagna' _* ] -> `True
| _ -> `False
in
......@@ -10,12 +9,12 @@ in
);;
let fun extr (Str -> Str) [ (('a' x::_) | _)* ] -> x
let fun extr (String -> String) [ (('a' x::_) | _)* ] -> x
in
extr "abcaxy";;
type Text = [ (String | <comment>[String])* ];;
let fun extr (Text -> Str) [ (x::String | _)* ] -> x
type Text = [ (Char | <comment>[ PCDATA ])* ];;
let fun extr (Text -> String) [ (x::PCDATA | _)* ] -> x
in
extr [ 'abc' 'def' <comment>['Blabla'] 'xyz' ];;
(* Examples from the white-paper *)
type Bib = <bib>[Book*];;
type Book = <book>[Title Year Author+];;
type Year = <year>[ '0'--'9'+ ];;
type Title = <title>[ PCDATA ];;
type Author = <author>[ PCDATA ];;
let bib0 =
match (load_xml "tests/bib.xml") with
| (x & Bib) -> x
| _ -> raise "Wrong type !" in
bib0;;
type Intern =
{ title = String; year = Int; authors = [ String+ ] };;
let bib1 : Bib =
<bib>[
<book>[
<title>"Persistent Object Systems"
<year>"1994"
<author>"M. Atkinson"
<author>"V. Benzaken"
<author>"D. Maier"
]
<book>[
<title>"OOP: a unified foundation"
<year>"1997"
<author>"G. Castagna"
]
];;
let fun intern (Bib -> [Intern*])
<bib>l -> map l with
<book>[ <title>t <year>y a::Author+ ] ->
{
title = t;
year = int_of y;
authors = map a with <author>x -> x
};;
let fun authors(Intern->[String+]; Book->[Author+])
| { authors = a }
| <book>[ <title>_ <year>_; a] -> a;;
let fun extract ([ (String|Author)+ ] -> [ String+ ])
l -> map l with
| <author>a -> a
| a -> a;;
let fun authors2 ( b : Intern|Book ) : [String+] = extract (authors b);;
type Flat = [ (Title Year Author+)* ];;
let fun flatten_bib (l : [Book*]) : Flat =
transform l with <book>x -> x;;
let intstr =
Sequence.plus (Types.char (Chars.char_class
(Chars.Unichar.from_char '0')
(Chars.Unichar.from_char '9')
)
)
let types =
[
"Empty", Types.empty;
......@@ -8,4 +15,5 @@ let types =
"Pair", Types.Product.any;
"Arrow", Types.Arrow.any;
"Record", Types.Record.any;
"String", Sequence.string;
];
......@@ -46,6 +46,7 @@ let any = Types.descr any_node
let seqseq = Types.descr (star_node any_node)
let star t = Types.descr (star_node (Types.cons t))
let plus t = let t = Types.cons t in Types.times t (star_node t)
let string = star (Types.Char.any)
let approx t =
......
......@@ -11,6 +11,7 @@ val map: (Types.descr -> Types.descr) -> Types.descr -> Types.descr
val star: Types.descr -> Types.descr
(* For a type t, returns [t*] *)
val plus: Types.descr -> Types.descr
val approx: Types.descr -> Types.descr
(* For a type t <= [Any*], returns the least type s such that:
......
......@@ -49,6 +49,13 @@ and abstr = {
fun_fv : string list;
}
and let_decl = {
let_pat : tpat;
let_body : texpr;
mutable let_compiled :
(Patterns.Compile.dispatcher * (string * int) list) option
}
and branches = {
mutable br_typ : Types.descr;
br_accept : Types.descr;
......@@ -76,3 +83,16 @@ let dispatcher brs =
brs.br_compiled <- Some x;
x
let dispatcher_let_decl l =
match l.let_compiled with
| Some d -> d
| None ->
let comp = Patterns.Compile.make_branches
(Types.descr (Patterns.accept l.let_pat))
[ Patterns.descr l.let_pat, () ] in
let x = match comp with
| (disp, [| l, () |]) -> (disp,l)
| _ -> assert false
in
l.let_compiled <- Some x;
x
......@@ -396,10 +396,22 @@ let rec expr { loc = loc; descr = d } =
}
)
let let_decl p e =
let (_,e) = expr e in
{ Typed.let_pat = pat p;
Typed.let_body = e;
Typed.let_compiled = None }
(* III. Type-checks *)
module Env = StringMap
type env = Types.descr Env.t
open Typed
let warning loc msg =
Format.fprintf Format.std_formatter
"Warning %a:@\n%s@\n" Location.print_loc loc msg
let check loc t s msg =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
......@@ -492,10 +504,6 @@ and type_check' loc env e constr precise = match e with
let constr' = Sequence.approx (Types.cap Sequence.any constr) in
let exact = Types.subtype (Sequence.star constr') constr in
(*
Format.fprintf Format.std_formatter
"(Map) constr = %a@; exact = %b\n@." Types.Print.print_descr constr exact;
*)
(* Note:
- could be more precise by integrating the decomposition
of constr inside Sequence.map.
......@@ -624,6 +632,32 @@ and branches_aux loc env targ tres constr precise = function
tres
)
and type_let_decl env l =
let acc = Types.descr (Patterns.accept l.let_pat) in
let t = type_check env l.let_body acc true in
let res = Patterns.filter t l.let_pat in
List.map (fun (x,t) -> (x, Types.descr t)) res
and type_rec_funs env l =
let types =
List.fold_left
(fun accu -> function {let_body={exp_descr=Abstraction a}} as l ->
let t = a.fun_typ in
let acc = Types.descr (Patterns.accept l.let_pat) in
if not (Types.subtype t acc) then
raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc));
let res = Patterns.filter t l.let_pat in
List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res
| _ -> assert false) [] l
in
let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
List.iter
(function { let_body = { exp_descr = Abstraction a } } as l ->
ignore (type_check env' l.let_body Types.any false)
| _ -> assert false) l;
types
and type_op loc op args =
match (op,args) with
| "+", [loc1,t1; loc2,t2] ->
......@@ -646,6 +680,12 @@ and type_op loc op args =
Types.any
| "raise", [loc1,t1] ->
Types.empty
| "int_of", [loc1,t1] ->
check loc1 t1 Sequence.string
"The argument of int_of must a string";
if not (Types.subtype t1 Builtin.intstr) then
warning loc "This application of int_of may fail";
Types.interval Intervals.any
| _ -> assert false
and type_int_binop f loc1 t1 loc2 t2 =
......
......@@ -16,8 +16,11 @@ val pat : Ast.ppat -> Typed.tpat
module Fv : Set.S with type elt = string
module Env : Map.S with type key = string
type env = Types.descr Env.t
val expr: Ast.pexpr -> Fv.t * Typed.texpr
val let_decl : Ast.ppat -> Ast.pexpr -> Typed.let_decl
val type_check:
Types.descr Env.t -> Typed.texpr -> Types.descr -> bool -> Types.descr
......@@ -25,4 +28,7 @@ val type_check:
has type [t] under typing environment [env]; if [precise=true],
also returns a possible more precise type for [e].
*)
val type_let_decl: env -> Typed.let_decl -> (string * Types.descr) list
val type_rec_funs: env -> Typed.let_decl list -> (string * Types.descr) list
(* Assume that all the expressions are Absstractions *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment