Procedural: we use the expected type rather than the inferred type when we perform...

we try to beta-reduce the elimination pattern when it does not match the goal/expected type

now nat/compare.ma and Z/z.ma are fully reconstructed :)

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index e736842b71ac8183dd8fa70caf6b1fc55bf8b39c..46d4431bde2b19be822125f269c70df37fbf927f 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -230,14 +230,14 @@ let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
-let mk_fwd_rewrite st dtext name tl direction v t ity =
+let mk_fwd_rewrite st dtext name tl direction v t ity ety =
    let compare premise = function
       | None   -> true
       | Some s -> s = premise
    in
    assert (List.length tl = 6);
    let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
-   let e = Cn.mk_pattern 1 predicate in
+   let e = Cn.mk_pattern 1 ety predicate in
    if (Cn.does_not_occur e) then st, [] else 
    match where with
       | C.ARel (_, _, i, premise) as w ->
@@ -258,10 +258,10 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
         end
       | _                         -> assert false
 
-let mk_rewrite st dtext where qs tl direction t = 
+let mk_rewrite st dtext where qs tl direction t ety = 
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
-   let e = Cn.mk_pattern 1 predicate in
+   let e = Cn.mk_pattern 1 ety predicate in
    let script = [T.Branch (qs, "")] in
    if (Cn.does_not_occur e) then script else
    T.Rewrite (direction, where, None, e, dtext) :: script
@@ -284,17 +284,17 @@ and proc_letin st what name v w t =
       let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
          | Some (C.ALetIn _, _), _ ->
            st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
-        | _, Some (ity, _)        ->
+        | _, Some (ity, ety)        ->
            let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl ->
-                 mk_fwd_rewrite st dtext intro tl true v t ity
+                 mk_fwd_rewrite st dtext intro tl true v t ity ety
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left st hd tl  ->
-                 mk_fwd_rewrite st dtext intro tl false v t ity
+                 mk_fwd_rewrite st dtext intro tl false v t ity ety
               | v                                                        ->
-                 assert (Ut.is_sober st.context (H.cic ity));
-                 let ity = H.acic_bc st.context ity in
+                 assert (Ut.is_sober st.context (H.cic ety));
+                 let ety = H.acic_bc st.context ety in
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+                 st, [T.Branch (qs, ""); T.Cut (intro, ety, dtext)]
            in
            st, C.Decl (H.cic ity), rqv
         | _, None                 ->
@@ -359,17 +359,22 @@ and proc_appl st what hd tl =
            let synth2 = I.S.add 1 synth in
            let names = H.get_ind_names uri tyno in
            let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
-            if List.length qs <> List.length names then
+            let ety = match get_inner_types st what with
+                | Some (_, ety) -> ety 
+                | None          -> 
+                  Cn.fake_annotate "" st.context (get_type "TC3" st what)
+           in
+           if List.length qs <> List.length names then
               let qs = proc_bkd_proofs (next st) synth [] classes tl in
               let b, hd = mk_exp_args hd tl classes synth in
               script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")]
            else if is_rewrite_right st hd then 
-              script2 @ mk_rewrite st dtext where qs tl2 false what
+              script2 @ mk_rewrite st dtext where qs tl2 false what ety
            else if is_rewrite_left st hd then 
-              script2 @ mk_rewrite st dtext where qs tl2 true what
+              script2 @ mk_rewrite st dtext where qs tl2 true what ety
            else
               let predicate = List.nth tl2 (parsno - i) in
-               let e = Cn.mk_pattern j predicate in
+               let e = Cn.mk_pattern j ety predicate in
               let using = Some hd in
               script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
@@ -393,7 +398,12 @@ and proc_case st what uri tyno u v ts =
       let ps, _ = 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 e = Cn.mk_pattern rpsno u in
+      let ety = match get_inner_types st what with
+         | Some (_, ety) -> ety 
+         | None          -> 
+           Cn.fake_annotate "" st.context (get_type "TC4" st what)
+      in
+      let e = Cn.mk_pattern rpsno ety u in
       let text = "" in
       let script = List.rev (mk_arg st v) in
       script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]   

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 8c9a1ddc6f04b6e6bb37e9bd6156f2cebd18482a..f6dd83be313c55c94bb961ba1262a03d00a81e59 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -44,80 +44,91 @@ let rec list_sub start length = function
     
 (* proof construction *******************************************************)
 
-let lift k n =
-   let rec lift_xns k (uri, t) = uri, lift_term k t
-   and lift_ms k = function
+let iter f k =
+   let rec iter_xns k (uri, t) = uri, iter_term k t
+   and iter_ms k = function
       | None   -> None
-      | Some t -> Some (lift_term k t)
-   and lift_fix len k (id, name, i, ty, bo) =
-      id, name, i, lift_term k ty, lift_term (k + len) bo
-   and lift_cofix len k (id, name, ty, bo) =
-      id, name, lift_term k ty, lift_term (k + len) bo
-   and lift_term k = function
+      | Some t -> Some (iter_term k t)
+   and iter_fix len k (id, name, i, ty, bo) =
+      id, name, i, iter_term k ty, iter_term (k + len) bo
+   and iter_cofix len k (id, name, ty, bo) =
+      id, name, iter_term k ty, iter_term (k + len) bo
+   and iter_term k = function
       | C.ASort _ as t -> t
       | C.AImplicit _ as t -> t
       | C.ARel (id, rid, m, b) as t -> 
-         if m < k then t else 
-        if m + n > 0 then C.ARel (id, rid, m + n, b) else
-        begin 
-           HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n);
-           assert false
-        end
-      | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
-      | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
-      | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
-      | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
-      | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
-      | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
-      | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
-      | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
-      | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
-      | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
-      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t)
-      | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
-      | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
+         if m < k then t else f k id rid m b
+      | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (iter_xns k) xnss)
+      | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (iter_xns k) xnss)
+      | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (iter_xns k) xnss)
+      | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (iter_xns k) xnss)
+      | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (iter_ms k) mss)
+      | C.AAppl (id, ts) -> C.AAppl (id, List.map (iter_term k) ts)
+      | C.ACast (id, te, ty) -> C.ACast (id, iter_term k te, iter_term k ty)
+      | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, iter_term k outty, iter_term k t, List.map (iter_term k) pl)
+      | C.AProd (id, n, s, t) -> C.AProd (id, n, iter_term k s, iter_term (succ k) t)
+      | C.ALambda (id, n, s, t) -> C.ALambda (id, n, iter_term k s, iter_term (succ k) t)
+      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, iter_term k ty, iter_term k s, iter_term (succ k) t)
+      | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (iter_fix (List.length fl) k) fl)
+      | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (iter_cofix (List.length fl) k) fl)
    in
-   lift_term k
+   iter_term k
 
-   let fake_annotate id c =
-      let get_binder c m =
-         try match List.nth c (pred m) with
-            | Some (C.Name s, _) -> s
-            | _ -> assert false
-         with
-            | Invalid_argument _ -> assert false
-      in
-      let mk_decl n v = Some (n, C.Decl v) in
-      let mk_def n v ty = Some (n, C.Def (v, ty)) in
-      let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in
-      let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in
-      let rec ann_xns c (uri, t) = uri, ann_term c t
-      and ann_ms c = function
-         | None -> None
-         | Some t -> Some (ann_term c t)
-      and ann_fix newc c (name, i, ty, bo) =
-         id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
-      and ann_cofix newc c (name, ty, bo) =
-         id, name, ann_term c ty, ann_term (List.rev_append newc c) bo
-      and ann_term c = function
-         | C.Sort sort -> C.ASort (id, sort)
-         | C.Implicit ann -> C.AImplicit (id, ann)
-         | C.Rel m -> C.ARel (id, id, m, get_binder c m)
-         | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss)
-         | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss)
-         | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss)
-         | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss)
-         | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss)
-         | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts)
-         | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty)
-         | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
-         | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
-         | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
-         | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t)
-         | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
-         | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
-      in
-      ann_term c
+let lift k n =
+   let f _ id rid m b =
+      if m + n > 0 then C.ARel (id, rid, m + n, b) else
+      begin 
+         HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n);
+        assert false
+      end
+   in
+   iter f k
+
+let subst k v =
+   let f k id rid m b =
+      if m = k then lift 1 (pred k) v else C.ARel (id, rid, pred m, b)
+   in
+   iter f k
+
+let fake_annotate id c =
+   let get_binder c m =
+      try match List.nth c (pred m) with
+         | Some (C.Name s, _) -> s
+         | _ -> assert false
+      with
+         | Invalid_argument _ -> assert false
+   in
+   let mk_decl n v = Some (n, C.Decl v) in
+   let mk_def n v ty = Some (n, C.Def (v, ty)) in
+   let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in
+   let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in
+   let rec ann_xns c (uri, t) = uri, ann_term c t
+   and ann_ms c = function
+      | None -> None
+      | Some t -> Some (ann_term c t)
+   and ann_fix newc c (name, i, ty, bo) =
+      id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
+   and ann_cofix newc c (name, ty, bo) =
+      id, name, ann_term c ty, ann_term (List.rev_append newc c) bo
+   and ann_term c = function
+      | C.Sort sort -> C.ASort (id, sort)
+      | C.Implicit ann -> C.AImplicit (id, ann)
+      | C.Rel m -> C.ARel (id, id, m, get_binder c m)
+      | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss)
+      | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss)
+      | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss)
+      | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss)
+      | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss)
+      | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts)
+      | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty)
+      | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
+      | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
+      | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
+      | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t)
+      | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
+      | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
+   in
+   ann_term c
 
 let mk_arel k = C.ARel ("", "", k, "")
 
@@ -184,8 +195,29 @@ let generalize n =
    in
    gen_term
 
-let mk_pattern psno predicate =
-   clear_absts (generalize psno) psno 0 predicate 
+let convert g ety k predicate =
+   let rec aux = function
+      | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) ->
+         C.ALambda (id, n, aux (b, u), aux (ety, pred))
+      | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) ->
+         C.AProd (id, n, aux (b, u), aux (ety, pred))
+      | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) ->
+         C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred))
+      | C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us ->
+         let map b u = aux (b,u) in
+        C.AAppl (id, List.map2 map bs us)
+      | C.ACast (_, ety, b), C.ACast (id, pred, u) ->
+         C.ACast (id, aux (ety, pred), aux (b, u))
+      | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
+        aux (ety, subst 1 v pred)       
+      | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
+         aux (ety, C.AAppl (id, subst 1 v pred :: vs))
+      | _, pred                                                 -> pred
+   in
+   g k (aux (ety, predicate))
+
+let mk_pattern psno ety predicate =
+   clear_absts (convert (generalize psno) ety) psno 0 predicate 
 
 let get_clears c p xtypes = 
    let meta = C.Implicit None in

diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli
index bc49b9a22cb4cb5658705dbcaabbe359aa92ee95..2108133314393e6f1f79e822e58ee720e1b7d6a0 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.mli
+++ b/helm/software/components/acic_procedural/proceduralConversion.mli
@@ -31,7 +31,7 @@ val lift: int -> int -> Cic.annterm -> Cic.annterm
 
 val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm
 
-val mk_pattern: int -> Cic.annterm -> Cic.annterm
+val mk_pattern: int -> Cic.annterm -> Cic.annterm -> Cic.annterm
 
 val get_clears: 
    Cic.context -> Cic.term -> (Cic.term * Cic.term) option ->