X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=eb355f2ea43c01a9eba147d8fc15e52f8b92256f;hb=65f34cf91a06b727d5387d92e70c875d15c88fd7;hp=437fed32db9ee9f749c3e7c688cccb15761e3669;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 437fed32d..eb355f2ea 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -19,9 +19,12 @@ let namer_of names =
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
 let tactic_of_ast = function
-  | TacticAst.Intros (_, _, names) ->
+  | TacticAst.Intros (_, None, names) ->
       (* TODO Zack implement intros length *)
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+  | TacticAst.Intros (_, Some num, names) ->
+      (* TODO Zack implement intros length *)
+      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -40,7 +43,8 @@ let tactic_of_ast = function
   | TacticAst.Cut (_, term) -> Tactics.cut term
   | TacticAst.Elim (_, term, _) ->
       (* TODO Zack implement "using" argument *)
-      Tactics.elim_intros_simpl term
+      (* old: Tactics.elim_intros_simpl term *)
+      Tactics.elim_intros term
   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
   | TacticAst.Auto (_,num) -> 
@@ -55,9 +59,19 @@ let tactic_of_ast = function
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.LetIn of 'term * 'ident
-  | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
+  | TacticAst.Reduce (_,reduction_kind,opts) ->
+      let terms, also_in_hypotheses = 
+        match opts with
+        | Some (l,`Goal) -> Some l, false
+        | Some (l,`Everywhere) -> Some l, true
+        | None -> None, false
+      in
+      (match reduction_kind with
+      | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
+      | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
+      | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) 
   | TacticAst.Rewrite (_,dir,t,ident) ->
       if dir = `Left then
         EqualityTactics.rewrite_tac ~term:t 
@@ -102,6 +116,31 @@ let eval_tactical status tac =
   in
   apply_tactic (tactical_of_ast tac)
 
+(** given a uri and a type list (the contructors types) builds a list of pairs
+ *  (name,uri) that is used to generate authomatic aliases **)
+let extract_alias types uri = 
+  fst(List.fold_left (
+    fun (acc,i) (name, _, _, cl) -> 
+      ((name, UriManager.string_of_uriref (uri,[i]))
+      ::
+      (fst(List.fold_left (
+        fun (acc,j) (name,_) ->
+          (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
+        ) (acc,1) cl))),i+1
+  ) ([],0) types)
+
+(** adds a (name,uri) list l to a disambiguation environment e **)
+let env_of_list l e = 
+  let module DT = DisambiguateTypes in
+  let module DTE = DisambiguateTypes.Environment in
+  List.fold_left (
+    fun e (name,uri) -> 
+      DTE.add 
+       (DT.Id name) 
+       (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
+       e
+  ) e l
+
 let eval_command status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> set_option status name value
@@ -131,6 +170,11 @@ let eval_command status cmd =
           "type you've declared!");
       MatitaLog.message (sprintf "%s defined" suri);
       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
+      let status = 
+        let name = UriManager.name_of_uri uri in
+        let new_env = env_of_list [(name,suri)] status.aliases in
+        {status with aliases = new_env }
+      in
       {status with proof_status = No_proof }
   | TacticAst.Inductive (loc, dummy_params, types) ->
       (* dummy_params are not real params, it is a list of nothing, and the only
@@ -149,8 +193,13 @@ let eval_command status cmd =
         CicTypeChecker.typecheck_mutual_inductive_defs uri
           (types, [], leftno) CicUniv.empty_ugraph
       in
+      let status = 
         MatitaSync.add_inductive_def
-          ~uri ~types ~params:[] ~leftno ~ugraph status;
+          ~uri ~types ~params:[] ~leftno ~ugraph status
+      in
+      let aliases = env_of_list (extract_alias types uri) status.aliases in
+      let status = {status with proof_status = No_proof } in
+      { status with aliases = aliases}
   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
       let uri = 
         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
@@ -180,7 +229,13 @@ let eval_command status cmd =
           "metasenv not empty while giving a definition with body";
       let body = CicMetaSubst.apply_subst subst body in
       let ty = CicMetaSubst.apply_subst subst ty in
-      MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
+      let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
+      let status = 
+        let suri = UriManager.string_of_uri uri in
+        let new_env = env_of_list [(name,suri)] status.aliases in
+        {status with aliases = new_env }
+      in
+      {status with proof_status = No_proof}
   | TacticAst.Theorem (_, _, None, _, _) ->
       command_error "The grammas should avoid having unnamed theorems!"
   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
@@ -292,9 +347,22 @@ let disambiguate_tactic status = function
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.LetIn of 'term * 'ident
-  | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
+  | TacticAst.Reduce (loc, reduction_kind, opts) ->
+      let status, opts = 
+        match opts with
+        | None -> status, None
+        | Some (l,pat) -> 
+            let status, l = 
+              List.fold_right (fun t (status,acc) ->
+                let status',t' = disambiguate_term status t in
+                status', t'::acc) 
+              l (status,[]) 
+            in
+            status, Some (l, pat)
+      in
+      status, TacticAst.Reduce (loc, reduction_kind, opts)
   | TacticAst.Rewrite (loc,dir,t,ident) ->
       let status, term = disambiguate_term status t in
       status, TacticAst.Rewrite (loc,dir,term,ident)
@@ -477,12 +545,14 @@ let eval_ast status ast =
   (* this disambiguation step should be deferred to support tacticals *)
   eval status st
 
-let eval_from_stream status str =
-  let st = CicTextualParser2.parse_statement str in
-  eval_ast status st
+let eval_from_stream status str cb =
+  let stl = CicTextualParser2.parse_statements str in
+  List.fold_left 
+    (fun status ast -> cb status ast;eval_ast status ast) status 
+  stl
   
 let eval_string status str =
-  eval_from_stream status (Stream.of_string str) 
+  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
   let options =