1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
27 string * (string * Cic.term) list * Cic.term * (string * Cic.term) list
29 let rec_ty uri leftno =
30 let rec_ty = Cic.MutInd (uri,0,[]) in
31 if leftno = 0 then rec_ty else
32 Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0))
34 let inductive_of_record (suri,params,ty,fields) =
35 let uri = UriManager.uri_of_string suri in
36 let name = UriManager.name_of_uri uri in
37 let leftno = List.length params in
41 Cic.Prod (Cic.Name name, ty, acc))
42 (params @ fields) (CicSubstitution.lift (List.length fields)
48 Cic.Prod(Cic.Name name,ty, t)
51 let types = [name,true,ty,["mk_" ^ name,constructor_ty]] in
53 Cic.InductiveDefinition (types, [],leftno,[`Class `Record])
56 CicTypeChecker.typecheck_mutual_inductive_defs uri
57 (types, [], leftno) CicUniv.empty_ugraph
59 types, leftno, obj, ugraph
61 let projections_of (suri,params,ty,fields) =
62 let uri = UriManager.uri_of_string suri in
63 let buri = UriManager.buri_of_uri uri in
64 let name = UriManager.name_of_uri uri in
65 let leftno = List.length params in
69 Cic.Prod(Cic.Name name,ty, t)
72 let mk_lambdas l start =
73 List.fold_right (fun (name,ty) acc ->
74 Cic.Lambda (Cic.Name name,ty,acc)) l start
76 let recty = rec_ty uri leftno in
78 let qualify name = buri ^ "/" ^ name ^ ".con" in
79 let mk_oty toapp typ =
80 Cic.Lambda (Cic.Name "w", recty, (
82 List.fold_right (fun (name,_) (acc,i) ->
83 let u = UriManager.uri_of_string (qualify name) in
84 (Cic.Appl ([Cic.Const (u,[])] @
85 CicUtil.mk_rels leftno i @ [Cic.Rel i]))
90 fun res t -> CicSubstitution.subst t res
91 ) (CicSubstitution.lift_from (List.length toapp + 1) 1 typ) l))
93 let toapp = try List.tl (List.rev fields) with Failure _-> [] in
95 fun (name, typ) (i, acc, toapp) ->
97 Cic.Lambda(Cic.Name "x", recty,
98 Cic.MutCase (uri,0,CicSubstitution.lift 1 (mk_oty toapp typ),
100 [CicSubstitution.lift 1
101 (mk_lambdas fields (Cic.Rel i))]))
103 i+1, ((qualify name, name, mk_lambdas params start) :: acc) ,
104 if toapp <> [] then List.tl toapp else []
106 fields (1, [], toapp)