- Coq/preamble: missing alias added

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b65d131e6a158f8af5d0ccfd495f1e2d96bb40b2..ae64d1f19af4c904e804cd3dd3fd48001c525d9b 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -174,6 +174,19 @@ let get_sub_names head l =
 
 let get_type msg st t = H.get_type msg st.context (H.cic t) 
 
+let clear_absts m =
+   let rec aux k n = function
+      | C.ALambda (id, s, v, t) when k > 0 -> 
+         C.ALambda (id, s, v, aux (pred k) n t)
+      | C.ALambda (_, _, _, t) when n > 0 -> 
+         aux 0 (pred n) (Cn.lift 1 (-1) t)
+      | t                  when n > 0 ->
+         Printf.eprintf "A2P.clear_absts: %u %s\n" n (Pp.ppterm (H.cic t));
+         assert false
+      | t                             -> t
+   in 
+   aux m
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "UNNAMED"
@@ -380,6 +393,26 @@ and proc_appl st what hd tl =
    in
    mk_preamble st what script
 
+and proc_case st what uri tyno u v ts =
+   let proceed, dtext = test_depth st in
+   let script = if proceed then
+      let synth, classes = I.S.empty, Cl.make ts in
+      let names = H.get_ind_names uri tyno in
+      let qs = proc_bkd_proofs (next st) synth names classes ts in
+      let lpsno, _ = H.get_ind_type uri tyno in
+      let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in
+      let _, rps = HEL.split_nth lpsno ps in
+      let rpsno = List.length rps in   
+      let predicate = clear_absts rpsno (1 - sort_disp) u in
+      let e = Cn.mk_pattern rpsno predicate in
+      let text = "" in
+      let script = List.rev (mk_arg st v) in
+      script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]   
+   else
+      [T.Apply (what, dtext)]
+   in
+   mk_preamble st what script
+
 and proc_other st what =
    let _, dtext = test_depth st in
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
@@ -398,13 +431,14 @@ and proc_proof st t =
       {st with context = context}
    in
    match t with
-      | C.ALambda (_, name, w, t) as what   -> proc_lambda (f st) what name w t
-      | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
-      | C.ARel _ as what                    -> proc_rel (f st) what
-      | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what
-      | C.AConst _ as what                  -> proc_const (f st) what
-      | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
-      | what                                -> proc_other (f st) what
+      | C.ALambda (_, name, w, t) as what        -> proc_lambda (f st) what name w t
+      | C.ALetIn (_, name, v, w, t) as what      -> proc_letin (f st) what name v w t
+      | C.ARel _ as what                         -> proc_rel (f st) what
+      | C.AMutConstruct _ as what                -> proc_mutconstruct (f st) what
+      | C.AConst _ as what                       -> proc_const (f st) what
+      | C.AAppl (_, hd :: tl) as what            -> proc_appl (f st) what hd tl
+      | C.AMutCase (_, uri, i, u, v, ts) as what -> proc_case (f st) what uri i u v ts
+      | what                                     -> proc_other (f st) what
 
 and proc_bkd_proofs st synth names classes ts =
 try