]> matita.cs.unibo.it Git - helm.git/commitdiff
New tactic cases (still to be documented).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Dec 2006 22:34:35 +0000 (22:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Dec 2006 22:34:35 +0000 (22:34 +0000)
It is necessary for the declarative language and it is useful anyway.

helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/matita.lang

index 8979129158b34bcd8a9ffa03577dca64bfb399e9..7a9b7b5ae05f7099244d3a7c70fa189fc5b85040 100644 (file)
@@ -49,6 +49,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | ApplyS of loc * 'term * (string * string) list
   | Assumption of loc
   | Auto of loc * (string * string) list
+  | Cases of loc * 'term * 'ident list
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident list
   | ClearBody of loc * 'ident
index 840c16351f86823aeef0bc25d18acda1fcdd1b30..0530697ada6b252b580405a4837ef7eca0e5eb68 100644 (file)
@@ -83,6 +83,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
+  | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^
+      pp_intros_specs (None, idents) 
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
index a747223c7dea4136e5a54a6b69f59eed4d0bc427..082eee5f95279cbb5265197849220bd3082e3311 100644 (file)
@@ -68,6 +68,9 @@ let tactic_of_ast status ast =
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
        ~universe:status.GrafiteTypes.universe
+  | GrafiteAst.Cases (_, what, names) ->
+      Tactics.cases_intros ~mk_fresh_name_callback:(namer_of names)
+        what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
index 9eb1e53fa68494ef25c32ef05f4f4adca64d4ed4..42fbabacd600fa3acd796367d482da2f9f4750df 100644 (file)
@@ -130,6 +130,9 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,params) ->
         metasenv,GrafiteAst.Auto (loc,params)
+    | GrafiteAst.Cases (loc, what, idents) ->
+        let metasenv,what = disambiguate_term context metasenv what in
+        metasenv,GrafiteAst.Cases (loc, what, idents)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in
index 1321f613b82e91a5acc8e793d14c76d49f687624..b2fb3616f6cc216866dd7a446b614e27ca7dd39c 100644 (file)
@@ -116,11 +116,15 @@ EXTEND
     | SYMBOL "<" -> `RightToLeft ]
   ];
   int: [ [ num = NUMBER -> int_of_string num ] ];
+  intros_names: [
+   [ idents = OPT ident_list0 ->
+      match idents with None -> [] | Some idents -> idents
+   ]
+  ];
   intros_spec: [
     [ OPT [ IDENT "names" ]; 
       num = OPT [ num = int -> num ]; 
-      idents = OPT ident_list0 ->
-        let idents = match idents with None -> [] | Some idents -> idents in
+      idents = intros_names ->
         num, idents
     ]
   ];
@@ -138,6 +142,9 @@ EXTEND
         GrafiteAst.Assumption loc
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
+    | IDENT "cases"; what = tactic_term;
+      (num, idents) = intros_spec ->
+       GrafiteAst.Cases (loc, what, idents)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
index 5f8533916b74190ad1dc980760250f6c0692a9c7..9f9da081830c94da80fdba1bde8df4d3e30e9333 100644 (file)
@@ -560,6 +560,100 @@ let elim_tac ~term =
   mk_tactic (elim_tac ~term)
 ;;
 
+let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+ let cases_tac ~term (proof, goal) =
+  let module T = CicTypeChecker in
+  let module U = UriManager in
+  let module R = CicReduction in
+  let module C = Cic in
+   let (curi,metasenv,proofbo,proofty) = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    let termty = CicReduction.whd context termty in
+    let (termty,metasenv',arguments,fresh_meta) =
+     TermUtil.saturate_term
+      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+    let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+    let uri,exp_named_subst,typeno,args =
+     match termty with
+        C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+      | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+          (uri,exp_named_subst,typeno,args)
+      | _ -> raise NotAnInductiveTypeToEliminate
+    in
+     let paramsno,patterns =
+      match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+         C.InductiveDefinition (tys,_,paramsno,_),_ ->
+          let _,_,_,cl = List.nth tys typeno in
+          let rec aux n context t =
+           match n,CicReduction.whd context t with
+              0,C.Prod (name,source,target) ->
+               let fresh_name =
+                mk_fresh_name_callback metasenv' context name
+                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
+                 ~typ:source
+               in
+                C.Lambda (fresh_name,C.Implicit None,
+                 aux 0 (Some (fresh_name,C.Decl source)::context) target)
+            | n,C.Prod (name,source,target) ->
+               let fresh_name =
+                mk_fresh_name_callback metasenv' context name
+                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
+                 ~typ:source
+               in
+                aux (n-1) (Some (fresh_name,C.Decl source)::context) target
+            | 0,_ -> C.Implicit None
+            | _,_ -> assert false
+          in
+           paramsno,
+           List.map (function (_,cty) -> aux paramsno context cty) cl 
+       | _ -> assert false
+     in
+      let outtype =
+       let target =
+        C.Lambda (C.Name "fixme",C.Implicit None,
+         ProofEngineReduction.replace_lifting
+          ~equality:(ProofEngineReduction.alpha_equivalence)
+          ~what:[CicSubstitution.lift (paramsno+1) term]
+          ~with_what:[C.Rel (paramsno+1)]
+          ~where:(CicSubstitution.lift (paramsno+1) ty))
+       in
+        let rec add_lambdas =
+         function
+            0 -> target
+          | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
+        in
+         add_lambdas paramsno
+      in
+       let term_to_refine =
+        C.MutCase (uri,typeno,outtype,term,patterns)
+       in
+prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
+        let refined_term,_,metasenv'',_ = 
+         CicRefine.type_of_aux' metasenv' context term_to_refine
+           CicUniv.empty_ugraph
+        in
+         let new_goals =
+          ProofEngineHelpers.compare_metasenvs
+           ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+         in
+         let proof' = curi,metasenv'',proofbo,proofty in
+          let proof'', new_goals' =
+           apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+          in
+           (* The apply_tactic can have closed some of the new_goals *)
+           let patched_new_goals =
+            let (_,metasenv''',_,_) = proof'' in
+             List.filter
+              (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
+              ) new_goals @ new_goals'
+           in
+            proof'', patched_new_goals
+ in
+  mk_tactic (cases_tac ~term)
+;;
+
+
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                     ?depth ?using what =
  Tacticals.then_ ~start:(elim_tac ~term:what)
index 6e0c821cca0333bfaf6b03ea5291f83ac02a6f3c..3e7a4858128fd2c26cf5625659603bcc14104d19 100644 (file)
@@ -77,6 +77,10 @@ val elim_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
 
+val cases_intros_tac:
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  Cic.term -> ProofEngineTypes.tactic 
+
 (* FG *)
 
 (* inserts a hole in the context *)
index c34355b8ea21fd382dcfa08c9d0e9cc728056ab7..82c343085a0c0b4ec38e35693db54acfebd4a8b5 100644 (file)
@@ -30,6 +30,7 @@ let apply = PrimitiveTactics.apply_tac
 let applyS = Auto.applyS_tac
 let assumption = VariousTactics.assumption_tac
 let auto = AutoTactic.auto_tac
+let cases_intros = PrimitiveTactics.cases_intros_tac
 let change = ReductionTactics.change_tac
 let clear = ProofEngineStructuralRules.clear
 let clearbody = ProofEngineStructuralRules.clearbody
index d765a8ac0759ae02b864d94e7f162f12e36edb87..c0702638f6d2780d9ca6f435a6fdf2693f5280fb 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 28 11:13:28 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Dec 20 23:48:06 CET 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -10,6 +10,9 @@ val assumption : ProofEngineTypes.tactic
 val auto :
   params:(string * string) list ->
   dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
+val cases_intros :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  Cic.term -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term -> ProofEngineTypes.tactic
@@ -24,8 +27,8 @@ val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int option) list ->
   ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate : dbd:HMysql.dbd -> 
-  universe:Universe.universe -> ProofEngineTypes.tactic
+val demodulate :
+  dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
 val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
index 02c7045ba0eac86922e58324157e6f0e96c0b510..fbb21d6d19ba3d4232a91b3dd8554888188eb15f 100644 (file)
@@ -85,6 +85,7 @@
     <keyword>assumption</keyword>
     <keyword>auto</keyword>
     <keyword>paramodulation</keyword>
+    <keyword>cases</keyword>
     <keyword>clear</keyword>
     <keyword>clearbody</keyword>
     <keyword>change</keyword>