]> matita.cs.unibo.it Git - helm.git/commitdiff
GrafiteAstPp: \n's finally fixed
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 29 Apr 2007 15:41:14 +0000 (15:41 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 29 Apr 2007 15:41:14 +0000 (15:41 +0000)
acic_procedural:
 - elimination patterns are generated correctly
 - comments on elimination cases added

helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/acic_procedural/proceduralClassify.mli
helm/software/components/acic_procedural/proceduralConversion.ml
helm/software/components/acic_procedural/proceduralConversion.mli
helm/software/components/acic_procedural/proceduralMode.ml
helm/software/components/acic_procedural/proceduralMode.mli
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/grafite/grafiteAstPp.ml

index c9423268ccb9d144cb1c536ee5cd258307d780b4..ff8aaea883c2541af693c5b19057e5ecb07074b7 100644 (file)
@@ -50,7 +50,8 @@ type status = {
    max_depth: int option;
    depth: int;
    context: C.context;
-   intros: string list
+   intros: string list;
+   case: int list
 }
 
 (* helpers ******************************************************************)
@@ -64,7 +65,7 @@ try
    let before2, after2 = HEL.split_nth n l2 in
    before1, before2, List.hd after1, List.hd after2
 with Invalid_argument _ -> failwith "A2P.split2_last"
-
+   
 let string_of_head = function
    | C.ASort _         -> "sort"
    | C.AConst _        -> "const"
@@ -90,6 +91,18 @@ let next st = {(clear st) with depth = succ st.depth}
 let add st entry intro =
    {st with context = entry :: st.context; intros = intro :: st.intros}
 
+let push st = {st with case = 1 :: st.case}
+
+let inc st =
+   {st with case = match st.case with 
+      | []       -> assert false
+      | hd :: tl -> succ hd :: tl
+   }
+
+let case st str =
+   let case = String.concat "." (List.rev_map string_of_int st.case) in
+   Printf.sprintf "case %s: %s" case str
+
 let test_depth st =
 try   
    let msg = Printf.sprintf "Depth %u: " st.depth in
@@ -119,21 +132,7 @@ let is_fwd_rewrite_left hd tl =
       | C.ARel _ -> true
       | _        -> false
    else false
-(*
-let get_ind_name uri tno xcno =
-try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
-      | C.InductiveDefinition (ts, _, _,_), _ -> ts 
-      | _                                     -> assert false
-   in
-   let tname, cs = match List.nth ts tno with
-      | (name, _, _, cs) -> name, cs
-   in
-   match xcno with
-      | None     -> tname
-      | Some cno -> fst (List.nth cs (pred cno))
-with Invalid_argument _ -> failwith "A2P.get_ind_name"
-*)
+
 let get_inner_types st v =
 try
    let id = Ut.id_of_annterm v in
@@ -163,7 +162,17 @@ let get_entry st id =
       | _ :: tl                                   -> aux tl
    in
    aux st.context
-   
+
+let get_ind_names uri tno =
+try   
+   let ts = match E.get_obj Un.empty_ugraph uri with
+      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
+      | _                                      -> assert false
+   in
+   match List.nth ts tno with
+      | (_, _, _, cs) -> List.map fst cs  
+with Invalid_argument _ -> failwith "A2P.get_ind_names"
+
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
@@ -185,7 +194,7 @@ let convert st ?name v =
    match get_inner_types st v with
       | None            -> []
       | Some (sty, ety) ->
-        let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
+        let e = Cn.hole "" in
          let csty, cety = cic sty, cic ety in
         if Ut.alpha_equivalence csty cety then [] else 
         match name with
@@ -278,39 +287,40 @@ and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
       let ty = get_type "TC2" st hd in
-      let (classes, rc) as h = Cl.classify st.context ty in
+      let classes, rc = Cl.classify st.context ty in
       let goal_arity = match get_inner_types st what with
          | None          -> 0
         | Some (ity, _) -> snd (PEH.split_with_whd (st.context, cic ity))
       in
-      let argsno = List.length classes in
-      let decurry = argsno - List.length tl in
+      let parsno, argsno = List.length classes, List.length tl in
+      let decurry = parsno - argsno in
       let diff = goal_arity - decurry in
       if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
       let rec mk_synth a n =
          if n < 0 then a else mk_synth (I.S.add n a) (pred n)
       in
       let synth = mk_synth I.S.empty decurry in
-      let text = "" (* Printf.sprintf "%u %s" argsno (Cl.to_string h) *) in
+      let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
       let script = List.rev (mk_arg st hd) @ convert st what in
       match rc with
-         | Some (i, j) ->
+         | Some (i, j, uri, tyno) ->
            let classes, tl, _, where = split2_last classes tl in
            let script = List.rev (mk_arg st where) @ script in
            let synth = I.S.add 1 synth in
-           let qs = proc_bkd_proofs (next st) synth classes tl in
+           let names = get_ind_names uri tyno in
+           let qs = proc_bkd_proofs (next st) synth names classes tl in
             if is_rewrite_right hd then 
               script @ mk_rewrite st dtext where qs tl false
            else if is_rewrite_left hd then 
               script @ mk_rewrite st dtext where qs tl true
            else
-              let predicate = List.nth tl (argsno - i) in
-               let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
+              let predicate = List.nth tl (parsno - i) in
+               let e = Cn.mk_pattern j predicate in
               let using = Some hd in
               script @
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
-           let qs = proc_bkd_proofs (next st) synth classes tl in
+           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, "")]
    else
@@ -331,15 +341,29 @@ and proc_proof st = function
    | C.AAppl (_, hd :: tl) as what    -> proc_appl st what hd tl
    | what                             -> proc_other st what
 
-and proc_bkd_proofs st synth classes ts =
+and proc_bkd_proofs st synth names classes ts =
 try 
+   let get_note =
+      let names = ref (names, push st) in
+      fun f -> 
+         match !names with 
+           | [], st       -> fun _ -> f st
+           | "" :: tl, st -> names := tl, st; fun _ -> f st
+           | hd :: tl, st -> 
+              let note = case st hd in
+              names := tl, inc st; 
+              fun b -> if b then T.Note note :: f st else f st
+   in
    let _, dtext = test_depth st in   
    let aux (inv, _) v =
       if I.overlaps synth inv then None else
-      if I.S.is_empty inv then Some (proc_proof st v) else
-      Some [T.Apply (v, dtext ^ "dependent")]
+      if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else
+      Some (fun _ -> [T.Apply (v, dtext ^ "dependent")])
    in  
-   List.rev (T.list_map2_filter aux classes ts)
+   let ps = T.list_map2_filter aux classes ts in
+   let b = List.length ps > 1 in
+   List.rev_map (fun f -> f b) ps
+
 with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
@@ -353,7 +377,7 @@ let proc_obj st = function
       let ast = proc_proof st v in
       let count = T.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
-      T.Theorem (s, t, text) :: ast @ [T.Qed ""]
+      T.Theorem (s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 
@@ -367,7 +391,8 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       max_depth = depth;
       depth     = 0;
       context   = [];
-      intros    = []
+      intros    = [];
+      case      = []
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in
index 4f9f99fcee76117056a100bd8f1a13dfb9fcfd24..755176e5c50cc4d4d280fcee4b373089ebbcb485 100644 (file)
@@ -23,6 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module UM  = UriManager
 module C   = Cic
 module D   = Deannotate
 module I   = CicInspect
@@ -32,7 +33,7 @@ module H   = ProceduralHelpers
 
 type dependence = I.S.t * bool
 
-type conclusion = (int * int) option
+type conclusion = (int * int * UM.uri * int) option
 
 (* debugging ****************************************************************)
 
@@ -43,8 +44,8 @@ let string_of_entry (inverse, b) =
 let to_string (classes, rc) =
    let linearize = String.concat " " (List.map string_of_entry classes) in
    match rc with
-      | None        -> linearize
-      | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
+      | None              -> linearize
+      | Some (i, j, _, _) -> Printf.sprintf "%s %u %u" linearize i j
 
 let out_table b =
    let map i (_, inverse) =
@@ -67,11 +68,11 @@ let classify_conclusion vs =
    let inside i = i > 1 && i <= List.length vs in
    match vs with
       | v0 :: v1 :: _ ->
-         let hd0, argsno0 = get_argsno v0 in
-        let hd1, argsno1 = get_argsno v1 in
+         let hd0, a0 = get_argsno v0 in
+        let hd1, a1 = get_argsno v1 in
         begin match hd0, hd1 with
-           | C.Rel i, C.MutInd _ when inside i -> Some (i, argsno0)
-           | _                                 -> None
+           | C.Rel i, C.MutInd (u, n, _) when inside i -> Some (i, a0, u, n)
+           | _                                         -> None
         end
       | _             -> None
  
index 9e478ca622c595cdb40d905f031f2c906674a029..aea3c6e8164dd1af743670cfd959a6d6d29a3997 100644 (file)
@@ -25,7 +25,7 @@
 
 type dependence = CicInspect.S.t * bool
 
-type conclusion = (int * int) option
+type conclusion = (int * int * UriManager.uri * int) option
 
 val classify: Cic.context -> Cic.term -> dependence list * conclusion
 
index 53898136940f369667b3625e126d5171690c61aa..80aae9e7f3668b83fcee3378d7cb148174b5c31c 100644 (file)
@@ -115,7 +115,7 @@ let generalize n =
       | C.AMutConstruct (id, _, _, _, _)
       | C.AMeta (id, _, _) -> meta id
       | C.ARel (id, _, m, _) -> 
-         if m = succ (k - n) then hole id else meta id
+         if succ (k - n) <= m && m <= k then hole id else meta id
       | C.AAppl (id, ts) -> 
          let ts = List.map (gen_term k) ts in
          if is_meta ts then meta id else C.AAppl (id, ts)
@@ -139,6 +139,6 @@ let generalize n =
    in
    gen_term 0
 
-let mk_pattern rpsno predicate =
-   let body = generalize rpsno predicate in
-   clear_absts 0 rpsno body
+let mk_pattern psno predicate =
+   let body = generalize psno predicate in
+   clear_absts 0 psno body
index 5cbb75da26efc3d86b70fd5142f1e37c1adc6f29..769cf3b9d08428baabf72ce7cd719ddc36f44d2c 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+val meta: Cic.id -> Cic.annterm
+
+val hole: Cic.id -> Cic.annterm
+
 val lift: int -> int -> Cic.annterm -> Cic.annterm
 
 val mk_pattern: int -> Cic.annterm -> Cic.annterm
index d2ddc6c9847c37d0c25dba76cc9a4dde0c9de096..e13846fc85a3ddee2b6dbb4f805be0ab7fac1de6 100644 (file)
@@ -51,7 +51,7 @@ let bkd c t =
    let classes, rc = Cl.classify c t in
    let premises, _ = PEH.split_with_whd (c, t) in
    match rc with
-      | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true
+      | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true
       | _ ->
          let _, conclusion = List.hd premises in
          is_appl true conclusion
index b55188600b80e6f433aef57e5ce5c852bee991c0..71356b6ff20daadba90ab9de4c67733474537416 100644 (file)
@@ -22,7 +22,8 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
-
+(*
 val is_eliminator: (Cic.context * Cic.term) list -> bool
 
 val bkd: Cic.context -> Cic.term -> bool
+*)
index ae153fe3d1d5b2b3abbe25f2c5bbd33ec8b49368..a1d120f807a161ac7aeb472e17d5518a63f28dcf 100644 (file)
@@ -45,6 +45,10 @@ let list_map2_filter map l1 l2 =
   in 
   filter [] (list_rev_map2 map l1 l2)
 
+let list_init f i =
+   let rec aux a j = if j < 0 then a else aux (f j :: a) (pred j) in
+   aux [] i
+
 (****************************************************************************)
 
 type name     = string
@@ -81,8 +85,14 @@ let floc = H.dummy_floc
 
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
-let mk_nlnote str a =
-   if str = "" then mk_note "" :: a else mk_note str :: mk_note "" :: a
+let mk_tacnote str a =
+   if str = "" then mk_note "" :: a else mk_note "" :: mk_note str :: a
+
+let mk_notenote str a =
+   if str = "" then a else mk_note str :: a
+
+let mk_thnote str a =
+   if str = "" then a else mk_note "" :: mk_note str :: a
 
 let mk_theorem name t = 
    let obj = N.Theorem (`Theorem, name, t, None) in
@@ -158,22 +168,22 @@ let mk_vb = G.Shift floc
 (* rendering ****************************************************************)
 
 let rec render_step sep a = function
-   | Note s                  -> mk_note s :: a
-   | Theorem (n, t, s)       -> mk_theorem n t :: mk_note s :: a 
-   | Qed s                   -> mk_qed :: mk_nlnote s a
-   | Id s                    -> mk_id sep :: mk_nlnote s a
-   | Intros (c, ns, s)       -> mk_intros c ns sep :: mk_nlnote s a
-   | Cut (n, t, s)           -> mk_cut n t sep :: mk_nlnote s a
-   | LetIn (n, t, s)         -> mk_letin n t sep :: mk_nlnote s a
-   | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_nlnote s a
-   | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_nlnote s a
-   | Apply (t, s)            -> mk_apply t sep :: mk_nlnote s a
-   | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_nlnote s a
-   | ClearBody (n, s)        -> mk_clearbody n sep :: mk_nlnote s a
+   | Note s                  -> mk_notenote s a
+   | Theorem (n, t, s)       -> mk_theorem n t :: mk_thnote s a 
+   | Qed s                   -> mk_qed :: mk_tacnote s a
+   | Id s                    -> mk_id sep :: mk_tacnote s a
+   | Intros (c, ns, s)       -> mk_intros c ns sep :: mk_tacnote s a
+   | Cut (n, t, s)           -> mk_cut n t sep :: mk_tacnote s a
+   | LetIn (n, t, s)         -> mk_letin n t sep :: mk_tacnote s a
+   | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
+   | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_tacnote s a
+   | Apply (t, s)            -> mk_apply t sep :: mk_tacnote s a
+   | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_tacnote s a
+   | ClearBody (n, s)        -> mk_clearbody n sep :: mk_tacnote s a
    | Branch ([], s)          -> a
    | Branch ([ps], s)        -> render_steps sep a ps
    | Branch (ps :: pss, s)   ->      
-      let a = mk_ob :: mk_nlnote s a in
+      let a = mk_ob :: mk_tacnote s a in
       let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in
       mk_punctation sep :: render_steps mk_cb a ps
 
index 3602e9df526ad60c25e27500baca1ba1bb9c6cab..67f771fbe5e45d23e7aa1fb99d941091c6d2b52b 100644 (file)
@@ -305,9 +305,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
   | Note (_,"") -> Printf.sprintf "\n"
-  | Note (_,str) -> Printf.sprintf "(* %s *)\n" str
+  | Note (_,str) -> Printf.sprintf "\n(* %s *)" str
   | Code (_,code) ->
-      Printf.sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+      Printf.sprintf "\n(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function