diff options
Diffstat (limited to 'kernel/term_typing.ml')
-rw-r--r-- | kernel/term_typing.ml | 302 |
1 files changed, 251 insertions, 51 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a316b449..a566028d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff +let mk_pure_proof c = (c, Univ.ContextSet.empty), [] -let handle_side_effects env body side_eff = - let handle_sideff t se = +let equal_eff e1 e2 = + let open Entries in + match e1, e2 with + | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> + Names.Constant.equal c1 c2 + | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> + CList.for_all2eq + (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) + cl1 cl2 + | _ -> false + +let rec uniq_seff = function + | [] -> [] + | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) +(* The list of side effects is in reverse order (most recent first). + * To keep the "topological" order between effects we have to uniq-ize from + * the tail *) +let uniq_seff l = List.rev (uniq_seff (List.rev l)) + +let inline_side_effects env body ctx side_eff = + let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = let cbl = match se with | SEsubproof (c,cb,b) -> [c,cb,b] | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in @@ -65,8 +84,8 @@ let handle_side_effects env body side_eff = let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> Vars.subst_instance_constr u' b - | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in - let fix_body (c,cb,b) t = + | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in + let fix_body (c,cb,b) (t,ctx) = match cb.const_body, b with | Def b, _ -> let b = Mod_subst.force_constr b in @@ -74,37 +93,86 @@ let handle_side_effects env body side_eff = if not poly then let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in - mkLetIn (cname c, b, b_ty, t) + mkLetIn (cname c, b, b_ty, t), + Univ.ContextSet.union ctx + (Univ.ContextSet.of_context cb.const_universes) else let univs = cb.const_universes in - sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) + sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx | OpaqueDef _, `Opaque (b,_) -> let poly = cb.const_polymorphic in if not poly then let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in - mkApp (mkLambda (cname c, b_ty, t), [|b|]) + mkApp (mkLambda (cname c, b_ty, t), [|b|]), + Univ.ContextSet.union ctx + (Univ.ContextSet.of_context cb.const_universes) else let univs = cb.const_universes in - sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) + sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx | _ -> assert false in - List.fold_right fix_body cbl t + let t, ctx = List.fold_right fix_body cbl (t,ctx) in + t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - Declareops.fold_side_effects handle_sideff body - (Declareops.uniquize_side_effects side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + +(* Given the list of signatures of side effects, checks if they match. + * I.e. if they are ordered descendants of the current revstruct *) +let check_signatures curmb sl = + let is_direct_ancestor (sl, curmb) (mb, how_many) = + match curmb with + | None -> None, None + | Some curmb -> + try + let mb = Ephemeron.get mb in + match sl with + | None -> sl, None + | Some n -> + if List.length mb >= how_many && CList.skipn how_many mb == curmb + then Some (n + how_many), Some mb + else None, None + with Ephemeron.InvalidKey -> None, None in + let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in + sl + +let skip_trusted_seff sl b e = + let rec aux sl b e acc = + match sl, kind_of_term b with + | (None|Some 0), _ -> b, e, acc + | Some sl, LetIn (n,c,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc) + | Some sl, App(hd,arg) -> + begin match kind_of_term hd with + | Lambda (n,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc) + | _ -> assert false + end + | _ -> assert false + in + aux sl b e [] + +let rec unzip ctx j = + match ctx with + | [] -> j + | `Let (n,c,ty) :: ctx -> + unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) } + | `Cut (n,ty,arg) :: ctx -> + unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - -let infer_declaration env kn dcl = + +let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> - let env = push_context uctx env in + let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in @@ -115,34 +183,41 @@ let infer_declaration env kn dcl = | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> - let env = push_context c.const_entry_universes env in + let env = push_context ~strict:true c.const_entry_universes env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> - let body = handle_side_effects env body side_eff in - let env' = push_context_set ctx env in - let j = infer env' body in + Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) -> + let body, uctx, signatures = + inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures trust signatures in + let env' = push_context_set uctx env in + let j = + let body,env',ectx = skip_trusted_seff valid_signatures body env' in + let j = infer env' body in + unzip ectx j in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst (`SomeWJ (typ,tyj)) in feedback_completion_typecheck feedback_id; - j.uj_val, ctx) in + j.uj_val, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> - let env = push_context c.const_entry_universes env in let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - assert(Univ.ContextSet.is_empty ctx); - let body = handle_side_effects env body side_eff in + let univsctx = Univ.ContextSet.of_context c.const_entry_universes in + let body, ctx, _ = inline_side_effects env body + (Univ.ContextSet.union univsctx ctx) side_eff in + let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in - let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in + let usubst, univs = + Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in @@ -176,14 +251,17 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty -let record_aux env s1 s2 = +let record_aux env s_ty s_bo suggested_expr = + let in_ty = keep_hyps env s_ty in let v = String.concat " " - (List.map (fun (id, _,_) -> Id.to_string id) - (keep_hyps env (Id.Set.union s1 s2))) in - Aux_file.record_in_aux "context_used" v + (CList.map_filter (fun (id, _,_) -> + if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None + else Some (Id.to_string id)) + (keep_hyps env s_bo)) in + Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) -let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) +let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = @@ -198,6 +276,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in + let sort evn l = + List.filter (fun (id,_,_) -> + List.exists (fun (id',_,_) -> Names.Id.equal id id') l) + (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map pi1 (named_context env) in @@ -215,19 +297,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (Opaqueproof.force_proof (opaque_tables env) lc) in (* we force so that cst are added to the env immediately after *) ignore(Opaqueproof.force_constraints (opaque_tables env) lc); - !suggest_proof_using kn env vars ids_typ context_ids; + let expr = + !suggest_proof_using (Constant.to_string kn) + env vars ids_typ context_ids in if !Flags.compilation_mode = Flags.BuildVo then - record_aux env ids_typ vars; + record_aux env ids_typ vars expr; vars in keep_hyps env (Idset.union ids_typ ids_def), def | None -> if !Flags.compilation_mode = Flags.BuildVo then - record_aux env Id.Set.empty Id.Set.empty; + record_aux env Id.Set.empty Id.Set.empty ""; [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) - declared, + sort env declared, match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> @@ -243,16 +327,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in let tps = - (* FIXME: incompleteness of the bytecode vm: we compile polymorphic - constants like opaque definitions. *) - if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant) - else - let res = - match proj with - | None -> compile_constant_body env def - | Some pb -> - compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)) - in Option.map Cemitcodes.from_val res + let res = + let comp_univs = if poly then Some univs else None in + match proj with + | None -> compile_constant_body env comp_univs def + | Some pb -> + (* The compilation of primitive projections is a bit tricky, because + they refer to themselves (the body of p looks like fun c => + Proj(p,c)). We break the cycle by building an ad-hoc compilation + environment. A cleaner solution would be that kernel projections are + simply Proj(i,c) with i an int and c a constr, but we would have to + get rid of the compatibility layer. *) + let cb = + { const_hyps = hyps; + const_body = def; + const_type = typ; + const_proj = proj; + const_body_code = None; + const_polymorphic = poly; + const_universes = univs; + const_inline_code = inline_code } + in + let env = add_constant kn cb env in + compile_constant_body env comp_univs def + in Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; @@ -263,11 +361,95 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_universes = univs; const_inline_code = inline_code } - (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant mb env kn ce = + build_constant_declaration kn env + (infer_declaration ~trust:mb env (Some kn) ce) + +let constant_entry_of_side_effect cb u = + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, []); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = + (match cb.const_type with RegularArity t -> Some t | _ -> None); + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = cb.const_universes; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } +;; + +let turn_direct (kn,cb,u,r as orig) = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b,c) -> + let pt = Future.from_val (b,c) in + kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r + | _ -> orig +;; + +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects constant_entry * side_effect_role + +let export_side_effects mb env ce = + match ce with + | ParameterEntry _ | ProjectionEntry _ -> [], ce + | DefinitionEntry c -> + let { const_entry_body = body } = c in + let _, eff = Future.force body in + let ce = DefinitionEntry { c with + const_entry_body = Future.chain ~greedy:true ~pure:true body + (fun (b_ctx, _) -> b_ctx, []) } in + let not_exists (c,_,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = match se with + | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] + | SEscheme (cl,k) -> + List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in + let cbl = List.filter not_exists cbl in + if cbl = [] then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let trusted = check_signatures mb signatures in + let push_seff env = function + | kn, cb, `Nothing, _ -> + Environ.add_constant kn cb env + | kn, cb, `Opaque(_, ctx), _ -> + let env = Environ.add_constant kn cb env in + Environ.push_context_set + ~strict:(not cb.const_polymorphic) ctx env in + let rec translate_seff sl seff acc env = + match sl, seff with + | _, [] -> List.rev acc, ce + | (None | Some 0), cbs :: rest -> + let env, cbs = + List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + let ce = constant_entry_of_side_effect ocb u in + let cb = translate_constant mb env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (env,[]) cbs in + translate_seff sl rest (cbs @ acc) env + | Some sl, cbs :: rest -> + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map (fun (kn,cb,u,r) -> + kn, cb, constant_entry_of_side_effect cb u, r) cbs in + translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env +;; let translate_local_assum env t = let j = infer env t in @@ -277,18 +459,36 @@ let translate_local_assum env t = let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in + if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin + match def with + | Undef _ -> () + | Def _ -> () + | OpaqueDef lc -> + let context_ids = List.map pi1 (named_context env) in + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env + (Opaqueproof.force_proof (opaque_tables env) lc) in + let expr = + !suggest_proof_using (Id.to_string id) + env ids_def ids_typ context_ids in + record_aux env ids_typ ids_def expr + end; def, typ, univs (* Insertion of inductive types. *) let translate_mind env kn mie = Indtypes.check_inductive env kn mie -let handle_entry_side_effects env ce = { ce with +let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> - (handle_side_effects env body side_eff, ctx), Declareops.no_seff); + let body, ctx',_ = inline_side_effects env body ctx side_eff in + (body, ctx'), []); } + +let inline_side_effects env body side_eff = + pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff) |