X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Fprocedural1.ml;h=a0c0331f38351a44ea6cc1154c24961c3a597c94;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=b3e11285049dde07d36b3c1b064f90dca9934a38;hpb=df3e9efe1690fb5d93061b657e6ddcc3c11745db;p=helm.git diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml index b3e112850..a0c0331f3 100644 --- a/helm/software/components/acic_procedural/procedural1.ml +++ b/helm/software/components/acic_procedural/procedural1.ml @@ -45,7 +45,6 @@ module Cl = ProceduralClassify module T = ProceduralTypes module Cn = ProceduralConversion module H = ProceduralHelpers -module X = ProceduralTeX type status = { sorts : (C.id, A.sort_kind) Hashtbl.t; @@ -140,14 +139,16 @@ try | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st) with Not_found -> None with Invalid_argument _ -> failwith "A2P.get_inner_types" -(* -let get_inner_sort st v = + +let is_proof st v = try let id = Ut.id_of_annterm v in - try Hashtbl.find st.sorts id - with Not_found -> `Type (CicUniv.fresh()) -with Invalid_argument _ -> failwith "A2P.get_sort" -*) + try match Hashtbl.find st.sorts id with + | `Prop -> true + | _ -> false + with Not_found -> H.is_proof st.context (H.cic v) +with Invalid_argument _ -> failwith "P1.is_proof" + let get_entry st id = let rec aux = function | [] -> assert false @@ -197,13 +198,14 @@ let mk_exp_args hd tl classes synth = let map v (cl, b) = if I.overlaps synth cl && b then v else meta "" in - let rec aux = function - | [] -> [] - | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl) + let rec aux b = function + | [] -> b, [] + | hd :: tl -> + if hd = meta "" then aux true tl else b, List.rev (hd :: tl) in let args = T.list_rev_map2 map tl classes in - let args = aux args in - if args = [] then hd else C.AAppl ("", hd :: args) + let b, args = aux false args in + if args = [] then b, hd else b, C.AAppl ("", hd :: args) let mk_convert st ?name sty ety note = let e = Cn.hole "" in @@ -240,8 +242,9 @@ let get_intro = function | C.Anonymous -> None | C.Name s -> Some s -let mk_preamble st what script = - convert st what @ script +let mk_preamble st what script = match script with + | T.Exact _ :: _ -> script + | _ -> convert st what @ script let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what @@ -269,7 +272,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = assert (Ut.is_sober st.context (H.cic ity)); let ity = H.acic_bc st.context ity in let br1 = [T.Id ""] in - let br2 = List.rev (T.Apply (w, "assumption") :: script None) in + let br2 = List.rev (T.Exact (w, "assumption") :: script None) in let text = "non-linear rewrite" in st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)] end @@ -319,24 +322,24 @@ and proc_letin st what name v w t = let qt = proc_proof (next (add st entry)) t in List.rev_append rqv qt else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script and proc_rel st what = let _, dtext = test_depth st in let text = "assumption" in - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_mutconstruct st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_const st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_appl st what hd tl = @@ -363,6 +366,7 @@ and proc_appl st what hd tl = let synth = mk_synth I.S.empty decurry in let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in let script = List.rev (mk_arg st hd) in + let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in match rc with | Some (i, j, uri, tyno) -> let classes2, tl2, _, where = split2_last classes tl in @@ -372,8 +376,8 @@ and proc_appl st what hd tl = let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in if List.length qs <> List.length names then let qs = proc_bkd_proofs (next st) synth [] classes tl in - let hd = mk_exp_args hd tl classes synth in - script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + 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 hd then script2 @ mk_rewrite st dtext where qs tl2 false what else if is_rewrite_left hd then @@ -387,10 +391,10 @@ and proc_appl st what hd tl = | None -> let names = get_sub_names hd tl in let qs = proc_bkd_proofs (next st) synth names classes tl in - let hd = mk_exp_args hd tl classes synth in - script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + let b, hd = mk_exp_args hd tl classes synth in + script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script @@ -410,14 +414,14 @@ and proc_case st what uri tyno u v ts = let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (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 - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_proof st t = @@ -457,7 +461,7 @@ try let aux (inv, _) v = if I.overlaps synth inv then None else if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else - Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")])) + Some (get_note (fun _ -> [T.Exact (v, dtext ^ "dependent")])) in let ps = T.list_map2_filter aux classes ts in let b = List.length ps > 1 in @@ -472,9 +476,10 @@ let th_flavours = [`Theorem; `Lemma; `Remark; `Fact] let def_flavours = [`Definition] -let get_flavour ?flavour attrs = +let get_flavour ?flavour st v attrs = let rec aux = function - | [] -> List.hd th_flavours + | [] -> + if is_proof st v then List.hd th_flavours else List.hd def_flavours | `Flavour fl :: _ -> fl | _ :: tl -> aux tl in @@ -484,7 +489,7 @@ let get_flavour ?flavour attrs = let proc_obj ?flavour ?(info="") st = function | C.AConstant (_, _, s, Some v, t, [], attrs) -> - begin match get_flavour ?flavour attrs with + begin match get_flavour ?flavour st v attrs with | flavour when List.mem flavour th_flavours -> let ast = proc_proof st v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in