Generation of inductive principle for Type[0].

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.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 3a108acccc5c079ee7e2426edf0d3490f60628c1..f1aea02da0a71efd0bece6fa26c0df667a5cc685 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -957,7 +957,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         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 ->
@@ -965,7 +967,19 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                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")

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 08c8b0f5609fddf3d17ef48a38c19d0571ad2914..2a02b7d1726a7fa34375239f13be55671a5d8b3c 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -34,6 +34,13 @@ let rec my_split_prods ~subst context n te =
    | (_, _) -> 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],_) ->
@@ -52,7 +59,7 @@ let mk_elims (uri,_,_,_,obj) =
        (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
@@ -62,7 +69,7 @@ let mk_elims (uri,_,_,_,obj) =
       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
@@ -96,7 +103,7 @@ let mk_elims (uri,_,_,_,obj) =
                           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
@@ -143,6 +150,6 @@ let mk_elims (uri,_,_,_,obj) =
        (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)]
   | _ -> []
 ;;

diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index 8366f1702286912ea50363a082ed249c2c17f452..677454550f8aa1c38008d884872d3371c8bfedef 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -11,4 +11,5 @@
 
 (* $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