Commit 8874bce9 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

- make the interface to ls_defn more straightforward

- assure generation of new variables on create_ls_defn
parent 38810ff7
...@@ -278,7 +278,7 @@ let print_type_decl fmt (ts,def) = match def with ...@@ -278,7 +278,7 @@ let print_type_decl fmt (ts,def) = match def with
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs () let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
let print_ls_defn fmt ld = let print_ls_defn fmt ld =
let _,vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
fprintf fmt " =@ %a" print_expr e; fprintf fmt " =@ %a" print_expr e;
List.iter forget_var vl List.iter forget_var vl
......
...@@ -43,24 +43,6 @@ type logic_decl = lsymbol * ls_defn option ...@@ -43,24 +43,6 @@ type logic_decl = lsymbol * ls_defn option
exception UnboundVars of Svs.t exception UnboundVars of Svs.t
exception IllegalConstructor of lsymbol exception IllegalConstructor of lsymbol
let check_fvs f =
let fvs = f_freevars Svs.empty f in
if Svs.is_empty fvs then f else raise (UnboundVars fvs)
let make_fs_defn fs vl t =
if fs.ls_constr then raise (IllegalConstructor fs);
let hd = t_app fs (List.map t_var vl) t.t_ty in
let fd = f_forall vl [] (f_equ hd t) in
fs, vl, Term t, check_fvs fd
let make_ps_defn ps vl f =
let hd = f_app ps (List.map t_var vl) in
let pd = f_forall vl [] (f_iff hd f) in
ps, vl, Fmla f, check_fvs pd
let make_ls_defn ls vl =
e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let extract_ls_defn f = let extract_ls_defn f =
let vl, ef = f_open_forall f in let vl, ef = f_open_forall f in
match ef.f_node with match ef.f_node with
...@@ -76,15 +58,28 @@ let extract_ls_defn f = ...@@ -76,15 +58,28 @@ let extract_ls_defn f =
end end
| _ -> assert false | _ -> assert false
let open_ls_defn (ls,vl,e,_) = (ls,vl,e) let check_fvs f =
let fvs = f_freevars Svs.empty f in
if Svs.is_empty fvs then f else raise (UnboundVars fvs)
let make_fs_defn fs vl t =
if fs.ls_constr then raise (IllegalConstructor fs);
let hd = t_app fs (List.map t_var vl) t.t_ty in
let fd = f_forall vl [] (f_equ hd t) in
extract_ls_defn fd
let make_ps_defn ps vl f =
let hd = f_app ps (List.map t_var vl) in
let pd = f_forall vl [] (f_iff hd f) in
extract_ls_defn pd
let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let open_fs_defn = function (_,vl,Term t,_) -> (vl,t) | _ -> assert false
let open_fs_defn = function let open_ps_defn = function (_,vl,Fmla f,_) -> (vl,f) | _ -> assert false
| (fs,vl,Term t,_) -> (fs,vl,t)
| _ -> assert false
let open_ps_defn = function let open_ls_defn (_,vl,e,_) = (vl,e)
| (ps,vl,Fmla f,_) -> (ps,vl,f)
| _ -> assert false
let ls_defn_axiom (_,_,_,f) = f let ls_defn_axiom (_,_,_,f) = f
......
...@@ -35,17 +35,17 @@ type ty_decl = tysymbol * ty_def ...@@ -35,17 +35,17 @@ type ty_decl = tysymbol * ty_def
type ls_defn type ls_defn
val make_ls_defn : lsymbol -> vsymbol list -> expr -> ls_defn type logic_decl = lsymbol * ls_defn option
val make_fs_defn : lsymbol -> vsymbol list -> term -> ls_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ls_defn
val open_ls_defn : ls_defn -> lsymbol * vsymbol list * expr val make_ls_defn : lsymbol -> vsymbol list -> expr -> logic_decl
val open_fs_defn : ls_defn -> lsymbol * vsymbol list * term val make_fs_defn : lsymbol -> vsymbol list -> term -> logic_decl
val open_ps_defn : ls_defn -> lsymbol * vsymbol list * fmla val make_ps_defn : lsymbol -> vsymbol list -> fmla -> logic_decl
val ls_defn_axiom : ls_defn -> fmla val open_ls_defn : ls_defn -> vsymbol list * expr
val open_fs_defn : ls_defn -> vsymbol list * term
val open_ps_defn : ls_defn -> vsymbol list * fmla
type logic_decl = lsymbol * ls_defn option val ls_defn_axiom : ls_defn -> fmla
(* inductive predicate declaration *) (* inductive predicate declaration *)
......
...@@ -160,7 +160,7 @@ let print_logic_decl drv ctxt fmt (ls,ld) = ...@@ -160,7 +160,7 @@ let print_logic_decl drv ctxt fmt (ls,ld) =
(print_list comma (print_type drv)) ls.ls_args (print_list comma (print_type drv)) ls.ls_args
(print_option_or_default "prop" (print_type drv)) ls.ls_value (print_option_or_default "prop" (print_type drv)) ls.ls_value
| Some ld -> | Some ld ->
let _,vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
begin match e with begin match e with
| Term t -> | Term t ->
(* TODO AC? *) (* TODO AC? *)
......
...@@ -292,7 +292,7 @@ let print_type_decl drv fmt d = ...@@ -292,7 +292,7 @@ let print_type_decl drv fmt d =
| _ -> print_type_decl drv fmt d; forget_tvs () | _ -> print_type_decl drv fmt d; forget_tvs ()
let print_ls_defn drv fmt ld = let print_ls_defn drv fmt ld =
let _,vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
fprintf fmt " =@ %a" (print_expr drv) e; fprintf fmt " =@ %a" (print_expr drv) e;
List.iter forget_var vl List.iter forget_var vl
......
...@@ -870,8 +870,8 @@ let add_logics dl th = ...@@ -870,8 +870,8 @@ let add_logics dl th =
match d.ld_type with match d.ld_type with
| None -> (* predicate *) | None -> (* predicate *)
let ps = Hashtbl.find psymbols id in let ps = Hashtbl.find psymbols id in
let defn = match d.ld_def with begin match d.ld_def with
| None -> None | None -> ps,None
| Some f -> | Some f ->
let f = dfmla denv f in let f = dfmla denv f in
let vl = match ps.ls_value with let vl = match ps.ls_value with
...@@ -879,13 +879,12 @@ let add_logics dl th = ...@@ -879,13 +879,12 @@ let add_logics dl th =
| _ -> assert false | _ -> assert false
in in
let env = env_of_vsymbol_list vl in let env = env_of_vsymbol_list vl in
Some (make_ps_defn ps vl (fmla env f)) make_ps_defn ps vl (fmla env f)
in end
ps, defn
| Some ty -> (* function *) | Some ty -> (* function *)
let fs = Hashtbl.find fsymbols id in let fs = Hashtbl.find fsymbols id in
let defn = match d.ld_def with begin match d.ld_def with
| None -> None | None -> fs,None
| Some t -> | Some t ->
let loc = t.pp_loc in let loc = t.pp_loc in
let t = dterm denv t in let t = dterm denv t in
...@@ -894,15 +893,13 @@ let add_logics dl th = ...@@ -894,15 +893,13 @@ let add_logics dl th =
| _ -> assert false | _ -> assert false
in in
let env = env_of_vsymbol_list vl in let env = env_of_vsymbol_list vl in
try Some (make_fs_defn fs vl (term env t)) try make_fs_defn fs vl (term env t)
with _ -> term_expected_type ~loc t.dt_ty (dty denv ty) with _ -> term_expected_type ~loc t.dt_ty (dty denv ty)
in end
fs, defn
in in
let dl = List.map type_decl dl in let dl = List.map type_decl dl in
List.fold_left add_decl th (create_logic_decls dl) List.fold_left add_decl th (create_logic_decls dl)
let term env t = let term env t =
let denv = create_denv env in let denv = create_denv env in
let t = dterm denv t in let t = dterm denv t in
......
...@@ -75,19 +75,19 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) = ...@@ -75,19 +75,19 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
match ld with match ld with
| None -> env,add_decl ctxt d | None -> env,add_decl ctxt d
| Some ld -> | Some ld ->
let _,vs,e = open_ls_defn ld in let vs,e = open_ls_defn ld in
match e with match e with
| Term t -> | Term t ->
let t = replacet env t in let t = replacet env t in
if t_s_any ffalse ((==) ls) t || isnotinlinedt t if t_s_any ffalse ((==) ls) t || isnotinlinedt t
then env, add_decl ctxt then env, add_decl ctxt
(create_logic_decl [(ls, Some (make_fs_defn ls vs t))]) (create_logic_decl [make_fs_defn ls vs t])
else {env with fs = Mls.add ls (vs,t) env.fs},ctxt else {env with fs = Mls.add ls (vs,t) env.fs},ctxt
| Fmla f -> | Fmla f ->
let f = replacep env f in let f = replacep env f in
if f_s_any ffalse ((==) ls) f || isnotinlinedf f if f_s_any ffalse ((==) ls) f || isnotinlinedf f
then env, add_decl ctxt then env, add_decl ctxt
(create_logic_decl [(ls,Some (make_ps_defn ls vs f))]) (create_logic_decl [make_ps_defn ls vs f])
else {env with ps = Mls.add ls (vs,f) env.ps},ctxt else {env with ps = Mls.add ls (vs,f) env.ps},ctxt
end end
| Dind dl -> | Dind dl ->
...@@ -97,10 +97,12 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) = ...@@ -97,10 +97,12 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
| Dlogic dl -> | Dlogic dl ->
env, env,
add_decl ctxt (create_logic_decl add_decl ctxt (create_logic_decl
(List.map (fun (ls,ld) -> ls, Util.option_map (fun ld -> (List.map (fun (ls,ld) -> match ld with
let _,vs,e = open_ls_defn ld in | None -> ls, None
let e = e_map (replacet env) (replacep env) e in | Some ld ->
make_ls_defn ls vs e) ld) dl)) let vs,e = open_ls_defn ld in
let e = e_map (replacet env) (replacep env) e in
make_ls_defn ls vs e) dl))
| Dtype dl -> env,add_decl ctxt d | Dtype dl -> env,add_decl ctxt d
| Dprop (k,pr,f) -> | Dprop (k,pr,f) ->
env,add_decl ctxt (create_prop_decl k pr (replacep env f)) env,add_decl ctxt (create_prop_decl k pr (replacep env f))
......
...@@ -241,9 +241,9 @@ let rewrite_elt rt rf d = ...@@ -241,9 +241,9 @@ let rewrite_elt rt rf d =
| Dlogic l -> [create_logic_decl (List.map | Dlogic l -> [create_logic_decl (List.map
(function (function
| (ls,Some def) -> | (ls,Some def) ->
let (ls,vsl,expr) = open_ls_defn def in let vsl,expr = open_ls_defn def in
let expr = e_map rt rf expr in let expr = e_map rt rf expr in
(ls,Some (make_ls_defn ls vsl expr)) make_ls_defn ls vsl expr
| l -> l) l)] | l -> l) l)]
| Dind indl -> [create_ind_decl | Dind indl -> [create_ind_decl
(List.map (fun (ls,pl) -> ls, (List.map (fun (ls,pl) -> ls,
......
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