diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/class.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 21 | ||||
-rw-r--r-- | toplevel/record.ml | 91 |
3 files changed, 49 insertions, 65 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 09013d173..d3acbe66b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -263,7 +263,7 @@ let build_id_coercion idf_opt source = let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry { const_entry_body = mkCast (val_f, typ_f); - const_entry_type = None; + const_entry_type = Some typ_f; const_entry_opaque = false } in let (_,kn) = declare_constant idf (constr_entry,NeverDischarge) in ConstRef kn diff --git a/toplevel/command.ml b/toplevel/command.ml index a6e42a73a..a670c2bda 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -354,14 +354,11 @@ let build_recursive lnameargsardef = let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = let ce = - { const_entry_body = - mkFix ((nvrec,i), - (Array.map (fun id -> Name id) namerec, - arrec, - recvec)); - const_entry_type = None; + { const_entry_body = mkFix ((nvrec,i),recdecls); + const_entry_type = Some arrec.(i); const_entry_opaque = false } in let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in (ConstRef kn) @@ -418,13 +415,11 @@ let build_corecursive lnameardef = let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = let ce = - { const_entry_body = - mkCoFix (i, (Array.map (fun id -> Name id) namerec, - arrec, - recvec)); - const_entry_type = None; + { const_entry_body = mkCoFix (i, recdecls); + const_entry_type = Some (arrec.(i)); const_entry_opaque = false } in let _,kn = declare_constant fi (DefinitionEntry ce,n) in @@ -462,8 +457,10 @@ let build_scheme lnamedepindsort = let n = NeverDischarge in let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = + let decltype = Retyping.get_type_of env0 Evd.empty decl in + let decltype = Evarutil.refresh_universes decltype in let ce = { const_entry_body = decl; - const_entry_type = None; + const_entry_type = Some decltype; const_entry_opaque = false } in let _,kn = declare_constant fi (DefinitionEntry ce,n) in ConstRef kn :: lrecref diff --git a/toplevel/record.ml b/toplevel/record.ml index ab3482c91..9edb4e1d5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -108,16 +108,14 @@ type field_status = | NoProjection of name | Projection of constr -type projection_status = - | NotDefinable of identifier list - | Definable of constr +exception NotDefinable of record_error (* This replaces previous projection bodies in current projection *) (* Undefined projs are collected and, at least one undefined proj occurs *) (* in the body of current projection then the latter can not be defined *) (* [c] is defined in ctxt [[params;fields]] and [l] is an instance of *) (* [[fields]] defined in ctxt [[params;x:ind]] *) -let subst_projection l c = +let subst_projection fid l c = let lv = List.length l in let bad_projs = ref [] in let rec substrec depth c = match kind_of_term c with @@ -136,10 +134,9 @@ let subst_projection l c = in let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) let c'' = substrec 0 c' in - if !bad_projs <> [] then - NotDefinable (List.rev !bad_projs) - else - Definable c'' + if !bad_projs <> [] then + raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); + c'' (* We build projections *) let declare_projections indsp coers fields = @@ -158,54 +155,44 @@ let declare_projections indsp coers fields = | Anonymous -> (nfi-1, None::sp_projs,NoProjection fi::subst) | Name fid -> - let abstract, c = match optci with - | Some ci -> false, ci - | None -> true, ti in - match subst_projection subst c with - | NotDefinable bad_projs -> - warning_or_error coe indsp (MissingProj (fid,bad_projs)); - (nfi-1, None::sp_projs,NoProjection fi::subst) - | Definable c' -> - (* [c'] is defined in context [params;x:rp] *) - let body = - if abstract then - (* [c''] is defined in context [params;x:rp;x:rp] *) - let c'' = liftn 1 2 c' in - let p = mkLambda (x, lift 1 rp, c'') in + try + let ccl = subst_projection fid subst ti in + let body = match optci with + | Some ci -> subst_projection fid subst ci + | None -> + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in let ci = Inductiveops.make_case_info env indsp (Some PrintLet) [| RegularPat |] in - mkCase (ci, p, mkRel 1, [|branch|]) - else c' in - let proj = - it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in - let name = - try - let cie = { - const_entry_body = proj; - const_entry_type = None; - const_entry_opaque = false } in - let sp = + mkCase (ci, p, mkRel 1, [|branch|]) in + let proj = + it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in + let projtyp = + it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in + let (sp,kn) = + try + let cie = { + const_entry_body = proj; + const_entry_type = Some projtyp; + const_entry_opaque = false } in declare_constant fid (DefinitionEntry cie,NeverDischarge) - in Some sp - with Type_errors.TypeError (ctx,te) -> begin - warning_or_error coe indsp (BadTypedProj (fid,ctx,te)); - None - end in - match name with - | None -> - (nfi-1, None::sp_projs, NoProjection fi::subst) - | Some (sp,kn) -> - let refi = ConstRef kn in - let constr_fi = mkConst kn in - if coe then begin - let cl = Class.class_of_ref (IndRef indsp) in - Class.try_add_new_coercion_with_source - refi NeverDischarge cl - end; - let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - let constr_fip = applist (constr_fi,proj_args) in - (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst)) + with Type_errors.TypeError (ctx,te) -> + raise (NotDefinable (BadTypedProj (fid,ctx,te))) in + let refi = ConstRef kn in + let constr_fi = mkConst kn in + if coe then begin + let cl = Class.class_of_ref (IndRef indsp) in + Class.try_add_new_coercion_with_source refi NeverDischarge cl + end; + let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in + let constr_fip = applist (constr_fi,proj_args) in + (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst) + with NotDefinable why -> + warning_or_error coe indsp why; + (nfi-1, None::sp_projs,NoProjection fi::subst)) (List.length fields,[],[]) coers (List.rev fields) in sp_projs |