diff options
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r-- | toplevel/classes.ml | 87 |
1 files changed, 44 insertions, 43 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index c7ba7fa44..f63ae3ecb 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -201,47 +201,47 @@ let new_class id par ar sup props = let params = ctx_params and fields = ctx_props in List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); match fields with - [(Name proj_name, _, field)] -> - let class_body = it_mkLambda_or_LetIn field params in - let class_type = - match ar with - Some _ -> Some (it_mkProd_or_LetIn arity params) - | None -> None - in - let class_entry = - { const_entry_body = class_body; - const_entry_type = class_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in - let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in - let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in - let proj_entry = - { const_entry_body = proj_body; - const_entry_type = Some proj_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); - set_rigid cst; - cref, [proj_name, proj_cst] - | _ -> - let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in - let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let kn = Record.declare_structure (snd id) idb arity_imps - params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) - in - IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - (List.rev fields) (Recordops.lookup_projections (kn,0))) + | [(Name proj_name, _, field)] -> + let class_body = it_mkLambda_or_LetIn field params in + let class_type = + match ar with + | Some _ -> Some (it_mkProd_or_LetIn arity params) + | None -> None + in + let class_entry = + { const_entry_body = class_body; + const_entry_type = class_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in + let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in + let proj_entry = + { const_entry_body = proj_body; + const_entry_type = Some proj_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); + set_rigid cst; + cref, [proj_name, Some proj_cst] + | _ -> + let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in + let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in + let kn = Record.declare_structure (snd id) idb arity_imps + params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) + in + IndRef (kn,0), (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) + (List.rev fields) (Recordops.lookup_projections (kn,0))) in let ctx_context = List.map (fun ((na, b, t) as d) -> @@ -256,7 +256,8 @@ let new_class id par ar sup props = cl_props = ctx_props; cl_projs = projs } in - List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p)) + List.iter2 (fun p sub -> + if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) k.cl_projs subs; add_class k @@ -429,7 +430,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau try let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) ([], props) k.cl_props |