specialize_term,fmla no more needed

parent 342f7914
......@@ -294,100 +294,3 @@ let specialize_lsymbol ~loc s =
let env = Htv.create 17 in
List.map (specialize_ty ~loc env) tl, option_map (specialize_ty ~loc env) t
let ident_of_vs ~loc vs =
{ id = vs.vs_name.id_string;
id_lab = List.map (fun l -> Lstr l) vs.vs_name.id_label;
(* FIXME: should we add this loc to id_lab? *)
id_loc = Util.default_option loc vs.vs_name.Ident.id_loc }
let rec specialize_pattern ~loc htv p =
{ dp_node = specialize_pattern_node ~loc htv p.pat_node;
dp_ty = specialize_ty ~loc htv p.pat_ty; }
and specialize_pattern_node ~loc htv = function
| Term.Pwild ->
Pwild
| Term.Pvar v ->
Pvar (ident_of_vs ~loc v)
| Term.Papp (s, pl) ->
Papp (s, List.map (specialize_pattern ~loc htv) pl)
| Term.Pas (p, v) ->
Pas (specialize_pattern ~loc htv p, ident_of_vs ~loc v)
| Term.Por (p, q) ->
Por (specialize_pattern ~loc htv p, specialize_pattern ~loc htv q)
let rec specialize_term ~loc htv t =
let dt =
{ dt_node = specialize_term_node ~loc htv t.t_node;
dt_ty = specialize_ty ~loc htv (t_type t); }
in
let add_label l t = { t with dt_node = Tnamed (l, t) } in
let dt = option_apply dt (fun p -> add_label (Lpos p) dt) t.t_loc in
List.fold_left (fun t l -> add_label (Lstr l) t) dt t.t_label
and specialize_term_node ~loc htv = function
| Term.Tvar v ->
Tvar v.vs_name.id_string (* TODO: correct? is capture possible? *)
| Term.Tconst c ->
Tconst c
| Term.Tapp (ls, tl) ->
Tapp (ls, List.map (specialize_term ~loc htv) tl)
| Term.Tif (f, t1, t2) ->
Tif (specialize_fmla ~loc htv f,
specialize_term ~loc htv t1, specialize_term ~loc htv t2)
| Term.Tlet (t1, t2) ->
let v, t2 = t_open_bound t2 in
Tlet (specialize_term ~loc htv t1,
ident_of_vs ~loc v, specialize_term ~loc htv t2)
| Term.Tcase (t1, bl) ->
let branch b = let p, t = t_open_branch b in
specialize_pattern ~loc htv p, specialize_term ~loc htv t
in
Tmatch (specialize_term ~loc htv t1, List.map branch bl)
| Term.Teps fb ->
let v, f = t_open_bound fb in
Teps (ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty,
specialize_fmla ~loc htv f)
| Tquant _ | Tbinop _ | Tnot _
| Ttrue | Tfalse -> assert false
and specialize_fmla ~loc htv f =
let df = specialize_fmla_node ~loc htv f.t_node in
let df = option_apply df (fun p -> Fnamed (Lpos p,df)) f.t_loc in
List.fold_left (fun f l -> Fnamed (Lstr l, f)) df f.t_label
and specialize_fmla_node ~loc htv = function
| Term.Tapp (ls, tl) ->
Fapp (ls, List.map (specialize_term ~loc htv) tl)
| Tquant (q, fq) ->
let vl, tl, f = t_open_quant fq in
let uquant v = ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty in
let tl = List.map (List.map (specialize_trigger ~loc htv)) tl in
Fquant (q, List.map uquant vl, tl, specialize_fmla ~loc htv f)
| Tbinop (b, f1, f2) ->
Fbinop (b, specialize_fmla ~loc htv f1, specialize_fmla ~loc htv f2)
| Tnot f1 ->
Fnot (specialize_fmla ~loc htv f1)
| Ttrue ->
Ftrue
| Tfalse ->
Ffalse
| Term.Tif (f1, f2, f3) ->
Fif (specialize_fmla ~loc htv f1,
specialize_fmla ~loc htv f2, specialize_fmla ~loc htv f3)
| Term.Tlet (t1, f2b) ->
let v, f2 = t_open_bound f2b in
Flet (specialize_term ~loc htv t1,
ident_of_vs ~loc v, specialize_fmla ~loc htv f2)
| Term.Tcase (t, fbl) ->
let branch b = let p, f = t_open_branch b in
specialize_pattern ~loc htv p, specialize_fmla ~loc htv f
in
Fmatch (specialize_term ~loc htv t, List.map branch fbl)
| Term.Tvar _ | Term.Tconst _ | Term.Teps _ -> assert false
and specialize_trigger ~loc htv e = if e.t_ty = None
then TRfmla (specialize_fmla ~loc htv e)
else TRterm (specialize_term ~loc htv e)
......@@ -100,10 +100,6 @@ val specialize_ty : loc:Ptree.loc -> type_var Htv.t -> ty -> dty
val specialize_lsymbol : loc:Ptree.loc -> lsymbol -> dty list * dty option
val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
val specialize_fmla : loc:Ptree.loc -> type_var Htv.t -> term -> dfmla
(** exported for programs *)
val tvsymbol_of_type_var : type_var -> tvsymbol
......@@ -86,18 +86,6 @@ let create_denv uc =
locals = Mstr.empty;
denv = Typing.create_denv (); }
let specialize_post ~loc htv ((v, f), ql) =
assert (v.vs_name.id_string = "result"); (* TODO *)
let specialize_exn (l, (v, f)) =
assert
(match v with Some v -> v.vs_name.id_string = "result" | None -> true);
let ty = option_map (fun v -> Denv.specialize_ty ~loc htv v.vs_ty) v in
(l, (ty, specialize_fmla ~loc htv f))
in
let ty = Denv.specialize_ty ~loc htv v.vs_ty in
let f = specialize_fmla ~loc htv f in
(ty, f), List.map specialize_exn ql
let loc_of_id id = Util.of_option id.Ident.id_loc
let loc_of_ls ls = ls.ls_name.Ident.id_loc
......
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