* http://helm.cs.unibo.it/
*)
-type record_spec =
- string * (string * Cic.term) list * Cic.term * (string * Cic.term) list
-
let rec_ty uri leftno =
let rec_ty = Cic.MutInd (uri,0,[]) in
if leftno = 0 then rec_ty else
Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0))
-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)]))))
-
+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
+ Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
+ assert (params = []); (* general case not implemented *)
+ let leftparams,ty =
+ let rec aux =
+ function
+ 0,ty -> [],ty
+ | n,Cic.Prod (Cic.Name name,s,t) ->
+ let leftparams,ty = aux (n - 1,t) in
+ (name,s)::leftparams,ty
+ | _,_ -> assert false
+ in
+ aux (paramsno,ty)
+ in
+ let fields =
+ let rec aux =
+ function
+ Cic.MutInd _, []
+ | Cic.Appl _, [] -> []
+ | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl)
+ | _,_ -> assert false
+ in
+ aux ((CicSubstitution.lift 1 ty),field_names)
+ in
+ let rec aux i =
+ function
+ 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, tl)
+ | None -> assert false)
+ | _,_ -> assert false
+ in
+ aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
+ | _ -> assert false