Work on recursive definitions

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

4 files changed, 124 insertions, 72 deletions

diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
index 3de0615aa6..f4827c7549 100644
--- a/contrib/subtac/interp.ml
+++ b/contrib/subtac/interp.ml
@@ -28,10 +28,10 @@ open Evarutil
 open Pretype_errors
 open Rawterm
 open Evarconv
-open Coercion
 open Pattern
 open Dyn
 
+open Subtac_coercion
 open Scoq
 open Coqlib
 open Printer
@@ -42,18 +42,20 @@ open Eterm
 type recursion_info = {
   arg_name: name;
   arg_type: types; (* A *)
+  args_after : rel_context;
   wf_relation: constr; (* R : A -> A -> Prop *)
   wf_proof: constr; (* : well_founded R *)
   f_type: types; (* f: A -> Set *)
   f_fulltype: types; (* Type with argument and wf proof product first *)
 }
 
-type prog_info = {
-  evd : evar_defs ref;
-  mutable evm: evar_map;
-  rec_info: recursion_info option;
-}
-
+let my_print_rec_info env t = 
+  str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
+  str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
+  str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
+  str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
+  str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
+  str "Full type: " ++ my_print_constr env t.f_fulltype
 
 (* Taken from pretyping.ml *)
 let evd_comb0 f isevars =
@@ -110,7 +112,7 @@ let check_branches_message loc env isevars c (explft,lft) =
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon loc env isevars j = function
    | None -> j
-   | Some typ -> evd_comb2 (inh_conv_coerce_to loc env) isevars j typ
+   | Some typ -> evd_comb2 (Subtac_coercion.inh_conv_coerce_to loc env) isevars j typ
 
 let push_rels vars env = List.fold_right push_rel vars env
 
@@ -168,10 +170,18 @@ let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
   | RType _ -> judge_of_new_Type ()
 
+let my_print_tycon env = function
+    Some t -> my_print_constr env t
+  | None -> str "None"
+
 (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [(evars_of isevars)] and *)
 (* the type constraint tycon *)
-let rec pretype tycon env isevars lvar = function
+let rec pretype tycon env isevars lvar c = 
+(*   trace (str "pretype for " ++ (my_print_rawconstr env c) ++  *)
+(* 	   str " and tycon "++ my_print_tycon env tycon ++  *)
+(* 	   str " in environment: " ++ my_print_env env); *)
+  match c with
 
   | RRef (loc,ref) ->
       inh_conv_coerce_to_tycon loc env isevars
@@ -268,12 +278,11 @@ let rec pretype tycon env isevars lvar = function
 	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
             let resty =
               whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
-	    let coercef, resty = Subtac_coercion.mu env isevars resty in
 	      match kind_of_term resty with
 	      | Prod (na,c1,c2) ->
 		  let hj = pretype (mk_tycon c1) env isevars lvar c in
 		  let newresj =
-      		    { uj_val = applist (app_opt coercef (j_val resj), [j_val hj]);
+      		    { uj_val = applist (j_val resj, [j_val hj]);
 		      uj_type = subst1 hj.uj_val c2 } in
 		  apply_rec env (n+1) newresj rest
 
@@ -385,9 +394,11 @@ let rec pretype tycon env isevars lvar = function
         user_err_loc (loc,"",
 	  str "If is only for inductive types with two constructors");
 
-      (* Make dependencies from arity signature impossible *)
+      (* Make dependencies from arity signature possible ! *)
       let arsgn,_ = get_arity env indf in
-      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+      let arsgn = List.map (fun (n,b,t) -> 
+			      debug 2 (str "If case arg: " ++ Nameops.pr_name n);
+			      (n,b,t)) arsgn in
       let nar = List.length arsgn in
       let psign = (na,None,build_dependent_inductive env indf)::arsgn in
       let pred,p = match po with
@@ -408,7 +419,13 @@ let rec pretype tycon env isevars lvar = function
 	let n = rel_context_length cs.cs_args in
 	let pi = liftn n 2 pred in
 	let pi = beta_applist (pi, [build_dependent_constructor cs]) in
-	let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in
+	let csgn = 
+	  List.map (fun (n,b,t) ->
+		      match n with 
+			  Name _ -> (n, b, t)
+			| Anonymous -> (Name (id_of_string "H"), b, t))
+	    cs.cs_args 
+	in
 	let env_c = push_rels csgn env in 
 	let bj = pretype (Some pi) env_c isevars lvar b in
 	it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
@@ -578,8 +595,9 @@ let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
   
 let make_fixpoint t id term = 
+  let term = it_mkLambda_or_LetIn term t.args_after in
   let term' = mkLambda (Name id, t.f_fulltype, term) in
-    mkApp (Lazy.force fix, 
+    mkApp (Lazy.force fixsub, 
 	   [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; 
 	      mkLambda (t.arg_name, t.arg_type, term') |])       
 
@@ -596,12 +614,23 @@ let find_with_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
+let require_library dirpath =
+  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
+    Library.require_library [qualid] None
+
+let list_split_at index l = 
+  let rec aux i acc = function
+      hd :: tl when i = index -> (List.rev acc), tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "list_split_at: Invalid argument"
+  in aux 0 [] l
+
 let subtac' recursive id l env (s, t) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
+  require_library "Coq.subtac.FixSub";
   try
     let evd = ref (create_evar_defs Evd.empty) in
-    let nonimplicit = ref Gset.empty in
     let coqintern evd env = Constrintern.intern_constr (evars_of evd) env in
     let coqinterp evd env = Constrintern.interp_constr (evars_of evd) env in
     let rec env_with_binders ((env, rels) as acc) = function
@@ -626,54 +655,62 @@ let subtac' recursive id l env (s, t) =
     trace (str "Creating env with binders");
     let env', binders_rel = env_with_binders (env, []) l in
     trace (str "New env created:" ++ my_print_context env');
-    let s, t = coqintern !evd env' s, coqintern !evd env' t in
-    trace (str "Begin infer_type of given spec");
-    let coqtype, rec_info, env' =
+    let s = coqintern !evd env' s in
+    trace (str "Internalized specification: " ++ my_print_rawconstr env s);
+    let coqtype, rec_info, env', binders_type, binders_term =
       match recursive with
-	  Some (StructRec id) ->
-	    assert(false)
-	| Some (WfRec (rel, (loc, n))) ->
-	    let coqrel = coqinterp !evd env rel in
+	  Some (Some (StructRec _) | None) -> assert(false)
+	| Some (Some (WfRec (rel, (loc, n)))) ->
+	    let index, ((n, def, ntype) as nrel) = find_with_index n (rel_context env') in
+	    let after, before = list_split_at index (rel_context env') in
+	    let envbefore = push_rel_context before env in
+	    let typeenv = env' in
+	    let coqrel = coqinterp !evd envbefore rel in
 	    let coqs, styp = interp env' evd s empty_tycon in
-	    let index, (_, _, ntype) = find_with_index n (rel_context env') in
+	    let fullcoqs = it_mkProd_or_LetIn coqs after in
 	    let ntype = lift index ntype in
+	    let ftype = mkLambda (n, ntype,  fullcoqs) in
+	    (*let termenv = 
+	      push_rel_context (subst_ctx (mkApp ((Lazy.force _sig).proj1, mkRel 1)) after) *)
+		
 	    let argtype = 
-	      mkApp ((Lazy.force sig_).intro, 
+	      mkApp ((Lazy.force sig_).typ, 
 		     [| ntype;
 			mkLambda (n, ntype, 
 				  mkApp (coqrel, [| mkRel 1; mkRel (index + 2)|])) |])
 	    in
-	    let ftype = mkProd (n, argtype, lift 1 coqs) in
-	    let fulltype =
-	      mkProd (n, argtype,
-		      mkProd(Anonymous,
-			     mkApp (coqrel, [| mkRel 1; mkRel 2 |]),
-			     Term.subst1 (mkRel 2) coqs))
-	    in
+	    let fulltype = mkProd (n, argtype, fullcoqs) in
 	    let proof = 
 	      let wf_rel = mkApp (Lazy.force well_founded, [| ntype; coqrel |]) in
-		make_existential dummy_loc env nonimplicit evd wf_rel (* TODO use env before rec arg *)
+		make_existential dummy_loc envbefore evd wf_rel
 	    in
 	    let rec_info = 
 	      { arg_name = n;
 		arg_type = ntype;
+		args_after = after;
 		wf_relation = coqrel;
 		wf_proof = proof;
 		f_type = ftype;
 		f_fulltype = fulltype;
 	      }
 	    in 
-	    let env' = push_rel (Name id, None, ftype) env' in 
-	      coqs, Some rec_info, env'
+	    let env' = push_rel (Name id, None, fulltype) env' in 
+	      coqs, Some rec_info, env', binders_rel, before
 	| None ->
 	    let coqs, _ = interp env' evd s empty_tycon in
-	      coqs, None, env'
+	      coqs, None, env', binders_rel, binders_rel
     in
+    (match rec_info with 
+	 Some rec_info -> trace (str "Got recursion info: " ++ my_print_rec_info env rec_info)
+       | None -> ());
     trace (str "Interpreted type: " ++ my_print_constr env' coqtype);
-    let coqt, ttyp = interp env' evd t empty_tycon in
+    let tycon = mk_tycon coqtype in
+    let t = coqintern !evd env' t in
+    trace (str "Internalized term: " ++ my_print_rawconstr env t);   
+    let coqt, ttyp = interp env' evd t tycon in
     trace (str "Interpreted term: " ++ my_print_constr env' coqt ++ spc () ++
 	   str "Infered type: " ++ my_print_constr env' ttyp);
-    let coercespec = Subtac_coercion.coerce dummy_loc env' nonimplicit evd ttyp coqtype in
+    let coercespec = Subtac_coercion.coerce dummy_loc env' evd ttyp coqtype in
     trace (str "Specs coercion successfull");
     let realt = app_opt coercespec coqt in
     trace (str "Term Specs coercion successfull: " ++ my_print_constr env' realt);
@@ -684,14 +721,14 @@ let subtac' recursive id l env (s, t) =
     in
     (try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !evd));
      with Not_found -> trace (str "Not found in pr_evar_map"));
-    let realt = it_mkLambda_or_LetIn realt binders_rel and
-      coqtype = it_mkProd_or_LetIn coqtype binders_rel
+    let realt = it_mkLambda_or_LetIn realt binders_term and
+      coqtype = it_mkProd_or_LetIn coqtype binders_type
     in
     let realt = Evarutil.nf_evar (evars_of !evd) realt in
     let coqtype = Evarutil.nf_evar (evars_of !evd) coqtype in
     trace (str "Coq term: " ++ my_print_constr env realt ++ spc ()
 	   ++ str "Coq type: " ++ my_print_constr env coqtype);
-    let evm = non_instanciated_map env nonimplicit evd in
+    let evm = non_instanciated_map env evd in
       (try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm);
        with Not_found -> trace (str "Not found in pr_evar_map"));
     let tac = Eterm.etermtac (evm, realt) in 
@@ -750,7 +787,10 @@ let subtac' recursive id l env (s, t) =
 	   | e -> raise e)
   
     | e -> 
-	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e))
+	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e));
+	raise e
+	
+	  
 	
 
 let subtac recursive id l env (s, t) =
diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml
index 799e8e6802..7a84898890 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/scoq.ml
@@ -5,7 +5,16 @@ open Term
 open Names
 open Util
 
-let init_constant dir s = gen_constant "Subtac" dir s
+(****************************************************************************)
+(* Library linking *)
+
+let contrib_name = "subtac"
+
+let subtac_dir = ["subtac"]
+let subfix_module = subtac_dir @ ["FixSub"]
+let init_constant dir s = gen_constant contrib_name dir s
+
+let fixsub = lazy (init_constant subfix_module "Fix_sub")
 
 let build_sig () = 
   { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
@@ -16,19 +25,19 @@ let build_sig () =
 
 let sig_ = lazy (build_sig ())
 
-let eqind = lazy (gen_constant "subtac" ["Init"; "Logic"] "eq")
+let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
 
-let boolind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "bool")
-let sumboolind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sumbool")
-let natind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "nat")
-let intind = lazy (gen_constant "subtac" ["ZArith"; "binint"] "Z")
-let existSind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sigS")
+let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
+let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
+let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
+let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
+let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
   
 let existS = lazy (build_sigma_set ())
 
 (* orders *)
-let well_founded = lazy (gen_constant "subtac" ["Init"; "Wf"] "well_founded")
-let fix = lazy (gen_constant "subtac" ["Init"; "Wf"] "Fix")
+let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
+let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
 
 let extconstr = Constrextern.extern_constr true (Global.env ())
 let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -37,6 +46,7 @@ open Pp
 
 let my_print_constr = Termops.print_constr_env
 let my_print_context = Termops.print_rel_context
+let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
 
 let mknewexist = 
@@ -65,8 +75,8 @@ let wf_relations = Hashtbl.create 10
 
 let std_relations () = 
   let add k v = Hashtbl.add wf_relations k v in
-    add (gen_constant "subtac" ["Init"; "Peano"] "lt")
-      (lazy (gen_constant "subtac" ["Arith"; "Wf_nat"] "lt_wf"))
+    add (init_constant ["Init"; "Peano"] "lt")
+      (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
       
 let std_relations = Lazy.lazy_from_fun std_relations
 
@@ -86,12 +96,11 @@ let app_opt c e =
       Some constr -> constr e
     | None -> e	
 
-let make_existential loc env nonimplicit isevars c =
+let make_existential loc env isevars c =
   let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
   let (key, args) = destEvar evar in
     debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
 	     Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str ""));
-    nonimplicit := Gset.add key !nonimplicit;
     evar
 
 let string_of_hole_kind = function
@@ -102,20 +111,16 @@ let string_of_hole_kind = function
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
       
-let non_instanciated_map env nonimplicit evd =
+let non_instanciated_map env evd =
   let evm = evars_of !evd in
     List.fold_left 
       (fun evm (key, evi) -> 
 	 let (loc,k) = evar_source key !evd in
 	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
-		    str (string_of_hole_kind k));
-	   if Gset.mem key !nonimplicit then
-	     begin
-	       debug 2 (str " and is not an implicit");
-	       Evd.add evm key evi
-	     end
-	   else
-	     let (loc,k) = evar_source key !evd in
+		      str (string_of_hole_kind k));
+	   match k with 
+	       QuestionMark -> Evd.add evm key evi
+	     | _ ->
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
       Evd.empty (Evarutil.non_instantiated evm)
diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4
index 987ab04888..657f11b306 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/sparser.ml4
@@ -119,7 +119,7 @@ let (wit_subtac_binders : subtac_binders_argtype),
   (rawwit_subtac_binders : subtac_binders_argtype) =
   Genarg.create_arg "subtac_binders"
 
-type subtac_fixannot_argtype = (Scoq.recursion_order, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type subtac_fixannot_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 
 let (wit_subtac_fixannot : subtac_fixannot_argtype),
   (globwit_subtac_fixannot : subtac_fixannot_argtype),
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index d65e95a5d5..015eb5d171 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -96,7 +96,7 @@ let rec mu env isevars t =
     | None -> (None, t)
   in aux t
 
-and coerce loc env nonimplicit isevars (x : Term.constr) (y : Term.constr) 
+and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
     : (Term.constr -> Term.constr) option 
     =
   trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
@@ -186,7 +186,7 @@ and coerce loc env nonimplicit isevars (x : Term.constr) (y : Term.constr)
 		Some 
 		  (fun x ->
 		     let cx = app_opt c x in
-		     let evar = make_existential dummy_loc env nonimplicit isevars (mkApp (p, [| cx |]))
+		     let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |]))
 		     in
 		       (mkApp 
 			  ((Lazy.force sig_).intro, 
@@ -194,10 +194,10 @@ and coerce loc env nonimplicit isevars (x : Term.constr) (y : Term.constr)
 	    | None -> raise NoCoercion
   in coerce_unify env x y
 
-let coerce_itf loc env nonimplicit isevars hj c1 =
+let coerce_itf loc env isevars hj c1 =
   let {uj_val = v; uj_type = t} = hj in
   let evars = ref isevars in
-  let coercion = coerce loc env nonimplicit evars t c1 in
+  let coercion = coerce loc env evars t c1 in
     !evars, {uj_val = app_opt coercion v;
 	     uj_type = t}
       
@@ -269,7 +269,12 @@ let inh_app_fun env isevars j =
  	   let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
       	   let p = lookup_path_to_fun_from i1 in
            (isevars,apply_coercion env p j t)
-	 with Not_found -> (isevars,j))
+	 with Not_found ->
+	   try 
+	     let coercef, t = mu env isevars t in
+	       (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
+	   with NoCoercion ->
+	     (isevars,j))
 
 let inh_tosort_force loc env isevars j =
   try
@@ -350,13 +355,15 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
 	 | _ -> raise NoCoercion))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to loc env nonimplicit isevars cj t =
+let inh_conv_coerce_to loc env isevars cj t =
+  trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ 
+	   str " and "++ my_print_constr env t);
   let (evd',cj') = 
     try 
       inh_conv_coerce_to_fail env isevars cj t
     with NoCoercion ->
       try
-	coerce_itf loc env nonimplicit isevars cj t
+	coerce_itf loc env isevars cj t
       with NoCoercion ->
 	let sigma = evars_of isevars in
 	  debug 2 (str "No coercion found");