]> matita.cs.unibo.it Git - helm.git/commitdiff
Procedural: "ByInduction" method ok
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 19 Dec 2006 19:21:36 +0000 (19:21 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 19 Dec 2006 19:21:36 +0000 (19:21 +0000)
GrafiteAstPp: letin tactic now works

helm/software/components/content_pres/content2Procedural.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/matita/contribs/prova.ma

index 6d64a0ef80e10ecc1940dc3774d0233d568d07c2..9be504913fc0ffcb628349d0dd30b76218138dd9 100644 (file)
@@ -24,6 +24,7 @@
  *)
 
 module H = HExtlib
+module U = UriManager
 module C = Content
 module G = GrafiteAst
 module N = CicNotationPt
@@ -35,6 +36,18 @@ let rec list_split n l =
    let l1, l2 = list_split (pred n) (List.tl l) in
    List.hd l :: l1, l2
 
+let cont sep a = match sep with 
+   | None     -> a
+   | Some sep -> sep :: a
+
+let list_rev_map_concat map sep a l =
+   let rec aux a = function
+      | []          -> a
+      | [x]         -> map a x
+      | x :: y :: l -> aux (sep :: map a x) (y :: l)  
+   in
+   aux a l
+
 (****************************************************************************)
 
 type name  = string
@@ -48,14 +61,19 @@ type step = Note of note
           | Qed of note
          | Intros of count option * name list * note
          | Elim of what * using option * note
+         | LetIn of name * what * note
          | Exact of what * note
          | Branch of step list list * note
 
+(* annterm constructors *****************************************************)
+
+let mk_arel i b = Cic.ARel ("", "", i, b)
+
 (* level 2 transformation ***************************************************)
 
 let mk_name = function
    | Some name -> name
-   | None      -> "_"
+   | None      -> "UNUSED" (**)
 
 let mk_intros_arg = function
    | `Declaration {C.dec_name = name}
@@ -70,17 +88,44 @@ let split_inductive n tl =
    let l1, l2 = list_split (int_of_string n) tl in
    List.hd (List.rev l2), l1
 
-let mk_what rpac = function
+let rec mk_apply_term aref ac ds cargs =
+   let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in
+   let _, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
+   Cic.AAppl (aref, List.rev row), ds 
+
+and mk_delta p ds =
+   let cmethod = p.C.proof_conclude.C.conclude_method in
+   let cargs = p.C.proof_conclude.C.conclude_args in
+   let capply = p.C.proof_apply_context in
+   let ccont = p.C.proof_context in
+   let caref = p.C.proof_conclude.C.conclude_aref in
+   match cmethod with
+      | "Exact"
+      | "Apply" when ccont = [] ->
+         let what, ds = mk_apply_term caref capply ds cargs in
+        let name = "PREVIOUS" in
+        mk_arel 1 name, LetIn (name, what, "") :: ds
+      | _ -> mk_arel 1 "COMPOUND", ds
+
+and mk_arg first (ac, row, ds) = function
+   | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} ->
+      ac, Cic.AConst (aref, U.uri_of_string uri, []) :: row, ds 
    | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} -> 
-      Cic.ARel ("", "", i, b)
+      ac, mk_arel i b :: row, ds
    | C.Premise {C.premise_n = None; C.premise_binder = None} -> 
-      Cic.ARel ("", "", 1, "COMPOUND")
-   | C.Term t -> t
-   | C.Premise _   -> assert false
-   | C.ArgMethod _ -> assert false
-   | C.ArgProof _  -> assert false
-   | C.Lemma _     -> assert false
-   | C.Aux _       -> assert false
+      begin match first, ac with
+         | _, hd :: tl -> 
+           let arg, ds = mk_delta hd ds in 
+           tl, arg :: row, ds
+        | false, []   -> ac, Cic.AImplicit ("", None) :: row, ds
+         | _           -> assert false
+      end
+   | C.Term t when first -> ac, t :: row, ds
+   | C.Term _            -> ac, Cic.AImplicit ("", None) :: row, ds
+   | C.Premise _         -> assert false
+   | C.ArgMethod _       -> assert false
+   | C.ArgProof _        -> assert false
+   | C.Aux _             -> assert false
 
 let rec mk_proof p =
    let names = mk_intros_args p.C.proof_context in
@@ -95,12 +140,14 @@ and mk_proof_body p =
    match cmethod, cargs with
       | "Intros+LetTac", [C.ArgProof p] -> mk_proof p 
       | "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
-        let rpac = List.rev capply in
         let whatm, ms = split_inductive n tl in (* actual rx params here *)
-         let what, qs = mk_what rpac whatm, List.map mk_subproof ms in
-        [Elim (what, Some using, ""); Branch (qs, "")] 
+         let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in
+        let what, qs = List.hd row, List.map mk_subproof ms in
+        List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")] 
       | _ ->  
-        [Note (Printf.sprintf "%s %u" cmethod (List.length cargs))] 
+        let text = 
+           Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs)
+        in [Note text] 
 
 and mk_subproof = function
    | C.ArgProof ({C.proof_name = Some n} as p) -> Note n :: mk_proof p
@@ -138,6 +185,10 @@ let mk_elim what using =
    let tactic = G.Elim (floc, what, using, Some 0, []) in
    mk_tactic tactic
 
+let mk_letin name what =
+   let tactic = G.LetIn (floc, what, name) in
+   mk_tactic tactic
+
 let mk_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
@@ -154,46 +205,36 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
 
 (* rendering ****************************************************************)
 
-let cont sep a = match sep with 
-   | None     -> a
-   | Some sep -> sep :: a
-
-let list_rev_map_concat map sep a l =
-   let rec aux a = function
-      | []          -> a
-      | [x]         -> map a x
-      | x :: y :: l -> aux (sep :: map a x) (y :: l)  
-   in
-   aux a l
-
 let rec render_step sep a = function
    | Note s            -> mk_note s :: a
    | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a 
    | Qed s             -> mk_note s :: mk_qed :: a
    | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
    | Elim (t, xu, s)   -> mk_note s :: cont sep (mk_elim t xu :: a)
+   | LetIn (n, t, s)   -> mk_note s :: cont sep (mk_letin n t :: a)
    | Exact (t, s)      -> mk_note s :: cont sep (mk_exact t :: a)
-(*   | Branch ([], s)    -> mk_note s :: cont sep a
-   | Branch ([ps], s)  -> mk_note s :: cont sep (render_steps a ps)
-*)   | Branch (pss, s)   ->
+   | Branch ([], s)    -> a
+   | Branch ([ps], s)  -> render_steps a ps
+   | Branch (pss, s)   ->
       let a =  mk_ob :: a in
       let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
       mk_note s :: cont sep body
 
 and render_steps a = function
-   | []                                      -> a
-   | [p]                                     -> render_step None a p
-   | (Note _ | Theorem _ | Qed _ as p) :: ps ->
+   | []                                          -> a
+   | [p]                                         -> render_step None a p
+   | (Note _ | Theorem _ | Qed _ as p) :: ps     ->
       render_steps (render_step None a p) ps 
-   | p :: ((Branch _ :: _) as ps)            ->
+   | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
       render_steps (render_step (Some mk_sc) a p) ps
-   | p :: ps                                 ->
+   | p :: ps                                     ->
       render_steps (render_step (Some mk_dot) a p) ps
 
 (* interface functions ******************************************************)
 
 let content2procedural ~ids_to_inner_sorts prefix cobj = 
-   prerr_endline "Phase 2 transformation";
+   prerr_endline "Level 2 transformation";
    let steps = mk_obj ids_to_inner_sorts prefix cobj in
    prerr_endline "grafite rendering";
    List.rev (render_steps [] steps)
+
index fea47d15ba12df4e956c2ce291b778c0e2393ca7..840c16351f86823aeef0bc25d18acda1fcdd1b30 100644 (file)
@@ -140,7 +140,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
-  | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
+  | LetIn (_, term, ident) -> sprintf "letin %s \\def %s" ident (term_pp term)
   | Reduce (_, kind, pat) ->
       sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
index 84331106d1f5587ef774bc80db7359115f5e160a..1b817c38e4a9920d9dea5919376dd2cb8c350e19 100644 (file)
@@ -21,6 +21,11 @@ alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
 alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
 alias id "pr0_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0_ind.con".
+alias id "subst0_gen_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_head.con".
+alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con".
+alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
+alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
+alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con".
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".