-let inductive_of_record (suri,params,ty,fields) =
- let uri = UriManager.uri_of_string suri in
- let name = UriManager.name_of_uri uri in
- let leftno = List.length params in
- let constructor_ty =
- List.fold_right (
- fun (name, ty) acc ->
- Cic.Prod (Cic.Name name, ty, acc))
- (params @ fields) (CicSubstitution.lift (List.length fields)
- (rec_ty uri leftno))
- in
- let ty =
- List.fold_right (
- fun (name,ty) t ->
- Cic.Prod(Cic.Name name,ty, t)
- ) params ty
- in
- let types = [name,true,ty,["mk_" ^ name,constructor_ty]] in
- let obj =
- Cic.InductiveDefinition (types, [],leftno,[`Class `Record])
- in
- let ugraph =
- CicTypeChecker.typecheck_mutual_inductive_defs uri
- (types, [], leftno) CicUniv.empty_ugraph
- in
- types, leftno, obj, ugraph
-
-let projections_of (suri,params,ty,fields) =
- let uri = UriManager.uri_of_string suri in
- let buri = UriManager.buri_of_uri uri in
- let name = UriManager.name_of_uri uri in
- let leftno = List.length params in
- let ty =
- List.fold_right (
- fun (name,ty) t ->
- Cic.Prod(Cic.Name name,ty, t)
- ) params ty
- in
- let mk_lambdas l start =
- List.fold_right (fun (name,ty) acc ->
- Cic.Lambda (Cic.Name name,ty,acc)) l start
- in
- let recty = rec_ty uri leftno in
- let _,projections,_ =
- let qualify name = buri ^ "/" ^ name ^ ".con" in
- let mk_oty toapp typ =
- Cic.Lambda (Cic.Name "w", recty, (
- let l,_ =
- List.fold_right (fun (name,_) (acc,i) ->
- let u = UriManager.uri_of_string (qualify name) in
- (Cic.Appl ([Cic.Const (u,[])] @
- CicUtil.mk_rels leftno i @ [Cic.Rel i]))
- :: acc, i+1
- ) toapp ([],1)
- in
- List.fold_left (
- fun res t -> CicSubstitution.subst t res
- ) (CicSubstitution.lift_from (List.length toapp + 1) 1 typ) l))
- in
- let toapp = try List.tl (List.rev fields) with Failure _-> [] in
- List.fold_right (
- fun (name, typ) (i, acc, toapp) ->
- let start =
- Cic.Lambda(Cic.Name "x", recty,
- Cic.MutCase (uri,0,CicSubstitution.lift 1 (mk_oty toapp typ),
- Cic.Rel 1,
- [CicSubstitution.lift 1
- (mk_lambdas fields (Cic.Rel i))]))
- in
- i+1, ((qualify name, name, mk_lambdas params start) :: acc) ,
- if toapp <> [] then List.tl toapp else []
- )
- fields (1, [], toapp)
- in
- projections
-
-
+let generate_one_proj uri params paramsno fields t i =
+ let mk_lambdas l start =
+ List.fold_right (fun (name,ty) acc ->
+ Cic.Lambda (Cic.Name name,ty,acc)) l start in
+ let recty = rec_ty uri paramsno in
+ let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in
+ Some
+ (mk_lambdas params
+ (Cic.Lambda (Cic.Name "w", recty,
+ Cic.MutCase (uri,0,outtype, Cic.Rel 1,
+ [mk_lambdas fields (Cic.Rel i)]))))