Backport code from command.ml to subtac_command.ml for definining

recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).


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

1 files changed, 61 insertions, 39 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 05bebf0f56..b7777e6222 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,6 +1,7 @@
 open Printf
 open Pp
 open Subtac_utils
+open Command
 
 open Term
 open Names
@@ -35,14 +36,17 @@ type obligation =
 
 type obligations = (obligation array * int)
 
+type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+
 type program_info = {
   prg_name: identifier;
   prg_body: constr;
   prg_type: constr;
   prg_obligations: obligations;
   prg_deps : identifier list;
-  prg_nvrec : int array;
+  prg_fixkind : Command.fixpoint_kind option ;
   prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+  prg_notations : notations ;
   prg_kind : definition_object_kind;
   prg_hook : definition_hook;
 }
@@ -159,39 +163,50 @@ let declare_definition prg =
 open Pp
 open Ppconstr
 
+let compute_possible_guardness_evidences (n,_) fixtype =
+  match n with 
+  | Some n -> [n] 
+  | None -> 
+      (* If recursive argument was not given by user, we try all args.
+	 An earlier approach was to look only for inductive arguments,
+	 but doing it properly involves delta-reduction, and it finally 
+         doesn't seem to worth the effort (except for huge mutual 
+	 fixpoints ?) *)
+      let m = Term.nb_prod fixtype in
+      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+	list_map_i (fun i _ -> i) 0 ctx
+
 let declare_mutual_definition l =
   let len = List.length l in
-  let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
-(*   let arrec =  *)
-(*     Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *)
-(*   in *)
-  let recvec, arrec = 
-    let l, l' = 
-      List.split
-	(List.map (fun x -> 
-	  let subs, typ = (subst_body x) in
-	    snd (decompose_lam_n len subs), 
-	  snd (decompose_prod_n len typ)) l)
-    in
-      Array.of_list l, Array.of_list l'
-  in
-  let nvrec = (List.hd l).prg_nvrec in
-  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
-  let rec declare i fi =
-    (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
-		  my_print_constr (Global.env()) (recvec.(i)));
-     with _ -> ());
-    let ce = 
-      { const_entry_body = mkFix ((nvrec,i),recdecls); 
-        const_entry_type = Some arrec.(i);
-        const_entry_opaque = false;
-        const_entry_boxed = true} in
-      Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+  let fixdefs, fixtypes, fiximps = 
+    list_split3
+      (List.map (fun x -> 
+	let subs, typ = (subst_body x) in
+	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
-  let lrefrec = Array.mapi declare namerec in
-    print_message (recursive_message lrefrec);
-    lrefrec.(0)    
-         
+  let fixkind = Option.get (List.hd l).prg_fixkind in
+  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
+  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+  let boxed = true (* TODO *) in
+  let fixnames = (List.hd l).prg_deps in
+  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
+  let indexes, fixdecls =
+    match fixkind with
+      | IsFixpoint wfl ->
+	  let possible_indexes =
+	    List.map2 compute_possible_guardness_evidences wfl fixtypes in
+	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
+      | IsCoFixpoint ->
+	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
+  in      
+  (* Declare the recursive definitions *)
+  let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
+    (* Declare notations *)
+    List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+    Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
+    (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+      
 let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
@@ -220,7 +235,7 @@ let try_tactics obls =
         
 let red = Reductionops.nf_betaiota
 
-let init_prog_info n b t deps nvrec obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
     Array.mapi
       (fun i (n, t, o, d) ->
@@ -231,7 +246,8 @@ let init_prog_info n b t deps nvrec obls impls kind hook =
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
+      prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
     
 let get_prog name =
   let prg_infos = !from_prg in
@@ -422,9 +438,15 @@ let show_obligations ?(msg=true) n =
 		    | Some _ -> ())
       obls
 
+let show_term n =
+  let prg = get_prog_err n in
+  let n = prg.prg_name in
+    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+	    ++ my_print_constr (Global.env ()) prg.prg_body)
+
 let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in
+  let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Flags.if_verbose ppnl (str ".");    
@@ -440,12 +462,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ())
 	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	  | _ -> res)
 	
-let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec =
-  let deps = List.map (fun (n, b, t, obls) -> n) l in
+let add_mutual_definitions l ?(kind=Definition) notations fixkind =
+  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
-      (fun acc (n, b, t, obls) ->
-	 let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in
-	   ProgMap.add n prg acc)
+      (fun acc (n, b, t, imps, obls) ->
+	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+	  ProgMap.add n prg acc)
       !from_prg l
   in
     from_prg := upd;