coq plugin (and alt-ergo driver): mutual recursion

parent da444d89
......@@ -18,6 +18,7 @@ transformation "inline_trivial"
*)
transformation "eliminate_builtin"
transformation "eliminate_mutual_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
......
......@@ -3,11 +3,13 @@ Require Export ZArith.
Open Scope Z_scope.
Require Export List.
Ltac ae := why "alt-ergo".
Ltac z3 := why "z3".
Ltac spass := why "spass".
Print length.
(* type definitions *)
Definition t := list.
......@@ -67,12 +69,18 @@ Goal id nat O = O.
ae.
Qed.
(* recursive function definition *)
Goal length (cons 1 (cons 2 nil)) = S (S O).
ae.
Qed.
(* recursive predicate definition *)
Print In.
Goal In 0 (cons 1 (cons 0 nil)).
ae.
try ae.
(* ICI *)
Admitted.
......@@ -124,9 +132,8 @@ with forest_size (f:forest) : Z := match f with
| Nil => 0
| Cons t f => tree_size t + forest_size f end.
Print tree_size.
Goal forall x : tree, x=x.
Goal tree_size Leaf = 0.
ae.
Qed.
......@@ -148,6 +155,21 @@ Goal forall x : ptree Z, x=x.
ae.
Qed.
Fixpoint ptree_size (a:Set) (t:ptree a) : Z := match t with
| PLeaf => 0
| PNode _ f => 1 + pforest_size _ f end
with pforest_size (a:Set) (f:pforest a) : Z := match f with
| PNil => 0
| PCons t f => ptree_size _ t + pforest_size _ f end.
Goal ptree_size _ (@PLeaf Z) = 0.
ae.
Qed.
Goal forall (a:Set), ptree_size a (PLeaf _) = 0.
(* TODO: intro context *)
Admitted.
(* the same, without parameters *)
Inductive ptree' : Type -> Type :=
......
......@@ -59,6 +59,14 @@ let get_prover s =
Hashtbl.add provers s (cp, drv);
cp, drv
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
let print_tvm fmt m =
Idmap.iter (fun id tv -> Format.fprintf fmt "%s->%a@ "
(string_of_id id) Why.Pretty.print_tv tv) m
let print_bv fmt m =
Idmap.iter (fun id vs -> Format.fprintf fmt "%s->%a@ "
(string_of_id id) Why.Pretty.print_vsty vs) m
(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]
......@@ -554,10 +562,12 @@ and decompose_definition dep env c =
ls, None
| Some b ->
let ty = Global.type_of_global r in
let (_, vars), env, _ = decomp_type_quantifiers env ty in
let (tvm, vars), env, ty = decomp_type_quantifiers env ty in
let tyl, _ = decompose_arrows ty in
let tyl = List.map (tr_type dep tvm env) tyl in
let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
let (bv, vsl), env, b =
decomp_lambdas dep tvm Idmap.empty env ls.ls_args b
decomp_lambdas dep tvm Idmap.empty env tyl b
in
begin match ls.ls_value with
| None ->
......
......@@ -70,7 +70,8 @@ let rec f_insert hd f = match f.f_node with
| _ -> f_iff_simp hd f
let add_ld func pred axl d = match d with
| _, None -> axl, d
| _, None ->
axl, d
| ls, Some ld ->
let vl,e = open_ls_defn ld in begin match e with
| Term t when func ->
......@@ -88,21 +89,24 @@ let add_ld func pred axl d = match d with
| _ -> axl, d
end
let elim func pred d = match d.d_node with
| Dlogic l ->
let elim func pred mutual d = match d.d_node with
| Dlogic l when not mutual || List.length l > 1 ->
let axl, l = map_fold_left (add_ld func pred) [] l in
let d = create_logic_decl l in
d :: List.rev axl
| _ -> [d]
let eliminate_definition_func =
Register.store (fun () -> Trans.decl (elim true false) None)
Register.store (fun () -> Trans.decl (elim true false false) None)
let eliminate_definition_pred =
Register.store (fun () -> Trans.decl (elim false true) None)
Register.store (fun () -> Trans.decl (elim false true false) None)
let eliminate_definition =
Register.store (fun () -> Trans.decl (elim true true) None)
Register.store (fun () -> Trans.decl (elim true true false) None)
let eliminate_mutual_recursion =
Register.store (fun () -> Trans.decl (elim true true true) None)
let () =
Register.register_transform "eliminate_definition_func"
......@@ -110,5 +114,8 @@ let () =
Register.register_transform "eliminate_definition_pred"
eliminate_definition_pred;
Register.register_transform "eliminate_definition"
eliminate_definition
eliminate_definition;
Register.register_transform "eliminate_mutual_recursion"
eliminate_mutual_recursion
......@@ -23,3 +23,4 @@ val eliminate_definition_func : Task.task Register.trans_reg
val eliminate_definition_pred : Task.task Register.trans_reg
val eliminate_definition : Task.task Register.trans_reg
val eliminate_mutual_recursion: Task.task Register.trans_reg
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