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

guard : ajout d'une projection des types vers les entiers

parent 1814780c
......@@ -267,6 +267,7 @@ let decl kept d = match d.d_node with
let empty_th =
let task = use_export None Theory.builtin_theory in
let task = Task.add_decl task d_ts_type in
let task = Task.add_logic_decl task [ls_int_of_ty,None] in
let task = Task.add_logic_decl task [Transform.fs_type,None] in
task
......
......@@ -44,19 +44,32 @@ let ls_selects_of_ts = Wts.memoize 63 (fun ts ->
create_fsymbol preid [ty_type] ty_type in
List.rev_map create_select ts.ts_args)
let ls_int_of_ty = create_fsymbol (id_fresh "int_of_ty") [ty_type] ty_int
(** definition of the previous selecting functions *)
let ls_selects_def_of_ts acc ts =
let ls = ls_of_ts ts in
let ls_selects = ls_selects_of_ts ts in
let vars = List.rev_map
(fun _ -> create_vsymbol (id_fresh "x") ty_type) ls_selects
(fun _ -> create_vsymbol (id_fresh "x") ty_type) ts.ts_args
in
let tvars = List.map t_var vars in
(** type to int *)
let id = string_of_int (id_hash ts.ts_name) in
let acc =
let t = t_app ls tvars ty_type in
let f = f_equ (t_app ls_int_of_ty [t] ty_int) (t_int_const id) in
let f = f_forall_close vars [[Term t]] f in
let prsymbol = create_prsymbol (id_clone ts.ts_name) in
create_prop_decl Paxiom prsymbol f :: acc
in
(** select *)
let ls_selects = ls_selects_of_ts ts in
let fmlas = List.rev_map2
(fun ls_select value ->
let t = t_app ls tvars ty_type in
let f = f_equ (t_app ls_select [t] ty_type) value in
let f = f_forall_close vars [] f in
let t = t_app ls_select [t] ty_type in
let f = f_equ t value in
let f = f_forall_close vars [[Term t]] f in
f)
ls_selects tvars in
let create_props ls_select fmla =
......
......@@ -33,6 +33,9 @@ val d_ts_type : decl
(* function symbol mapping ty_type^n to ty_type *)
val ls_of_ts : tysymbol -> lsymbol
(* function symbol mapping ty_type^n to int *)
val ls_int_of_ty : lsymbol
(* function symbol selecting ty_type from ty_type^n *)
val ls_selects_of_ts : tysymbol -> lsymbol list
......
......@@ -83,7 +83,7 @@ end
theory TestEnco
use import int.Int
meta "encoding_decorate : kept" type int
meta "encoding : kept" type int
type mytype 'a
logic id(x: int) : int = x
logic id2(x: int) : int = id(x)
......
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