Commit 98fa7858 authored by François Bobot's avatar François Bobot
Browse files

clean libencoding

parent 2d164a4d
......@@ -37,11 +37,6 @@ let ls_of_ts = Wts.memoize 63 (fun ts ->
let args = List.map (const ty_type) ts.ts_args in
create_fsymbol (id_clone ts.ts_name) args ty_type)
(* test whether a function symbol has ty_type as ls_value *)
let is_ls_of_ts ls = match ls.ls_value with
| Some { ty_node = Tyapp (ts,_) } when ts_equal ts ts_type -> true
| _ -> false
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
| Tyvar tv ->
......@@ -109,8 +104,6 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
let ls = ls_of_const ty_base t in
consts := Sls.add ls !consts;
t_app ls [] ty_base
(* | Tapp (fs,_) when is_ls_of_ts fs -> *)
(* t *)
| Tapp (fs,tl) ->
let fs = lsmap fs in
let ty = of_option fs.ls_value in
......@@ -179,7 +172,7 @@ let d_monomorph ty_base kept lsmap d =
| Dlogic ldl ->
let conv (ls,ld) =
let ls =
if ls_equal ls ps_equ (* || is_ls_of_ts ls *) then ls else lsmap ls
if ls_equal ls ps_equ then ls else lsmap ls
in
match ld with
| Some ld ->
......
......@@ -33,9 +33,6 @@ val d_ts_type : decl
(* function symbol mapping ty_type^n to ty_type *)
val ls_of_ts : tysymbol -> lsymbol
(* test whether a function symbol has ty_type as ls_value *)
val is_ls_of_ts : lsymbol -> bool
(* convert a type to a term of type ty_type *)
val term_of_ty : vsymbol Mtv.t -> ty -> term
......
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