typage des termes et des formules (suite)

parent ea9cdc7b
......@@ -183,6 +183,7 @@ val t_label_add : label -> term -> term
val f_app : psymbol -> term list -> fmla
val f_forall : vsymbol -> fmla -> fmla
val f_exists : vsymbol -> fmla -> fmla
val f_quant : quant -> vsymbol -> fmla -> fmla
val f_and : fmla -> fmla -> fmla
val f_or : fmla -> fmla -> fmla
val f_implies : fmla -> fmla -> fmla
......
......@@ -13,7 +13,15 @@ logic length : 'a list -> int
logic is_nil : 'a list -> prop
axiom a : forall x:'a list. if true then not false else false
logic eq : 'a, 'a -> prop
axiom a : forall x:'a list. forall y: 'a list. eq(x, y)
......
......@@ -16,6 +16,7 @@
open Util
open Format
open Pp
open Term
open Ptree
......@@ -29,6 +30,10 @@ type error =
| Clash of string
| PredicateExpected
| TermExpected
| UnboundSymbol of string
| TermExpectedType of (formatter -> unit) * (formatter -> unit)
(* actual / expected *)
| BadNumberOfArguments of Name.t * int * int
exception Error of error
......@@ -52,6 +57,14 @@ let report fmt = function
fprintf fmt "syntax error: predicate expected"
| TermExpected ->
fprintf fmt "syntax error: term expected"
| UnboundSymbol s ->
fprintf fmt "Unbound symbol '%s'" s
| BadNumberOfArguments (s, n, m) ->
fprintf fmt "@[Symbol `%a' is aplied to %d terms,@ " Name.print s n;
fprintf fmt "but is expecting %d arguments@]" m
| TermExpectedType (ty1, ty2) ->
fprintf fmt "@[This term has type "; ty1 fmt;
fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
(** typing environments *)
......@@ -107,11 +120,24 @@ and type_var = {
mutable type_val : dty option;
}
let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
| Tyvar { type_val = None; tvsymbol = v } ->
fprintf fmt "'%a" Name.print v
| Tyapp (s, []) ->
fprintf fmt "%a" Name.print s.Ty.ts_name
| Tyapp (s, [t]) ->
fprintf fmt "%a %a" print_dty t Name.print s.Ty.ts_name
| Tyapp (s, l) ->
fprintf fmt "(%a) %a"
(print_list comma print_dty) l Name.print s.Ty.ts_name
let create_type_var =
let t = ref 0 in
fun ~user x ->
fun ~user tv ->
incr t;
{ tag = !t; user = user; tvsymbol = Name.from_string x; type_val = None }
{ tag = !t; user = user; tvsymbol = tv; type_val = None }
let rec occurs v = function
| Tyvar { type_val = Some t } -> occurs v t
......@@ -142,19 +168,36 @@ let rec unify t1 t2 = match t1, t2 with
(** environment + destructive type variables environment *)
module Htv = Hashtbl.Make(Name)
type denv = {
env : env;
dvars : (string, type_var) Hashtbl.t;
utyvars : (string, type_var) Hashtbl.t; (* user type vars *)
dtyvars : type_var Htv.t; (* destructive type vars *)
dvars : dty M.t;
}
let create_denv env = { env = env; dvars = Hashtbl.create 17 }
let create_denv env = {
env = env;
utyvars = Hashtbl.create 17;
dtyvars = Htv.create 17;
dvars = M.empty;
}
let find_type_var x env =
let find_user_type_var x env =
try
Hashtbl.find env.utyvars x
with Not_found ->
let v = create_type_var ~user:true (Name.from_string x) in
Hashtbl.add env.utyvars x v;
v
let find_type_var tv env =
try
Hashtbl.find env.dvars x
Htv.find env.dtyvars tv
with Not_found ->
let v = create_type_var ~user:true x in
Hashtbl.add env.dvars x v;
let v = create_type_var ~user:false tv in
Htv.add env.dtyvars tv v;
v
(** typing types *)
......@@ -162,7 +205,7 @@ let find_type_var x env =
(* parsed types -> intermediate types *)
let rec dty env = function
| PPTvarid (x, _) ->
Tyvar (find_type_var x env)
Tyvar (find_user_type_var x env)
| PPTexternal (p, id, loc) ->
if not (M.mem id env.env.tysymbols) then error ~loc (UnboundType id);
let s = M.find id env.env.tysymbols in
......@@ -172,13 +215,19 @@ let rec dty env = function
Tyapp (s, List.map (dty env) p)
(* intermediate types -> types *)
let rec ty env = function
let rec ty = function
| Tyvar { type_val = Some t } ->
ty env t
ty t
| Tyvar { tvsymbol = tv } ->
Ty.ty_var tv
| Tyapp (s, tl) ->
Ty.ty_app s (List.map (ty env) tl)
Ty.ty_app s (List.map ty tl)
let rec specialize env t = match t.Ty.ty_node with
| Ty.Tyvar tv ->
Tyvar (find_type_var tv env)
| Ty.Tyapp (s, tl) ->
Tyapp (s, List.map (specialize env) tl)
(** typing terms and formulas *)
......@@ -186,7 +235,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
| Tbvar of int
| Tvar of vsymbol
| Tvar of string
| Tapp of fsymbol * dterm list
| Tlet of dterm * string * dterm
(* | Tcase of dterm * tbranch list *)
......@@ -194,7 +243,7 @@ and dterm_node =
and dfmla =
| Fapp of psymbol * dterm list
| Fquant of quant * string * dfmla
| Fquant of quant * string * dty * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
......@@ -210,7 +259,38 @@ let binop = function
| PPiff -> Fiff
| _ -> assert false
let rec dterm env t = match t.pp_desc with
let specialize_fsymbol x env =
let s = find_fsymbol x env.env in
let tl, t = s.fs_scheme in
s, List.map (specialize env) tl, specialize env t
let rec dterm env t =
let n, ty = dterm_node t.pp_loc env t.pp_desc in
{ dt_node = n; dt_ty = ty }
and dterm_node loc env = function
| PPvar x ->
begin try
(* local variable *)
let ty = M.find x env.dvars in
Tvar x, ty
with Not_found -> try
(* 0-arity symbol (constant) *)
let s, tyl, ty = specialize_fsymbol x env in
let n = List.length tyl in
if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
Tapp (s, []), ty
with Not_found ->
error ~loc (UnboundSymbol x)
end
| PPapp (x, tl) ->
begin try
let s, tyl, ty = specialize_fsymbol x env in
let tl = dtype_args s.fs_name loc env tyl tl in
Tapp (s, tl), ty
with Not_found ->
error ~loc (UnboundSymbol x)
end
| _ ->
assert false (*TODO*)
......@@ -227,13 +307,51 @@ and dfmla env e = match e.pp_desc with
error ~loc:e.pp_loc PredicateExpected
| PPif (a, b, c) ->
Fif (dfmla env a, dfmla env b, dfmla env c)
| PPforall (id, pt, _, a) -> (* TODO: triggers *)
assert false (*TODO*)
| PPforall (id, ty, _, a) -> (* TODO: triggers *)
let ty = dty env ty in
let env = { env with dvars = M.add id ty env.dvars } in
Fquant (Fforall, id, ty, dfmla env a)
| PPexists (id, ty, a) -> (* TODO: triggers *)
let ty = dty env ty in
let env = { env with dvars = M.add id ty env.dvars } in
Fquant (Fexists, id, ty, dfmla env a)
| PPapp (x, tl) ->
let s, tyl =
try
let s = find_psymbol x env.env in
s, List.map (specialize env) s.ps_scheme
with Not_found ->
error ~loc:e.pp_loc (UnboundSymbol x)
in
let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
Fapp (s, tl)
| _ ->
assert false (*TODO*)
let rec term env t =
assert false (*TODO*)
and dtype_args s loc env el tl =
let n = List.length el and m = List.length tl in
if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
let rec check_arg = function
| [], [] ->
[]
| a :: al, t :: bl ->
let loc = t.pp_loc in
let t = dterm env t in
if not (unify a t.dt_ty) then
error ~loc (TermExpectedType ((fun f -> print_dty f t.dt_ty),
(fun f -> print_dty f a)));
t :: check_arg (al, bl)
| _ ->
assert false
in
check_arg (el, tl)
let rec term env t = match t.dt_node with
| Tvar x ->
assert (M.mem x env);
t_var (M.find x env)
| Tapp (s, tl) ->
t_app s (List.map (term env) tl) (ty t.dt_ty)
and fmla env = function
| Ftrue ->
......@@ -246,8 +364,13 @@ and fmla env = function
f_binary op (fmla env f1) (fmla env f2)
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| _ ->
assert false (*TODO*)
| Fquant (q, x, t, f1) ->
let v = create_vsymbol (Name.from_string x) (ty t) in
let env = M.add x v env in
f_quant q v (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
(** building environments *)
......@@ -268,7 +391,7 @@ let add_function loc pl t env id =
if M.mem id env.fsymbols then error ~loc (Clash id);
let denv = create_denv env in
let pl = List.map (dty denv) pl and t = dty denv t in
let pl = List.map (ty denv) pl and t = ty denv t in
let pl = List.map ty pl and t = ty t in
let s = create_fsymbol (Name.from_string id) (pl, t) false in
{ env with fsymbols = M.add id s env.fsymbols }
......@@ -276,19 +399,19 @@ let add_predicate loc pl env id =
if M.mem id env.psymbols then error ~loc (Clash id);
let denv = create_denv env in
let pl = List.map (dty denv) pl in
let pl = List.map (ty denv) pl in
let pl = List.map ty pl in
let s = create_psymbol (Name.from_string id) pl in
{ env with psymbols = M.add id s env.psymbols }
let fmla env f =
let denv = create_denv env in
let f = dfmla denv f in
fmla denv f
fmla M.empty f
let term env t =
let denv = create_denv env in
let t = dterm denv t in
term denv t
term M.empty t
let axiom loc s f env =
ignore (fmla env f);
......
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