The way the code has been branched is very messy: we generate an AST and
from it a new command NObj that is recursively processed in GrafiteEngine.
However, disambiguation needs the alias. Thus the aliases for the inductive
principle are immediately generated and added while the others are delayed.
let obj = uri,height,[],[],obj_kind in
let status = NCicLibrary.add_obj status obj in
prerr_endline (NCicPp.ppobj obj);
let obj = uri,height,[],[],obj_kind in
let status = NCicLibrary.add_obj status obj in
prerr_endline (NCicPp.ppobj obj);
- let objs = NCicElim.mk_elims obj in
+ let boxml = NCicElim.mk_elims obj in
+(*
+ let objs = [] in
let timestamp,uris_rev =
List.fold_left
(fun (status,uris_rev) (uri,_,_,_,_) as obj ->
let timestamp,uris_rev =
List.fold_left
(fun (status,uris_rev) (uri,_,_,_,_) as obj ->
status,uri::uris_rev
) (status,[]) objs in
let uris = uri::List.rev uris_rev in
status,uri::uris_rev
) (status,[]) objs in
let uris = uri::List.rev uris_rev in
- status#set_ng_mode `CommandMode,`New uris
+*)
+ let status = status#set_ng_mode `CommandMode in
+let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+ List.fold_left
+ (fun (status,uris) boxml ->
+ let status,nuris =
+ eval_ncommand opts status
+ ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+ in
+ match uris,nuris with
+ `New uris, `New nuris -> status,`New (nuris@uris)
+ | _ -> assert false
+ ) (status,`New [] (* uris *)) boxml
| GrafiteAst.NCopy (log,tgt,src_uri, map) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
| GrafiteAst.NCopy (log,tgt,src_uri, map) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
| (_, _) -> raise (Failure "my_split_prods")
;;
| (_, _) -> raise (Failure "my_split_prods")
;;
+let mk_appl =
+ function
+ [] -> assert false
+ | [x] -> x
+ | l -> CicNotationPt.Appl l
+;;
+
let mk_elims (uri,_,_,_,obj) =
match obj with
NCic.Inductive (true,leftno,[it],_) ->
let mk_elims (uri,_,_,_,obj) =
match obj with
NCic.Inductive (true,leftno,[it],_) ->
(fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
(CicNotationPt.Binder
(`Forall,
(fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
(CicNotationPt.Binder
(`Forall,
- (rec_arg,Some (CicNotationPt.Appl (mk_id ind_name :: params @ args))),
+ (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))),
CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in
let args = args @ [rec_arg] in
let k_names = List.map (function _,name,_ -> name_of_k name) cl in
CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in
let args = args @ [rec_arg] in
let k_names = List.map (function _,name,_ -> name_of_k name) cl in
List.map (function name -> name, None) k_names @
List.map (function name -> name, None) args in
let recno = List.length final_params in
List.map (function name -> name, None) k_names @
List.map (function name -> name, None) args in
let recno = List.length final_params in
- let cty = CicNotationPt.Appl (p_name :: args) in
+ let cty = mk_appl (p_name :: args) in
let ty = Some cty in
let branches =
List.map
let ty = Some cty in
let branches =
List.map
k_names @
List.map (fun _ -> CicNotationPt.Implicit)
(List.tl args) @
k_names @
List.map (fun _ -> CicNotationPt.Implicit)
(List.tl args) @
- [CicNotationPt.Appl (name::abs)])))
+ [mk_appl (name::abs)])))
| _ -> mk_id name,None
) cargs in
let cargs,recursive_args = List.split cargs_and_recursive_args in
| _ -> mk_id name,None
) cargs in
let cargs,recursive_args = List.split cargs_and_recursive_args in
(BoxPp.render_to_string ~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false) 80
(CicNotationPres.mpres_of_box boxml)));
(BoxPp.render_to_string ~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false) 80
(CicNotationPres.mpres_of_box boxml)));
+ [CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)]
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val mk_elims: NCic.obj -> NCic.obj list
+(* val mk_elims: NCic.obj -> NCic.obj list *)
+val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list