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

coq-plugin: inductive types (in progress)

parent 490f7095
......@@ -6,5 +6,5 @@ Parameter foo : Set -> Set.
Definition t : Set := foo Z.
Definition u : Set := foo t.
Goal forall x:u, x=x.
Goal forall x:nat, x=x.
......@@ -256,7 +256,7 @@ and tr_global_ts env r =
let b = force b in
let (tv, vars), env, t = decomp_type_lambdas env b in
let def = Some (tr_type tv env t) in
Ty.create_tysymbol id vars None
Ty.create_tysymbol id vars def
(* FIXME: is it correct to use None when NotFO? *)
| None ->
let tv =
......@@ -268,7 +268,31 @@ and tr_global_ts env r =
task := Task.add_ty_decl !task [ts, Decl.Tabstract];
| IndRef i ->
assert false (*TODO*)
Format.eprintf "ici@.";
let mib, _ = Global.lookup_inductive i in
let make_one_ts j _ =
let r = IndRef (ith_mutual_inductive i j) in
let ty = Global.type_of_global r in
let tv, _, t = decomp_type_quantifiers env ty in
if not (is_Set t) && not (is_Type t) then raise NotFO;
let id = preid_of_id (Nametab.id_of_global r) in
let tv = (fun x -> Ty.create_tvsymbol (preid_of_id x)) tv
let ts = Ty.create_tysymbol id tv None in
add_global global_ts r (Some ts)
Array.iteri make_one_ts mib.mind_packets;
let make_one j ib =
let ls = [] in
let r = IndRef (ith_mutual_inductive i j) in
let ts = lookup_global global_ts r in
ts, Decl.Talgebraic ls
let decl = Array.mapi make_one mib.mind_packets in
let decl = Array.to_list decl in
task := Task.add_ty_decl !task decl;
lookup_global global_ts r
(* assumption: t:T:Set *)
and tr_term tv bv env t =
Supports Markdown
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