From 8f8d3ad5a02faed2ddcaa22f49a9099175445ef4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 16:18:12 +0000 Subject: [PATCH] The `Record class now records also the name of the fields (used to generate the projections) --- helm/matita/matitaEngine.ml | 19 +++++--- helm/ocaml/cic/cic.ml | 3 +- helm/ocaml/cic/cicPushParser.ml | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +++- helm/ocaml/cic_proof_checking/cicRecord.ml | 46 +++++++++---------- helm/ocaml/cic_proof_checking/cicRecord.mli | 3 +- helm/ocaml/cic_transformations/cic2Xml.ml | 2 +- 7 files changed, 47 insertions(+), 36 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index d9297bce5..e5bb82786 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -235,8 +235,8 @@ let generate_elimination_principles uri status = List.fold_left (fun status sort -> elim sort status) status [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] -let generate_projections uri status = - let projections = CicRecord.projections_of uri in +let generate_projections uri fields status = + let projections = CicRecord.projections_of uri fields in List.fold_left (fun status (uri, name, bo) -> try @@ -328,12 +328,17 @@ let eval_command status cmd = let status = MatitaSync.add_obj uri obj status in match obj with Cic.Constant _ -> status - | Cic.InductiveDefinition (_,_,_,attrs) - when List.mem (`Class `Record) attrs -> + | Cic.InductiveDefinition (_,_,_,attrs) -> let status = generate_elimination_principles uri status in - generate_projections uri status - | Cic.InductiveDefinition (_,_,_,_) -> - generate_elimination_principles uri status + let rec get_record_attrs = + function + [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + None -> status (* not a record *) + | Some fields -> generate_projections uri fields status) | Cic.CurrentProof _ | Cic.Variable _ -> assert false diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 23bb7661b..ba51157ff 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -57,7 +57,8 @@ type object_class = [ `Coercion | `Elim of sort (** elimination principle; if sort is Type, the universe is * not relevant *) - | `Record (** inductive type that encodes a record *) + | `Record of string list (** inductive type that encodes a record; + the arguments are the record fields *) | `Projection (** record projection *) ] diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml index f9f14df10..3051fb81f 100644 --- a/helm/ocaml/cic/cicPushParser.ml +++ b/helm/ocaml/cic/cicPushParser.ml @@ -606,7 +606,7 @@ let end_element ctxt tag = | ("class", "coercion") :: tl -> mk_obj_attributes (`Class `Coercion :: acc) tl | ("class", "record") :: tl -> - mk_obj_attributes (`Class `Record :: acc) tl + mk_obj_attributes (`Class (`Record []) :: acc) tl | ("class", "projection") :: tl -> mk_obj_attributes (`Class `Projection :: acc) tl | ("class", "elimProp") :: tl -> diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 4a12727c7..2f9bb97a5 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -400,14 +400,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = (*here the explicit_named_substituion is assumed to be of length 0 *) let mutind = Cic.MutInd (uri,0,[]) in if params = [] then mutind - else Cic.Appl (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in + else + Cic.Appl + (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in let con = List.fold_left (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) concl fields' in let con' = add_params con in let tyl = [name,true,ty',["mk_" ^ name,con']] in - Cic.InductiveDefinition (tyl,[],List.length params,[`Class `Record]) + let field_names = List.map fst fields in + Cic.InductiveDefinition + (tyl,[],List.length params,[`Class (`Record field_names)]) | TacticAst.Theorem (_,name,ty,bo) -> let ty' = interpretate_term [] env None false ty in match bo with diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml index d8dd2dc47..a251bad87 100644 --- a/helm/ocaml/cic_proof_checking/cicRecord.ml +++ b/helm/ocaml/cic_proof_checking/cicRecord.ml @@ -40,7 +40,7 @@ let generate_one_proj uri params paramsno fields t i = Cic.MutCase (uri,0,outtype, Cic.Rel 1, [mk_lambdas fields (Cic.Rel i)])))) -let projections_of uri = +let projections_of uri field_names = let buri = UriManager.buri_of_uri uri in let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in match obj with @@ -60,32 +60,32 @@ let projections_of uri = let fields = let rec aux = function - Cic.MutInd _ - | Cic.Appl _ -> [] - | Cic.Prod (Cic.Name name,s,t) -> (name,s)::aux t - | _ -> assert false + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl) + | _,_ -> assert false in - aux (CicSubstitution.lift 1 ty) + aux ((CicSubstitution.lift 1 ty),field_names) in let rec aux i = function - Cic.MutInd _ - | Cic.Appl _ -> [] - | Cic.Prod (Cic.Name name,s,t) -> + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> (match generate_one_proj uri leftparams paramsno fields s i with - Some p -> - let puri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - (puri,name,p) :: - aux (i - 1) - (CicSubstitution.subst - (Cic.Appl - (Cic.Const (puri,[]) :: - CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) - ) t) - | None -> assert false) - | _ -> assert false + Some p -> + let puri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + (puri,name,p) :: + aux (i - 1) + (CicSubstitution.subst + (Cic.Appl + (Cic.Const (puri,[]) :: + CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) + ) t, tl) + | None -> assert false) + | _,_ -> assert false in - aux (List.length fields) (CicSubstitution.lift 2 ty) + aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) | _ -> assert false diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli index 04ee188b5..b966f317c 100644 --- a/helm/ocaml/cic_proof_checking/cicRecord.mli +++ b/helm/ocaml/cic_proof_checking/cicRecord.mli @@ -24,4 +24,5 @@ *) (** projections_of [uri] returns uri * name * term *) -val projections_of: UriManager.uri -> (UriManager.uri * string * Cic.term) list +val projections_of: + UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 1facd4fd9..8bf8d5f3b 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -266,7 +266,7 @@ let xml_of_attrs attributes = | `Elim Cic.CProp -> "elimCProp" | `Elim Cic.Set -> "elimSet" | `Elim (Cic.Type _) -> "elimType" - | `Record -> "record" + | `Record _ -> "record" | `Projection -> "projection" in let xml_attr_of = function -- 2.39.2