diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-17 16:07:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 01:38:33 +0200 |
| commit | 6007579ade085a60664e6b0d4596ff98c51aabf9 (patch) | |
| tree | 58c0b5ae6c6f77b31df07e0bd906f56c23ec044a /interp | |
| parent | c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 (diff) | |
Using more general information for primitive records.
This brings more compatibility with handling of mutual primitive records
in the kernel.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 13 | ||||
| -rw-r--r-- | interp/discharge.ml | 7 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 |
3 files changed, 13 insertions, 9 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index aa737239b..e79cc6079 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,11 +383,14 @@ let inInductive : inductive_obj -> obj = rebuild_function = infer_inductive_subtyping } let declare_projections univs mind = + (** FIXME: handle mutual records *) + let mind = (mind, 0) in let env = Global.env () in - let spec,_ = Inductive.lookup_mind_specif env (mind,0) in + let spec,_ = Inductive.lookup_mind_specif env mind in match spec.mind_record with - | Some (Some (_, kns, _)) -> - let projs = Inductiveops.compute_projections env (mind, 0) in + | PrimRecord info -> + let _, kns, _ = info.(0) in + let projs = Inductiveops.compute_projections env mind in Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in let univs = match univs with @@ -410,8 +413,8 @@ let declare_projections univs mind = assert (Constant.equal kn kn') ) kns projs; true, true - | Some None -> true,false - | None -> false,false + | FakeRecord -> true,false + | NotRecord -> false,false (* for initial declaration *) let declare_mind mie = diff --git a/interp/discharge.ml b/interp/discharge.ml index e16a955d9..0e44a8b46 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -111,9 +111,10 @@ let process_inductive info modlist mib = let section_decls' = Context.Named.map discharge section_decls in let (params',inds') = abstract_inductive section_decls' nparamdecls inds in let record = match mib.mind_record with - | Some (Some (id, _, _)) -> Some (Some id) - | Some None -> Some None - | None -> None + | PrimRecord info -> + Some (Some (Array.map pi1 info)) + | FakeRecord -> Some None + | NotRecord -> None in { mind_entry_record = record; mind_entry_finite = mib.mind_finite; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 74618a290..5bf46282f 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -113,7 +113,7 @@ let type_of_global_ref gr = "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record <> None then + if mib.Declarations.mind_record <> Declarations.NotRecord then begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" |