Commit 0e46a420 authored by Francois Bobot's avatar Francois Bobot
Browse files

Encoding_decorate : Correction, ajout des définitions des logics avant de...

  Encoding_decorate : Correction, ajout des définitions des logics avant de faire le clone. Dommage que theory ne verifie plus les knowns sinon l'exception aurait été levé lors du clone plutôt que lors du flat_theory.
parent 23ca2d16
......@@ -75,15 +75,20 @@ let load_prelude env =
let name = ts.ts_name.id_short in
let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
let ty = (ty_app ts []) in
let add_fsymbol fs task =
let decl = Decl.create_logic_decl [fs,None] in
add_decl task decl in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] ty in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [ty] undeco in
let th_uc = add_fsymbol d2ty (add_fsymbol ty2u th_uc) in
let th_inst = create_inst
~ts:[type_t,ts]
~ls:[logic_d2t,d2ty;logic_t2u,ty2u]
~lemma:[] ~goal:[] in
let lconv = { d2t = d2ty; t2u = ty2u} in
let th_uc = clone_export th_uc builtin th_inst in
let task = flat_theory task (close_theory th_uc) in
let th = close_theory th_uc in
let task = flat_theory task th in
task,Mts.add ts lconv spmap
in
let task,specials =
......
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