Commit 12e61f59 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-09-25 22:48:47 by cvscast] Cleaning

Original author: cvscast
Date: 2003-09-25 22:48:47+00:00
parent bbab8a37
......@@ -4,13 +4,12 @@ open Ident
let quiet = ref false
let toplevel = ref false
let typing_env = State.ref "Cduce.typing_env" Env.empty
let typing_env = State.ref "Cduce.typing_env" Builtin.env
let eval_env = State.ref "Cduce.eval_env" Env.empty
let enter_global_value x v t =
eval_env := Env.add x v !eval_env;
typing_env := Env.add x t !typing_env
typing_env := Typer.enter_value x t !typing_env
let rec is_abstraction = function
| Ast.Abstraction _ -> true
......@@ -32,14 +31,14 @@ let print_value ppf v =
Location.protect ppf (fun ppf -> Value.print ppf v)
let dump_env ppf =
Format.fprintf ppf "Types:%t@." Typer.dump_global_types;
Format.fprintf ppf "Namespace prefixes:@\n%t" Typer.dump_global_ns;
Format.fprintf ppf "Types:%a@." Typer.dump_types !typing_env;
Format.fprintf ppf "Namespace prefixes:@\n%a" Typer.dump_ns !typing_env;
Format.fprintf ppf "Namespace prefixes used for pretty-printing:@.%t"
Ns.InternalPrinter.dump;
Format.fprintf ppf "Values:@\n";
Env.iter
(fun x v ->
let t = Env.find x !typing_env in
let t = Typer.find_value x !typing_env in
Format.fprintf ppf "@[val %a : @[%a = %a@]@]@."
U.print (Id.value x) print_norm t print_value v
)
......@@ -102,41 +101,41 @@ let rec print_exn ppf = function
let debug ppf = function
| `Subtype (t1,t2) ->
Format.fprintf ppf "[DEBUG:subtype]@.";
let t1 = Types.descr (Typer.typ t1)
and t2 = Types.descr (Typer.typ t2) in
let t1 = Types.descr (Typer.typ !typing_env t1)
and t2 = Types.descr (Typer.typ !typing_env t2) in
let s = Types.subtype t1 t2 in
Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<=" print_norm t2 s
| `Sample t ->
Format.fprintf ppf "[DEBUG:sample]@.";
(try
let t = Types.descr (Typer.typ t) in
let t = Types.descr (Typer.typ !typing_env t) in
Format.fprintf ppf "%a@." print_sample (Sample.get t)
with Not_found ->
Format.fprintf ppf "Empty type : no sample !@.")
| `Filter (t,p) ->
Format.fprintf ppf "[DEBUG:filter]@.";
let t = Typer.typ t
and p = Typer.pat p in
let t = Typer.typ !typing_env t
and p = Typer.pat !typing_env p in
let f = Patterns.filter (Types.descr t) p in
List.iter (fun (x,t) ->
Format.fprintf ppf " %a:%a@." U.print (Id.value x)
print_norm (Types.descr t)) f
| `Accept p ->
Format.fprintf ppf "[DEBUG:accept]@.";
let p = Typer.pat p in
let p = Typer.pat !typing_env p in
let t = Patterns.accept p in
Format.fprintf ppf " %a@." Types.Print.print (Types.descr t)
| `Compile (t,pl) ->
Format.fprintf ppf "[DEBUG:compile]@.";
let t = Typer.typ t
and pl = List.map Typer.pat pl in
let t = Typer.typ !typing_env t
and pl = List.map (Typer.pat !typing_env) pl in
Patterns.Compile.debug_compile ppf t pl
let insert_bindings ppf =
List.iter2
(fun (x,t) (y,v) ->
assert (x = y);
typing_env := Env.add x t !typing_env;
typing_env := Typer.enter_value x t !typing_env;
eval_env := Env.add x v !eval_env;
if not !quiet then
Format.fprintf ppf "val %a : @[@[%a@] =@ @[%a@]@]@."
......@@ -144,7 +143,7 @@ let insert_bindings ppf =
let rec collect_funs ppf accu = function
| { descr = Ast.FunDecl e } :: rest ->
let (_,e) = Typer.expr e in
let (_,e) = Typer.expr !typing_env e in
collect_funs ppf (e::accu) rest
| rest ->
let typs = Typer.type_rec_funs !typing_env accu in
......@@ -157,7 +156,8 @@ let rec collect_types ppf accu = function
| { descr = Ast.TypeDecl (x,t) } :: rest ->
collect_types ppf ((x,t) :: accu) rest
| rest ->
Typer.register_global_types accu;
typing_env :=
Typer.enter_types (Typer.type_defs !typing_env accu) !typing_env;
rest
let rec phrases ppf phs = match phs with
......@@ -169,10 +169,10 @@ let rec phrases ppf phs = match phs with
Typer.register_schema name schema;
phrases ppf rest
| { descr = Ast.Namespace (pr,ns) } :: rest ->
Typer.register_global_ns pr ns;
typing_env := Typer.enter_ns pr ns !typing_env;
phrases ppf rest
| { descr = Ast.EvalStatement e } :: rest ->
let (fv,e) = Typer.expr e in
let (fv,e) = Typer.expr !typing_env e in
let t = Typer.type_check !typing_env e Types.any true in
Typer.report_unused_branches ();
if not !quiet then
......@@ -182,7 +182,7 @@ let rec phrases ppf phs = match phs with
Format.fprintf ppf "- : @[@[%a@] =@ @[%a@]@]@." print_norm t print_value v;
phrases ppf rest
| { descr = Ast.LetDecl (p,e) } :: rest ->
let decl = Typer.let_decl p e in
let decl = Typer.let_decl !typing_env p e in
let typs = Typer.type_let_decl !typing_env decl in
Typer.report_unused_branches ();
let vals = Eval.eval_let_decl !eval_env decl in
......@@ -198,7 +198,7 @@ let rec phrases ppf phs = match phs with
dump_env ppf;
phrases ppf rest
| { descr = Ast.Directive `Reinit_ns } :: rest ->
Typer.set_ns_table_for_printer ();
Typer.set_ns_table_for_printer !typing_env;
phrases ppf rest
| [] -> ()
......
......@@ -18,12 +18,10 @@ let types =
"Bool", bool
]
let () =
List.iter
(fun (n,t) ->
Typer.register_global_types
[ Ident.ident (Ident.U.mk n),
Location.mknoloc (Ast.Internal t)])
let env =
List.fold_left
(fun accu (n,t) -> Typer.enter_type (Ident.ident (Ident.U.mk n)) t accu)
Typer.empty_env
types
(* Operators *)
......
(*
No values exported.
Are you looking for builtin types? Then look at types/builtin_defs.mli
*)
val env: Typer.env
(* Typing environment with built-in types *)
......@@ -14,15 +14,51 @@ let warning loc msg =
Location.html_hilight (loc,`Full)
msg
type tenv = {
tenv_names : Types.t Env.t;
type item =
| Type of Types.t
| Value of Types.t
type env = {
ids : item Env.t;
tenv_nspref: Ns.table;
}
let empty_env = {
ids = Env.empty;
tenv_nspref = Ns.empty_table;
}
let enter_type id t env =
{ env with ids = Env.add id (Type t) env.ids }
let enter_types l env =
{ env with ids =
List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }
let find_type id env =
match Env.find id env.ids with
| Type t -> t
| Value _ -> raise Not_found
let enter_value id t env =
{ env with ids = Env.add id (Value t) env.ids }
let enter_values l env =
{ env with ids =
List.fold_left (fun accu (id,t) -> Env.add id (Value t) accu) env.ids l }
let find_value id env =
match Env.find id env.ids with
| Value t -> t
| _ -> raise Not_found
(* Namespaces *)
let set_ns_table_for_printer env =
Ns.InternalPrinter.set_table env.tenv_nspref
let get_ns_table tenv = tenv.tenv_nspref
let enter_ns p ns env =
{ env with tenv_nspref = Ns.add_prefix p ns env.tenv_nspref }
let protect_error_ns loc f x =
try f x
with Ns.UnknownPrefix ns ->
......@@ -165,7 +201,7 @@ let mk_slot () =
(* This environment is used in phase (1) to eliminate recursion *)
type penv = {
penv_tenv : tenv;
penv_tenv : env;
penv_derec : derecurs_slot Env.t;
}
......@@ -343,7 +379,7 @@ let rec derecurs env p = match p.descr with
| PatVar v ->
(try PAlias (Env.find v env.penv_derec)
with Not_found ->
try PType (Env.find v env.penv_tenv.tenv_names)
try PType (find_type v env.penv_tenv)
with Not_found -> PCapture v)
| SchemaVar (kind, schema, item) ->
PType (derecurs_schema env kind schema item)
......@@ -591,14 +627,14 @@ and pat_node s : Patterns.node =
(* For the toplevel ... *)
let register_types glb b =
let type_defs env b =
List.iter
(fun (v,p) ->
if Env.mem v glb.tenv_names
then raise_loc_generic p.loc ("Multiple definition for type " ^ (Ident.to_string v))
if Env.mem v env.ids
then raise_loc_generic p.loc ("Identifier " ^ (Ident.to_string v) ^ " is already bound")
) b;
let env = derecurs_def (penv glb) b in
let b = List.map (fun (v,p) -> (v,p,compile (derecurs env p))) b in
let penv = derecurs_def (penv env) b in
let b = List.map (fun (v,p) -> (v,p,compile (derecurs penv p))) b in
flush_defs ();
let b =
List.map
......@@ -610,17 +646,17 @@ let register_types glb b =
("This definition yields an empty type for " ^ (Ident.to_string v));
(v,t)) b in
List.iter (fun (v,t) -> Types.Print.register_global (Id.value v) t) b;
let n = List.fold_left (fun accu (v,t) -> Env.add v t accu) glb.tenv_names b in
{ glb with tenv_names = n }
b
let register_ns glb p ns =
{ glb with tenv_nspref = Ns.add_prefix p ns glb.tenv_nspref }
let dump_types ppf glb =
Env.iter (fun v _ -> Format.fprintf ppf " %a" Ident.print v) glb.tenv_names
let dump_types ppf env =
Env.iter (fun v ->
function
(Type _) -> Format.fprintf ppf " %a" Ident.print v
| _ -> ()) env.ids
let dump_ns ppf glb =
Ns.dump_table ppf glb.tenv_nspref
let dump_ns ppf env =
Ns.dump_table ppf env.tenv_nspref
let do_typ loc r =
......@@ -629,11 +665,11 @@ let do_typ loc r =
check_no_capture loc (fv_slot s);
typ_node s
let typ glb p =
do_typ p.loc (derecurs (penv glb) p)
let typ env p =
do_typ p.loc (derecurs (penv env) p)
let pat glb p =
let s = compile_slot (derecurs (penv glb) p) in
let pat env p =
let s = compile_slot (derecurs (penv env) p) in
flush_defs ();
try pat_node s
with Patterns.Error e -> raise_loc_generic p.loc e
......@@ -643,7 +679,7 @@ let pat glb p =
(* II. Build skeleton *)
type op = [ `Unary of tenv -> Typed.unary_op | `Binary of tenv -> Typed.binary_op ]
type op = [ `Unary of env -> Typed.unary_op | `Binary of env -> Typed.binary_op ]
let op_table : (string,op) Hashtbl.t = Hashtbl.create 31
let register_unary_op s f = Hashtbl.add op_table s (`Unary f)
let register_binary_op s f = Hashtbl.add op_table s (`Binary f)
......@@ -664,18 +700,18 @@ let exp loc fv e =
}
let rec expr glb loc = function
| LocatedExpr (loc,e) -> expr glb loc e
let rec expr env loc = function
| LocatedExpr (loc,e) -> expr env loc e
| Forget (e,t) ->
let (fv,e) = expr glb loc e and t = typ glb t in
let (fv,e) = expr env loc e and t = typ env t in
exp loc fv (Typed.Forget (e,t))
| Var s ->
exp loc (Fv.singleton s) (Typed.Var s)
| Apply (e1,e2) ->
let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
exp loc (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 env t1, typ env t2))
a.fun_iface in
let t = List.fold_left
(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
......@@ -683,7 +719,7 @@ let rec expr glb loc = function
let iface = List.map
(fun (t1,t2) -> (Types.descr t1, Types.descr t2))
iface in
let (fv0,body) = branches glb a.fun_body in
let (fv0,body) = branches env a.fun_body in
let fv = match a.fun_name with
| None -> fv0
| Some f -> Fv.remove f fv0 in
......@@ -696,79 +732,79 @@ let rec expr glb loc = function
} in
exp loc fv e
| (Integer _ | Char _ | Atom _) as c ->
exp loc Fv.empty (Typed.Cst (const glb loc c))
exp loc Fv.empty (Typed.Cst (const env loc c))
| Pair (e1,e2) ->
let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
| Xml (e1,e2) ->
let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2))
| Dot (e,l) ->
let (fv,e) = expr glb loc e in
exp loc fv (Typed.Dot (e,parse_label glb loc l))
let (fv,e) = expr env loc e in
exp loc fv (Typed.Dot (e,parse_label env loc l))
| RemoveField (e,l) ->
let (fv,e) = expr glb loc e in
exp loc fv (Typed.RemoveField (e,parse_label glb loc l))
let (fv,e) = expr env loc e in
exp loc fv (Typed.RemoveField (e,parse_label env loc l))
| RecordLitt r ->
let fv = ref Fv.empty in
let r = parse_record glb loc
let r = parse_record env loc
(fun e ->
let (fv2,e) = expr glb loc e
let (fv2,e) = expr env loc e
in fv := Fv.cup !fv fv2; e)
r in
exp loc !fv (Typed.RecordLitt r)
| String (i,j,s,e) ->
let (fv,e) = expr glb loc e in
let (fv,e) = expr env loc e in
exp loc fv (Typed.String (i,j,s,e))
| Op (op,le) ->
let (fvs,ltes) = List.split (List.map (expr glb loc) le) in
let (fvs,ltes) = List.split (List.map (expr env loc) le) in
let fv = List.fold_left Fv.cup Fv.empty fvs in
(try
(match (ltes,find_op op) with
| [e], `Unary op -> exp loc fv (Typed.UnaryOp (op glb, e))
| [e1;e2], `Binary op -> exp loc fv (Typed.BinaryOp (op glb, e1,e2))
| [e], `Unary op -> exp loc fv (Typed.UnaryOp (op env, e))
| [e1;e2], `Binary op -> exp loc fv (Typed.BinaryOp (op env, e1,e2))
| _ -> assert false)
with Not_found -> assert false)
| Match (e,b) ->
let (fv1,e) = expr glb loc e
and (fv2,b) = branches glb b in
let (fv1,e) = expr env loc e
and (fv2,b) = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
| Map (e,b) ->
let (fv1,e) = expr glb loc e
and (fv2,b) = branches glb b in
let (fv1,e) = expr env loc e
and (fv2,b) = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
| Transform (e,b) ->
let (fv1,e) = expr glb loc e
and (fv2,b) = branches glb b in
let (fv1,e) = expr env loc e
and (fv2,b) = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
| Xtrans (e,b) ->
let (fv1,e) = expr glb loc e
and (fv2,b) = branches glb b in
let (fv1,e) = expr env loc e
and (fv2,b) = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
| Validate (e,schema,elt) ->
let (fv,e) = expr glb loc e in
let (fv,e) = expr env loc e in
exp loc fv (Typed.Validate (e, schema, elt))
| Try (e,b) ->
let (fv1,e) = expr glb loc e
and (fv2,b) = branches glb b in
let (fv1,e) = expr env loc e
and (fv2,b) = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
| NamespaceIn (pr,ns,e) ->
let glb = register_ns glb pr ns in
expr glb loc e
let env = enter_ns pr ns env in
expr env loc e
| Ref (e,t) ->
let (fv,e) = expr glb loc e and t = typ glb t in
let (fv,e) = expr env loc e and t = typ env t in
exp loc fv (Typed.Ref (e,t))
and branches glb b =
and branches env b =
let fv = ref Fv.empty in
let accept = ref Types.empty in
let branch (p,e) =
let cur_br = !cur_branch in
cur_branch := [];
let (fv2,e) = expr glb noloc e in
let (fv2,e) = expr env noloc e in
let br_loc = merge_loc p.loc e.Typed.exp_loc in
let p = pat glb p in
let p = pat env p in
(match Fv.pick (Fv.diff (Patterns.fv p) fv2) with
| None -> ()
| Some x ->
......@@ -797,38 +833,20 @@ let rec expr glb loc = function
}
)
let expr glb = expr glb noloc
let expr env = expr env noloc
let let_decl glb p e =
let (_,e) = expr glb e in
{ Typed.let_pat = pat glb p;
let let_decl env p e =
let (_,e) = expr env e in
{ Typed.let_pat = pat env p;
Typed.let_body = e;
Typed.let_compiled = None }
(* Hide global "typing/parsing" environment *)
let glb = State.ref "Typer.glb_env"
{ tenv_names = Env.empty;
tenv_nspref = Ns.empty_table }
let pat p = pat !glb p
let typ t = typ !glb t
let expr e = expr !glb e
let let_decl p e = let_decl !glb p e
let register_global_types l = glb := register_types !glb l
let dump_global_types ppf = dump_types ppf !glb
let register_global_ns p ns = glb := register_ns !glb p ns
let dump_global_ns ppf = dump_ns ppf !glb
let set_ns_table_for_printer () = Ns.InternalPrinter.set_table !glb.tenv_nspref
(* III. Type-checks *)
type env = Types.descr Env.t
open Typed
let require loc t s =
......@@ -880,7 +898,7 @@ and type_check' loc env e constr precise = match e with
in
let env = match a.fun_name with
| None -> env
| Some f -> Env.add f a.fun_typ env in
| Some f -> enter_value f a.fun_typ env in
List.iter
(fun (t1,t2) ->
let acc = a.fun_body.br_accept in
......@@ -940,10 +958,9 @@ and type_check' loc env e constr precise = match e with
| Var s ->
let t =
try Env.find s env
try find_value s env
with Not_found ->
raise_loc loc
(UnboundId (s, Env.mem s !glb.tenv_names) ) in
raise_loc loc (UnboundId (s, Env.mem s env.ids) ) in
check loc t constr
| Cst c ->
......@@ -1071,9 +1088,8 @@ and branches_aux loc env targ tres constr precise = function
else
( b.br_used <- true;
let res = Patterns.filter targ' p in
let env' = List.fold_left
(fun env (x,t) -> Env.add x (Types.descr t) env)
env res in
let res = List.map (fun (x,t) -> (x,Types.descr t)) res in
let env' = enter_values res env in
let t = type_check env' b.br_body constr precise in
let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc in
......@@ -1116,13 +1132,13 @@ and type_rec_funs env l =
(fun accu -> function
| { exp_descr=Abstraction { fun_typ = t; fun_name = Some f };
exp_loc=loc } ->
if Env.mem f !glb.tenv_names then
if Env.mem f env.ids then
error loc "This function name clashes with a type name";
(f,t) :: accu
| _ -> assert false
) [] l
in
let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
let env' = enter_values types env in
List.iter (fun e -> ignore (type_check env' e Types.any false)) l;
types
......
......@@ -10,28 +10,30 @@ exception Error of string
val warning: Location.loc -> string -> unit
val error: Location.loc -> string -> 'a
type tenv
(*
val typ_def: tenv -> (id * Ast.ppat) list -> (id * Types.t)
val typ_expr: tenv -> Ast.ppat -> Types.Node.t
val pat_expr: tenv -> Ast.ppat -> Patterns.node
*)
type env
val empty_env: env
val get_ns_table : env -> Ns.table
val get_ns_table : tenv -> Ns.table
val enter_ns : U.t -> Ns.t -> env -> env
val register_global_types : (id * Ast.ppat) list -> unit
val register_global_ns : U.t -> Ns.t -> unit
val dump_global_types: Format.formatter -> unit
val dump_global_ns: Format.formatter -> unit
val enter_value: id -> Types.t -> env -> env
val enter_values: (id * Types.t) list -> env -> env
val find_value: id -> env -> Types.t
val set_ns_table_for_printer: unit -> unit
val enter_type: id -> Types.t -> env -> env
val enter_types: (id * Types.t) list -> env -> env
val find_type: id -> env -> Types.t
val typ : Ast.ppat -> Typed.ttyp
val pat : Ast.ppat -> Typed.tpat
val expr: Ast.pexpr -> fv * Typed.texpr
val let_decl : Ast.ppat -> Ast.pexpr -> Typed.let_decl
val type_defs: env -> (id * Ast.ppat) list -> (id * Types.t) list
val typ: env -> Ast.ppat -> Types.Node.t
val pat: env -> Ast.ppat -> Patterns.node
type env = Types.descr Env.t
val dump_types: Format.formatter -> env -> unit
val dump_ns: Format.formatter -> env -> unit
val set_ns_table_for_printer: env -> unit
val expr: env -> Ast.pexpr -> fv * Typed.texpr
val let_decl : env -> Ast.ppat -> Ast.pexpr -> Typed.let_decl
val type_check:
env -> Typed.texpr -> Types.descr -> bool -> Types.descr
......@@ -39,9 +41,9 @@ 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 -> (id * Types.descr) list
val type_let_decl: env -> Typed.let_decl -> (id * Types.t) list