the decompose tactic is now working

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index aff9144cc0cef8124fa492a9f7ea74ca7a7e4b64..9fc24acf1c5df35887cf2c10ef94db962559bd0c 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -68,7 +68,15 @@ let tactic_of_ast = function
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
   | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
-  | GrafiteAst.Decompose (_,term) -> Tactics.decompose term
+  | GrafiteAst.Decompose (_, types, what, names) -> 
+      let to_type = function
+         | GrafiteAst.Type (uri, typeno) -> uri, typeno
+        | GrafiteAst.Ident _            -> assert false
+      in
+      let user_types = List.rev_map to_type types in
+      let dbd = MatitaDb.instance () in
+      let mk_fresh_name_callback = namer_of names in
+      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
@@ -185,9 +193,18 @@ let disambiguate_tactic status = function
       status, GrafiteAst.Cut (loc, ident, cic)
   | GrafiteAst.DecideEquality loc ->
       status, GrafiteAst.DecideEquality loc
-  | GrafiteAst.Decompose (loc,term) ->
-      let status,term = disambiguate_term status term in
-      status, GrafiteAst.Decompose(loc,term)
+  | GrafiteAst.Decompose (loc, types, what, names) ->
+      let disambiguate (status, types) = function
+         | GrafiteAst.Type _   -> assert false
+        | GrafiteAst.Ident id ->
+           match disambiguate_term status (CicNotationPt.Ident (id, None)) with
+              | status, Cic.MutInd (uri, tyno, _) ->
+                 status, (GrafiteAst.Type (uri, tyno) :: types)
+               | _                                 -> 
+                 raise Disambiguate.NoWellTypedInterpretation
+      in
+      let status, types = List.fold_left disambiguate (status, []) types in
+      status, GrafiteAst.Decompose(loc, types, what, names)  
   | GrafiteAst.Discriminate (loc,term) ->
       let status,term = disambiguate_term status term in
       status, GrafiteAst.Discriminate(loc,term)