X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=483378ce6c47f6f6df337687d71e133624bf9bd3;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=9815580b6444ef8bb31669e0fd60aaae5cebb60b;hpb=797f61edb93f41eb2c5e281bc9457f6bff633063;p=helm.git diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 9815580b6..483378ce6 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -54,7 +54,8 @@ type status = { intros: string option list; clears: string list; clears_note: string; - case: int list + case: int list; + skip_thm_and_qed : bool; } (* helpers ******************************************************************) @@ -197,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) -> @@ -249,7 +253,7 @@ let mk_fwd_rewrite st dtext name tl direction t = match where with | C.ARel (_, _, i, premise) as v -> let where = Some (premise, name) in - let _script = convert_elim st ~name:(premise, i) t v e in +(* let _script = convert_elim st ~name:(premise, i) t v e in *) let script = mk_arg st what @ mk_arg st v (* @ script *) in let st = {st with context = Cn.clear st.context premise} in st, T.Rewrite (direction, what, where, e, dtext) :: script @@ -259,13 +263,13 @@ let mk_rewrite st dtext where qs tl direction t = assert (List.length tl = 5); let predicate = List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in - let script = convert_elim st t t e in + let script = [] (* convert_elim st t t e *) in script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")] 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 @@ -278,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 @@ -291,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 @@ -350,7 +355,7 @@ and proc_appl st what hd tl = let predicate = List.nth tl (parsno - i) in let e = Cn.mk_pattern j predicate in let using = Some hd in - convert_elim st what what e @ script @ + (* convert_elim st what what e @ *) script @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth [] classes tl in @@ -376,15 +381,15 @@ and proc_proof st t = in let context, clears = Cn.get_clears st.context (H.cic t) xtypes in let note = Pp.ppcontext st.context ^ note in - {st with context = context; clears = clears; clears_note = note} + {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.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 @@ -422,13 +427,15 @@ let proc_obj st = function let ast = proc_proof st v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in - T.Theorem (Some s, t, "") :: ast @ [T.Qed text] + if st.skip_thm_and_qed then ast + else T.Theorem (Some s, t, "") :: ast @ [T.Qed text] | _ -> failwith "not a theorem" (* interface functions ******************************************************) -let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = +let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth +?(skip_thm_and_qed=false) prefix aobj = let st = { sorts = ids_to_inner_sorts; types = ids_to_inner_types; @@ -439,7 +446,8 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = intros = []; clears = []; clears_note = ""; - case = [] + case = []; + skip_thm_and_qed = skip_thm_and_qed; } in HLog.debug "Procedural: level 2 transformation"; let steps = proc_obj st aobj in