Matitaweb: large commit porting to the new Matita 0.95 syntax.

[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 2021114853c7368a86fc5512715d69b814837812..630d6a6e399cdc0c631cf68ae5b3a513743ebc19 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -493,7 +493,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, None) ->
+  | GrafiteAst.NCoercion (loc, name, compose, None) ->
      let status, t, ty, source, target =
        let o_t = NotationPt.Ident (name,`Ambiguous) in
        let metasenv,subst, status,t =
@@ -514,13 +514,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
          | _ -> assert false in aux ty in
        status, o_t, NotationPt.NCic ty, source, target in
      let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
+       target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
-  | GrafiteAst.NCoercion (loc, name, Some (t, ty, source, target)) ->
+  | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
+       target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -544,7 +546,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
               (match spec with
               | NReference.Def _ -> NReference.Def height
               | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-              | NReference.CoFix _ -> NReference.CoFix height
+              | NReference.CoFix i -> NReference.CoFix i
               | NReference.Ind _ | NReference.Con _
               | NReference.Decl as s -> s))
           | t -> NCicUtils.map status (fun _ () -> ()) () fix t
@@ -593,7 +595,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                try
                 let nstatus =
                  eval_ncommand ~include_paths opts status
-                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
                 in
                 if nstatus#ng_mode <> `CommandMode then
                   begin
@@ -611,9 +613,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              ) status boxml in             
            let _,_,_,_,nobj = obj in 
            let status = match nobj with
-               NCic.Inductive (is_ind,leftno,[it],_) ->
-                 let _,ind_name,ty,cl = it in
-                 List.fold_left 
+               NCic.Inductive (is_ind,leftno,itl,_) ->
+                 List.fold_left (fun status it ->      
+                 (let _,ind_name,ty,cl = it in
+                  List.fold_left 
                    (fun status outsort ->
                       let status = status#set_ng_mode `ProofMode in
                       try
@@ -633,7 +636,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                   status
                   (NCic.Prop::
                     List.map (fun s -> NCic.Type s)
-                    (NCicEnvironment.get_universes status))
+                    (NCicEnvironment.get_universes status)))) status itl
               | _ -> status
            in
            let coercions =
@@ -656,7 +659,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                  let status, nuris = 
                    NCicCoercDeclaration.
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                      status (name,t,cpos,arity) in
+                      
+                     status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
                   eval_alias status (mode,aliases)
                with GrafiteDisambiguate.Error _ -> 
@@ -700,7 +704,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in
        eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
-  | GrafiteAst.NObj (loc,obj) ->
+  | GrafiteAst.NObj (loc,obj,index) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
      else
@@ -715,26 +719,30 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let status = status#set_ng_mode `ProofMode in
       (match nmenv with
           [] ->
-           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,true))
+           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed
+           (Stdpp.dummy_loc,index))
         | _ -> status)
-  | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
+  | GrafiteAst.NDiscriminator (loc, indty) -> 
       if status#ng_mode <> `CommandMode then
         raise (GrafiteTypes.Command_error "Not in command mode")
       else
         let status = status#set_ng_mode `ProofMode in
         let metasenv,subst,status,indty =
-          GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
-        let indtyno, (_,_,tys,_,_) = match indty with
-            NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
-              indtyno, NCicEnvironment.get_checked_indtys r
+          GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in
+        let indtyno, (_,_,tys,_,_), leftno = match indty with
+            NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
+              indtyno, NCicEnvironment.get_checked_indtys status r, leftno
           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
-        let it = List.nth tys indtyno in
-        let status,obj =  NDestructTac.mk_discriminator it status in
+        let (_,ind_name,_,_ as it) = List.nth tys indtyno in
+        let status,obj =
+          NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr")
+           it leftno status status#baseuri in
         let _,_,menv,_,_ = obj in
           (match menv with
-               [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+               [] -> eval_ncommand ~include_paths opts status
+                 ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
              | _ -> prerr_endline ("Discriminator: non empty metasenv");
-                    status, []) *)
+                    status)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
@@ -776,7 +784,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (match menv with
           [] ->
             eval_ncommand ~include_paths opts status
-             ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
+             ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
         | _ -> assert false)
   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
       eval_add_constraint status [`Type,u1] [`Type,u2]