Matitaweb:

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index 630d6a6e399cdc0c631cf68ae5b3a513743ebc19..02dfb00127adddb88455891d20ff78e87f82715e 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -34,6 +34,8 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let prerr_endline _ = () 
+
 let basic_eval_unification_hint (t,n) status =
  NCicUnifHint.add_user_provided_hint status t n
 ;;
@@ -134,12 +136,13 @@ let eval_alias status data=
 let basic_eval_input_notation (l1,l2) status =
   GrafiteParser.extend status l1 
    (fun env loc ->
-     let rec get_disamb = function
+     (* let rec get_disamb = function
      | [] -> Stdpp.dummy_loc,None,None
-     | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
+     | (_,(csym,NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
      | _::tl -> get_disamb tl
-     in
-     let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
+     in *)
+     let l2' = 
+       TermContentPres.instantiate_level2 status env (*(get_disamb env)*) l2 in
      prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
      NotationPt.AttributedTerm (`Loc loc,l2')) 
 ;;
@@ -639,6 +642,65 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                     (NCicEnvironment.get_universes status)))) status itl
               | _ -> status
            in
+           let status = match nobj with
+               NCic.Inductive (is_ind,leftno,itl,_) ->
+                 (* first leibniz *)
+                 let status' = List.fold_left
+                   (fun status it ->
+                      let _,ind_name,ty,cl = it in
+                      let status = status#set_ng_mode `ProofMode in
+                      try
+                       prerr_endline ("creazione discriminatore per " ^ ind_name);
+                       (let status,invobj =
+                         NDestructTac.mk_discriminator ~use_jmeq:false
+                          (ind_name ^ "_discr")
+                          it leftno status status#baseuri in
+                       let _,_,menv,_,_ = invobj in
+                        (match menv with
+                             [] -> eval_ncommand ~include_paths opts status
+                                    ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
+                           | _ -> status))
+                       (* XXX *)
+                      with 
+                      | NDestructTac.ConstructorTooBig k -> 
+                          prerr_endline (Printf.sprintf 
+                           "unable to generate leibniz discrimination principle (constructor %s too big)"
+                           k);
+                          HLog.warn (Printf.sprintf 
+                           "unable to generate leibniz discrimination principle (constructor %s too big)"
+                           k);
+                           let status = status#set_ng_mode `CommandMode in status
+                      | _ -> 
+                          prerr_endline "error in generating discrimination principle";
+                          (*HLog.warn "error in generating discrimination principle"; *)
+                                let status = status#set_ng_mode `CommandMode in
+                                status)
+                  status itl
+                in
+                (* then JMeq *)
+                List.fold_left
+                   (fun status it ->
+                      let _,ind_name,ty,cl = it in
+                      let status = status#set_ng_mode `ProofMode in
+                      try
+                       prerr_endline ("creazione discriminatore per " ^ ind_name);
+                       (let status,invobj =
+                         NDestructTac.mk_discriminator ~use_jmeq:true
+                          (ind_name ^ "_jmdiscr")
+                          it leftno status status#baseuri in
+                       let _,_,menv,_,_ = invobj in
+                        (match menv with
+                             [] -> eval_ncommand ~include_paths opts status
+                                    ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
+                           | _ -> status))
+                       (* XXX *)
+                      with _ -> (*HLog.warn "error in generating discrimination principle"; *)
+                          prerr_endline "error in generating discrimination principle";
+                                let status = status#set_ng_mode `CommandMode in
+                                status)
+                  status' itl
+              | _ -> status
+           in
            let coercions =
             match obj with
               _,_,_,_,NCic.Inductive
@@ -832,7 +894,8 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
-       raise (GrafiteTypes.Command_error "Not in proof mode")
+       (prerr_endline ("not in proof mode 2: " ^ GrafiteAstPp.pp_executable status ~map_unicode_to_tex:false ex);
+       raise (GrafiteTypes.Command_error "Not in proof mode"))
       else
        let status =
         List.fold_left