Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit c941d961 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Add model_projection meta on t'int and t'real.

parent 1fd57917
......@@ -153,6 +153,9 @@ let meta_range = register_meta "range_type" [MTtysymbol; MTlsymbol]
let meta_float = register_meta "float_type" [MTtysymbol; MTlsymbol; MTlsymbol]
~desc:"Projection@ and@ finiteness@ of@ a@ floating-point@ type."
let meta_projection = register_meta "model_projection" [MTlsymbol]
~desc:"Declares@ the@ projection."
(** Theory *)
type theory = {
......
......@@ -80,6 +80,7 @@ val list_metas : unit -> meta list
val meta_range : meta
val meta_float : meta
val meta_projection: meta
(** {2 Theories} *)
......
......@@ -412,6 +412,7 @@ let add_range_decl uc add_decl add_meta ts rg =
let pj = create_fsymbol id [ty_app ts []] ty_int in
let uc = add_decl uc (Decl.create_param_decl pj) in
let uc = add_meta uc meta_range [MAts ts; MAls pj] in
let uc = add_meta uc meta_projection [MAls pj] in
(* create max attribute *)
let nm = ts.ts_name.id_string ^ "'maxInt" in
let id = id_derive nm ts.ts_name in
......@@ -430,6 +431,7 @@ let add_float_decl uc add_decl add_meta ts fmt =
let id = id_derive nm ts.ts_name in
let pj = create_fsymbol id [ty_app ts []] ty_real in
let uc = add_decl uc (Decl.create_param_decl pj) in
let uc = add_meta uc meta_projection [MAls pj] in
(* FIXME: "t'is_finite" is probably better *)
let nm = ts.ts_name.id_string ^ "'isFinite" in
let id = id_derive nm ts.ts_name in
......
......@@ -62,10 +62,6 @@ let debug_decl decl =
Debug.dprintf debug "Declaration %s @." s
*)
(* Meta to tag projection functions *)
let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
~desc:"Declares@ the@ projection."
let intro_const_equal_to_term
~term
~id_new
......@@ -252,7 +248,7 @@ let encapsulate env projs : Task.task Trans.trans =
meta_transform2 (fun d -> introduce_projs env map_projs d.Task.task_decl.td_node)
let intro_projections_counterexmp env =
Trans.on_tagged_ls meta_projection (encapsulate env)
Trans.on_tagged_ls Theory.meta_projection (encapsulate env)
let () = Trans.register_env_transform "intro_projections_counterexmp" intro_projections_counterexmp
......
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