Commit 460e93f8 authored by Andrei Paskevich's avatar Andrei Paskevich

switch Typing to the new Dterm-based API

Also:

- Make [Highord.pred 'a] an alias for [Highord.func 'a bool],
rename [Highorg.(@!)] to [(@)], remove [Highorg.(@?)], remove
the quantifiers [\!] and [\?] and only leave [\] which is the
only true lambda now;

- Allow mixing bool and Prop in logic, Dterm will introduce
coercions where necessary (trying to minimize the number of
if-then-else in the term context).
parent fc68f4f7
......@@ -113,7 +113,7 @@ LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \
LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer
LIB_PARSER = ptree denv glob parser typing lexer
LIB_PARSER = ptree glob parser typing lexer
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection
......
......@@ -8,8 +8,7 @@ end
theory HighOrd
syntax type func "((%1) -> (%2))"
syntax type pred "((%1) -> bool)"
syntax function (@!) "((%1) (%2))"
syntax predicate (@?) "((%1) (%2))"
syntax function (@) "((%1) (%2))"
end
theory option.Option
......
......@@ -30,12 +30,17 @@ let dty_fresh = let i = ref 0 in fun () -> Dvar (ref (Dind (incr i; !i)))
let dty_of_ty ty = Duty ty
let rec ty_of_dty ~strict = function
| Dvar { contents = Dval dty } -> ty_of_dty ~strict dty
| Dvar { contents = Dval (Duty ty) } ->
ty
| Dvar ({ contents = Dval dty } as r) ->
let ty = ty_of_dty ~strict dty in
r := Dval (Duty ty); ty
| Dvar r ->
if strict then Loc.errorm "undefined type variable";
let ty = ty_var (create_tvsymbol (id_fresh "xi")) in
r := Dval (Duty ty); ty
| Dapp (ts,dl) -> ty_app ts (List.map (ty_of_dty ~strict) dl)
if strict then Loc.errorm "undefined type variable";
let ty = ty_var (create_tvsymbol (id_fresh "xi")) in
r := Dval (Duty ty); ty
| Dapp (ts,dl) ->
ty_app ts (List.map (ty_of_dty ~strict) dl)
| Duty ty -> ty
let rec occur_check i = function
......@@ -65,12 +70,9 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with
List.iter2 dty_unify dl1 dl2
| _ -> raise Exit
(*
exception DTypeMismatch of dty * dty
let dty_unify dty1 dty2 =
try dty_unify dty1 dty2 with Exit -> raise (DTypeMismatch (dty1,dty2))
*)
let dty_int = Duty ty_int
let dty_real = Duty ty_real
let dty_bool = Duty ty_bool
let rec print_dty ht inn fmt = function
| Dvar { contents = Dval dty } ->
......@@ -147,13 +149,12 @@ and dpattern_node =
type dterm = {
dt_node : dterm_node;
dt_dty : dty option;
dt_label : Slab.t;
dt_loc : Loc.position option;
dt_uloc : Loc.position option;
}
and dterm_node =
| DTvar of string
| DTvar of string * dty
| DTgvar of vsymbol
| DTconst of Number.constant
| DTapp of lsymbol * dterm list
| DTif of dterm * dterm * dterm
......@@ -165,54 +166,62 @@ and dterm_node =
| DTnot of dterm
| DTtrue
| DTfalse
| DTcast of dterm * ty
| DTuloc of dterm * Loc.position
| DTlabel of dterm * Slab.t
(** Environment *)
type denv = dty Mstr.t
type denv = dterm_node Mstr.t
exception TermExpected
exception FmlaExpected
exception DuplicateVar of string
exception UnboundVar of string
let denv_get_var ?loc denv n =
let dty = Mstr.find_exn (UnboundVar n) n denv in
{ dt_node = DTvar n;
dt_dty = Some dty;
dt_label = Slab.empty;
dt_loc = loc;
dt_uloc = None }
let denv_get denv n = Mstr.find_exn (UnboundVar n) n denv
let denv_get_opt denv n = Mstr.find_opt n denv
let dty_of_dterm dt = match dt.dt_dty with
| None -> Loc.error ?loc:dt.dt_loc TermExpected
| Some dty -> dty
let denv_empty = Mstr.empty
let denv_add_var denv id dty =
Mstr.add (preid_name id) dty denv
let n = preid_name id in
Mstr.add n (DTvar (n, dty)) denv
let denv_add_let denv dt id =
Mstr.add (preid_name id) (dty_of_dterm dt) denv
let n = preid_name id in
Mstr.add n (DTvar (n, dty_of_dterm dt)) denv
let denv_add_quant denv vl =
let add acc (id,dty) = let n = preid_name id in
Mstr.add_new (DuplicateVar n) n dty acc in
Mstr.add_new (DuplicateVar n) n (DTvar (n, dty)) acc in
let s = List.fold_left add Mstr.empty vl in
Mstr.set_union s denv
let denv_add_pat denv dp =
let rec get dp = match dp.dp_node with
| DPwild -> Mstr.empty
| DPvar id -> Mstr.singleton (preid_name id) dp.dp_dty
| DPvar id ->
let n = preid_name id in
Mstr.singleton n (DTvar (n, dp.dp_dty))
| DPapp (_,dpl) ->
let join n _ _ = raise (DuplicateVar n) in
let add acc dp = Mstr.union join acc (get dp) in
List.fold_left add Mstr.empty dpl
| DPor (dp1,dp2) ->
let join _ dty1 dty2 = dty_unify dty1 dty2; Some dty1 in
let join _ dtn1 dtn2 = match dtn1, dtn2 with
| DTvar (_,dty1), DTvar (_,dty2) -> dty_unify dty1 dty2; Some dtn1
| _ -> assert false in
Mstr.union join (get dp1) (get dp2)
| DPas (dp,id) ->
let n = preid_name id in
Mstr.add_new (DuplicateVar n) n dp.dp_dty (get dp) in
Mstr.add_new (DuplicateVar n) n (DTvar (n, dp.dp_dty)) (get dp)
in
Mstr.set_union (get dp) denv
(** Unification tools *)
......@@ -233,13 +242,17 @@ let darg_expected_type ?loc dt_dty dty =
let dterm_expected_type dt dty = match dt.dt_dty with
| Some dt_dty -> darg_expected_type ?loc:dt.dt_loc dt_dty dty
| None -> Loc.error ?loc:dt.dt_loc TermExpected
| None -> begin try dty_unify dty_bool dty with Exit ->
Loc.error ?loc:dt.dt_loc TermExpected end
let dfmla_expected_type dt dty = match dt.dt_dty, dty with
| Some dt_dty, Some dty -> darg_expected_type ?loc:dt.dt_loc dt_dty dty
| Some _, None -> Loc.error ?loc:dt.dt_loc FmlaExpected
| None, Some _ -> Loc.error ?loc:dt.dt_loc TermExpected
| None, None -> ()
let dfmla_expected_type dt = match dt.dt_dty with
| Some dt_dty -> begin try dty_unify dt_dty dty_bool with Exit ->
Loc.error ?loc:dt.dt_loc FmlaExpected end
| None -> ()
let dexpr_expected_type dt dty = match dty with
| Some dty -> dterm_expected_type dt dty
| None -> dfmla_expected_type dt
(** Constructors *)
......@@ -261,17 +274,22 @@ let dpattern ?loc node =
let dterm ?loc node =
let get_dty = function
| DTvar _ -> Loc.errorm "Invalid argument, use Dterm.denv_get_var"
| DTconst (Number.ConstInt _) -> Some (dty_of_ty ty_int)
| DTconst (Number.ConstReal _) -> Some (dty_of_ty ty_real)
| DTvar (_,dty) ->
Some dty
| DTgvar vs ->
Some (dty_of_ty vs.vs_ty)
| DTconst (Number.ConstInt _) ->
Some dty_int
| DTconst (Number.ConstReal _) ->
Some dty_real
| DTapp (ls,dtl) ->
let dtyl, dty = specialize_ls ls in
dty_unify_app ls dterm_expected_type dtl dtyl;
dty
| DTif (df,dt1,dt2) ->
dfmla_expected_type df None;
dfmla_expected_type dt2 dt1.dt_dty;
dt1.dt_dty
dfmla_expected_type df;
dexpr_expected_type dt2 dt1.dt_dty;
if dt2.dt_dty = None then None else dt1.dt_dty
| DTlet (dt,_,df) ->
ignore (dty_of_dterm dt);
df.dt_dty
......@@ -281,41 +299,38 @@ let dterm ?loc node =
dterm_expected_type dt dp1.dp_dty;
let check (dp,df) =
dpat_expected_type dp dp1.dp_dty;
dfmla_expected_type df df1.dt_dty in
dexpr_expected_type df df1.dt_dty in
List.iter check bl;
df1.dt_dty
let is_fmla (_,df) = df.dt_dty = None in
if List.exists is_fmla bl then None else df1.dt_dty
| DTeps (_,dty,df) ->
dfmla_expected_type df None;
dfmla_expected_type df;
Some dty
| DTquant (_,_,_,df) ->
dfmla_expected_type df None;
dfmla_expected_type df;
None
| DTbinop (_,df1,df2) ->
dfmla_expected_type df1 None;
dfmla_expected_type df2 None;
dfmla_expected_type df1;
dfmla_expected_type df2;
None
| DTnot df ->
dfmla_expected_type df None;
dfmla_expected_type df;
None
| DTtrue | DTfalse ->
None
in
(* we put here [Some dty_bool] instead of [None] because we can
always replace [true] by [True] and [false] by [False], so that
there is no need to count these constructs as "formulas" which
require explicit if-then-else conversion to bool *)
Some dty_bool
| DTcast (dt,ty) ->
let dty = dty_of_ty ty in
dterm_expected_type dt dty;
Some dty
| DTuloc (dt,_)
| DTlabel (dt,_) ->
dt.dt_dty in
let dty = Loc.try1 ?loc get_dty node in
{ dt_node = node; dt_dty = dty;
dt_label = Slab.empty;
dt_loc = loc; dt_uloc = None }
let dterm_type_cast dt ty =
dterm_expected_type dt (dty_of_ty ty); dt
let dterm_add_label dt lab =
{ dt with dt_label = Slab.add lab dt.dt_label }
let dterm_set_labels dt slab =
{ dt with dt_label = slab }
let dterm_set_uloc dt loc =
{ dt with dt_uloc = Some loc }
{ dt_node = node; dt_dty = dty; dt_loc = loc }
(** Final stage *)
......@@ -363,55 +378,108 @@ let check_exists_implies q f = match q, f.t_node with
"form \"exists x. P -> Q\" is likely an error (use \"not P \\/ Q\" if not)"
| _ -> ()
let term ~strict ~keep_loc env dt =
let rec get uloc env dt =
let uloc = if dt.dt_uloc = None then uloc else dt.dt_uloc in
let t = Loc.try4 ?loc:dt.dt_loc try_get uloc env dt.dt_dty dt.dt_node in
let loc = if keep_loc then dt.dt_loc else None in
let loc = if uloc = None then loc else uloc in
if loc = None && Slab.is_empty dt.dt_label
then t else t_label ?loc dt.dt_label t
and try_get uloc env dty = function
| DTvar n ->
let term ~strict ~keep_loc env prop dt =
let t_label loc labs t =
if loc = None && Slab.is_empty labs
then t else t_label ?loc labs t in
let rec strip uloc labs dt = match dt.dt_node with
| DTcast (dt,_) -> strip uloc labs dt
| DTuloc (dt,loc) -> strip (Some loc) labs dt
| DTlabel (dt,s) -> strip uloc (Slab.union labs s) dt
| _ -> uloc, labs, dt in
let rec get uloc env prop dt =
let uloc, labs, dt = strip uloc Slab.empty dt in
let tloc = if keep_loc then dt.dt_loc else None in
let tloc = if uloc <> None then uloc else tloc in
let t = t_label tloc labs (Loc.try5 ?loc:dt.dt_loc
try_get uloc env prop dt.dt_dty dt.dt_node) in
match t.t_ty with
| Some _ when prop -> t_label tloc Slab.empty
(Loc.try2 ?loc:dt.dt_loc t_equ t t_bool_true)
| None when not prop -> t_label tloc Slab.empty
(t_if t t_bool_true t_bool_false)
| _ -> t
and try_get uloc env prop dty = function
| DTvar (n,_) ->
t_var (Mstr.find_exn (UnboundVar n) n env)
| DTgvar vs ->
t_var vs
| DTconst c ->
t_const c
| DTapp (ls,[]) when ls_equal ls fs_bool_true ->
if prop then t_true else t_bool_true
| DTapp (ls,[]) when ls_equal ls fs_bool_false ->
if prop then t_false else t_bool_false
| DTapp (ls,[dt1;dt2]) when ls_equal ls ps_equ ->
(* avoid putting formulas into a term context *)
if dt1.dt_dty = None || dt2.dt_dty = None
then t_iff (get uloc env true dt1) (get uloc env true dt2)
else t_equ (get uloc env false dt1) (get uloc env false dt2)
| DTapp (ls,dtl) ->
t_app ls (List.map (get uloc env) dtl) (Opt.map (ty_of_dty ~strict) dty)
| DTif (df,dt1,dt2) ->
t_if (get uloc env df) (get uloc env dt1) (get uloc env dt2)
t_app ls (List.map (get uloc env false) dtl)
(Opt.map (ty_of_dty ~strict) dty)
| DTlet (dt,id,df) ->
let t = get uloc env dt in
let prop = prop || dty = None in
let t = get uloc env false dt in
let v = create_vsymbol id (t_type t) in
let env = Mstr.add (preid_name id) v env in
let f = get uloc env df in
let f = get uloc env prop df in
check_used_var f.t_vars v;
t_let_close v t f
| DTif (df,dt1,dt2) ->
let prop = prop || dty = None in
t_if (get uloc env true df)
(get uloc env prop dt1) (get uloc env prop dt2)
| DTcase (dt,bl) ->
let prop = prop || dty = None in
let branch (dp,df) =
let env, p = pattern ~strict env dp in
let f = get uloc env df in
let f = get uloc env prop df in
Svs.iter (check_used_var f.t_vars) p.pat_vars;
t_close_branch p f in
t_case (get uloc env dt) (List.map branch bl)
t_case (get uloc env false dt) (List.map branch bl)
| DTeps (id,dty,df) ->
let v = create_vsymbol id (ty_of_dty ~strict dty) in
let env = Mstr.add (preid_name id) v env in
let f = get uloc env df in
let f = get uloc env true df in
check_used_var f.t_vars v;
t_eps_close v f
| DTquant (q,vl,dll,df) ->
let env, vl = quant_vars ~strict env vl in
let trl = List.map (List.map (get uloc env)) dll in
let f = get uloc env df in
let tr_get dt = get uloc env (dt.dt_dty = None) dt in
let trl = List.map (List.map tr_get) dll in
let f = get uloc env true df in
List.iter (check_used_var f.t_vars) vl;
check_exists_implies q f;
t_quant_close q vl trl f
| DTbinop (op,df1,df2) ->
t_binary op (get uloc env df1) (get uloc env df2)
t_binary op (get uloc env true df1) (get uloc env true df2)
| DTnot df ->
t_not (get uloc env df)
| DTtrue -> t_true
| DTfalse -> t_false
t_not (get uloc env true df)
| DTtrue ->
if prop then t_true else t_bool_true
| DTfalse ->
if prop then t_false else t_bool_false
| DTcast _ | DTuloc _ | DTlabel _ ->
assert false (* already stripped *)
in
get None env dt
get None env prop dt
let fmla ~strict ~keep_loc env dt = term ~strict ~keep_loc env true dt
let term ~strict ~keep_loc env dt = term ~strict ~keep_loc env false dt
(** Exception printer *)
let () = Exn_printer.register (fun fmt e -> match e with
| TermExpected ->
Format.fprintf fmt "syntax error: term expected"
| FmlaExpected ->
Format.fprintf fmt "syntax error: formula expected"
| DuplicateVar s ->
Format.fprintf fmt "duplicate variable %s" s
| UnboundVar s ->
Format.fprintf fmt "unbound variable %s" s
| _ -> raise e)
......@@ -40,13 +40,12 @@ and dpattern_node =
type dterm = private {
dt_node : dterm_node;
dt_dty : dty option;
dt_label : Slab.t;
dt_loc : Loc.position option;
dt_uloc : Loc.position option;
}
and dterm_node =
| DTvar of string
| DTvar of string * dty
| DTgvar of vsymbol
| DTconst of Number.constant
| DTapp of lsymbol * dterm list
| DTif of dterm * dterm * dterm
......@@ -58,6 +57,9 @@ and dterm_node =
| DTnot of dterm
| DTtrue
| DTfalse
| DTcast of dterm * ty
| DTuloc of dterm * Loc.position
| DTlabel of dterm * Slab.t
(** Environment *)
......@@ -66,7 +68,9 @@ exception FmlaExpected
exception DuplicateVar of string
exception UnboundVar of string
type denv (** bound variables *)
type denv = dterm_node Mstr.t (** bound variables *)
val denv_empty : denv (** Mstr.empty *)
val denv_add_var : denv -> preid -> dty -> denv
......@@ -76,7 +80,9 @@ val denv_add_quant : denv -> (preid * dty) list -> denv
val denv_add_pat : denv -> dpattern -> denv
val denv_get_var : ?loc:Loc.position -> denv -> string -> dterm
val denv_get : denv -> string -> dterm_node (** raises UnboundVar *)
val denv_get_opt : denv -> string -> dterm_node option
(** Constructors *)
......@@ -84,15 +90,7 @@ val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
val dterm : ?loc:Loc.position -> dterm_node -> dterm
val dterm_type_cast : dterm -> ty -> dterm
val dterm_add_label : dterm -> label -> dterm
val dterm_set_labels : dterm -> Slab.t -> dterm
val dterm_set_uloc : dterm -> Loc.position -> dterm
(** Final stage *)
val term : strict:bool -> keep_loc:bool -> vsymbol Mstr.t -> dterm -> term
val fmla : strict:bool -> keep_loc:bool -> vsymbol Mstr.t -> dterm -> term
......@@ -829,20 +829,13 @@ let t_tuple tl =
let fs_func_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in
create_fsymbol (id_fresh "infix @!") [ty_func ty_a ty_b; ty_a] ty_b
let ps_pred_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix @?") [ty_pred ty_a; ty_a]
create_fsymbol (id_fresh "infix @") [ty_func ty_a ty_b; ty_a] ty_b
let t_func_app fn t = t_app_infer fs_func_app [fn; t]
let t_pred_app pr t = ps_app ps_pred_app [pr; t]
let t_func_app_l = List.fold_left t_func_app
let t_pred_app pr t = t_equ (t_func_app pr t) t_bool_true
let t_pred_app_l pr tl = match List.rev tl with
| t::tl -> t_pred_app (t_func_app_l pr (List.rev tl)) t
| _ -> Pervasives.invalid_arg "t_pred_app_l"
let t_func_app_l fn tl = List.fold_left t_func_app fn tl
let t_pred_app_l pr tl = t_equ (t_func_app_l pr tl) t_bool_true
(** Term library *)
......
......@@ -297,14 +297,13 @@ val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
val is_fs_tuple_id : ident -> int option
val fs_func_app : lsymbol (* value-typed higher-order application *)
val ps_pred_app : lsymbol (* prop-typed higher-order application *)
val fs_func_app : lsymbol (* higher-order application symbol *)
val t_func_app : term -> term -> term
val t_pred_app : term -> term -> term
val t_func_app : term -> term -> term (* value-typed application *)
val t_pred_app : term -> term -> term (* prop-typed application *)
val t_func_app_l : term -> term list -> term
val t_pred_app_l : term -> term list -> term
val t_func_app_l : term -> term list -> term (* value-typed application *)
val t_pred_app_l : term -> term list -> term (* prop-typed application *)
(** {2 Term library} *)
......
......@@ -836,10 +836,10 @@ let bool_theory =
let highord_theory =
let uc = empty_theory (id_fresh "HighOrd") ["why3"] in
let uc = use_export uc bool_theory in
let uc = add_ty_decl uc ts_func in
let uc = add_ty_decl uc ts_pred in
let uc = add_param_decl uc fs_func_app in
let uc = add_param_decl uc ps_pred_app in
close_theory uc
let tuple_theory = Hint.memo 17 (fun n ->
......
......@@ -220,11 +220,13 @@ let ts_func =
let tv_b = create_tvsymbol (id_fresh "b") in
create_tysymbol (id_fresh "func") [tv_a;tv_b] None
let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
let ts_pred =
let tv_a = create_tvsymbol (id_fresh "a") in
create_tysymbol (id_fresh "pred") [tv_a] None
let def = Some (ty_func (ty_var tv_a) ty_bool) in
create_tysymbol (id_fresh "pred") [tv_a] def
let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
let ty_pred ty_a = ty_app ts_pred [ty_a]
let ts_tuple_ids = Hid.create 17
......
......@@ -115,7 +115,7 @@ val ts_func : tysymbol
val ts_pred : tysymbol
val ty_func : ty -> ty -> ty
val ty_pred : ty -> ty
val ty_pred : ty -> ty (* ty_pred 'a == ty_func 'a bool *)
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Format
open Pp
open Stdlib
open Ident
open Ptree
open Ty
open Term
(** types with destructive type variables *)
type dty_view =
| Tyvar of type_var
| Tyuvar of tvsymbol
| Tyapp of tysymbol * dty_view list
and type_var = {
tag : int;
tvsymbol : tvsymbol;
mutable type_val : dty_view option;
type_var_loc : loc option;
}
let tyuvar tv = Tyuvar tv
let rec type_inst s ty = match ty.ty_node with
| Ty.Tyvar n -> Mtv.find n s
| Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)
let tyapp ts tyl = match ts.ts_def with
| None ->
Tyapp (ts, tyl)
| Some ty ->
let add m v t = Mtv.add v t m in
try
let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
type_inst s ty
with Invalid_argument _ ->
Loc.errorm "this type expects %d parameters" (List.length ts.ts_args)
type dty = dty_view
let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
| Tyvar { type_val = None; tvsymbol = tv }
| Tyuvar tv ->
Pretty.print_tv fmt tv
| Tyapp (s, []) ->
fprintf fmt "%s" s.ts_name.id_string
| Tyapp (s, [t]) ->
fprintf fmt "%s %a" s.ts_name.id_string print_dty t
| Tyapp (s, l) ->
fprintf fmt "%s %a" s.ts_name.id_string (print_list space print_dty) l
let create_ty_decl_var =
let t = ref 0 in
fun ?loc tv ->
incr t;
{ tag = !t; tvsymbol = tv; type_val = None; type_var_loc = loc }
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc tv)
let rec occurs v = function
| Tyvar { type_val = Some t } -> occurs v t
| Tyvar { tag = t; type_val = None } -> v.tag = t
| Tyuvar _ -> false
| Tyapp (_, l) -> List.exists (occurs v) l
(* destructive type unification *)
let rec unify t1 t2 = match t1, t2 with
| Tyvar { type_val = Some t1 }, _ ->
unify t1 t2
| _, Tyvar { type_val = Some t2 } ->
unify t1 t2
| Tyvar v1, Tyvar v2 when v1.tag = v2.tag ->
true
(* instantiable variables *)
| Tyvar v, t | t, Tyvar v ->
not (occurs v t) && (v.type_val <- Some t; true)
(* recursive types *)
| Tyapp (s1, l1), Tyapp (s2, l2) ->
ts_equal s1 s2 && List.length l1 = List.length l2 &&
List.for_all2 unify l1 l2
| Tyapp _, _ | _, Tyapp _ ->
false
(* other cases *)
| Tyuvar tv1, Tyuvar tv2 ->
tv_equal tv1 tv2
(* intermediate types -> types *)
let rec ty_of_dty = function
| Tyvar { type_val = Some t } ->
ty_of_dty t
| Tyvar { type_val = None; type_var_loc = loc } ->
Loc.errorm ?loc "undefined type variable"
| Tyuvar tv ->
ty_var tv
| Tyapp (s, tl) ->
ty_app s (List.map ty_of_dty tl)
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar tv -> Tyuvar tv
| Ty.Tyapp (ts,tl) -> Tyapp (ts, List.map dty_of_ty tl)
type ident = Ptree.ident
type dpattern = { dp_node : dpattern_node; dp_ty : dty }
and dpattern_node =
| Pwild
| Pvar of ident
| Papp of lsymbol * dpattern list
| Por of dpattern * dpattern
| Pas of dpattern * ident
let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
let get_labels (ll,p) = function
| Lstr l -> Slab.add l ll, p
| Lpos p -> ll, Some p
in
let label,p = List.fold_left get_labels (Slab.empty,None) ll in
id_user ~label x (Opt.get_def loc p)
let create_user_vs id ty = create_vsymbol (create_user_id id) ty
let rec pattern_env env p = match p.dp_node with
| Pwild -> env
| Papp (_, pl) -> List.fold_left pattern_env env pl
| Por (p, _) -> pattern_env env p
| Pvar id ->
let vs = create_user_vs id (ty_of_dty p.dp_ty) in
Mstr.add id.id vs env
| Pas (p, id) ->
let vs = create_user_vs id (ty_of_dty p.dp_ty) in
pattern_env (Mstr.add id.id vs env) p
let get_pat_var env p x = try Mstr.find x env with Not_found ->
raise (Term.UncoveredVar (create_vsymbol (id_fresh x) (ty_of_dty p.dp_ty)))
let rec pattern_pat env p = match p.dp_node with
| Pwild -> pat_wild (ty_of_dty p.dp_ty)
| Pvar x -> pat_var (get_pat_var env p x.id)
| Pas (p, x) -> pat_as (pattern_pat env p) (get_pat_var env p x.id)
| Por (p, q) -> pat_or (pattern_pat env p) (pattern_pat env q)
| Papp (s, pl) ->
pat_app s (List.map (pattern_pat env) pl) (ty_of_dty p.dp_ty)
let pattern env p = let env = pattern_env env p in env, pattern_pat env p
type dterm = { dt_node : dterm_node; dt_ty : dty }