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

coq-plugin: synchronization of global tables

parent 60a63902
......@@ -3,9 +3,43 @@ Require Export ZArith.
Open Scope Z_scope.
Require Export List.
Parameter foo : Set -> Set.
Definition t : Set := foo Z.
Definition u : Set := foo t.
(* Inductive types *)
Goal forall x: list nat, x=x.
(* Mutually inductive types *)
Inductive tree : Set :=
| Leaf : tree
| Node : Z -> forest -> tree
with forest : Set :=
| Nil : forest
| Cons : tree -> forest -> forest.
Goal forall x : tree, x=x.
(* Polymorphic, Mutually inductive types *)
Inductive ptree (a:Set) : Set :=
| PLeaf : ptree a
| PNode : a -> pforest a -> ptree a
with pforest (a:Set) : Set :=
| PNil : pforest a
| PCons : ptree a -> pforest a -> pforest a.
Goal forall x : ptree Z, x=x.
(* the same, without parameters *)
Inductive ptree' : Type -> Type :=
| PLeaf' : forall (a:Type), ptree' a
| PNode' : forall (a:Type), a -> pforest' a -> ptree' a
with pforest' : Type -> Type :=
| PNil' : forall (a:Type), pforest' a
| PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a.
Goal forall x : ptree' Z, x=x.
why.
......@@ -151,7 +151,20 @@ let decompose_arrows =
(* Coq globals *)
let global_ts = ref Refmap.empty
(* let global_ls = ref Refmap.empty *)
let global_ls = ref Refmap.empty
(* synchronization *)
let () =
Summary.declare_summary "Why globals"
{ Summary.freeze_function =
(fun () -> !global_ts, !global_ls);
Summary.unfreeze_function =
(fun (ts,ls) -> global_ts := ts; global_ls := ls);
Summary.init_function =
(fun () -> ());
Summary.survive_module = true;
Summary.survive_section = true;
}
let lookup_global table r = match Refmap.find r !table with
| None -> raise NotFO
......@@ -306,7 +319,9 @@ and tr_global_ts env r =
let l, _ = decompose_arrows t in
let l = List.map (tr_type tv env) l in
let id = preid_of_id (Nametab.id_of_global r) in
Term.create_lsymbol id l (Some tyj)
let ls = Term.create_lsymbol id l (Some tyj) in
add_global global_ls r (Some ls);
ls
in
let ls = Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc) in
ts, Decl.Talgebraic ls
......
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