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 module PER  = ProofEngineReduction
  36 module Ut   = CicUtil
  37
  38 (* fresh name generator *****************************************************)
  39
  40 let split name =
  41    let rec aux i =
  42       if i <= 0 then assert false else
  43       let c = name.[pred i] in
  44       if c >= '0' && c <= '9' then aux (pred i)
  45       else Str.string_before name i, Str.string_after name i
  46    in
  47    let before, after = aux (String.length name) in
  48    let i = if after = "" then -1 else int_of_string after in
  49    before, i
  50
  51 let join (s, i) =
  52    C.Name (if i < 0 then s else s ^ string_of_int i)
  53
  54 let mk_fresh_name context (name, k) =
  55    let rec aux i = function
  56       | []                            -> name, i
  57       | Some (C.Name s, _) :: entries ->
  58          let m, j = split s in
  59          if m = name && j >= i then aux (succ j) entries else aux i entries
  60       | _ :: entries                  -> aux i entries
  61    in
  62    join (aux k context)
  63
  64 let mk_fresh_name context = function
  65    | C.Anonymous -> C.Anonymous
  66    | C.Name s    -> mk_fresh_name context (split s)
  67
  68 (* helper functions *********************************************************)
  69
  70 let rec list_fold_right_cps g map l a =
  71    match l with
  72       | []       -> g a
  73       | hd :: tl ->
  74          let h a = map g hd a in
  75          list_fold_right_cps h map tl a
  76
  77 let rec list_fold_left_cps g map a = function
  78    | []       -> g a
  79    | hd :: tl ->
  80       let h a = list_fold_left_cps g map a tl in
  81       map h a hd
  82
  83 let rec list_map_cps g map = function
  84    | []       -> g []
  85    | hd :: tl ->
  86       let h hd =
  87          let g tl = g (hd :: tl) in
  88          list_map_cps g map tl
  89       in
  90       map h hd
  91
  92 let identity x = x
  93
  94 let compose f g x = f (g x)
  95
  96 let fst3 (x, _, _) = x
  97
  98 let refine c t =
  99    let error e =
 100       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
 101       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
 102       raise e
 103    in
 104    try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with
 105       | Rf.RefineFailure s as e ->
 106          Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
 107          error e
 108       | e                       ->
 109          Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
 110          error e
 111
 112 let get_type msg c t =
 113    let log s =
 114       prerr_endline ("TC: " ^ s);
 115       prerr_endline ("TC: context: " ^ Pp.ppcontext c);
 116       prerr_string "TC: term   : "; Ut.pp_term prerr_string [] c t;
 117       prerr_newline (); prerr_endline ("TC: location: " ^ msg)
 118    in
 119    try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
 120       | TC.TypeCheckerFailure s as e ->
 121         log ("failure: " ^ Lazy.force s); raise e
 122       | TC.AssertFailure s as e      ->
 123         log ("assert : " ^ Lazy.force s); raise e
 124
 125 let get_tail c t =
 126    match PEH.split_with_whd (c, t) with
 127       | (_, hd) :: _, _ -> hd
 128       | _               -> assert false
 129
 130 let is_proof c t =
 131    match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
 132       | C.Sort C.Prop -> true
 133       | C.Sort _      -> false
 134       | _             -> assert false
 135
 136 let is_sort = function
 137    | C.Sort _ -> true
 138    | _        -> false
 139
 140 let is_unsafe h (c, t) = true
 141
 142 let is_not_atomic = function
 143    | C.Sort _
 144    | C.Rel _
 145    | C.Const _
 146    | C.Var _
 147    | C.MutInd _
 148    | C.MutConstruct _ -> false
 149    | _                -> true
 150
 151 let is_atomic t = not (is_not_atomic t)
 152
 153 let get_ind_type uri tyno =
 154    match E.get_obj Un.default_ugraph uri with
 155       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
 156       | _                                           -> assert false
 157
 158 let get_ind_names uri tno =
 159 try
 160    let ts = match E.get_obj Un.default_ugraph uri with
 161       | C.InductiveDefinition (ts, _, _, _), _ -> ts
 162       | _                                      -> assert false
 163    in
 164    match List.nth ts tno with
 165       | (_, _, _, cs) -> List.map fst cs
 166 with Invalid_argument _ -> failwith "get_ind_names"
 167
 168 let get_default_eliminator context uri tyno ty =
 169    let _, (name, _, _, _) = get_ind_type uri tyno in
 170    let ext = match get_tail context (get_type "get_def_elim" context ty) with
 171       | C.Sort C.Prop      -> "_ind"
 172       | C.Sort C.Set       -> "_rec"
 173       | C.Sort (C.CProp _) -> "_rect"
 174       | C.Sort (C.Type _)  -> "_rect"
 175       | t                  ->
 176          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
 177          assert false
 178    in
 179    let buri = UM.buri_of_uri uri in
 180    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
 181    C.Const (uri, [])
 182
 183 let get_ind_parameters c t =
 184    let ty = get_type "get_ind_pars 1" c t in
 185    let ps = match get_tail c ty with
 186       | C.MutInd _                  -> []
 187       | C.Appl (C.MutInd _ :: args) -> args
 188       | _                           -> assert false
 189    in
 190    let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
 191       | C.Sort C.Prop -> 0
 192       | C.Sort _      -> 1
 193       | _             -> assert false
 194    in
 195    ps, disp
 196
 197 let cic = D.deannotate_term
 198
 199 let occurs c ~what ~where =
 200    let result = ref false in
 201    let equality c t1 t2 =
 202       let r = Ut.alpha_equivalence t1 t2 in
 203       result := !result || r; r
 204    in
 205    let context, what, with_what = c, [what], [C.Rel 0] in
 206    let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
 207    !result
 208
 209 let name_of_uri uri tyno cno =
 210    let get_ind_type tys tyno =
 211       let s, _, _, cs = List.nth tys tyno in s, cs
 212    in
 213    match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
 214       | C.Variable (s, _, _, _, _), _, _                     -> s
 215       | C.Constant (s, _, _, _, _), _, _                     -> s
 216       | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
 217          let s, _ = get_ind_type tys i in s
 218       | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
 219          let _, cs = get_ind_type tys i in
 220          let s, _ = List.nth cs (pred j) in s
 221       | _                                                    -> assert false
 222
 223 (* Ensuring Barendregt convenction ******************************************)
 224
 225 let rec add_entries map c = function
 226    | []       -> c
 227    | hd :: tl ->
 228       let sname, w = map hd in
 229       let entry = Some (Cic.Name sname, C.Decl w) in
 230       add_entries map (entry :: c) tl
 231
 232 let get_sname c i =
 233    try match List.nth c (pred i) with
 234       | Some (Cic.Name sname, _) -> sname
 235       | _                        -> assert false
 236    with
 237       | Failure _          -> assert false
 238       | Invalid_argument _ -> assert false
 239
 240 let cic_bc c t =
 241    let get_fix_decl (sname, i, w, v) = sname, w in
 242    let get_cofix_decl (sname, w, v) = sname, w in
 243    let rec bc c = function
 244       | C.LetIn (name, v, ty, t) ->
 245          let name = mk_fresh_name c name in
 246          let entry = Some (name, C.Def (v, ty)) in
 247          let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
 248          C.LetIn (name, v, ty, t)
 249       | C.Lambda (name, w, t) ->
 250          let name = mk_fresh_name c name in
 251          let entry = Some (name, C.Decl w) in
 252          let w, t = bc c w, bc (entry :: c) t in
 253          C.Lambda (name, w, t)
 254       | C.Prod (name, w, t) ->
 255          let name = mk_fresh_name c name in
 256          let entry = Some (name, C.Decl w) in
 257          let w, t = bc c w, bc (entry :: c) t in
 258          C.Prod (name, w, t)
 259       | C.Appl vs ->
 260          let vs = List.map (bc c) vs in
 261          C.Appl vs
 262       | C.MutCase (uri, tyno, u, v, ts) ->
 263          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 264          C.MutCase (uri, tyno, u, v, ts)
 265       | C.Cast (t, u) ->
 266          let t, u = bc c t, bc c u in
 267          C.Cast (t, u)
 268       | C.Fix (i, fixes) ->
 269          let d = add_entries get_fix_decl c fixes in
 270          let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
 271          let fixes = List.map bc_fix fixes in
 272          C.Fix (i, fixes)
 273       | C.CoFix (i, cofixes) ->
 274          let d = add_entries get_cofix_decl c cofixes in
 275          let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
 276          let cofixes = List.map bc_cofix cofixes in
 277          C.CoFix (i, cofixes)
 278       | t -> t
 279    in
 280    bc c t
 281
 282 let acic_bc c t =
 283    let get_fix_decl (id, sname, i, w, v) = sname, cic w in
 284    let get_cofix_decl (id, sname, w, v) = sname, cic w in
 285    let rec bc c = function
 286       | C.ALetIn (id, name, v, ty, t) ->
 287          let name = mk_fresh_name c name in
 288          let entry = Some (name, C.Def (cic v, cic ty)) in
 289          let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
 290          C.ALetIn (id, name, v, ty, t)
 291       | C.ALambda (id, name, w, t) ->
 292          let name = mk_fresh_name c name in
 293          let entry = Some (name, C.Decl (cic w)) in
 294          let w, t = bc c w, bc (entry :: c) t in
 295          C.ALambda (id, name, w, t)
 296       | C.AProd (id, name, w, t) ->
 297          let name = mk_fresh_name c name in
 298          let entry = Some (name, C.Decl (cic w)) in
 299          let w, t = bc c w, bc (entry :: c) t in
 300          C.AProd (id, name, w, t)
 301       | C.AAppl (id, vs) ->
 302          let vs = List.map (bc c) vs in
 303          C.AAppl (id, vs)
 304       | C.AMutCase (id, uri, tyno, u, v, ts) ->
 305          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 306          C.AMutCase (id, uri, tyno, u, v, ts)
 307       | C.ACast (id, t, u) ->
 308          let t, u = bc c t, bc c u in
 309          C.ACast (id, t, u)
 310       | C.AFix (id, i, fixes) ->
 311          let d = add_entries get_fix_decl c fixes in
 312          let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
 313          let fixes = List.map bc_fix fixes in
 314          C.AFix (id, i, fixes)
 315       | C.ACoFix (id, i, cofixes) ->
 316          let d = add_entries get_cofix_decl c cofixes in
 317          let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
 318          let cofixes = List.map bc_cofix cofixes in
 319          C.ACoFix (id, i, cofixes)
 320       | C.ARel (id1, id2, i, sname) ->
 321          let sname = get_sname c i in
 322          C.ARel (id1, id2, i, sname)
 323       | t -> t
 324    in
 325    bc c t