From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 08:58:18 +0000 (+0000)
Subject: Generation of inductive principle for Type[0].
X-Git-Tag: make_still_working~3674
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c515405206bfeb9f99d3e175b7f1e390ba299f28;p=helm.git

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 3a108accc..f1aea02da 100644
--- 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 08c8b0f56..2a02b7d17 100644
--- 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 8366f1702..677454550 100644
--- 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