Commit 91e01461 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre Committed by Guillaume Melquiond

fixed why3tac with inhabited types

parent ebd056a5
......@@ -142,12 +142,23 @@ let coq_iff = lazy (constant "iff")
let is_constant t c = try t = Lazy.force c with _ -> false
let coq_WhyType =
lazy (gen_constant_in_modules "why" [["Why3"; "BuiltIn"]] "WhyType")
let rec is_WhyType c = match kind_of_term c with
| App (f, [|_|]) -> is_constant f coq_WhyType
| Cast (c, _, _) -> is_WhyType c
| _ -> false
let has_WhyType env c = is_WhyType (type_of env Evd.empty c)
(* not first-order expressions *)
exception NotFO
(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
env names, and returns the new variables together with the new
environment *)
(*
let coq_rename_vars env vars =
let avoid = ref (ids_of_named_context (Environ.named_context env)) in
List.fold_right
......@@ -156,8 +167,9 @@ let coq_rename_vars env vars =
avoid := id :: !avoid;
id :: newvars, Environ.push_named (id, None, t) newenv)
vars ([],env)
*)
let coq_rename_var env (na,t) =
let coq_rename_var env na t =
let avoid = ids_of_named_context (Environ.named_context env) in
let id = next_name_away na avoid in
id, Environ.push_named (id, None, t) env
......@@ -182,32 +194,40 @@ let rec_names_for c =
(* extract the prenex type quantifications i.e.
type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
let decomp_type_quantifiers env t =
let rec loop vars t = match kind_of_term t with
let add m id =
let tv = Ty.create_tvsymbol (preid_of_id id) in
Idmap.add id (Some (Ty.ty_var tv)) m, tv
in
let rec loop env tvm vars t = match kind_of_term t with
| Prod (n, a, t) when is_Set a || is_Type a ->
loop ((n, a) :: vars) t
let n, env = coq_rename_var env n a in
let t = subst1 (mkVar n) t in
let tvm, tv = add tvm n in
loop env tvm (tv :: vars) t
| Prod (n, a, t) when is_WhyType a ->
let n, env = coq_rename_var env n a in
let t = subst1 (mkVar n) t in
loop env tvm vars t
| _ ->
let vars, env = coq_rename_vars env vars in
let t = substl (List.map mkVar vars) t in
let add m id =
let tv = Ty.create_tvsymbol (preid_of_id id) in
Idmap.add id (Some (Ty.ty_var tv)) m, tv
in
let tvm, vars = Util.map_fold_left add Idmap.empty vars in
(tvm, List.rev vars), env, t
in
loop [] t
loop env Idmap.empty [] t
(* decomposes the first n type lambda abstractions correspondings to
the list of type variables vars *)
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
| vars, Lambda (n, a, t) when is_WhyType a ->
let id, env = coq_rename_var env n a in
let t = subst1 (mkVar id) t in
loop tvm env vars t
| tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
let id, env = coq_rename_var env (n, a) in
let id, env = coq_rename_var env n a in
let t = subst1 (mkVar id) t in
let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
loop tvm env vars t
| [], _ ->
tvm, env, t
| _ ->
raise NotFO (*TODO: eta-expansion*)
in
......@@ -230,7 +250,7 @@ let decomp_lambdas _dep _tvm bv env vars t =
| [], _ ->
(bv, List.rev vsl), env, t
| ty :: vars, Lambda (n, a, t) ->
let id, env = coq_rename_var env (n, a) in
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 (Some vs) bv in
......@@ -434,6 +454,7 @@ let rec tr_type dep tvm env t =
begin try
let r = global_of_constr f in
let ts = tr_task_ts dep env r in
let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
assert (List.length ts.Ty.ts_args = List.length cl);
(* since t:Set *)
Ty.ty_app ts (List.map (tr_type dep tvm env) cl)
......@@ -846,6 +867,7 @@ and tr_term dep tvm bv env t =
let ls = tr_task_ls dep env r in
begin match ls.Term.ls_value with
| Some _ ->
let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
let k = get_poly_arity ls in
let cl = skip_k_args k cl in
let ty = type_of env Evd.empty t in
......@@ -872,8 +894,7 @@ and tr_term dep tvm bv env t =
(* abstract app l *)
and quantifiers n a b dep tvm bv env =
let vars, env = coq_rename_vars env [n,a] in
let id = match vars with [x] -> x | _ -> assert false in
let id, env = coq_rename_var env n a in
let b = subst1 (mkVar id) b in
let t = tr_type dep tvm env a in
let vs = Term.create_vsymbol (preid_of_id id) t in
......@@ -988,6 +1009,7 @@ and tr_formula dep tvm bv env f = match kind_of_term f with
let ls = tr_task_ls dep env r in
begin match ls.Term.ls_value with
| None ->
let args = List.filter (fun c -> not (has_WhyType env c)) args in
let k = get_poly_arity ls in
let args = skip_k_args k args in
Term.ps_app ls (List.map (tr_term dep tvm bv env) args)
......@@ -1014,6 +1036,9 @@ let tr_goal gl =
| (id, None, ty) :: ctxt when is_fo_kind ty ->
let tvm = Idmap.add id None tvm in
tr_ctxt tvm bv ctxt
| (id, None, ty) :: ctxt when is_WhyType ty ->
let bv = Idmap.add id None bv in
tr_ctxt tvm bv ctxt
| (id, None, ty) :: ctxt ->
let t = type_of env Evd.empty ty in
begin try
......
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