logic typing: user type variables are now a distinct constructor (of dty)

parent 6519cc50
......@@ -31,17 +31,18 @@ open Theory
type dty_view =
| Tyvar of type_var
| Tyuvar of tvsymbol
| Tyapp of tysymbol * dty_view list
and type_var = {
tag : int;
user : bool;
tvsymbol : tvsymbol;
mutable type_val : dty_view option;
type_var_loc : loc option;
}
let tyvar v = Tyvar v
let tyuvar tv = Tyuvar tv
let rec type_inst s ty = match ty.ty_node with
| Ty.Tyvar n -> Mtv.find n s
......@@ -62,8 +63,9 @@ let tvsymbol_of_type_var tv = tv.tvsymbol
let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
| Tyvar { type_val = None; tvsymbol = v } ->
Pretty.print_tv fmt v
| 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]) ->
......@@ -77,14 +79,14 @@ let rec view_dty = function
let create_ty_decl_var =
let t = ref 0 in
fun ?loc ~user tv ->
fun ?loc tv ->
incr t;
{ tag = !t; user = user; tvsymbol = tv; type_val = None;
type_var_loc = loc }
{ tag = !t; tvsymbol = tv; type_val = None; type_var_loc = loc }
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 *)
......@@ -95,27 +97,26 @@ let rec unify t1 t2 = match t1, t2 with
unify t1 t2
| Tyvar v1, Tyvar v2 when v1.tag = v2.tag ->
true
(* instantiable variables *)
| Tyvar ({user=false} as v), t
| t, Tyvar ({user=false} as v) ->
(* instantiable variables *)
| Tyvar v, t | t, Tyvar v ->
not (occurs v t) && (v.type_val <- Some t; true)
(* recursive types *)
(* 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 *)
| Tyvar {user=true; tag=t1}, Tyvar {user=true; tag=t2} ->
t1 = t2
(* 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; user = false; type_var_loc = loc } ->
| Tyvar { type_val = None; type_var_loc = loc } ->
Loc.errorm ?loc "undefined type variable"
| Tyvar { tvsymbol = tv } ->
| Tyuvar tv ->
ty_var tv
| Tyapp (s, tl) ->
ty_app s (List.map ty_of_dty tl)
......@@ -280,7 +281,7 @@ let find_type_var ~loc env tv =
try
Htv.find env tv
with Not_found ->
let v = create_ty_decl_var ~loc ~user:false tv in
let v = create_ty_decl_var ~loc (create_tvsymbol (id_clone tv.tv_name)) in
Htv.add env tv v;
v
......
......@@ -28,15 +28,17 @@ open Theory
type type_var
val find_type_var : loc:Ptree.loc -> type_var Htv.t -> tvsymbol -> type_var
val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
val create_ty_decl_var : ?loc:Ptree.loc -> tvsymbol -> type_var
type dty
val tyvar : type_var -> dty
val tyuvar: tvsymbol -> dty
val tyapp : tysymbol -> dty list -> dty
type dty_view =
| Tyvar of type_var
| Tyuvar of tvsymbol
| Tyapp of tysymbol * dty list
val view_dty : dty -> dty_view
......
......@@ -105,32 +105,28 @@ let unify_raise ~loc ty1 ty2 =
environment + local variables.
It is only local to this module and created with [create_denv] below. *)
let create_user_tv =
let hs = Hashtbl.create 17 in
fun s -> try Hashtbl.find hs s with Not_found ->
let tv = create_tvsymbol (id_fresh s) in
Hashtbl.add hs s tv;
tv
(* TODO: shouldn't we localize this ident? *)
let create_user_type_var x =
tyuvar (create_user_tv x)
type denv = {
utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
dvars : dty Mstr.t; (* local variables, to be bound later *)
}
let create_denv () = {
utyvars = Hashtbl.create 17;
dvars = Mstr.empty;
}
let create_user_type_var x =
(* TODO: shouldn't we localize this ident? *)
let v = create_tvsymbol (id_fresh x) in
create_ty_decl_var ~user:true v
let find_user_type_var x env =
try
Hashtbl.find env.utyvars x
with Not_found ->
let v = create_user_type_var x in
Hashtbl.add env.utyvars x v;
v
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
let add_var x ty denv = { dvars = Mstr.add x ty denv.dvars }
let print_denv fmt denv =
Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars
......@@ -159,17 +155,17 @@ let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
let rec dty uc env = function
let rec dty uc = function
| PPTtyvar {id=x} ->
tyvar (find_user_type_var x env)
create_user_type_var x
| PPTtyapp (p, x) ->
let loc = qloc x in
let ts = specialize_tysymbol loc x uc in
let tyl = List.map (dty uc env) p in
let tyl = List.map (dty uc) p in
Loc.try2 loc tyapp ts tyl
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
tyapp ts (List.map (dty uc env) tyl)
tyapp ts (List.map (dty uc) tyl)
let find_ns get_id find p ns =
let loc = qloc p in
......@@ -336,7 +332,7 @@ let check_pat_linearity p =
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
tyvar (create_ty_decl_var ~loc ~user:false tv)
tyvar (create_ty_decl_var ~loc tv)
let rec dpat uc env pat =
let env, n, ty = dpat_node pat.pat_loc uc env pat.pat_desc in
......@@ -348,7 +344,7 @@ and dpat_node loc uc env = function
env, Pwild, ty
| PPpvar x ->
let ty = fresh_type_var loc in
let env = { env with dvars = Mstr.add x.id ty env.dvars } in
let env = { dvars = Mstr.add x.id ty env.dvars } in
env, Pvar x, ty
| PPpapp (x, pl) ->
let s, tyl, ty = specialize_fsymbol x uc in
......@@ -380,7 +376,7 @@ and dpat_node loc uc env = function
env, Papp (s, pl), ty
| PPpas (p, x) ->
let env, p = dpat uc env p in
let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
let env = { dvars = Mstr.add x.id p.dp_ty env.dvars } in
env, Pas (p,x), p.dp_ty
| PPpor (p, q) ->
let env, p = dpat uc env p in
......@@ -477,7 +473,7 @@ and dterm_node ~localize loc uc env = function
| PPlet (x, e1, e2) ->
let e1 = dterm ~localize uc env e1 in
let ty = e1.dt_ty in
let env = { env with dvars = Mstr.add x.id ty env.dvars } in
let env = { dvars = Mstr.add x.id ty env.dvars } in
let e2 = dterm ~localize uc env e2 in
Tlet (e1, x, e2), e2.dt_ty
| PPmatch (e1, bl) ->
......@@ -503,7 +499,7 @@ and dterm_node ~localize loc uc env = function
| PPcast (e1, ty) ->
let loc = e1.pp_loc in
let e1 = dterm ~localize uc env e1 in
let ty = dty uc env ty in
let ty = dty uc ty in
unify_raise ~loc e1.dt_ty ty;
e1.dt_node, ty
| PPif (e1, e2, e3) ->
......@@ -513,19 +509,19 @@ and dterm_node ~localize loc uc env = function
unify_raise ~loc e3.dt_ty e2.dt_ty;
Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
| PPeps (x, ty, e1) ->
let ty = dty uc env ty in
let env = { env with dvars = Mstr.add x.id ty env.dvars } in
let ty = dty uc ty in
let env = { dvars = Mstr.add x.id ty env.dvars } in
let e1 = dfmla ~localize uc env e1 in
Teps (x, ty, e1), ty
| PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
check_quant_linearity uqu;
let uquant env (idl,ty) =
let ty = dty uc env ty in
let ty = dty uc ty in
let id = match idl with
| Some id -> id
| None -> assert false
in
{ env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
{ dvars = Mstr.add id.id ty env.dvars }, (id,ty)
in
let env, uqu = map_fold_left uquant env uqu in
let trigger e =
......@@ -639,12 +635,12 @@ and dfmla_node ~localize loc uc env = function
| PPquant (q, uqu, trl, a) ->
check_quant_linearity uqu;
let uquant env (idl,ty) =
let ty = dty uc env ty in
let ty = dty uc ty in
let id = match idl with
| Some id -> id
| None -> assert false
in
{ env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
{ dvars = Mstr.add id.id ty env.dvars }, (id,ty)
in
let env, uqu = map_fold_left uquant env uqu in
let trigger e =
......@@ -683,7 +679,7 @@ and dfmla_node ~localize loc uc env = function
| PPlet (x, e1, e2) ->
let e1 = dterm ~localize uc env e1 in
let ty = e1.dt_ty in
let env = { env with dvars = Mstr.add x.id ty env.dvars } in
let env = { dvars = Mstr.add x.id ty env.dvars } in
let e2 = dfmla ~localize uc env e2 in
Flet (e1, x, e2)
| PPmatch (e1, bl) ->
......@@ -808,7 +804,7 @@ let add_types dl th =
let vl = List.map (fun id ->
if Hashtbl.mem vars id.id then
error ~loc:id.id_loc (DuplicateTypeVar id.id);
let i = create_tvsymbol (create_user_id id) in
let i = create_user_tv id.id in
Hashtbl.add vars id.id i;
i) d.td_params
in
......@@ -855,18 +851,11 @@ let add_types dl th =
in
let csymbols = Hashtbl.create 17 in
let decl d (abstr,algeb,alias) =
let ts, denv' = match Hashtbl.find tysymbols d.td_ident.id with
let ts = match Hashtbl.find tysymbols d.td_ident.id with
| None ->
assert false
| Some ts ->
let denv' = create_denv () in
let vars = denv'.utyvars in
List.iter
(fun v ->
Hashtbl.add vars v.tv_name.id_string
(create_ty_decl_var ~user:true v))
ts.ts_args;
ts, denv'
ts
in
match d.td_def with
| TDabstract -> ts::abstr, algeb, alias
......@@ -874,7 +863,7 @@ let add_types dl th =
| TDalgebraic cl ->
let ht = Hashtbl.create 17 in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let param (_,t) = ty_of_dty (dty th' denv' t) in
let param (_,t) = ty_of_dty (dty th' t) in
let projection (id,_) fty = match id with
| None -> None
| Some id ->
......@@ -949,7 +938,7 @@ let add_logics dl th =
let v = create_user_id d.ld_ident in
let denv = create_denv () in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty th denv t) in
let type_ty (_,t) = ty_of_dty (dty th t) in
let pl = List.map type_ty d.ld_params in
let add d = match d.ld_type with
| None -> (* predicate *)
......@@ -972,8 +961,8 @@ let add_logics dl th =
let dadd_var denv (x, ty) = match x with
| None -> denv
| Some id ->
let ty = dty th' denv ty in
{ denv with dvars = Mstr.add id.id ty denv.dvars }
let ty = dty th' ty in
{ dvars = Mstr.add id.id ty denv.dvars }
in
let denv = Hashtbl.find denvs id in
let denv = List.fold_left dadd_var denv d.ld_params in
......@@ -1005,7 +994,7 @@ let add_logics dl th =
| None -> fs :: abst, defn
| Some t ->
let loc = t.pp_loc in
let ty = dty th' denv ty in
let ty = dty th' ty in
let t = dterm th' denv t in
unify_raise ~loc t.dt_ty ty;
let vl = match fs.ls_value with
......@@ -1043,7 +1032,7 @@ let add_inductives s dl th =
let create_symbol th d =
let id = d.in_ident.id in
let v = create_user_id d.in_ident in
let type_ty (_,t) = ty_of_dty (dty th denv t) in
let type_ty (_,t) = ty_of_dty (dty th t) in
let pl = List.map type_ty d.in_params in
let ps = create_psymbol v pl in
Hashtbl.add psymbols id ps;
......
......@@ -56,13 +56,13 @@ val specialize_psymbol :
val specialize_tysymbol :
Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol
val create_user_tv: string -> tvsymbol
val create_user_type_var : string -> Denv.dty
type denv
val create_denv : unit -> denv
val create_user_type_var : string -> Denv.type_var
val find_user_type_var : string -> denv -> Denv.type_var
val mem_var : string -> denv -> bool
val find_var : string -> denv -> Denv.dty
val add_var : string -> Denv.dty -> denv -> denv
......@@ -70,7 +70,7 @@ val add_var : string -> Denv.dty -> denv -> denv
val type_term : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val type_fmla : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val dty : theory_uc -> denv -> Ptree.pty -> Denv.dty
val dty : theory_uc -> Ptree.pty -> Denv.dty
val dterm : ?localize:(Ptree.loc option option) ->
theory_uc -> denv -> Ptree.lexpr -> Denv.dterm
val dfmla : ?localize:(Ptree.loc option option) ->
......
......@@ -103,7 +103,8 @@ let rec create_regions ~user n =
[]
else
let tv = create_tvsymbol (id_fresh "rho") in
tyvar (create_ty_decl_var ~user tv) :: create_regions ~user (n - 1)
let r = if user then tyuvar tv else tyvar (create_ty_decl_var tv) in
r :: create_regions ~user (n - 1)
(* region variables are collected in the following list of lists
so that we can check after typing that two region variables in the same
......@@ -120,16 +121,19 @@ let push_region_var tv vloc = match !region_vars with
let check_region_vars () =
let values = Htv.create 17 in
let check tv (v, loc) = match view_dty (tyvar v) with
let check_tv tv tv' loc =
try
let tv'' = Htv.find values tv' in
if not (tv_equal tv tv'') then
errorm ~loc "this application would create an alias";
with Not_found ->
Htv.add values tv' tv
in
let check tv (v, loc) = match view_dty v with
| Tyvar v' ->
let tv' = tvsymbol_of_type_var v' in
begin try
let tv'' = Htv.find values tv' in
if not (tv_equal tv tv'') then
errorm ~loc "this application would create an alias";
with Not_found ->
Htv.add values tv' tv
end
check_tv tv (tvsymbol_of_type_var v') loc
| Tyuvar tv' ->
check_tv tv tv' loc
| Tyapp _ ->
assert false
in
......@@ -146,13 +150,13 @@ let rec specialize_ty ?(policy=Region_var) ~loc htv ty = match ty.ty_node with
let n = (get_mtsymbol ts).mt_regions in
let mk_region ty = match ty.ty_node with
| Ty.Tyvar _ when policy = Region_ret ->
tyvar (Typing.create_user_type_var "fresh")
tyuvar (create_tvsymbol (id_fresh "fresh"))
| Ty.Tyvar tv when policy = Region_var ->
let v = Denv.find_type_var ~loc htv tv in
push_region_var tv (v, loc);
push_region_var tv (tyvar v, loc);
tyvar v
| Ty.Tyvar tv (* policy = Region_glob *) ->
tyvar (create_ty_decl_var ~user:true tv)
tyuvar tv
| Ty.Tyapp _ ->
assert false
in
......@@ -172,8 +176,7 @@ let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
in
Sreg.iter
(fun r ->
let v = create_ty_decl_var ~user:true r.R.r_tv in
push_region_var r.R.r_tv (v, loc))
push_region_var r.R.r_tv (tyuvar r.R.r_tv, loc))
globals;
dcurrying
(List.map (fun pv -> specialize_type_v ~loc htv pv.pv_tv) bl)
......@@ -205,7 +208,7 @@ let specialize_exception loc x uc =
let create_type_var loc =
let tv = Ty.create_tvsymbol (id_user "a" loc) in
tyvar (create_ty_decl_var ~loc ~user:false tv)
tyvar (create_ty_decl_var ~loc tv)
let add_pure_var id ty denv = match view_dty ty with
| Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
......@@ -272,7 +275,7 @@ let rec dpurify_utype_v = function
(* user indicates whether region type variables can be instantiated *)
let rec dtype ~user env = function
| PPTtyvar {id=x} ->
tyvar (Typing.find_user_type_var x env.denv)
Typing.create_user_type_var x
| PPTtyapp (p, x) ->
let loc = Typing.qloc x in
let ts = Typing.specialize_tysymbol loc x (impure_uc env.uc) in
......@@ -811,18 +814,18 @@ let create_ivsymbol id ty =
in
{ i_impure = vs; i_effect = vse; i_pure = vsp }
let rec dty_of_ty denv ty = match ty.ty_node with
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar v ->
Denv.tyvar (Typing.find_user_type_var v.tv_name.id_string denv)
Typing.create_user_type_var v.tv_name.id_string
| Ty.Tyapp (ts, tyl) ->
Denv.tyapp ts (List.map (dty_of_ty denv) tyl)
Denv.tyapp ts (List.map dty_of_ty tyl)
let iadd_local env x ty =
let v = create_ivsymbol x ty in
let s = v.i_impure.vs_name.id_string in
let env = { env with
i_denv =
(let dty = dty_of_ty env.i_denv v.i_pure.vs_ty in
(let dty = dty_of_ty v.i_pure.vs_ty in
add_pure_var s dty env.i_denv);
i_impures = Mstr.add s v env.i_impures;
i_effects = Mstr.add s v.i_effect env.i_effects;
......@@ -1952,8 +1955,7 @@ let create_ienv denv = {
}
let type_type uc ty =
let denv = create_denv uc in
let dty = Typing.dty (impure_uc uc) denv.denv ty in
let dty = Typing.dty (impure_uc uc) ty in
Denv.ty_of_dty dty
let add_pure_decl uc ?loc ls =
......
......@@ -31,13 +31,6 @@ open Mlw_ty.T
open Mlw_expr
open Mlw_module
let create_user_tv =
let hs = Hashtbl.create 17 in
fun s -> try Hashtbl.find hs s with Not_found ->
let tv = create_tvsymbol (id_fresh s) in
Hashtbl.add hs s tv;
tv
type dity =
| Dvar of dvar ref
| Duvar of tvsymbol
......@@ -73,7 +66,7 @@ and reg_of_dreg = function
| Rvar { contents = Rval dreg } -> reg_of_dreg dreg
let create_user_type_variable x =
Duvar (create_user_tv x.id)
Duvar (Typing.create_user_tv x.id)
let create_type_variable () =
Dvar (ref (Dtvs (create_tvsymbol (id_fresh "a"))))
......
......@@ -430,9 +430,11 @@ and dexpr_desc ~userloc denv loc = function
expected_type e res;
ppat, e in
DEmatch (e1, List.map branch bl), res
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Eabsurd ->
DEabsurd, create_type_variable ()
| Ptree.Eassert (ass, lexpr) ->
DEassert (ass, lexpr), dity_unit
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Eraise (_q, _e1) ->
assert false (*TODO*)
......@@ -440,8 +442,6 @@ and dexpr_desc ~userloc denv loc = function
assert false (*TODO*)
| Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
assert false (*TODO*)
| Ptree.Eassert (_ass, _lexpr) ->
assert false (*TODO*)
| Ptree.Emark (_id, _e1) ->
assert false (*TODO*)
| Ptree.Eany (_type_c) ->
......@@ -480,7 +480,7 @@ and dlambda ~userloc denv bl _var (p, e, q) =
and dpost _denv (q, _ql) =
q, [] (* TODO *)
let rec expr locals de = match de.dexpr_desc with
let rec expr uc locals de = match de.dexpr_desc with
| DElocal x ->
assert (Mstr.mem x locals);
begin match Mstr.find x locals with
......@@ -488,32 +488,32 @@ let rec expr locals de = match de.dexpr_desc with
| LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
end
| DElet (x, { dexpr_desc = DEfun (bl, tr) }, de2) ->
let def1 = expr_fun locals x bl tr in
let def1 = expr_fun uc locals x bl tr in
let locals = Mstr.add x.id (LetA def1.rec_ps) locals in
let e2 = expr locals de2 in
let e2 = expr uc locals de2 in
e_rec [def1] e2
| DEfun (bl, tr) ->
let x = { id = "fn"; id_loc = de.dexpr_loc; id_lab = [] } in
let def = expr_fun locals x bl tr in
let def = expr_fun uc locals x bl tr in
let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
e_rec [def] e2
| DElet (x, de1, de2) ->
let e1 = expr locals de1 in
let e1 = expr uc locals de1 in
let def1 = create_let_defn (Denv.create_user_id x) e1 in
let locals = Mstr.add x.id def1.let_var locals in
let e2 = expr locals de2 in
let e2 = expr uc locals de2 in
e_let def1 e2
| DEletrec (rdl, de1) ->
let rdl = expr_rec locals rdl in
let rdl = expr_rec uc locals rdl in
let add_rd { rec_ps = ps } = Mstr.add ps.ps_name.id_string (LetA ps) in
let e1 = expr (List.fold_right add_rd rdl locals) de1 in
let e1 = expr uc (List.fold_right add_rd rdl locals) de1 in
e_rec rdl e1
| DEapply (de1, del) ->
let el = List.map (expr locals) del in
let el = List.map (expr uc locals) del in
begin match de1.dexpr_desc with
| DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.dexpr_type)
| DEglobal_ls ls -> e_lapp ls el (ity_of_dity de.dexpr_type)
| _ -> e_app (expr locals de1) el
| _ -> e_app (expr uc locals de1) el
end
| DEglobal_pv pv ->
e_value pv
......@@ -526,29 +526,32 @@ let rec expr locals de = match de.dexpr_desc with
assert (ls.ls_args = []);
e_lapp ls [] (ity_of_dity de.dexpr_type)
| DEif (de1, de2, de3) ->
e_if (expr locals de1) (expr locals de2) (expr locals de3)
e_if (expr uc locals de1) (expr uc locals de2) (expr uc locals de3)
| DEassign (de1, de2) ->
e_assign (expr locals de1) (expr locals de2)
e_assign (expr uc locals de1) (expr uc locals de2)
| DEconstant c ->
e_const c
| DElazy (LazyAnd, de1, de2) ->
e_lazy_and (expr locals de1) (expr locals de2)
e_lazy_and (expr uc locals de1) (expr uc locals de2)
| DElazy (LazyOr, de1, de2) ->
e_lazy_or (expr locals de1) (expr locals de2)
e_lazy_or (expr uc locals de1) (expr uc locals de2)
| DEnot de1 ->
e_not (expr locals de1)
e_not (expr uc locals de1)
| DEmatch (de1, bl) ->
let e1 = expr locals de1 in
let e1 = expr uc locals de1 in
let vtv = vtv_of_expr e1 in
let branch (pp,de) =
let vm, pp = make_ppattern pp vtv in
let locals = Mstr.fold (fun s pv -> Mstr.add s (LetV pv)) vm locals in
pp, expr locals de in
pp, expr uc locals de in
e_case e1 (List.map branch bl)
| DEassert (ass, lexpr) ->
(* let f = Typing.type_fmla (get_theory uc) *)
assert false (*TODO*)
| _ ->
assert false (*TODO*)
and expr_rec locals rdl =
and expr_rec uc locals rdl =
let step1 locals (id, dity, bl, var, tr) =
let vta = match vty_of_dity dity with
| VTarrow vta -> vta
......@@ -557,21 +560,21 @@ and expr_rec locals rdl =
Mstr.add id.id (LetA ps) locals, (ps, bl, var, tr)
in
let locals, rdl = Util.map_fold_left step1 locals rdl in
let step2 (ps, bl, var, tr) = ps, expr_lam locals bl var tr in
let step2 (ps, bl, var, tr) = ps, expr_lam uc locals bl var tr in
create_rec_defn (List.map step2 rdl)
and expr_fun locals x bl tr =
let lam = expr_lam locals bl [] tr in
and expr_fun uc locals x bl tr =
let lam = expr_lam uc locals bl [] tr in
create_fun_defn (Denv.create_user_id x) lam
and expr_lam locals bl _var (_, e, _) =
and expr_lam uc locals bl _var (_, e, _) =
let binder (id, ghost, dity) =
let vtv = vty_value ~ghost (ity_of_dity dity) in
create_pvsymbol (Denv.create_user_id id) vtv in
let pvl = List.map binder bl in
let add_binder pv = Mstr.add pv.pv_vs.vs_name.id_string (LetV pv) in
let locals = List.fold_right add_binder pvl locals in
let e = expr locals e in
let e = expr uc locals e in
let ty = match e.e_vty with
| VTarrow _ -> ty_tuple []
| VTvalue vtv -> ty_of_ity vtv.vtv_ity in
......@@ -1048,17 +1051,17 @@ let add_module lib path mm mt m =
let e = dexpr ~userloc:None (create_denv uc) e in
let pd = match e.dexpr_desc with
| DEfun (bl, tr) ->
let def = expr_fun Mstr.empty id bl tr in
let def = expr_fun uc Mstr.empty id bl tr in
create_rec_decl [def]
| _ ->
let e = expr Mstr.empty e in
let e = expr uc Mstr.empty e in
let def = create_let_defn (Denv.create_user_id id) e in
create_let_decl def
in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dletrec rdl ->
let rdl = dletrec ~userloc:None (create_denv uc) rdl in
let rdl = expr_rec Mstr.empty rdl in
let rdl = expr_rec uc Mstr.empty rdl in
let pd = create_rec_decl rdl in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dexn (id, pty) ->
......
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