Commit 995f52a6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

coq plugin: match

parent af1d7b2f
......@@ -25,7 +25,6 @@ transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
theory BuiltIn
syntax type int "int"
syntax type real "real"
......
......@@ -24,13 +24,12 @@ Qed.
Definition p (x:nat) := x=O.
Goal p O.
spass.
ae.
Qed.
Definition eq (A:Set) (x y : A) := x=y.
Goal eq nat O O.
why "z3".
ae.
(*
why "z3". (* BUG encoding decorate ici ? *)
......@@ -38,12 +37,13 @@ Qed.
*)
Admitted.
Parameter mem : forall (A:Set), A -> list A -> Prop.
Definition q (A:Set) (x:A) (y:list A) := mem A x y.
Definition pred (n:nat) := match n with
| O => O
| S p => p
end.
Goal q nat O (cons O nil).
(*why.*)
Goal pred (S O) = O.
ae.
Admitted.
(* function definition *)
......@@ -57,7 +57,7 @@ Qed.
Definition id A (x:A) := x.
Goal id nat O = O.
spass.
ae.
Qed.
(* inductive types *)
......@@ -67,7 +67,7 @@ Parameter P : (nat -> nat) -> Prop.
Goal forall (a:Set), forall x:nat, x=S O -> P S ->
let y := (S (S O)) in S x=y.
intros.
spass.
ae.
Qed.
Goal forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y.
......@@ -77,9 +77,20 @@ Qed.
Goal forall x: list nat, x=x.
intros.
spass.
ae.
Qed.
Goal forall x, (match x with (S (S _)) => True | _ => False end).
(* BUG *)
Admitted.
Goal forall a, forall (x: list (list a)), match x with nil => 1 | x :: r => 2 end <= 2.
intros.
try ae.
Admitted.
(* Mutually inductive types *)
Inductive tree : Set :=
......@@ -91,7 +102,11 @@ with forest : Set :=
| Cons : tree -> forest -> forest.
Goal forall x : tree, x=x.
spass.
ae.
Qed.
Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1.
ae.
Qed.
(* Polymorphic, Mutually inductive types *)
......
......@@ -160,7 +160,7 @@ let decomp_type_quantifiers env t =
(* decomposes the first n type lambda abstractions correspondings to
the list of type variables vars *)
let decomp_type_lambdas env vars t =
let decomp_type_lambdas tvm env vars t =
let rec loop tvm env vars t = match vars, kind_of_term t with
| [], _ ->
tvm, env, t
......@@ -172,7 +172,7 @@ let decomp_type_lambdas env vars t =
| _ ->
assert false (*TODO: eta-expansion*)
in
loop Idmap.empty env vars t
loop tvm env vars t
let decompose_arrows =
let rec arrows_rec l c = match kind_of_term c with
......@@ -182,6 +182,23 @@ let decompose_arrows =
in
arrows_rec []
let decomp_lambdas _dep _tvm env vars t =
let rec loop bv vsl env vars t = match vars, kind_of_term t with
| [], _ ->
(bv, List.rev vsl), env, t
| ty :: vars, Lambda (n, a, t) ->
let id, env = coq_rename_var env (n, a) in
let t = subst1 (mkVar id) t in
let vs = create_vsymbol (preid_of_id id) ty in
let bv = Idmap.add id vs bv in
loop bv (vs :: vsl) env vars t
| _ ->
assert false (*TODO: eta-expansion*)
in
loop Idmap.empty [] env vars t
let rec skip_k_args k cl = match k, cl with
| 0, _ -> cl
| _, _ :: cl -> skip_k_args (k-1) cl
......@@ -348,7 +365,7 @@ and tr_global_ts dep env r =
let ts = match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
let tvm, env, t = decomp_type_lambdas env vars b in
let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
let def = Some (tr_type dep' tvm env t) in
Ty.create_tysymbol id vars def
(* FIXME: is it correct to use None when NotFO? *)
......@@ -467,7 +484,7 @@ and tr_global_ls dep env r =
let ld = match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
let tvm, env, b = decomp_type_lambdas env vars b in
let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
let (bv, vsl), env, b = decomp_lambdas dep' tvm env args b in
begin match ls.ls_value with
| None ->
......@@ -490,21 +507,6 @@ and tr_global_ls dep env r =
raise NotFO
and decomp_lambdas _dep _tvm env vars t =
let rec loop bv vsl env vars t = match vars, kind_of_term t with
| [], _ ->
(bv, List.rev vsl), env, t
| ty :: vars, Lambda (n, a, t) ->
let id, env = coq_rename_var env (n, a) in
let t = subst1 (mkVar id) t in
let vs = create_vsymbol (preid_of_id id) ty in
let bv = Idmap.add id vs bv in
loop bv (vs :: vsl) env vars t
| _ ->
assert false (*TODO: eta-expansion*)
in
loop Idmap.empty [] env vars t
(* translation of a Coq term
assumption: t:T:Set *)
and tr_term dep tvm bv env t =
......@@ -557,6 +559,26 @@ and tr_term dep tvm bv env t =
(* first-order terms *)
| Var id when Idmap.mem id bv ->
Term.t_var (Idmap.find id bv)
| Case (ci, _, e, br) ->
let ty = type_of env Evd.empty e in
let ty = tr_type dep tvm env ty in
let e = tr_term dep tvm bv env e in
let branch j bj =
let tj = type_of env Evd.empty bj in
let (_,tvars), _, tj = decomp_type_quantifiers env tj in
let tyl, _ = decompose_arrows tj in
let tyl = List.map (tr_type dep tvm env) tyl in
let tvm, env, bj = decomp_type_lambdas tvm env tvars bj in
let (bv, vars), env, bj = decomp_lambdas dep tvm env tyl bj in
let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
let ls = tr_global_ls dep env (ConstructRef cj) in
if List.length vars <> List.length ls.ls_args then raise NotFO;
let pat = pat_app ls (List.map pat_var vars) ty in
[pat], tr_term dep tvm bv env bj
in
let ty = type_of env Evd.empty t in
let ty = tr_type dep tvm env ty in
t_case [e] (Array.to_list (Array.mapi branch br)) ty
| _ ->
let f, cl = decompose_app t in
let r = global_of_constr f in
......@@ -669,6 +691,26 @@ and tr_formula dep tvm bv env f =
(* TODO: we could eta-expanse *)
raise NotFO
end
| Case (ci, _, e, br), [] ->
let ty = type_of env Evd.empty e in
let ty = tr_type dep tvm env ty in
let t = tr_term dep tvm bv env e in
let branch j bj =
let tj = type_of env Evd.empty bj in
let (_,tvars), _, tj = decomp_type_quantifiers env tj in
let tyl, _ = decompose_arrows tj in
let tyl = List.map (tr_type dep tvm env) tyl in
let tvm, env, bj = decomp_type_lambdas tvm env tvars bj in
let (bv, vars), env, bj = decomp_lambdas dep tvm env tyl bj in
let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
let ls = tr_global_ls dep env (ConstructRef cj) in
if List.length vars <> List.length ls.ls_args then raise NotFO;
let pat = pat_app ls (List.map pat_var vars) ty in
[pat], tr_formula dep tvm bv env bj
in
f_case [t] (Array.to_list (Array.mapi branch br))
| Case _, _ :: _ ->
raise NotFO (* TODO: we could possibly swap case and application *)
| _ ->
let r = global_of_constr c in (*TODO: may fail *)
let ls = tr_task_ls dep env r in
......
......@@ -4,7 +4,7 @@ timelimit = 2
[prover alt-ergo]
name = "Alt-Ergo"
command = "why-cpulimit %t %m alt-ergo %f 2>&1"
command = "why-cpulimit %t %m alt-ergo -debug %f"
driver = "drivers/alt_ergo.drv"
[prover coq]
......
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