helm/software/components/acic_procedural/proceduralHelpers.ml

   1 (* Copyright (C) 2003-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module C    = Cic
  27 module Rf   = CicRefine
  28 module Un   = CicUniv
  29 module Pp   = CicPp
  30 module TC   = CicTypeChecker
  31 module PEH  = ProofEngineHelpers
  32 module E    = CicEnvironment
  33 module UM   = UriManager
  34 module D    = Deannotate
  35
  36 (* fresh name generator *****************************************************)
  37
  38 let split name =
  39    let rec aux i =
  40       if i <= 0 then assert false else
  41       let c = name.[pred i] in
  42       if c >= '0' && c <= '9' then aux (pred i)
  43       else Str.string_before name i, Str.string_after name i
  44    in
  45    let before, after = aux (String.length name) in
  46    let i = if after = "" then -1 else int_of_string after in
  47    before, i
  48
  49 let join (s, i) =
  50    C.Name (if i < 0 then s else s ^ string_of_int i)
  51
  52 let mk_fresh_name context (name, k) =
  53    let rec aux i = function
  54       | []                            -> name, i
  55       | Some (C.Name s, _) :: entries ->
  56          let m, j = split s in
  57          if m = name && j >= i then aux (succ j) entries else aux i entries
  58       | _ :: entries                  -> aux i entries
  59    in
  60    join (aux k context)
  61
  62 let mk_fresh_name context = function
  63    | C.Anonymous -> C.Anonymous
  64    | C.Name s    -> mk_fresh_name context (split s)
  65
  66 (* helper functions *********************************************************)
  67
  68 let rec list_map_cps g map = function
  69    | []       -> g []
  70    | hd :: tl ->
  71       let h hd =
  72          let g tl = g (hd :: tl) in
  73          list_map_cps g map tl
  74       in
  75       map h hd
  76
  77 let identity x = x
  78
  79 let compose f g x = f (g x)
  80
  81 let fst3 (x, _, _) = x
  82
  83 let refine c t =
  84    try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
  85    with e ->
  86       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
  87       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
  88       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
  89       raise e
  90
  91 let get_type c t =
  92    try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
  93    with e ->
  94       Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
  95       Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
  96       raise e
  97
  98 let get_tail c t =
  99    match PEH.split_with_whd (c, t) with
 100       | (_, hd) :: _, _ -> hd
 101       | _               -> assert false
 102
 103 let is_proof c t =
 104    match get_tail c (get_type c (get_type c t)) with
 105       | C.Sort C.Prop -> true
 106       | C.Sort _      -> false
 107       | _             -> assert false
 108
 109 let is_sort = function
 110    | C.Sort _ -> true
 111    | _        -> false
 112
 113 let is_unsafe h (c, t) = true
 114
 115 let is_not_atomic = function
 116    | C.Sort _
 117    | C.Rel _
 118    | C.Const _
 119    | C.Var _
 120    | C.MutInd _
 121    | C.MutConstruct _ -> false
 122    | _                -> true
 123
 124 let is_atomic t = not (is_not_atomic t)
 125
 126 let get_ind_type uri tyno =
 127    match E.get_obj Un.empty_ugraph uri with
 128       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
 129       | _                                           -> assert false
 130
 131 let get_default_eliminator context uri tyno ty =
 132    let _, (name, _, _, _) = get_ind_type uri tyno in
 133    let ext = match get_tail context (get_type context ty) with
 134       | C.Sort C.Prop     -> "_ind"
 135       | C.Sort C.Set      -> "_rec"
 136       | C.Sort C.CProp    -> "_rec"
 137       | C.Sort (C.Type _) -> "_rect"
 138       | t                 ->
 139          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
 140          assert false
 141    in
 142    let buri = UM.buri_of_uri uri in
 143    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
 144    C.Const (uri, [])
 145
 146 let get_ind_parameters c t =
 147    let ty = get_type c t in
 148    let ps = match get_tail c ty with
 149       | C.MutInd _                  -> []
 150       | C.Appl (C.MutInd _ :: args) -> args
 151       | _                           -> assert false
 152    in
 153    let disp = match get_tail c (get_type c ty) with
 154       | C.Sort C.Prop -> 0
 155       | C.Sort _      -> 1
 156       | _             -> assert false
 157    in
 158    ps, disp
 159
 160 let cic = D.deannotate_term
 161
 162 (* Ensuring Barendregt convenction ******************************************)
 163
 164 let rec add_entries map c = function
 165    | []       -> c
 166    | hd :: tl ->
 167       let sname, w = map hd in
 168       let entry = Some (Cic.Name sname, C.Decl w) in
 169       add_entries map (entry :: c) tl
 170
 171 let get_sname c i =
 172    try match List.nth c (pred i) with
 173       | Some (Cic.Name sname, _) -> sname
 174       | _                        -> assert false
 175    with
 176       | Failure _          -> assert false
 177       | Invalid_argument _ -> assert false
 178
 179 let cic_bc c t =
 180    let get_fix_decl (sname, i, w, v) = sname, w in
 181    let get_cofix_decl (sname, w, v) = sname, w in
 182    let rec bc c = function
 183       | C.LetIn (name, v, t) ->
 184          let name = mk_fresh_name c name in
 185          let entry = Some (name, C.Def (v, None)) in
 186          let v, t = bc c v, bc (entry :: c) t in
 187          C.LetIn (name, v, t)
 188       | C.Lambda (name, w, t) ->
 189          let name = mk_fresh_name c name in
 190          let entry = Some (name, C.Decl w) in
 191          let w, t = bc c w, bc (entry :: c) t in
 192          C.Lambda (name, w, t)
 193       | C.Prod (name, w, t) ->
 194          let name = mk_fresh_name c name in
 195          let entry = Some (name, C.Decl w) in
 196          let w, t = bc c w, bc (entry :: c) t in
 197          C.Prod (name, w, t)
 198       | C.Appl vs ->
 199          let vs = List.map (bc c) vs in
 200          C.Appl vs
 201       | C.MutCase (uri, tyno, u, v, ts) ->
 202          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 203          C.MutCase (uri, tyno, u, v, ts)
 204       | C.Cast (t, u) ->
 205          let t, u = bc c t, bc c u in
 206          C.Cast (t, u)
 207       | C.Fix (i, fixes) ->
 208          let d = add_entries get_fix_decl c fixes in
 209          let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
 210          let fixes = List.map bc_fix fixes in
 211          C.Fix (i, fixes)
 212       | C.CoFix (i, cofixes) ->
 213          let d = add_entries get_cofix_decl c cofixes in
 214          let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
 215          let cofixes = List.map bc_cofix cofixes in
 216          C.CoFix (i, cofixes)
 217       | t -> t
 218    in
 219    bc c t
 220
 221 let acic_bc c t =
 222    let get_fix_decl (id, sname, i, w, v) = sname, cic w in
 223    let get_cofix_decl (id, sname, w, v) = sname, cic w in
 224    let rec bc c = function
 225       | C.ALetIn (id, name, v, t) ->
 226          let name = mk_fresh_name c name in
 227          let entry = Some (name, C.Def (cic v, None)) in
 228          let v, t = bc c v, bc (entry :: c) t in
 229          C.ALetIn (id, name, v, t)
 230       | C.ALambda (id, name, w, t) ->
 231          let name = mk_fresh_name c name in
 232          let entry = Some (name, C.Decl (cic w)) in
 233          let w, t = bc c w, bc (entry :: c) t in
 234          C.ALambda (id, name, w, t)
 235       | C.AProd (id, name, w, t) ->
 236          let name = mk_fresh_name c name in
 237          let entry = Some (name, C.Decl (cic w)) in
 238          let w, t = bc c w, bc (entry :: c) t in
 239          C.AProd (id, name, w, t)
 240       | C.AAppl (id, vs) ->
 241          let vs = List.map (bc c) vs in
 242          C.AAppl (id, vs)
 243       | C.AMutCase (id, uri, tyno, u, v, ts) ->
 244          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 245          C.AMutCase (id, uri, tyno, u, v, ts)
 246       | C.ACast (id, t, u) ->
 247          let t, u = bc c t, bc c u in
 248          C.ACast (id, t, u)
 249       | C.AFix (id, i, fixes) ->
 250          let d = add_entries get_fix_decl c fixes in
 251          let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
 252          let fixes = List.map bc_fix fixes in
 253          C.AFix (id, i, fixes)
 254       | C.ACoFix (id, i, cofixes) ->
 255          let d = add_entries get_cofix_decl c cofixes in
 256          let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
 257          let cofixes = List.map bc_cofix cofixes in
 258          C.ACoFix (id, i, cofixes)
 259       | C.ARel (id1, id2, i, sname) ->
 260          let sname = get_sname c i in
 261          C.ARel (id1, id2, i, sname)
 262       | t -> t
 263    in
 264    bc c t