- doubleTypeInference: we check for unreferenced letins in the inferred type also...

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

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index 777ccd5f5101b797f2cb92a48e53cb0c83bc2c7d..06fc9b35843bf330a0020cd836acd47d443e52aa 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -57,7 +57,7 @@ type status = {
    case     : int list
 }
 
-let debug = ref false
+let debug = ref true
 
 (* helpers ******************************************************************)
 
@@ -135,8 +135,8 @@ let get_inner_types st v =
 try
    let id = Ut.id_of_annterm v in
    try match Hashtbl.find st.types id with
-      | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
-      | {A.annsynthesized = st; A.annexpected = None}    -> Some (st, st)
+      | {A.annsynthesized = ity; A.annexpected = Some ety} -> Some (ity, ety)
+      | {A.annsynthesized = ity; A.annexpected = None}     -> Some (ity, ity)
    with Not_found -> None
 with Invalid_argument _ -> failwith "P2.get_inner_types"
 
@@ -289,15 +289,20 @@ let mk_fwd_rewrite st dtext name tl direction v t ity ety =
         end
       | _                         -> assert false
 
-let mk_rewrite st dtext where qs tl direction t ety = 
+let mk_rewrite st dtext where qs tl direction t ity = 
+   let ppterm t = 
+      let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a
+   in 
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
-   let e = Cn.mk_pattern 1 ety predicate in
+   let dtext = if !debug then dtext ^ ppterm (H.cic predicate) else dtext in
+   let e = Cn.mk_pattern 1 ity 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
 
 let rec proc_lambda st what name v t =
+   let dtext = if !debug then CicPp.ppcontext st.context else "" in
    let name = match name with
       | C.Anonymous -> H.mk_fresh_name true st.context anonymous_premise
       | name        -> name
@@ -305,7 +310,7 @@ let rec proc_lambda st what name v t =
    let entry = Some (name, C.Decl (H.cic v)) in
    let intro = get_intro name in
    let script = proc_proof (add st entry) t in
-   let script = T.Intros (Some 1, [intro], "") :: script in
+   let script = T.Intros (Some 1, [intro], dtext) :: script in
    mk_preamble st what script
 
 and proc_letin st what name v w t =
@@ -367,9 +372,9 @@ and proc_appl st what hd tl =
       in
       let classes, rc = Cl.classify st.context ty in
       let goal_arity, goal = match get_inner_types st what with
-         | None            -> 0, None
-        | Some (ity, ety) -> 
-          snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ety)
+         | None          -> 0, None
+        | Some (ity, _) -> 
+          snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ity)
       in
       let parsno, argsno = List.length classes, List.length tl in
       let decurry = parsno - argsno in
@@ -397,8 +402,8 @@ 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
-            let ety = match get_inner_types st what with
-                | Some (_, ety) -> ety 
+            let ity = match get_inner_types st what with
+                | Some (ity, _) -> ity 
                 | None          -> 
                   Cn.fake_annotate "" st.context (get_type "TC3" st what)
            in
@@ -407,12 +412,12 @@ and proc_appl st what hd tl =
               let b, hd, qs = mk_exp_args hd tl classes synth qs 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 ety
+              script2 @ mk_rewrite st dtext where qs tl2 false what ity
            else if is_rewrite_left st hd then 
-              script2 @ mk_rewrite st dtext where qs tl2 true what ety
+              script2 @ mk_rewrite st dtext where qs tl2 true what ity
            else
               let predicate = List.nth tl2 (parsno - i) in
-               let e = Cn.mk_pattern j ety predicate in
+               let e = Cn.mk_pattern j ity predicate in
               let using = Some hd in
               script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
@@ -436,12 +441,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 ety = match get_inner_types st what with
-         | Some (_, ety) -> ety 
+      let ity = match get_inner_types st what with
+         | Some (ity, _) -> ity 
          | None          -> 
            Cn.fake_annotate "" st.context (get_type "TC4" st what)
       in
-      let e = Cn.mk_pattern rpsno ety u in
+      let e = Cn.mk_pattern rpsno ity u in
       let text = "" in
       let script = List.rev (mk_arg st v) in
       script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]   
@@ -458,14 +463,17 @@ and proc_other st what =
 
 and proc_proof st t = 
    let f st =
+(*      
       let xtypes, note = match get_inner_types st t with
          | Some (it, et) -> Some (H.cic it, H.cic et), 
          (Printf.sprintf "\nInferred: %s\nExpected: %s"
          (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
-      in
-      let context, _clears = Cn.get_clears st.context (H.cic t) xtypes in
+      in    
+      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       {st with context = context}
+*)
+      st
    in
    match t with
       | C.ALambda (_, name, w, t) as what        -> proc_lambda (f st) what name w t