2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
18 "x_" ^ string_of_int !i
22 let id = if id = "_" then fresh_name () else id in
23 CicNotationPt.Ident (id,None)
26 (*CSC: cut&paste from nCicReduction.split_prods, but does not check that
27 the return type is a sort *)
28 let rec my_split_prods ~subst context n te =
29 match (n, NCicReduction.whd ~subst context te) with
30 | (0, _) -> context,te
31 | (n, NCic.Prod (name,so,ta)) ->
32 my_split_prods ~subst ((name,(NCic.Decl so))::context) (n - 1) ta
33 | (n, _) when n <= 0 -> context,te
34 | (_, _) -> raise (Failure "my_split_prods")
41 | l -> CicNotationPt.Appl l
44 let mk_elim uri leftno [it] (outsort,suffix) =
45 let _,ind_name,ty,cl = it in
46 let srec_name = ind_name ^ "_" ^ suffix in
47 let rec_name = mk_id srec_name in
48 let name_of_k id = mk_id ("H_" ^ id) in
49 let p_name = mk_id "Q_" in
50 let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
51 let params = List.rev_map (function name,_ -> mk_id name) params in
52 let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
53 let args = List.rev_map (function name,_ -> mk_id name) args in
54 let rec_arg = mk_id (fresh_name ()) in
57 (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
60 (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))),
61 CicNotationPt.Sort outsort)) in
62 let args = args @ [rec_arg] in
63 let k_names = List.map (function _,name,_ -> name_of_k name) cl in
65 List.map (function name -> name, None) params @
67 List.map (function name -> name, None) k_names @
68 List.map (function name -> name, None) args in
69 let cty = mk_appl (p_name :: args) in
73 (function (_,name,ty) ->
74 let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
75 let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
76 let cargs_and_recursive_args =
79 _,NCic.Def _ -> assert false
80 | name,NCic.Decl ty ->
81 let context,ty = my_split_prods ~subst:[] [] (-1) ty in
84 | NCic.Appl (NCic.Const nref::_)
86 let NReference.Ref (uri',_) = nref in
89 let abs = List.rev_map (fun id,_ -> mk_id id) context in
90 let name = mk_id name in
94 CicNotationPt.Binder (`Lambda,(id,None),res))
101 List.map (fun _ -> CicNotationPt.Implicit)
103 [mk_appl (name::abs)])))
104 | _ -> mk_id name,None
106 let cargs,recursive_args = List.split cargs_and_recursive_args in
107 let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
108 CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
109 mk_appl (name_of_k name :: cargs @ recursive_args)
112 let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
113 let recno = List.length final_params in
114 let where = recno - 1 in
116 CicNotationPt.LetRec (`Inductive,
117 [final_params, (rec_name,ty), bo, where], rec_name)
121 (BoxPp.render_to_string
122 ~map_unicode_to_tex:false
123 (function x::_ -> x | _ -> assert false)
124 80 (CicNotationPres.render (fun _ -> None)
125 (TermContentPres.pp_ast res)));
126 prerr_endline "#####";
127 let cobj = ("xxx", [], None, `Joint {
128 Content.joint_id = "yyy";
129 joint_kind = `Recursive [recno];
132 Content.def_name = Some srec_name;
138 (fun x t -> CicNotationPt.Binder(`Forall,x,t))
144 let ids_to_nrefs = Hashtbl.create 1 in
145 let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
147 (BoxPp.render_to_string ~map_unicode_to_tex:false
148 (function x::_ -> x | _ -> assert false) 80
149 (CicNotationPres.mpres_of_box boxml)));
151 CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
156 NCic.Prop -> `Prop,"ind"
158 let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
160 if String.sub u 0 4 = "Type" then
161 `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
162 else if String.sub u 0 5 = "CProp" then
163 `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
167 with Failure _ -> assert false)
170 let mk_elims (uri,_,_,_,obj) =
172 NCic.Inductive (true,leftno,itl,_) ->
173 List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s))
175 List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
179 (********************* Projections **********************)
185 | l -> CicNotationPt.Appl l
188 let rec count_prods = function NCic.Prod (_,_,t) -> 1 + count_prods t | _ -> 0;;
190 let rec nth_prod projs n ty =
192 NCic.Prod (_,s,_) when n=0 -> projs, s
193 | NCic.Prod (name,_,t) -> nth_prod (name::projs) (n-1) t
197 (* this code should be unified with NTermCicContent.nast_of_cic0,
198 but the two contexts have different types *)
201 NCic.Rel i -> List.nth rels (i - 1)
202 | NCic.Const _ as t ->
204 (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
205 | NCic.Sort s -> CicNotationPt.Sort (fst (ast_of_sort s))
207 | NCic.Implicit _ -> assert false
208 | NCic.Appl l -> CicNotationPt.Appl (List.map (pp rels) l)
209 | NCic.Prod (n,s,t) ->
211 CicNotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t)
212 | NCic.Lambda (n,s,t) ->
214 CicNotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t)
215 | NCic.LetIn (n,s,ty,t) ->
217 CicNotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t)
218 | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
219 let name = NUri.name_of_uri uri in
220 let case_indty = Some (name, None) in
221 let constructors, leftno =
222 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in
223 let _,_,_,cl = List.nth tys n in
226 let rec eat_branch n rels ty pat =
228 | NCic.Prod (name, s, t), _ when n > 0 ->
229 eat_branch (pred n) rels t pat
230 | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
231 let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in
232 (mk_id name, Some (pp rels s)) :: cv, rhs
233 | _, _ -> [], pp rels pat
238 (fun (_, name, ty) pat ->
239 let capture_variables,rhs = eat_branch leftno rels ty pat in
240 CicNotationPt.Pattern (name, None, capture_variables), rhs
241 ) constructors patterns
242 with Invalid_argument _ -> assert false
244 CicNotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns)
247 let mk_projection leftno tyname consname consty (projname,_,_) i =
248 let argsno = count_prods consty - leftno in
249 let rec aux names ty leftno =
252 let arg = mk_id "xxx" in
253 let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
254 let bvar = mk_id "yyy" in
255 let underscore = CicNotationPt.Ident ("_",None),None in
257 HExtlib.mk_list underscore i @ [bvar,None] @
258 HExtlib.mk_list underscore (argsno - i -1) in
259 let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in
260 let projs,outtype = nth_prod [] i ty in
263 (fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs
265 let outtype = pp rels outtype in
266 let outtype= CicNotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
268 (`Lambda, (arg,Some arg_ty),
269 CicNotationPt.Case (arg,None,Some outtype,[branch]))
270 | _,NCic.Prod (name,_,t) ->
271 let name = mk_id name in
273 (`Lambda, (name,None), aux (name::names) t (leftno - 1))
274 | _,_ -> assert false
276 let res = aux [] consty leftno in
278 (BoxPp.render_to_string
279 ~map_unicode_to_tex:false
280 (function x::_ -> x | _ -> assert false)
281 80 (CicNotationPres.render (fun _ -> None)
282 (TermContentPres.pp_ast res)));*)
283 CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
286 let mk_projections (_,_,_,_,obj) =
289 (true,leftno,[_,tyname,_,[_,consname,consty]],(_,`Record fields))
291 HExtlib.list_mapi (mk_projection leftno tyname consname consty) fields