Rewrite of Program Fixpoint to overcome the previous limitations:

- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments. 
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.


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

7 files changed, 27 insertions, 29 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 91a9eeefaf..9723f2c223 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -873,7 +873,8 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 and extern_recursion_order scopes vars = function
     RStructRec -> CStructRec
   | RWfRec c -> CWfRec (extern true scopes vars c)
-  | RMeasureRec c -> CMeasureRec (extern true scopes vars c)
+  | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, 
+				     Option.map (extern true scopes vars) r)
 
 
 let extern_rawconstr vars c =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a447fbe8da..172d032b55 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -289,7 +289,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty, l,impl,argsc = List.assoc id impls in
+    let ty,l,impl,argsc = List.assoc id impls in
     let l = List.map 
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
     let tys = string_of_ty ty in
@@ -298,8 +298,9 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
-  then
-    RVar (loc,id), [], [], []
+  then (
+    Dumpglob.dump_reference loc "<>" (string_of_id id) "var";
+    RVar (loc,id), [], [], [])
   (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
@@ -794,9 +795,9 @@ let check_projection isproj nargs r =
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
-let set_hole_implicit i = function
-  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
-  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
+let set_hole_implicit i b = function
+  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i,b))
+  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
@@ -857,7 +858,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
-	     let intern_ro_arg c f =
+	     let intern_ro_arg f =
 	       let idx = 
 		 match n with
 		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
@@ -866,22 +867,18 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	       let before, after = list_chop idx bl in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
-	       let ro =
-		 match c with 
-		   | None -> RStructRec 
-		   | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c') 
-	       in 
+	       let ro = f (intern (ids', unb, tmp_scope, scopes)) in 
 	       let n' = Option.map (fun _ -> List.length before) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, ((ids',_,_,_),rbl) =
-	       (match order with
-		 | CStructRec -> 
-		     intern_ro_arg None (fun _ -> RStructRec)
-		 | CWfRec c ->
-		     intern_ro_arg (Some c) (fun r -> RWfRec r)
-		 | CMeasureRec c ->
-		     intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+	       match order with
+	       | CStructRec -> 
+		   intern_ro_arg (fun _ -> RStructRec)
+	       | CWfRec c ->
+		   intern_ro_arg (fun f -> RWfRec (f c))
+	       | CMeasureRec (m,r) ->
+		   intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
 	     in
 	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
@@ -1153,7 +1150,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
+	    RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: 
 	      aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
@@ -1216,7 +1213,7 @@ let intern_pattern env patt =
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -1354,7 +1351,7 @@ let interp_context_gen understand_type understand_judgment env bl =
 	      let impls = 
 		if k = Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
-		    (ExplByPos (n, na), (true, true)) :: impls
+		    (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
 		(push_rel d env, d::params, succ n, impls)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 126eff8596..25bcc66b0a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -47,7 +47,7 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a9d3704471..4495c22c67 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -254,7 +254,7 @@ let implicits_of_rawterm l =
 		    Name id -> Some id
 		  | Anonymous -> None
 	      in
-		(ExplByPos (i, name), (true, true)) :: rest
+		(ExplByPos (i, name), (true, true, true)) :: rest
 	    else rest
       | RLetIn (loc, na, t, b) -> aux i b
       | _ -> []
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index dc83e2135c..57eff0b863 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier *
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e0a8ca600e..666f9022bd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -375,7 +375,7 @@ let rec subst_aconstr subst bound raw =
 
   | APatVar _ | ASort _ -> raw
 
-  | AHole (Evd.ImplicitArg (ref,i)) ->
+  | AHole (Evd.ImplicitArg (ref,i,b)) ->
       let ref',t = subst_global subst ref in 
 	if ref' == ref then raw else
 	  AHole (Evd.InternalHole)
@@ -683,7 +683,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
-  | CMeasureRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
 
 type constr_pattern_expr = constr_expr
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3039269671..1982a08fd3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -161,7 +161,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
-  | CMeasureRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
 
 (** Anonymous defs allowed ?? *)
 and local_binder =