Partly fixes #3225. Removed some old experimental stuff in funind.

1 files changed, 0 insertions, 244 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e7732a503..045beb37c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -247,247 +247,3 @@ END
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 ["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
 END
-
-
-
-
-
-(* FINDUCTION *)
-
-(* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
-  (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-let prNamedConstr s c =
-  begin
-    msg(str "");
-    msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
-    msg(str "");
-  end
-
-
-
-(** Information about an occurrence of a function call (application)
-    inside a term. *)
-type fapp_info = {
-  fname: constr; (** The function applied *)
-  largs: constr list; (** List of arguments *)
-  free: bool; (** [true] if all arguments are debruijn free *)
-  max_rel: int; (** max debruijn index in the funcall *)
-  onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
-}
-
-
-(** [constr_head_match(a b c) a] returns true, false otherwise. *)
-let constr_head_match u t=
-  if isApp u
-  then
-    let uhd,args= destApp u in
-    Constr.equal uhd t
-  else false
-
-(** [hdMatchSub inu t] returns the list of occurrences of [t] in
-    [inu]. DeBruijn are not pushed, so some of them may be unbound in
-    the result. *)
-let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
-  let subres =
-    match kind_of_term inu with
-      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
-	  hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
-      | Fix (_,(lna,tl,bl))  -> (* not sure Fix is correct *)
-	  Array.fold_left
-	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
-	    [] bl
-      | _ -> (* Cofix will be wrong *)
-	  fold_constr
-	    (fun l cstr ->
-	      l @ hdMatchSub cstr test) [] inu in
-  if not (test inu) then subres
-  else
-    let f,args = decompose_app inu in
-    let freeset = Termops.free_rels inu in
-    let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in
-    {fname = f; largs = args; free = Int.Set.is_empty freeset;
-    max_rel = max_rel; onlyvars = List.for_all isVar args }
-    ::subres
-
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkEq typ c1 c2 =
-  mkApp (make_eq(),[| typ; c1; c2|])
-
-
-let poseq_unsafe idunsafe cstr gl =
-  let typ = Tacmach.pf_unsafe_type_of gl cstr in
-  tclTHEN
-    (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
-    (tclTHENFIRST
-      (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr)))
-      (Proofview.V82.of_tactic Tactics.reflexivity))
-    gl
-
-
-let poseq id cstr gl =
-  let x = Tactics.fresh_id [] id gl in
-  poseq_unsafe x cstr gl
-
-(* dirty? *)
-
-let list_constr_largs = ref []
-
-let rec poseq_list_ids_rec lcstr gl =
-  match lcstr with
-    | [] -> tclIDTAC gl
-    | c::lcstr' ->
-	match kind_of_term c with
-	  | Var _ ->
-	      (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
-	  | _ ->
-	      let _ = prstr "c = " in
-	      let _ = prconstr c in
-	      let _ = prstr "\n" in
-	      let typ = Tacmach.pf_unsafe_type_of gl c in
-	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
-	      let x = Tactics.fresh_id [] cname gl in
-	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
-	      let _ = prstr " list_constr_largs = " in
-	      let _ = prlistconstr !list_constr_largs in
-	      let _ = prstr "\n" in
-
-	      tclTHEN
-		(poseq_unsafe x c)
-		(poseq_list_ids_rec lcstr')
-		gl
-
-let poseq_list_ids lcstr gl =
-  let _ = list_constr_largs := [] in
-  poseq_list_ids_rec lcstr gl
-
-(** [find_fapp test g] returns the list of [app_info] of all calls to
-    functions that satisfy [test] in the conclusion of goal g. Trivial
-    repetition (not modulo conversion) are deleted. *)
-let find_fapp (test:constr -> bool) g : fapp_info list =
-  let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
-  let res =
-    List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
-  (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
-  res)
-
-
-
-(** [finduction id filter g] tries to apply functional induction on
-    an occurrence of function [id] in the conclusion of goal [g]. If
-    [id]=[None] then calls to any function are selected. In any case
-    [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
-    (nexttac:Proof_type.tactic) g =
-  let test = match oid with
-    | Some id ->
-       let idref = const_of_id id in
-       (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
-       let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in
-	(fun u -> constr_head_match u idconstr) (* select only id *)
-    | None -> (fun u -> isApp u) in (* select calls to any function *)
-  let info_list = find_fapp test g in
-  let ordered_info_list = heuristic info_list in
-  prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
-  if List.is_empty ordered_info_list then Errors.error "function not found in goal\n";
-  let taclist: Proof_type.tactic list =
-    List.map
-      (fun info ->
-	(tclTHEN
-	  (tclTHEN (poseq_list_ids info.largs)
-	    (
-	      fun gl ->
-		  (functional_induction
-		    true (applist (info.fname, List.rev !list_constr_largs))
-		    None None) gl))
-	  nexttac)) ordered_info_list in
-  (* we try each (f t u v) until one does not fail *)
-  (* TODO: try also to mix functional schemes *)
-  tclFIRST taclist g
-
-
-
-
-(** [chose_heuristic oi x] returns the heuristic for reordering
-    (and/or forgetting some elts of) a list of occurrences of
-     function calls infos to chose first with functional induction. *)
-let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
-  match oi with
-    | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
-    | None ->
-	(* Default heuristic: put first occurrences where all arguments
-	   are *bound* (meaning already introduced) variables *)
-	let ordering x y =
-	  if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
-	  else if x.free && x.onlyvars then -1
-	  else if y.free && y.onlyvars then 1
-	  else 0 (* both not pertinent *)
-	in
-	List.sort ordering
-
-
-
-TACTIC EXTEND finduction
-    ["finduction" ident(id) natural_opt(oi)] ->
-      [
-	match oi with
-	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
-	  | _ ->
-	      let heuristic = chose_heuristic oi in
-	      Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
-      ]
-END
-
-
-
-TACTIC EXTEND fauto
-    [ "fauto" tactic(tac)] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
-      ]
-  |
-    [ "fauto" ] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic tclIDTAC)
-      ]
-
-END
-
-
-TACTIC EXTEND poseq
-  [ "poseq" ident(x) constr(c) ] ->
-      [ Proofview.V82.tactic (poseq x c) ]
-END
-
-VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
-  [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
-END
-
-VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
-  [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
-      "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
-     [
-       let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
-       let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
-       let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in
-       let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in
-       let ar1 = List.length (fst (decompose_prod f1type)) in
-       let ar2 = List.length (fst (decompose_prod f2type)) in
-       let _ =
-	 if not (Int.equal ar1 (List.length cl1)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
-       let _ =
-	 if not (Int.equal ar2 (List.length cl2)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
-       Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
-     ]
-END