diff options
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index bbd043c8..b172acb1 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -164,14 +164,6 @@ let evaluable_constant cst env = try let _ = constant_value env (cst, Univ.Instance.empty) in true with Not_found | NotEvaluableConst _ -> false -let is_projection cst env = - not (Option.is_empty (lookup_constant cst env).const_proj) - -let lookup_projection p env = - match (lookup_constant (Projection.constant p) env).const_proj with - | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection.") - (* Mutual Inductives *) let scrape_mind env kn= try @@ -191,7 +183,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined.") + Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in @@ -201,10 +193,23 @@ let add_mind kn mib env = KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in let new_globals = { env.env_globals with - env_inductives = new_inds; - env_inductives_eq = new_inds_eq} in + env_inductives = new_inds; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } +let lookup_projection p env = + let mind,i = Projection.inductive p in + let mib = lookup_mind mind env in + match mib.mind_record with + | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection") + | PrimRecord infos -> + let _,labs,typs = infos.(i) in + let parg = Projection.arg p in + if not (Label.equal labs.(parg) (Projection.label p)) + then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection") + else if not (Int.equal mib.mind_nparams (Projection.npars p)) + then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection") + else typs.(parg) (* Modules *) |