Commit f5ce6ef2 authored by Andrei Paskevich's avatar Andrei Paskevich

Coq: preserve Set-typed lambdas

parent 65cd4261
......@@ -6,9 +6,8 @@ time "why3cpulimit time : %s s"
(* À discuter *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
......
......@@ -145,6 +145,8 @@ let rec print_ty info fmt ty =
| [ty] -> print_ty info fmt ty
| _ -> fprintf fmt "(%a)%%type" (print_list star (print_ty info)) tl
end
| Tyapp (ts, [l;r]) when ts_equal ts ts_func ->
fprintf fmt "(%a ->@ %a)" (print_ty info) l (print_ty info) r
| Tyapp (ts, tl) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_ty info) fmt tl
......@@ -277,14 +279,26 @@ and print_tnode _opl opr info fmt t = match t.t_node with
(print_term info) t
(print_list newline (print_tbranch info)) bl
| Teps fb ->
let v,f = t_open_bound fb in
fprintf fmt (protect_on opr "epsilon %a.@ %a")
(print_vsty info) v (print_opl_fmla info) f;
forget_var v
let vl,_,t0 = t_open_lambda t in
if vl = [] then begin
let v,f = t_open_bound fb in
fprintf fmt (protect_on opr "epsilon %a.@ %a")
(print_vsty info) v (print_opl_fmla info) f;
forget_var v
end else begin
if t0.t_ty = None then unsupportedTerm t
"Coq: Prop-typed lambdas are not supported";
fprintf fmt (protect_on opr "fun %a =>@ %a")
(print_list space (print_vsty info)) vl
(print_opl_term info) t0;
List.iter forget_var vl
end
| Tapp (fs,[]) when is_fs_tuple fs ->
fprintf fmt "tt"
| Tapp (fs,pl) when is_fs_tuple fs ->
fprintf fmt "%a" (print_paren_r (print_term info)) pl
| Tapp (fs,[l;r]) when ls_equal fs fs_func_app ->
fprintf fmt "(%a@ %a)" (print_opr_term info) l (print_opr_term info) r
| Tapp (fs, tl) ->
begin match query_syntax info.info_syn fs.ls_name with
| Some s ->
......
......@@ -63,14 +63,26 @@ let get_canonical =
let res = get_canonical ls in
Hls.add ht ls res; res
let rec lift_f acc t0 = match t0.t_node with
| (Tapp (ps, [t1; {t_node = Teps fb}])
| Tapp (ps, [{t_node = Teps fb}; t1]))
when ls_equal ps ps_equ ->
type to_elim =
| All (* eliminate all epsilon-terms *)
| NonLambda (* preserve lambda-terms *)
| NonLambdaSet (* preserve lambda-terms with value-typed body *)
let to_elim el t = match el with
| All -> true
| NonLambda -> not (t_is_lambda t)
| NonLambdaSet ->
let vl,_,t = t_open_lambda t in
vl = [] || t.t_ty = None
let rec lift_f el acc t0 = match t0.t_node with
| (Tapp (ps, [t1; {t_node = Teps fb} as t2])
| Tapp (ps, [{t_node = Teps fb} as t2; t1]))
when ls_equal ps ps_equ && to_elim el t2 ->
let vs, f = t_open_bound fb in
let f = t_let_close_simp vs t1 f in
lift_f acc (t_label_copy t0 f)
| Teps fb ->
lift_f el acc (t_label_copy t0 f)
| Teps fb when to_elim el t0 ->
let vl = Mvs.keys (t_vars t0) in
let vs, f = t_open_bound fb in
let acc, t = match is_canonical vs f with
......@@ -79,7 +91,7 @@ let rec lift_f acc t0 = match t0.t_node with
let ld, ax, cs = get_canonical ls in
(ld :: abst, ax :: axml), fs_app cs [] vs.vs_ty
| None ->
let (abst,axml), f = lift_f acc f in
let (abst,axml), f = lift_f el acc f in
let tyl = List.map (fun x -> x.vs_ty) vl in
let ls = create_fsymbol (id_clone vs.vs_name) tyl vs.vs_ty in
let t = fs_app ls (List.map t_var vl) vs.vs_ty in
......@@ -90,26 +102,26 @@ let rec lift_f acc t0 = match t0.t_node with
in
acc, t_label_copy t0 t
| _ ->
t_map_fold lift_f acc t0
t_map_fold (lift_f el) acc t0
let lift_l (acc,dl) (ls,ld) =
let lift_l el (acc,dl) (ls,ld) =
let vl, t, close = open_ls_defn_cb ld in
match t.t_node with
| Teps fb ->
| Teps fb when to_elim el t ->
let vs, f = t_open_bound fb in
let (abst,axml), f = lift_f acc f in
let (abst,axml), f = lift_f el acc f in
let t = t_app ls (List.map t_var vl) t.t_ty in
let f = t_forall_close_merge vl (t_subst_single vs t f) in
let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
let ax = create_prop_decl Paxiom (create_prsymbol id) f in
(create_param_decl ls :: abst, ax :: axml), dl
| _ ->
let acc, t = lift_f acc t in
let acc, t = lift_f el acc t in
acc, close ls vl t :: dl
let lift_d d = match d.d_node with
let lift_d el d = match d.d_node with
| Dlogic dl ->
let (abst,axml), dl = List.fold_left lift_l (([],[]),[]) dl in
let (abst,axml), dl = List.fold_left (lift_l el) (([],[]),[]) dl in
if dl = [] then List.rev_append abst (List.rev axml) else
let d = create_logic_decl (List.rev dl) in
let add_ax (axml1, axml2) ax =
......@@ -118,10 +130,20 @@ let lift_d d = match d.d_node with
let axml1, axml2 = List.fold_left add_ax ([],[]) axml in
List.rev_append abst (axml1 @ d :: axml2)
| _ ->
let (abst,axml), d = decl_map_fold lift_f ([],[]) d in
let (abst,axml), d = decl_map_fold (lift_f el) ([],[]) d in
List.rev_append abst (List.rev_append axml [d])
let eliminate_epsilon = Trans.decl lift_d None
let eliminate_epsilon = Trans.decl (lift_d All) None
let eliminate_nl_epsilon = Trans.decl (lift_d NonLambda) None
let eliminate_nls_epsilon = Trans.decl (lift_d NonLambdaSet) None
let () = Trans.register_transform "eliminate_epsilon" eliminate_epsilon
~desc:"Eliminate@ lambda-terms@ and@ other@ comprehension@ forms."
let () = Trans.register_transform "eliminate_non_lambda_epsilon"
eliminate_nl_epsilon
~desc:"Eliminate@ all@ comprehension@ forms@ except@ lambda-terms."
let () = Trans.register_transform "eliminate_non_lambda_set_epsilon"
eliminate_nls_epsilon
~desc:"Eliminate@ all@ comprehension@ forms@ except@ value-typed@ lambda-terms."
......@@ -10,3 +10,4 @@
(********************************************************************)
val eliminate_epsilon : Task.task Trans.trans
val eliminate_nl_epsilon : Task.task Trans.trans
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