oblivion ugraph everywhere outside the kernel

[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 f39aa18bd96ee3a162baa10fa6da07ca3b6f8805..e71f443d9cefa3c79fb87a2294099270cab019ed 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -167,7 +167,7 @@ let get_entry st id =
 
 let get_ind_names uri tno =
 try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
+   let ts = match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (ts, _, _, _), _ -> ts 
       | _                                      -> assert false
    in
@@ -198,7 +198,10 @@ let mk_convert st ?name sty ety note =
    let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
       note (Pp.ppterm csty) (Pp.ppterm cety)
    in
+   assert (Ut.is_sober csty); 
+   assert (Ut.is_sober cety);
    if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
+   let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
       | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
       | Some (id, i) -> 
@@ -266,7 +269,7 @@ let mk_rewrite st dtext where qs tl direction t =
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
-      | None          -> true
+      | None          -> false
       | Some (it, et) -> 
          DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in
@@ -279,7 +282,7 @@ let rec proc_lambda st name v t =
    let intro = get_intro name in
    proc_proof (add st entry intro) t
 
-and proc_letin st what name v t =
+and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
@@ -292,11 +295,12 @@ and proc_letin st what name v t =
                  mk_fwd_rewrite st dtext intro tl false v
               | v                                                     ->
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+                 let ity = H.acic_bc st.context ity in
+                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
            st, C.Decl (H.cic ity), rqv
         | None          ->
-           st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
+           st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -317,6 +321,11 @@ and proc_mutconstruct st what =
    let script = [T.Apply (what, dtext)] in 
    mk_intros st what script
 
+and proc_const st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st what script
+
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
@@ -380,12 +389,13 @@ and proc_proof st t =
       {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
-      | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
-      | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t
-      | C.ARel _ as what                 -> proc_rel (f st) what
-      | C.AMutConstruct _ as what        -> proc_mutconstruct (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)           -> proc_lambda st 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
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -414,7 +424,8 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =   
+let is_theorem pars =
+   pars = [] ||
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars