1 files changed, 465 insertions, 0 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
new file mode 100644
index 00000000..4e6ea802
--- /dev/null
+++ b/plugins/cc/cctac.ml
@@ -0,0 +1,465 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+(* This file is the interface between the c-c algorithm and Coq *)
+
+open Evd
+open Proof_type
+open Names
+open Libnames
+open Nameops
+open Inductiveops
+open Declarations
+open Term
+open Termops
+open Tacmach
+open Tactics
+open Tacticals
+open Typing
+open Ccalgo
+open Tacinterp
+open Ccproof
+open Pp
+open Util
+open Format
+
+let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
+
+let _f_equal = constant ["Init";"Logic"] "f_equal"
+
+let _eq_rect = constant ["Init";"Logic"] "eq_rect"
+
+let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+
+let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+
+let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+
+let _eq = constant ["Init";"Logic"] "eq"
+
+let _False = constant ["Init";"Logic"] "False"
+
+let whd env=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let whd_delta env=
+   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+(* decompose member of equality in an applicative format *)
+
+let sf_of env sigma c = family_of_sort (sort_of env sigma c)
+
+let rec decompose_term env sigma t=
+    match kind_of_term (whd env t) with
+      App (f,args)->
+	let tf=decompose_term env sigma f in
+	let targs=Array.map (decompose_term env sigma) args in
+	  Array.fold_left (fun s t->Appli (s,t)) tf targs
+    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+	let b = pop _b in
+	let sort_b = sf_of env sigma b in
+	let sort_a = sf_of env sigma a in
+	Appli(Appli(Product (sort_a,sort_b) ,
+		    decompose_term env sigma a),
+	      decompose_term env sigma b)
+    | Construct c->
+	let (oib,_)=Global.lookup_inductive (fst c) in
+	let nargs=mis_constructor_nargs_env env c in
+	  Constructor {ci_constr=c;
+		       ci_arity=nargs;
+		       ci_nhyps=nargs-oib.mind_nparams}
+    | _ ->if closed0 t then (Symb t) else raise Not_found
+
+(* decompose equality in members and type *)
+
+let atom_of_constr env sigma term =
+  let wh =  (whd_delta env term) in
+  let kot = kind_of_term wh in
+    match kot with
+      App (f,args)->
+	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+	  then `Eq (args.(0),
+		   decompose_term env sigma args.(1),
+		   decompose_term env sigma args.(2))
+	  else `Other (decompose_term env sigma term)
+    | _ -> `Other (decompose_term env sigma term)
+
+let rec pattern_of_constr env sigma c =
+  match kind_of_term (whd env c) with
+      App (f,args)->
+	let pf = decompose_term env sigma f in
+	let pargs,lrels = List.split
+	  (array_map_to_list (pattern_of_constr env sigma) args) in
+	  PApp (pf,List.rev pargs),
+	List.fold_left Intset.union Intset.empty lrels
+    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+	let b =pop _b in
+	let pa,sa = pattern_of_constr env sigma a in
+	let pb,sb = pattern_of_constr env sigma (pop b) in
+	let sort_b = sf_of env sigma b in
+	let sort_a = sf_of env sigma a in
+	  PApp(Product (sort_a,sort_b),
+	       [pa;pb]),(Intset.union sa sb)
+    | Rel i -> PVar i,Intset.singleton i
+    | _ ->
+	let pf = decompose_term env sigma c in
+	  PApp (pf,[]),Intset.empty
+
+let non_trivial = function
+    PVar _ -> false
+  | _ -> true
+
+let patterns_of_constr env sigma nrels term=
+  let f,args=
+    try destApp (whd_delta env term) with _ -> raise Not_found in
+	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+	then
+	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
+	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
+	  let valid1 =
+	    if Intset.cardinal rels1 <> nrels then Creates_variables
+	    else if non_trivial patt1 then Normal
+	    else Trivial args.(0)
+	  and valid2 =
+	    if Intset.cardinal rels2 <> nrels then Creates_variables
+	    else if non_trivial patt2 then Normal
+	    else Trivial args.(0) in
+	    if valid1 <> Creates_variables
+	      || valid2 <> Creates_variables  then
+	      nrels,valid1,patt1,valid2,patt2
+	    else raise Not_found
+	else raise Not_found
+
+let rec quantified_atom_of_constr env sigma nrels term =
+  match kind_of_term (whd_delta env term) with
+      Prod (_,atom,ff) ->
+	if eq_constr ff (Lazy.force _False) then
+	  let patts=patterns_of_constr env sigma nrels atom in
+	      `Nrule patts
+	else
+	  quantified_atom_of_constr env sigma (succ nrels) ff
+    | _ ->
+	let patts=patterns_of_constr env sigma nrels term in
+	    `Rule patts
+
+let litteral_of_constr env sigma term=
+  match kind_of_term (whd_delta env term) with
+    | Prod (_,atom,ff) ->
+	if eq_constr ff (Lazy.force _False) then
+	  match (atom_of_constr env sigma atom) with
+	      `Eq(t,a,b) -> `Neq(t,a,b)
+	    | `Other(p) -> `Nother(p)
+	else
+	  begin
+	    try
+	      quantified_atom_of_constr env sigma 1 ff
+	    with Not_found ->
+	      `Other (decompose_term env sigma term)
+	  end
+    | _ ->
+	atom_of_constr env sigma term
+
+
+(* store all equalities from the context *)
+
+let rec make_prb gls depth additionnal_terms =
+  let env=pf_env gls in
+  let sigma=sig_sig gls in
+  let state = empty depth gls in
+  let pos_hyps = ref [] in
+  let neg_hyps =ref [] in
+    List.iter
+      (fun c ->
+	 let t = decompose_term env sigma c in
+	   ignore (add_term state t)) additionnal_terms;
+    List.iter
+      (fun (id,_,e) ->
+	 begin
+	   let cid=mkVar id in
+	   match litteral_of_constr env sigma e with
+	       `Eq (t,a,b) -> add_equality state cid a b
+	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
+	     | `Other ph ->
+		 List.iter
+		   (fun (cidn,nh) ->
+		      add_disequality state (HeqnH (cid,cidn)) ph nh)
+		   !neg_hyps;
+		 pos_hyps:=(cid,ph):: !pos_hyps
+	     | `Nother nh ->
+		 List.iter
+		   (fun (cidp,ph) ->
+		      add_disequality state (HeqnH (cidp,cid)) ph nh)
+		   !pos_hyps;
+		 neg_hyps:=(cid,nh):: !neg_hyps
+	     | `Rule patts -> add_quant state id true patts
+	     | `Nrule patts -> add_quant state id false patts
+	 end) (Environ.named_context_of_val gls.it.evar_hyps);
+    begin
+      match atom_of_constr env sigma gls.it.evar_concl with
+	  `Eq (t,a,b) -> add_disequality state Goal a b
+	|	`Other g ->
+		  List.iter
+	      (fun (idp,ph) ->
+		 add_disequality state (HeqG idp) ph g) !pos_hyps
+    end;
+    state
+
+(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
+
+let build_projection intype outtype (cstr:constructor) special default gls=
+  let env=pf_env gls in
+  let (h,argv) =
+    try destApp intype with
+	Invalid_argument _ -> (intype,[||])  in
+  let ind=destInd h in
+  let types=Inductiveops.arities_of_constructors env ind in
+  let lp=Array.length types in
+  let ci=pred (snd cstr) in
+  let branch i=
+    let ti=Term.prod_appvect types.(i) argv in
+    let rc=fst (decompose_prod_assum ti) in
+    let head=
+      if i=ci then special else default in
+      it_mkLambda_or_LetIn head rc in
+  let branches=Array.init lp branch in
+  let casee=mkRel 1 in
+  let pred=mkLambda(Anonymous,intype,outtype) in
+  let case_info=make_case_info (pf_env gls) ind RegularStyle in
+  let body= mkCase(case_info, pred, casee, branches) in
+  let id=pf_get_new_id (id_of_string "t") gls in
+    mkLambda(Name id,intype,body)
+
+(* generate an adhoc tactic following the proof tree  *)
+
+let _M =mkMeta
+
+let rec proof_tac p gls =
+  match p.p_rule with
+      Ax c -> exact_check c gls
+    | SymAx c ->
+	let l=constr_of_term p.p_lhs and
+	    r=constr_of_term p.p_rhs in
+        let typ = refresh_universes (pf_type_of gls l) in
+	  exact_check
+	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+    | Refl t ->
+	let lr = constr_of_term t in
+	let typ = refresh_universes (pf_type_of gls lr) in
+	exact_check
+	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+    | Trans (p1,p2)->
+	let t1 = constr_of_term p1.p_lhs and
+	    t2 = constr_of_term p1.p_rhs and
+	    t3 = constr_of_term p2.p_rhs in
+	let typ = refresh_universes (pf_type_of gls t2) in
+	let prf =
+	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
+	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
+    | Congr (p1,p2)->
+	let tf1=constr_of_term p1.p_lhs
+	and tx1=constr_of_term p2.p_lhs
+	and tf2=constr_of_term p1.p_rhs
+	and tx2=constr_of_term p2.p_rhs in
+	let typf = refresh_universes (pf_type_of gls tf1) in
+	let typx = refresh_universes (pf_type_of gls tx1) in
+	let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
+	let id = pf_get_new_id (id_of_string "f") gls in
+	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+	let lemma1 =
+	  mkApp(Lazy.force _f_equal,
+		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
+	let lemma2=
+	  mkApp(Lazy.force _f_equal,
+		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+	let prf =
+	  mkApp(Lazy.force _trans_eq,
+		[|typfx;
+		  mkApp(tf1,[|tx1|]);
+		  mkApp(tf2,[|tx1|]);
+		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
+	  tclTHENS (refine prf)
+	    [tclTHEN (refine lemma1) (proof_tac p1);
+  	     tclFIRST
+	       [tclTHEN (refine lemma2) (proof_tac p2);
+		reflexivity;
+		fun gls ->
+		  errorlabstrm  "Congruence"
+		    (Pp.str
+		       "I don't know how to handle dependent equality")]] gls
+  | Inject (prf,cstr,nargs,argind) ->
+	 let ti=constr_of_term prf.p_lhs in
+	 let tj=constr_of_term prf.p_rhs in
+	 let default=constr_of_term p.p_lhs in
+	 let intype=refresh_universes (pf_type_of gls ti) in
+	 let outtype=refresh_universes (pf_type_of gls default) in
+	 let special=mkRel (1+nargs-argind) in
+	 let proj=build_projection intype outtype cstr special default gls in
+	 let injt=
+	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
+	   tclTHEN (refine injt) (proof_tac prf) gls
+
+let refute_tac c t1 t2 p gls =
+  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
+  let intype=refresh_universes (pf_type_of gls tt1) in
+  let neweq=
+    mkApp(Lazy.force _eq,
+	  [|intype;tt1;tt2|]) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let false_t=mkApp (c,[|mkVar hid|]) in
+    tclTHENS (assert_tac (Name hid) neweq)
+      [proof_tac p; simplest_elim false_t] gls
+
+let convert_to_goal_tac c t1 t2 p gls =
+  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
+  let sort=refresh_universes (pf_type_of gls tt2) in
+  let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
+  let e=pf_get_new_id (id_of_string "e") gls in
+  let x=pf_get_new_id (id_of_string "X") gls in
+  let identity=mkLambda (Name x,sort,mkRel 1) in
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
+    tclTHENS (assert_tac (Name e) neweq)
+      [proof_tac p;exact_check endt] gls
+
+let convert_to_hyp_tac c1 t1 c2 t2 p gls =
+  let tt2=constr_of_term t2 in
+  let h=pf_get_new_id (id_of_string "H") gls in
+  let false_t=mkApp (c2,[|mkVar h|]) in
+    tclTHENS (assert_tac (Name h) tt2)
+      [convert_to_goal_tac c1 t1 t2 p;
+       simplest_elim false_t] gls
+
+let discriminate_tac cstr p gls =
+  let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+  let intype=refresh_universes (pf_type_of gls t1) in
+  let concl=pf_concl gls in
+  let outsort=mkType (new_univ ()) in
+  let xid=pf_get_new_id (id_of_string "X") gls in
+  let tid=pf_get_new_id (id_of_string "t") gls in
+  let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
+  let trivial=pf_type_of gls identity in
+  let outtype=mkType (new_univ ()) in
+  let pred=mkLambda(Name xid,outtype,mkRel 1) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let proj=build_projection intype outtype cstr trivial concl gls in
+  let injt=mkApp (Lazy.force _f_equal,
+		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|outtype;trivial;pred;identity;concl;injt|]) in
+  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
+    tclTHENS (assert_tac (Name hid) neweq)
+      [proof_tac p;exact_check endt] gls
+
+(* wrap everything *)
+
+let build_term_to_complete uf meta pac =
+  let cinfo = get_constructor_info uf pac.cnode in
+  let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
+  let dummy_args = List.rev (list_tabulate meta pac.arity) in
+  let all_args = List.rev_append real_args dummy_args in
+    applistc (mkConstruct cinfo.ci_constr) all_args
+
+let cc_tactic depth additionnal_terms gls=
+  Coqlib.check_required_library ["Coq";"Init";"Logic"];
+  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
+  let state = make_prb gls depth additionnal_terms in
+  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
+  let sol = execute true state in
+  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
+  let uf=forest state in
+    match sol with
+	None -> tclFAIL 0 (str "congruence failed") gls
+      | Some reason ->
+	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
+	  match reason with
+	      Discrimination (i,ipac,j,jpac) ->
+		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+		  discriminate_tac cstr p gls
+	    | Incomplete ->
+		let metacnt = ref 0 in
+		let newmeta _ = incr metacnt; _M !metacnt in
+		let terms_to_complete =
+		  List.map
+		    (build_term_to_complete uf newmeta)
+		    (epsilons uf) in
+		  Pp.msgnl
+		    (Pp.str "Goal is solvable by congruence but \
+ some arguments are missing.");
+		  Pp.msgnl
+		    (Pp.str "  Try " ++
+		     hov 8
+		       begin
+			 str "\"congruence with (" ++
+			 prlist_with_sep
+			   (fun () -> str ")" ++ pr_spc () ++ str "(")
+			   (print_constr_env (pf_env gls))
+			   terms_to_complete ++
+			 str ")\","
+		       end);
+		  Pp.msgnl
+		    (Pp.str "  replacing metavariables by arbitrary terms.");
+		  tclFAIL 0 (str "Incomplete") gls
+	    | Contradiction dis ->
+		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+		let ta=term uf dis.lhs and tb=term uf dis.rhs in
+		  match dis.rule with
+		      Goal -> proof_tac p gls
+		    | Hyp id -> refute_tac id ta tb p gls
+		    | HeqG id ->
+			convert_to_goal_tac id ta tb p gls
+		    | HeqnH (ida,idb) ->
+			convert_to_hyp_tac ida ta idb tb p gls
+
+
+let cc_fail gls =
+  errorlabstrm  "Congruence" (Pp.str "congruence failed.")
+
+let congruence_tac depth l =
+  tclORELSE
+    (tclTHEN (tclREPEAT introf) (cc_tactic depth l))
+    cc_fail
+
+(* Beware: reflexivity = constructor 1 = apply refl_equal
+   might be slow now, let's rather do something equivalent
+   to a "simple apply refl_equal" *)
+
+let simple_reflexivity () = apply (Lazy.force _refl_equal)
+
+(* The [f_equal] tactic.
+
+   It mimics the use of lemmas [f_equal], [f_equal2], etc.
+   This isn't particularly related with congruence, apart from
+   the fact that congruence is called internally.
+*)
+
+let f_equal gl =
+  let cut_eq c1 c2 =
+    let ty = refresh_universes (pf_type_of gl c1) in
+    tclTHENTRY
+      (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
+      (simple_reflexivity ())
+  in
+  try match kind_of_term (pf_concl gl) with
+    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
+	begin match kind_of_term t, kind_of_term t' with
+	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+	      let rec cuts i =
+		if i < 0 then tclTRY (congruence_tac 1000 [])
+		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+	      in cuts (Array.length v - 1) gl
+	  | _ -> tclIDTAC gl
+	end
+    | _ -> tclIDTAC gl
+  with Type_errors.TypeError _ -> tclIDTAC gl