Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.

May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 257 insertions, 0 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
new file mode 100644
index 0000000000..34eff9a176
--- /dev/null
+++ b/contrib/subtac/subtac_command.ml
@@ -0,0 +1,257 @@
+
+open Closure
+open RedFlags
+open Declarations
+open Entries
+open Dyn
+open Libobject
+open Pattern
+open Matching
+open Pp
+open Rawterm
+open Sign
+open Tacred
+open Util
+open Names
+open Nameops
+open Libnames
+open Nametab
+open Pfedit
+open Proof_type
+open Refiner
+open Tacmach
+open Tactic_debug
+open Topconstr
+open Term
+open Termops
+open Tacexpr
+open Safe_typing
+open Typing
+open Hiddentac
+open Genarg
+open Decl_kinds
+open Mod_subst
+open Printer
+open Inductiveops
+open Syntax_def
+open Pretyping
+
+open Tacinterp
+open Vernacexpr
+open Notation
+
+open Interp
+open Scoq
+
+
+(*********************************************************************)
+(* Functions to parse and interpret constructions *)
+
+let interp_gen kind isevars env 
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
+  let c' = Constrintern.intern_gen (kind=Pretyping.IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
+  let c'' = Interp_fixpoint.rewrite_cases c' in
+    understand_gen kind isevars env c''
+    
+
+let interp_constr isevars env c =
+  interp_gen (OfType None) isevars env c 
+
+let interp_type isevars env ?(impls=([],[])) c =
+  interp_gen IsType isevars env ~impls c
+
+let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+  interp_gen (OfType (Some typ)) isevars env ~impls c 
+
+let interp_open_constr isevars env c =
+  understand_tcc isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+
+let interp_constr_judgment isevars env c =
+  understand_judgment isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+
+(* try to find non recursive definitions *)
+
+let list_chop_hd i l = match list_chop i l with
+  | (l1,x::l2) -> (l1,x,l2)
+  | _ -> assert false
+
+let collect_non_rec env = 
+  let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
+    try
+      let i = 
+        list_try_find_i
+          (fun i f ->
+             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+             then i else failwith "try_find_i")
+          0 lnamerec 
+      in
+      let (lf1,f,lf2) = list_chop_hd i lnamerec in
+      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
+      let (lar1,ar,lar2) = list_chop_hd i larrec in
+      let newlnv = 
+	try 
+	  match list_chop i nrec with 
+            | (lnv1,_::lnv2) -> (lnv1@lnv2)
+	    | _ -> [] (* nrec=[] for cofixpoints *)
+        with Failure "list_chop" -> []
+      in 
+      searchrec ((f,def,ar)::lnonrec) 
+	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
+    with Failure "try_find_i" -> 
+      (List.rev lnonrec,
+       (Array.of_list lnamerec, Array.of_list ldefrec,
+        Array.of_list larrec, Array.of_list nrec))
+  in 
+  searchrec [] 
+
+let recursive_message v =
+  match Array.length v with
+    | 0 -> error "no recursive definition"
+    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+		    spc () ++ str "are recursively defined")
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+  let sigma = Evd.empty
+  and env0 = Global.env()
+  and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef
+  in 
+  let lnameargsardef = 
+    List.map (fun (f, d) -> Interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
+      lnameargsardef
+  in
+  let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
+  and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
+  in
+  (* Build the recursive context and notations for the recursive types *)
+  let (rec_sign,rec_impls,arityl) = 
+    List.fold_left 
+      (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
+        let arityc = Command.generalize_constr_expr arityc bl in
+	let isevars = ref (Evd.create_evar_defs sigma) in
+        let isevars, arity = interp_type isevars env0 arityc in
+	let impl = 
+	  if Impargs.is_implicit_args()
+	  then Impargs.compute_implicits env0 arity
+	  else [] in
+	let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+          (Environ.push_named (recname,None,arity) env, impls', (isevars, arity)::arl))
+      (env0,[],[]) lnameargsardef in
+  let arityl = List.rev arityl in
+  let notations = 
+    List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
+      lnameargsardef [] in
+
+  let recdef =
+
+    (* Declare local notations *)
+    let fs = States.freeze() in
+    let def = 
+      try
+	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
+	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
+	List.map2
+	  (fun ((_,_,bl,_,def),_) (evm, arity) ->
+             let def = abstract_constr_expr def bl in
+               interp_casted_constr (ref (Evd.create_evar_defs evm)) rec_sign ~impls:([],rec_impls)
+		def arity)
+          lnameargsardef arityl
+      with e ->
+	States.unfreeze fs; raise e in
+    States.unfreeze fs; def 
+  in
+
+  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
+    collect_non_rec env0 lrecnames recdef arityl nv in
+  let nvrec' = Array.map fst nvrec in(* ignore rec order *)
+  let declare arrec defrec =
+    let recvec = 
+      Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+    let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+    let rec declare i fi =
+      trace (str "Declaring: " ++ pr_id fi);
+      let ce = 
+	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
+          const_entry_type = Some arrec.(i);
+          const_entry_opaque = false;
+          const_entry_boxed = boxed} in
+      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+      in (ConstRef kn)
+    in 
+      (* declare the recursive definitions *)
+    let lrefrec = Array.mapi declare namerec in
+      Options.if_verbose ppnl (recursive_message lrefrec);
+      (*  (* The others are declared as normal definitions *)
+	  let var_subst id = (id, Constrintern.global_reference id) in
+	  let _ = 
+	  List.fold_left
+	  (fun subst (f,def,t) ->
+	  let ce = { const_entry_body = replace_vars subst def;
+	  const_entry_type = Some t;
+          const_entry_opaque = false;
+	  const_entry_boxed = boxed } in
+	  let _ =
+	  Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+	  in
+      	  warning ((string_of_id f)^" is non-recursively defined");
+      	  (var_subst f) :: subst)
+	  (List.map var_subst (Array.to_list namerec))
+	  lnonrec 
+	  in*)
+      List.iter (fun (df,c,scope) ->
+		   Metasyntax.add_notation_interpretation df [] c scope) notations
+  in 
+  let declare l = 
+    let recvec = Array.of_list l
+    and arrec = Array.map snd arrec
+    in declare arrec recvec
+  in
+  let recdefs = Array.length defrec in
+    trace (int recdefs ++ str " recursive definitions");
+    (* Solve remaining evars *)
+  let rec solve_evars i acc = 
+    if i < recdefs then
+      let (evm, def) = defrec.(i) in
+	if Evd.dom evm = [] then 
+	  solve_evars (succ i) (def :: acc)
+	else
+	  let _,typ = arrec.(i) in
+	  let id = namerec.(i) in
+	    (* Generalize by the recursive prototypes  *)
+	  let def = 
+	    Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+	  and typ = 
+	    Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
+	  let tac = Eterm.etermtac (evm, def) in 
+	  let _ =
+	    trace (str "Starting proof of a fixpoint def:" ++ spc () ++ my_print_constr env0 def ++
+		   spc () ++ str " with goal: " ++ my_print_constr env0 typ ++
+		   spc () ++ str " with evar map = " ++ Evd.pr_evar_map evm)
+	  in
+	    begin
+	      Command.start_proof (id_of_string (string_of_id id ^ "_evars"))  goal_kind typ
+		(fun _ gr -> 
+		   let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+		   let constant = match gr with Libnames.ConstRef c -> c
+		     | _ -> assert(false)
+		   in
+		     try 
+		       let def = Environ.constant_value (Global.env ()) constant in
+		       let _ = trace (str "Got constant value") in		 
+		       let _, c = decompose_lam_n recdefs def in
+		       let _ = trace (str "Fixpoint body is: " ++ spc () ++ my_print_constr (Global.env ()) c) in
+			 solve_evars (succ i) (c :: acc)
+		     with Environ.NotEvaluableConst cer ->
+		       match cer with
+			   Environ.NoBody -> trace (str "Constant has no body")
+			 | Environ.Opaque -> trace (str "Constant is opaque")
+		);
+	      trace (str "Started proof");
+	      Pfedit.by tac;
+	      trace (str "Applied eterm tac");
+	    end
+    else declare (List.rev acc)
+  in solve_evars 0 []
+
+