Commit d265007d authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-03-23 21:09:48 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-23 21:09:49+00:00
parent e7b95c2b
......@@ -4,7 +4,6 @@ open Ident
let quiet = ref false
let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty
let glb_env = State.ref "Cduce.glb_env" Typer.TypeEnv.empty
let eval_env = Eval.global_env
let print_norm ppf d =
......@@ -15,9 +14,9 @@ let print_value ppf v =
Location.protect ppf (fun ppf -> Value.print ppf v)
let dump_env ppf =
Format.fprintf ppf "Global types:";
Typer.TypeEnv.iter (fun x _ -> Format.fprintf ppf " %s" x) !glb_env;
Format.fprintf ppf ".@\n";
(* Format.fprintf ppf "Global types:";
List.iter (fun x _ -> Format.fprintf ppf " %s" x) (Typer.global_types ());
Format.fprintf ppf ".@\n"; *)
Eval.Env.iter
(fun x v ->
let t = Typer.Env.find x !typing_env in
......@@ -83,23 +82,23 @@ let rec print_exn ppf = function
let debug ppf = function
| `Subtype (t1,t2) ->
Format.fprintf ppf "[DEBUG:subtype]@\n";
let t1 = Types.descr (Typer.typ !glb_env t1)
and t2 = Types.descr (Typer.typ !glb_env t2) in
let t1 = Types.descr (Typer.typ t1)
and t2 = Types.descr (Typer.typ t2) in
Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
(Types.subtype t1 t2)
| `Filter (t,p) ->
Format.fprintf ppf "[DEBUG:filter]@\n";
let t = Typer.typ !glb_env t
and p = Typer.pat !glb_env p in
let t = Typer.typ t
and p = Typer.pat p in
let f = Patterns.filter (Types.descr t) p in
List.iter (fun (x,t) ->
Format.fprintf ppf " %s:%a@\n" (Id.value x)
print_norm (Types.descr t)) f
| `Compile2 (t,pl) ->
Format.fprintf ppf "[DEBUG:compile2]@\n";
(* let t = Types.descr (Typer.typ !glb_env t) in
(* let t = Types.descr (Typer.typ t) in
let pl = List.map (fun p ->
let p = Typer.pat !glb_env p in
let p = Typer.pat p in
let a = Types.descr (Patterns.accept p) in
(Some p, Types.cap a t)) pl in
let d = Patterns.Compiler.make_dispatcher t pl in
......@@ -108,13 +107,13 @@ let debug ppf = function
| `Accept p ->
Format.fprintf ppf "[DEBUG:accept]@\n";
let p = Typer.pat !glb_env p in
let p = Typer.pat p in
let t = Patterns.accept p in
Format.fprintf ppf " %a@\n" Types.Print.print t
| `Compile (t,pl) ->
Format.fprintf ppf "[DEBUG:compile]@\n";
let t = Typer.typ !glb_env t
and pl = List.map (Typer.pat !glb_env) pl in
let t = Typer.typ t
and pl = List.map Typer.pat pl in
Patterns.Compile.debug_compile ppf t pl
| `Normal_record p -> assert false
......@@ -123,7 +122,7 @@ let debug ppf = function
let mk_builtin () =
let bi = List.map (fun (n,t) -> [n, mknoloc (Ast.Internal t)])
Builtin.types in
glb_env := List.fold_left Typer.register_global_types !glb_env bi
List.iter Typer.register_global_types bi
let () = mk_builtin ()
......@@ -153,7 +152,7 @@ let run ppf ppf_err input =
let phrase ph =
match ph.descr with
| Ast.EvalStatement e ->
let (fv,e) = Typer.expr !glb_env e in
let (fv,e) = Typer.expr e in
let t = Typer.type_check !typing_env e Types.any true in
Location.dump_loc ppf e.Typed.exp_loc;
if not !quiet then
......@@ -163,7 +162,7 @@ let run ppf ppf_err input =
Format.fprintf ppf "=> @[%a@]@\n@." print_value v
| Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> ()
| Ast.LetDecl (p,e) ->
let decl = Typer.let_decl !glb_env p e in
let decl = Typer.let_decl p e in
type_decl decl;
eval_decl decl
| Ast.TypeDecl _ -> ()
......@@ -172,7 +171,7 @@ let run ppf ppf_err input =
in
let do_fun_decls decls =
let decls = List.map (fun (p,e) -> Typer.let_decl !glb_env p e) decls in
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
in
......@@ -201,7 +200,7 @@ let run ppf ppf_err input =
(typs, (p,e)::funs)
| _ -> accu
) ([],[]) p in
glb_env := Typer.register_global_types !glb_env type_decls;
Typer.register_global_types type_decls;
phrases [] p;
true
with
......
......@@ -2,7 +2,6 @@ val quiet: bool ref
val typing_env: Typer.env ref (* Types of toplevel bindings *)
val eval_env: Eval.env ref (* Values of toplevel bindings *)
val glb_env: Typer.glb ref (* Global types *)
val print_exn: Format.formatter -> exn -> unit
......
......@@ -149,3 +149,10 @@ and hash_regexp = function
| Star x -> 5 + 17 * (hash_regexp x)
| WeakStar x -> 6 + 17 * (hash_regexp x)
| SeqCapture (x,y) -> 7 + 17 * (Id.hash x) + 257 * (hash_regexp y)
module PpatTable = Hashtbl.Make
(struct
type t = ppat
let equal = equal_ppat
let hash = hash_ppat
end)
(* TODO:
- rewrite type-checking of operators to propagate constraint
- rewrite translation of types and patterns -> hash cons
CONTINUE THIS...
Problem with same name for recursive binders in different
recursive type/patterns definitions because of hash-consing
*)
......@@ -12,11 +15,10 @@ open Ast
open Ident
module S = struct type t = string let compare = compare end
module StringSet = Set.Make(S)
module TypeEnv = Map.Make(S)
module Env = Map.Make(Ident.Id)
(*
module StringSet = Set.Make(S)
*)
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr * string
......@@ -26,55 +28,6 @@ exception UnboundId of string
let raise_loc loc exn = raise (Location (loc,exn))
(* Internal representation as a graph (desugar recursive types and regexp),
to compute freevars, etc... *)
type ti = {
id : int;
mutable seen : bool;
mutable loc' : loc;
mutable fv : fv option;
mutable descr': descr;
mutable type_node: Types.node option;
mutable pat_node: Patterns.node option
}
and descr =
| IAlias of string * ti
| IType of Types.descr
| IOr of ti * ti
| IAnd of ti * ti
| IDiff of ti * ti
| ITimes of ti * ti
| IXml of ti * ti
| IArrow of ti * ti
| IOptional of ti
| IRecord of bool * ti label_map
| ICapture of id
| IConstant of id * Types.const
type glb = ti TypeEnv.t
let mk' =
let counter = ref 0 in
fun loc ->
incr counter;
let rec x = {
id = !counter;
seen = false;
loc' = loc;
fv = None;
descr' = IAlias ("__dummy__", x);
type_node = None;
pat_node = None
} in
x
let cons loc d =
let x = mk' loc in
x.descr' <- d;
x
(* Note:
Compilation of Regexp is implemented as a ``rewriting'' of
the parsed syntax, in order to be able to print its result
......@@ -183,6 +136,7 @@ module Regexp = struct
defs := [];
mk_loc !re_loc (Recurs (n,d))
(*
module H = Hashtbl.Make(
struct
type t = Ast.regexp * Ast.ppat
......@@ -204,9 +158,338 @@ module Regexp = struct
let c = compile loc regexp queue in
H.add hash (regexp,queue) c;
c
*)
end
let compile_regexp = Regexp.compile noloc
(*
type descr =
| IType of Types.descr
| IOr of descr * descr
| IAnd of descr * descr
| IDiff of descr * descr
| ITimes of slot * slot
| IXml of slot * slot
| IArrow of slot * slot
| IOptional of slot descr
| IRecord of bool * slot label_map
| ICapture of id
| IConstant of id * Types.const
and slot = {
mutable fv : fv option;
mutable hash : int option;
mutable rank1: int; mutable rank2: int;
mutable gen1 : int; mutable gen2: int;
mutable d : slot descr option
}
let descr s =
match s.d with
| Some d -> d
| None -> assert false
let gen = ref 0
let rank = ref 0
let rec hash_descr = function
| IType x -> Types.hash_descr x
| IOr (d1,d2) -> 1 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IAnd (d1,d2) -> 2 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IDiff (d1,d2) -> 3 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IOptional d -> 4 + 17 * (hash_descr d)
| ITimes (s1,s2) -> 5 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IXml (s1,s2) -> 6 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IArrow (s1,s2) -> 7 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IRecord (o,r) -> (if o then 8 else 9) + 17 * (LabelMap.hash hash_slot r)
| ICapture x -> 10 + 17 * (Id.hash x)
| IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.hash_const y)
and hash_slot s =
if s.gen1 = !gen then 13 * s.rank1
else (
incr rank;
s.rank1 <- !rank; s.gen1 <- !gen;
hash_descr (descr s)
)
let rec equal_descr d1 d2 =
(d1 == d2) ||
match (d1,d2) with
| IType x1, IType x2 -> Types.equal_descr x1 x2
| IOr (x1,y1), IOr (x2,y2)
| IAnd (x1,y1), IAnd (x2,y2)
| IDiff (x1,y1), IDiff (x2,y2) -> (equal_descr x1 x2) && (equal_descr y1 y2)
| IOptional x1, IOptional x2 -> equal_descr x1 x2
| ITimes (x1,y1), ITimes (x2,y2)
| IXml (x1,y1), IXml (x2,y2)
| IArrow (x1,y1), IArrow (x2,y2) -> (equal_slot x1 x2) && (equal_slot y1 y2)
| IRecord (o1,r1), IRecord (o2,r2) -> (o1 = o2) && (LabelMap.equal equal_slot r1 r2)
| ICapture x1, ICapture x2 -> Id.equal x1 x2
| IConstant (x1,y1), IConstant (x2,y2) -> (Id.equal x1 x2) && (Types.equal_const y1 y2)
| _ -> false
and equal_slot s1 s2 =
((s1.gen1 = !gen) && (s2.gen2 = !gen) && (s1.rank1 = s2.rank2))
||
((s1.gen1 <> !gen) && (s2.gen2 <> !gen) && (
incr rank;
s1.rank1 <- !rank; s1.gen1 <- !gen;
s2.rank2 <- !rank; s2.gen2 <- !gen;
equal_descr (descr s1) (descr s2)
))
module Arg = struct
type t = slot
let hash s =
match s.hash with
| Some h -> h
| None ->
incr gen; rank := 0;
let h = hash_slot s in
s.hash <- Some h;
h
let equal s1 s2 = incr gen; rank := 0; equal_slot s1 s2
end
module SlotTable = Hashtbl.Make(Arg)
let rec fv_slot s =
match s.fv with
| Some x -> x
| None ->
if s.gen1 = !gen then IdSet.empty
else (s.gen1 <- !gen; fv_descr (descr s))
and fv_descr = function
| IOr (d1,d2)
| IAnd (d1,d2)
| IDiff (d1,d2) -> IdSet.cup (fv_descr d1) (fv_descr d2)
| IOptional d -> fv_descr d
| ITimes (s1,s2)
| IXml (s1,s2)
| IArrow (s1,s2) -> IdSet.cup (fv_slot s1) (fv_slot s2)
| IRecord (o,r) -> List.fold_left IdSet.cup IdSet.empty (LabelMap.map_to_list fv_slot r)
| ICapture x | IConstant (x,_) -> IdSet.singleton x
| _ -> IdSet.empty
let compute_fv s =
match s.fv with
| Some x -> ()
| None ->
incr gen;
let x = fv_slot s in
s.fv <- Some x
let counter = ref 0
let todo = ref []
let rec flush_fv () =
List.iter compute_fv !todo;
todo := []
let mk () =
let s =
{ d = None;
fv = None;
hash = None;
rank1 = 0; rank2 = 0;
gen1 = 0; gen2 = 0 } in
todo := s :: !todo;
s
let compile_hash = Ast.PpatTable.create 65
let defs = ref []
let rec compile env { loc = loc; descr = d } =
match (d : Ast.ppat') with
| PatVar v ->
let (d,loop) =
try TypeEnv.find v env
with Not_found ->
raise_loc_generic loc ("Undefined type variable " ^ v) in
if !loop then
raise_loc_generic loc ("Unguarded recursion on type/pattern variable " ^ v);
loop := true;
let r = compile env d in
loop := false;
r
| Recurs (t, b) -> compile (compile_many env b) t
| Regexp (r,q) -> compile env (Regexp.compile loc r q)
| Internal t -> IType t
| Or (t1,t2) -> IOr (compile env t1, compile env t2)
| And (t1,t2) -> IAnd (compile env t1, compile env t2)
| Diff (t1,t2) -> IDiff (compile env t1, compile env t2)
| Prod (t1,t2) -> ITimes (compile_slot env t1, compile_slot env t2)
| XmlT (t1,t2) -> IXml (compile_slot env t1, compile_slot env t2)
| Arrow (t1,t2) -> IArrow (compile_slot env t1, compile_slot env t2)
| Optional t -> IOptional (compile env t)
| Record (o,r) -> IRecord (o, LabelMap.map (compile_slot env) r)
| Constant (x,v) -> IConstant (x,v)
| Capture x -> ICapture x
and compile_slot env ({ loc = loc; descr = d } as p) =
try Ast.PpatTable.find compile_hash p
with Not_found ->
let s = mk () in
defs := (s,p,env) :: !defs;
Ast.PpatTable.add compile_hash p s;
s
and compile_many env b =
List.fold_left (fun env (v,p) -> TypeEnv.add v (p,ref false) env) env b
let rec flush_defs () =
match !defs with
| [] -> ()
| (s,p,env)::t -> defs := t; s.d <- Some (compile env p); flush_defs ()
let typ_nodes = SlotTable.create 67
let pat_nodes = SlotTable.create 67
let rec typ = function
| IType t -> t
| IOr (s1,s2) -> Types.cup (typ s1) (typ s2)
| IAnd (s1,s2) -> Types.cap (typ s1) (typ s2)
| IDiff (s1,s2) -> Types.diff (typ s1) (typ s2)
| ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
| IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2)
| IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
| IOptional s -> Types.Record.or_absent (typ s)
| IRecord (o,r) -> Types.record' (o, LabelMap.map typ_node r)
| ICapture x | IConstant (x,_) -> assert false
and typ_node s : Types.node =
try SlotTable.find typ_nodes s
with Not_found ->
let x = Types.make () in
SlotTable.add typ_nodes s x;
Types.define x (typ (descr s));
x
let rec pat d : Patterns.descr =
if IdSet.is_empty (fv_descr d)
then Patterns.constr (typ d)
else pat_aux d
and pat_aux = function
| IOr (s1,s2) -> Patterns.cup (pat s1) (pat s2)
| IAnd (s1,s2) -> Patterns.cap (pat s1) (pat s2)
| IDiff (s1,s2) when IdSet.is_empty (fv_descr s2) ->
let s2 = Types.neg (typ s2) in
Patterns.cap (pat s1) (Patterns.constr s2)
| IDiff _ ->
raise (Patterns.Error "Difference not allowed in patterns")
| ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
| IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
| IOptional _ ->
raise (Patterns.Error "Optional field not allowed in record patterns")
| IRecord (o,r) ->
let pats = ref [] in
let aux l s =
if IdSet.is_empty (fv_slot s) then typ_node s
else
( pats := Patterns.record l (pat_node s) :: !pats;
Types.any_node )
in
let constr = Types.record' (o,LabelMap.mapi aux r) in
List.fold_left Patterns.cap (Patterns.constr constr) !pats
(* TODO: can avoid constr when o=true, and all fields have fv *)
| ICapture x -> Patterns.capture x
| IConstant (x,c) -> Patterns.constant x c
| IArrow _ ->
raise (Patterns.Error "Arrow not allowed in patterns")
| IType _ -> assert false
and pat_node s : Patterns.node =
try SlotTable.find pat_nodes s
with Not_found ->
let x = Patterns.make (fv_slot s) in
SlotTable.add pat_nodes s x;
Patterns.define x (pat (descr s));
x
let glb = State.ref "Typer.glb_env" TypeEnv.empty
let register_global_types b =
List.iter (fun (v, { loc = loc }) ->
if TypeEnv.mem v !glb
then raise_loc_generic loc ("Multiple definition for type " ^ v)
) b;
glb := compile_many !glb b;
let b = List.map (fun (v,p) -> (v,p,compile !glb p)) b in
flush_defs ();
flush_fv ();
List.iter (fun (v,p,s) ->
if not (IdSet.is_empty (fv_descr s)) then
raise_loc_generic p.loc "Capture variables are not allowed in types";
Types.Print.register_global v (typ s)) b
let typ p =
let s = compile_slot !glb p in
flush_defs ();
flush_fv ();
if IdSet.is_empty (fv_slot s) then typ_node s
else raise_loc_generic p.loc "Capture variables are not allowed in types"
let pat p =
let s = compile_slot !glb p in
flush_defs ();
flush_fv ();
try pat_node s
with Patterns.Error e -> raise_loc_generic p.loc e
| Location (loc,exn) when loc = noloc -> raise (Location (p.loc, exn))
*)
(* Internal representation as a graph (desugar recursive types and regexp),
to compute freevars, etc... *)
type ti = {
id : int;
mutable seen : bool;
mutable loc' : loc;
mutable fv : fv option;
mutable descr': descr;
mutable type_node: Types.node option;
mutable pat_node: Patterns.node option
}
and descr =
| IAlias of string * ti
| IType of Types.descr
| IOr of ti * ti
| IAnd of ti * ti
| IDiff of ti * ti
| ITimes of ti * ti
| IXml of ti * ti
| IArrow of ti * ti
| IOptional of ti
| IRecord of bool * ti label_map
| ICapture of id
| IConstant of id * Types.const
type glb = ti TypeEnv.t
let mk' =
let counter = ref 0 in
fun loc ->
incr counter;
let rec x = {
id = !counter;
seen = false;
loc' = loc;
fv = None;
descr' = IAlias ("__dummy__", x);
type_node = None;
pat_node = None
} in
x
let cons loc d =
let x = mk' loc in
x.descr' <- d;
x
let rec compile env { loc = loc; descr = d } : ti =
......@@ -376,24 +659,26 @@ let mk_typ e =
else raise_loc_generic e.loc' "Capture variables are not allowed in types"
let typ glb e =
mk_typ (compile glb e)
let glb = State.ref "Typer.glb_env" TypeEnv.empty
let typ e =
mk_typ (compile !glb e)
let pat glb e =
pat_node (compile glb e)
let pat e =
pat_node (compile !glb e)
let register_global_types glb b =
let env' = compile_many glb b in
List.fold_left
(fun glb (v,{ loc = loc }) ->
let register_global_types b =
let env' = compile_many !glb b in
List.iter
(fun (v,{ loc = loc }) ->
let t = TypeEnv.find v env' in
let d = Types.descr (mk_typ t) in
(* let d = Types.normalize d in*)
Types.Print.register_global v d;
if TypeEnv.mem v glb
if TypeEnv.mem v !glb
then raise_loc_generic loc ("Multiple definition for type " ^ v);
TypeEnv.add v t glb
) glb b
glb := TypeEnv.add v t !glb
) b
......@@ -404,19 +689,19 @@ module Fv = IdSet
(* IDEA: introduce a node Loc in the AST to override nolocs
in sub-expressions *)
let rec expr loc' glb { loc = loc; descr = d } =
let rec expr loc' { loc = loc; descr = d } =
let loc = if loc = noloc then loc' else loc in
let (fv,td) =
match d with
| Forget (e,t) ->
let (fv,e) = expr loc glb e and t = typ glb t in
let (fv,e) = expr loc e and t = typ t in
(fv, Typed.Forget (e,t))
| Var s -> (Fv.singleton s, Typed.Var s)
| Apply (e1,e2) ->
let (fv1,e1) = expr loc glb e1 and (fv2,e2) = expr loc glb e2 in
let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
(Fv.cup fv1 fv2, Typed.Apply (e1,e2))
| Abstraction a ->
let iface = List.map (fun (t1,t2) -> (typ glb t1, typ glb t2))
let iface = List.map (fun (t1,t2) -> (typ t1, typ t2))
a.fun_iface in
let t = List.fold_left
(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
......@@ -424,7 +709,7 @@ let rec expr loc' glb { loc = loc; descr = d } =
let iface = List.map
(fun (t1,t2) -> (Types.descr t1, Types.descr t2))
iface in
let (fv0,body) = branches loc glb a.fun_body in
let (fv0,body) = branches loc a.fun_body in
let fv = match a.fun_name with
| None -> fv0
| Some f -> Fv.remove f fv0 in
......@@ -439,46 +724,46 @@ let rec expr loc' glb { loc = loc; descr = d } =
)
| Cst c -> (Fv.empty, Typed.Cst c)
| Pair (e1,e2) ->
let (fv1,e1) = expr loc glb e1 and (fv2,e2) = expr loc glb e2 in
let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
(Fv.cup fv1 fv2, Typed.Pair (e1,e2))