Declarative Proof Language: main commit

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

1 files changed, 90 insertions, 32 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ee4b672a1..48c9238e0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -50,10 +50,10 @@ let norm_goal sigma gl =
   let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   let ngl =
-    { evar_concl = ncl;
-      evar_hyps = map_named_val red_fun gl.evar_hyps; 
-      evar_body = gl.evar_body} in
-  if Evd.eq_evar_info ngl gl then None else Some ngl
+    { gl with 
+	evar_concl = ncl;
+	evar_hyps = map_named_val red_fun gl.evar_hyps } in
+    if Evd.eq_evar_info ngl gl then None else Some ngl
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -91,9 +91,9 @@ let rec frontier p =
     	(List.flatten gll,
          (fun retpfl ->
             let pfl' = mapshape (List.map List.length gll) vl retpfl in
-            { open_subgoals = and_status (List.map pf_status pfl');
-              goal = p.goal;
-              ref = Some(r,pfl')}))
+              { p with
+		  open_subgoals = and_status (List.map pf_status pfl');
+		  ref = Some(r,pfl')}))
 
 
 let rec frontier_map_rec f n p =
@@ -111,9 +111,9 @@ let rec frontier_map_rec f n p =
             (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
             (n,[]) pfl in
         let pfl' = List.rev rpfl' in
-        { open_subgoals = and_status (List.map pf_status pfl');
-          goal = p.goal;
-          ref = Some(r,pfl')}
+        { p with
+	    open_subgoals = and_status (List.map pf_status pfl');
+            ref = Some(r,pfl')}
 
 let frontier_map f n p =
   let nmax = p.open_subgoals in
@@ -137,9 +137,9 @@ let rec frontier_mapi_rec f i p =
             (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
             (i,[]) pfl in
         let pfl' = List.rev rpfl' in
-        { open_subgoals = and_status (List.map pf_status pfl');
-          goal = p.goal;
-          ref = Some(r,pfl')}
+        { p with 
+	    open_subgoals = and_status (List.map pf_status pfl');
+            ref = Some(r,pfl')}
 
 let frontier_mapi f p = frontier_mapi_rec f 1 p
 
@@ -152,10 +152,10 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
 
 (* leaf g is the canonical incomplete proof of a goal g *)
 
-let leaf g = {
-  open_subgoals = 1;
-  goal = g;
-  ref = None }
+let leaf g = 
+  { open_subgoals = 1;
+    goal = g;
+    ref = None }
 
 (* Tactics table. *)
 
@@ -187,15 +187,19 @@ let lookup_tactic s =
 let check_subproof_connection gl spfl =
   list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
 
-let abstract_tactic_expr te tacfun gls =
-  let (sgl_sigma,v) = tacfun gls in
-  let hidden_proof = v (List.map leaf sgl_sigma.it) in
+
+let abstract_operation syntax semantics gls =
+  let (sgl_sigma,validation) = semantics gls in
+  let hidden_proof = validation (List.map leaf sgl_sigma.it) in
   (sgl_sigma,
    fun spfl ->
      assert (check_subproof_connection sgl_sigma.it spfl);
      { open_subgoals = and_status (List.map pf_status spfl);
        goal = gls.it;
-       ref = Some(Tactic(te,hidden_proof),spfl) })
+       ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_tactic_expr te tacfun gls =
+  abstract_operation (Tactic te) tacfun gls	
 
 let refiner = function
   | Prim pr as r ->
@@ -209,8 +213,21 @@ let refiner = function
                goal = goal_sigma.it;
                ref = Some(r,spfl) })))
 
-  | Tactic _ -> failwith "Refiner: should not occur"
+
+  | Nested (_,_) | Decl_proof _ -> 
+      failwith "Refiner: should not occur"
       
+	(* Daimon is a canonical unfinished proof *)
+
+  | Daimon -> 
+      fun gls -> 
+	({it=[];sigma=gls.sigma},  
+	 fun spfl -> 
+	   assert (spfl=[]);
+	   { open_subgoals = 0;
+             goal = gls.it;
+             ref = Some(Daimon,[])})
+
    (* [Local_constraints lc] makes the local constraints be [lc] and
       normalizes evars *)
 
@@ -271,14 +288,16 @@ let extract_open_proof sigma pf =
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
 	  
-    | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
+    | {ref=Some(Nested(_,hidden_proof),spfl)} ->
 	let sgl,v = frontier hidden_proof in
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
-	  
+ 
     | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
+
+    | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
 	  
-    | {ref=None;goal=goal} ->
+    | {ref=(None|Some(Daimon,[]));goal=goal} ->
 	let visible_rels =
           map_succeed
             (fun id ->
@@ -680,9 +699,9 @@ let descend n p =
                        let pf'       = List.hd pfl' in
                        let spfl      = left@(pf'::right) in
                        let newstatus = and_status (List.map pf_status spfl) in
-                       { open_subgoals = newstatus;
-			 goal          = p.goal;
-			 ref           = Some(r,spfl) }
+                       { p with 
+			   open_subgoals = newstatus;
+			   ref           = Some(r,spfl) }
                      else 
 		       error "descend: validation"))
 	     | _ -> assert false)
@@ -699,7 +718,7 @@ let traverse n pts = match n with
 	       tpfsigma = pts.tpfsigma })
   | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
       (match pts.tpf.ref with
-	 | Some (Tactic (_,spf),_) ->
+	 | Some (Nested (_,spf),_) ->
 	     let v = (fun pfl -> pts.tpf) in 
 	     { tpf = spf;
                tstack = (-1,v)::pts.tstack;
@@ -718,10 +737,11 @@ let app_tac sigr tac p =
   sigr := gll.sigma;
   v (List.map leaf gll.it)
 
-(* solve the nth subgoal with tactic tac *)
-let solve_nth_pftreestate n tac pts =
+(* modify proof state at current position *)
+
+let map_pftreestate f pts =
   let sigr = ref pts.tpfsigma in
-  let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+  let tpf' = f sigr pts.tpf in
   let tpf'' =
     if !sigr == pts.tpfsigma then tpf'
     else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
@@ -729,6 +749,12 @@ let solve_nth_pftreestate n tac pts =
     tpfsigma = !sigr;
     tstack   = pts.tstack }
 
+(* solve the nth subgoal with tactic tac *)
+
+let solve_nth_pftreestate n tac =
+  map_pftreestate 
+    (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
+ 
 let solve_pftreestate = solve_nth_pftreestate 1
 
 (* This function implements a poor man's undo at the current goal.
@@ -880,6 +906,38 @@ let prev_unproven pts =
 let rec top_of_tree pts = 
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
+let change_rule f pts =
+  let mark_top _ pt =
+    match pt.ref with
+	Some (oldrule,l) -> 
+	  {pt with ref=Some (f oldrule,l)}
+      | _ -> invalid_arg "change_rule" in
+    map_pftreestate mark_top pts
+
+let match_rule p pts =
+  match (proof_of_pftreestate pts).ref with
+      Some (r,_) -> p r
+    | None -> false
+
+let rec up_until_matching_rule p pts = 
+  if is_top_pftreestate pts then 
+    raise Not_found
+  else
+    let one_up = traverse 0 pts in
+      if match_rule p one_up then 
+	pts
+      else
+	up_until_matching_rule p one_up
+
+let rec up_to_matching_rule p pts = 
+  if match_rule p pts then 
+    pts
+  else
+    if is_top_pftreestate pts then 
+      raise Not_found
+    else
+      let one_up = traverse 0 pts in
+      	up_to_matching_rule p one_up
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}