Commit 59ecc013 authored by Andrei Paskevich's avatar Andrei Paskevich

use "syntax" instead of meta syntax_dist_smt

parent 9201ba9a
......@@ -137,8 +137,8 @@ theory array.Array
meta "encoding : lskept" logic get
meta "encoding : lskept" logic set
meta "smt_dist_syntax" logic get, "(%1[%2])"
meta "smt_dist_syntax" logic set, "(%1 WITH [%2] := %3)"
syntax logic get "(%1[%2])"
syntax logic set "(%1 WITH [%2] := %3)"
end
(*
......
......@@ -154,9 +154,9 @@ theory array.Array
meta "encoding : lskept" logic set
meta "encoding : lskept" logic create_const
meta "smt_dist_syntax" logic get, "(select %1 %2)"
meta "smt_dist_syntax" logic set, "(store %1 %2 %3)"
meta "smt_dist_syntax" logic create_const, "(const[%t0] %1)"
syntax logic get "(select %1 %2)"
syntax logic set "(store %1 %2 %3)"
syntax logic create_const "(const[%t0] %1)"
end
......
......@@ -288,9 +288,6 @@ let print_decl info fmt d = match d.d_node with
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let meta_dist_syntax =
Theory.register_meta "smt_dist_syntax" [MTlsymbol;MTstring]
let distingued =
let dist_syntax mls = function
| [MAls ls;MAstr s] -> Mls.add ls s mls
......@@ -301,7 +298,7 @@ let distingued =
Mid.add lsdis.ls_name (Mls.find ls syntax) mls
with Not_found -> mls end
| _ -> assert false in
Trans.on_meta meta_dist_syntax (fun syntax ->
Trans.on_meta meta_syntax_logic (fun syntax ->
let syntax = List.fold_left dist_syntax Mls.empty syntax in
Trans.on_meta Encoding.meta_lsinst (fun dis ->
let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
......
......@@ -292,9 +292,6 @@ let print_decl info fmt d = match d.d_node with
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let meta_dist_syntax =
Theory.register_meta "smt_dist_syntax" [MTlsymbol;MTstring]
let distingued =
let dist_syntax mls = function
| [MAls ls;MAstr s] -> Mls.add ls s mls
......@@ -305,7 +302,7 @@ let distingued =
Mid.add lsdis.ls_name (Mls.find ls syntax) mls
with Not_found -> mls end
| _ -> assert false in
Trans.on_meta meta_dist_syntax (fun syntax ->
Trans.on_meta meta_syntax_logic (fun syntax ->
let syntax = List.fold_left dist_syntax Mls.empty syntax in
Trans.on_meta Encoding.meta_lsinst (fun dis ->
let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
......
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