New files for subtac

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

2 files changed, 407 insertions, 0 deletions

diff --git a/contrib/subtac/interp_fixpoint.ml b/contrib/subtac/interp_fixpoint.ml
new file mode 100644
index 000000000..819135709
--- /dev/null
+++ b/contrib/subtac/interp_fixpoint.ml
@@ -0,0 +1,206 @@
+open Global
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Topconstr
+
+open Subtac_coercion
+open Scoq
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+
+
+let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args)
+
+let mkSubset name typ prop = 
+  mkAppExplC (sig_ref,
+	      [ typ; mkLambdaC ([name], typ, prop) ])
+	      
+let mkProj1 u p x = 
+  mkAppExplC (proj1_sig_ref, [ u; p; x ])
+
+let mkProj2 u p x = 
+  mkAppExplC (proj2_sig_ref, [ u; p; x ])
+
+let list_of_local_binders l = 
+  let rec aux acc = function
+      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl
+    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+	aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl
+    | [] -> List.rev acc
+  in aux [] l
+       
+let abstract_constr_expr_bl c bl =
+  List.fold_right (fun (n, t) c -> mkLambdaC ([n], t, c)) bl c
+
+let pr_binder_list b = 
+  List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
+		     Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) 
+
+
+let rec rewrite_rec_calls l c = c
+
+let rewrite_fixpoint env l (f, decl) = 
+  let (id, (n, ro), bl, typ, body) = f in
+  let body = rewrite_rec_calls l body in
+    match ro with
+	CStructRec -> ((id, (n, ro), bl, typ, body), decl)
+      | CWfRec wfrel -> 
+	  let bls = list_of_local_binders bl in
+	  let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ 
+			 Ppconstr.pr_binders bl ++ str " : " ++ 
+			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
+			 Ppconstr.pr_constr_expr body)
+	  in
+	  let after, before = list_chop n bls in
+	  let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
+			 pr_binder_list before ++ str "; after the recursion arg: " ++
+			 pr_binder_list after)
+	  in
+	  let ((locn, name), ntyp), before = match before with
+	      hd :: tl -> hd, tl
+	    | _ -> assert(false) (* Rec arg must be in before *)
+	  in
+	  let nid = match name with
+	      Name id -> id
+	    | Anonymous -> assert(false) (* Rec arg _must_ be named *)
+	  in
+	  let _wfproof = 
+	    let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in
+	      (*make_existential_expr dummy_loc before wf_rel*)
+	      mkRefC lt_wf_ref
+	  in
+	  let nid', accproofid = 
+	    let nid = string_of_id nid in
+	      id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
+	  in
+	  let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
+	  let coqP = abstract_constr_expr_bl typ after in
+	  let body' =
+	    let prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
+	    let lamprop = mkLambdaC ([lnid'], ntyp, prop) in
+	    let typnid' = mkSubset lnid' ntyp prop in
+	    let body' = (* body abstracted by rec call *)
+	      mkLambdaC ([(dummy_loc, Name id)], 
+			 mkProdC ([lnid'], typnid', coqP),
+			 body)
+	    in
+	      mkAppC (body',
+		      [mkLambdaC 
+			 ([lnid'], typnid',
+			  mkAppC (mkIdentC id, 
+				  [mkProj1 ntyp lamprop (mkIdentC nid');
+				   (mkAppExplC (acc_inv_ref,
+						[ ntyp; wfrel;
+						  mkIdentC nid;
+						  mkIdentC accproofid;
+						  mkProj1 ntyp lamprop (mkIdentC nid');
+						  mkProj2 ntyp lamprop (mkIdentC nid') ])) ]))])
+	  in
+	  let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
+	  let bl' = 
+	    let rec aux acc = function
+		Topconstr.LocalRawDef _ as x :: tl -> 
+		  aux (x :: acc) tl
+	      | Topconstr.LocalRawAssum (bl, typ) as assum :: tl ->
+		  let rec aux' bl' = function
+		      ((loc, name') as x) :: tl ->
+			if name' = name then
+			  LocalRawAssum (List.rev (x :: bl'), typ) ::
+			    LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
+			    if tl = [] then [] else [LocalRawAssum (tl, typ)]
+			else aux' (x :: bl') tl
+		    | [] -> [assum]
+		  in aux (acc @ List.rev (aux' [] bl)) tl
+	      | [] -> List.rev acc
+	    in aux [] bl
+	  in
+	  let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ 
+			 Ppconstr.pr_binders bl' ++ str " : " ++ 
+			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
+			 Ppconstr.pr_constr_expr body')
+	  in (id, (succ n, ro), bl', typ, body'), decl
+
+let list_mapi f = 
+  let rec aux i = function 
+      hd :: tl -> f i hd :: aux (succ i) tl 
+    | [] -> []
+  in aux 0
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+  let tml = list_mapi (fun i (c, (n, opt)) -> c, 
+		       ((match n with
+			    Name id -> (match c with
+					  | RVar (_, id') when id = id' ->
+					      Name (id_of_string (string_of_id id ^ "'"))
+					  | _ -> n)
+			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
+			opt)) tml 
+  in
+  let mkHole = RHole (dummy_loc, InternalHole) in
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+		       [mkHole; c; n])
+  in
+  let eqs_types = 
+    List.map
+      (fun (c, (n, _)) ->
+	 let id = match n with Name id -> id | _ -> assert false in
+	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
+	   Name heqid, mkeq c (RVar (dummy_loc, id)))
+      tml
+  in
+  let po = 
+    List.fold_right
+      (fun (n,t) acc ->
+	 RProd (dummy_loc, n, t, acc))
+      eqs_types (match po with 
+		     Some e -> e
+		   | None -> mkHole)
+  in
+  let eqns =   
+    List.map (fun (loc, idl, cpl, c) ->
+		let c' = 
+		  List.fold_left 
+		    (fun acc (n, t) ->
+		       RLambda (dummy_loc, n, t, acc))
+		    c eqs_types
+		in (loc, idl, cpl, c'))
+      eqns
+  in
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+			      [mkHole; c])
+  in
+  let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
+  let case = RCases (loc,Some po,tml,eqns) in
+  let app = RApp (dummy_loc, case, refls) in
+    app
+
+let rec rewrite_cases c = 
+  match c with 
+      RCases _ -> let c' = map_rawconstr rewrite_cases c in
+	(match c' with 
+	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+	   | _ -> assert(false))
+    | _ -> map_rawconstr rewrite_cases c
+	  
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
new file mode 100644
index 000000000..c34338236
--- /dev/null
+++ b/contrib/subtac/subtac.ml
@@ -0,0 +1,201 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Global
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Vernacexpr
+
+open Subtac_coercion
+open Scoq
+open Coqlib
+open Printer
+open Subtac_errors
+open Context
+open Eterm
+
+let require_library dirpath =
+  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
+    Library.require_library [qualid] None
+
+let subtac_one_fixpoint env isevars (f, decl) = 
+  let ((id, n, bl, typ, body), decl) = 
+    Interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
+  in
+  let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
+		 Ppconstr.pr_constr_expr body)
+  in ((id, n, bl, typ, body), decl)
+    
+	      
+let subtac_fixpoint isevars l = 
+  (* TODO: Copy command.build_recursive *)
+  ()
+(*
+let save id const (locality,kind) hook =
+  let {const_entry_body = pft;
+       const_entry_type = tpo;
+       const_entry_opaque = opacity } = const in
+  let l,r = match locality with
+    | Local when Lib.sections_are_opened () ->
+        let k = logical_kind_of_goal_kind kind in
+	let c = SectionLocalDef (pft, tpo, opacity) in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
+	(Local, VarRef id)
+    | Local ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn)
+    | Global ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn) in
+  Pfedit.delete_current_proof ();
+  hook l r;
+  definition_message id
+
+let save_named opacity =
+  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  save id const persistence hook
+
+let check_anonymity id save_ident =
+  if atompart_of_id id <> "Unnamed_thm" then
+    error "This command can only be used for unnamed theorem"
+(*
+    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
+*)
+
+let save_anonymous opacity save_ident =
+  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  save save_ident const persistence hook
+
+let save_anonymous_with_strength kind opacity save_ident =
+  let id,(const,_,hook) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  (* we consider that non opaque behaves as local for discharge *)
+  save save_ident const (Global, Proof kind) hook
+
+let subtac_end_proof = function
+  | Admitted -> admit ()
+  | Proved (is_opaque,idopt) ->
+    if_verbose show_script ();
+    match idopt with
+    | None -> save_named is_opaque
+    | Some ((_,id),None) -> save_anonymous is_opaque id
+    | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
+
+	*)
+let subtac (loc, command) =
+  check_required_library ["Coq";"Init";"Datatypes"];
+  check_required_library ["Coq";"Init";"Specif"];
+  require_library "Coq.subtac.FixSub";
+  try
+    match command with
+	VernacDefinition (defkind, (locid, id), expr, hook) -> 
+	  let env = Global.env () in
+	  let isevars = ref (create_evar_defs Evd.empty) in
+	    (match expr with
+		 ProveBody (bl, c) -> 
+		   let evm, c, ctyp = Interp.subtac_process env isevars id bl c None in
+		     trace (str "Starting proof");
+		     Command.start_proof id goal_kind c hook;
+		     trace (str "Started proof");	     
+		     
+	       | DefineBody (bl, _, c, tycon) -> 
+		   let evm, c, ctyp = Interp.subtac_process env isevars id bl c tycon in
+		   let tac = Eterm.etermtac (evm, c) in 
+		     trace (str "Starting proof");
+		     Command.start_proof id goal_kind ctyp hook;
+		     trace (str "Started proof");
+		     Pfedit.by tac)
+      | VernacFixpoint (l, b) -> 
+	  let _ = trace (str "Building fixpoint") in
+	  ignore(Subtac_command.build_recursive l b)
+      (*| VernacEndProof e -> 
+	  subtac_end_proof e*)
+
+      | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
+  with 
+    | Typing_error e ->
+	msg_warning (str "Type error in Program tactic:");
+	let cmds = 
+	  (match e with
+	     | NonFunctionalApp (loc, x, mux, e) ->
+		 str "non functional application of term " ++ 
+		 e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
+	     | NonSigma (loc, t) ->
+		 str "Term is not of Sigma type: " ++ t
+	     | NonConvertible (loc, x, y) ->
+		 str "Unconvertible terms:" ++ spc () ++
+		   x ++ spc () ++ str "and" ++ spc () ++ y
+	     | IllSorted (loc, t) ->
+		 str "Term is ill-sorted:" ++ spc () ++ t
+	  )
+	in msg_warning cmds
+	     
+    | Subtyping_error e ->
+	msg_warning (str "(Program tactic) Subtyping error:");
+	let cmds = 
+	  match e with
+	    | UncoercibleInferType (loc, x, y) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ x ++ spc () ++ str "and" ++ spc () ++ y
+	    | UncoercibleInferTerm (loc, x, y, tx, ty) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
+		++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
+	    | UncoercibleRewrite (x, y) ->
+		str "Uncoercible terms:" ++ spc ()
+		++ x ++ spc () ++ str "and" ++ spc () ++ y
+	in msg_warning cmds
+    
+    | Type_errors.TypeError (env, e) ->
+	debug 2 (Himsg.explain_type_error env e)
+	  
+    | Pretype_errors.PretypeError (env, e) ->
+	debug 2 (Himsg.explain_pretype_error env e)
+	  
+    | Stdpp.Exc_located (loc, e) ->
+	debug 2 (str "Parsing exception: ");
+	(match e with
+	   | Type_errors.TypeError (env, e) ->
+	       debug 2 (Himsg.explain_type_error env e)
+		 
+	   | Pretype_errors.PretypeError (env, e) ->
+	       debug 2 (Himsg.explain_pretype_error env e)
+
+	   | e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e))
+  
+    | e -> 
+	msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e)
+
+