diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 41 |
1 files changed, 25 insertions, 16 deletions
diff --git a/library/lib.ml b/library/lib.ml index 3311965652..31f9835951 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -380,11 +380,14 @@ let find_opening_node id = *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types + type variable_context = variable_info list -type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t +type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t * + variable_context Univ.in_universe_context Names.Mindmap.t let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * + Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" @@ -392,18 +395,19 @@ let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab -let add_section_variable id impl = +let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl)::vars,repl,abs)::sl + sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> - (id',impl,b,t) :: aux (idl,hyps) + | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + let l, r = aux (idl,hyps) in + (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r | (id::idl,hyps) -> aux (idl,hyps) - | [], _ -> [] + | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context sign = @@ -413,23 +417,26 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t)) - +let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx + let add_section_replacement f g hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let sechyps = extract_hyps (vars,hyps) in + let sechyps,ctx = extract_hyps (vars,hyps) in + let ctx = Univ.ContextSet.to_context ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f args exps,g sechyps abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in add_section_replacement f f -let add_section_constant kn = +let add_section_constant is_projection kn = + (* let g x (l1,l2) = (Names.Cmap.add kn (Univ.Instance.empty,[||]) l1,l2) in *) let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f + (* if is_projection then add_section_replacement g f *) + (* else *) add_section_replacement f f let replacement_context () = pi2 (List.hd !sectab) @@ -445,7 +452,9 @@ let rec list_mem_assoc x = function let section_instance = function | VarRef id -> - if list_mem_assoc id (pi1 (List.hd !sectab)) then [||] + if List.exists (fun (id',_,_,_) -> Names.id_eq id id') + (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) @@ -459,8 +468,8 @@ let full_replacement_context () = List.map pi2 !sectab let full_section_segment_of_constant con = List.map (fun (vars,_,(x,_)) -> fun hyps -> named_of_variable_context - (try Names.Cmap.find con x - with Not_found -> extract_hyps (vars, hyps))) !sectab + (try fst (Names.Cmap.find con x) + with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab (*************) (* Sections. *) |