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 (* raw cic prettyprinter ****************************************************)
  39
  40 let xiter out so ss sc map l =
  41    let rec aux = function
  42       | hd :: tl when tl <> [] -> map hd; out ss; aux tl
  43       | hd :: tl               -> map hd; aux tl
  44       | []                     -> ()
  45    in
  46    out so; aux l; out sc
  47
  48 let abst s w = Some (s, C.Decl w)
  49
  50 let abbr s v w = Some (s, C.Def (v, w))
  51
  52 let pp_sort out = function
  53    | C.Type _  -> out "*Type"
  54    | C.Prop    -> out "*Prop"
  55    | C.CProp _ -> out "*CProp"
  56    | C.Set     -> out "*Set"
  57
  58 let pp_name out = function
  59    | C.Name s    -> out s
  60    | C.Anonymous -> out "_"
  61
  62 let pp_rel out c i =
  63    try match List.nth c (pred i) with
  64       | None           -> out (Printf.sprintf "%u[?]" i)
  65       | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
  66    with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
  67
  68 let pp_implict out = function
  69    | None         -> out "?"
  70    | Some `Closed -> out "?[Closed]"
  71    | Some `Type   -> out "?[Type]"
  72    | Some `Hole   -> out "?[Hole]"
  73
  74 let pp_uri out a =
  75    out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
  76
  77 let rec pp_term out e c = function
  78    | C.Sort h                      -> pp_sort out h
  79    | C.Rel i                       -> pp_rel out c i
  80    | C.Implicit x                  -> pp_implict out x
  81    | C.Meta (i, iss)               ->
  82       let map = function None   -> out "_" | Some v -> pp_term out e c v in
  83       out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
  84    | C.Var (a, xss)              ->
  85       pp_uri out a; pp_xss out e c xss
  86    | C.Const (a, xss)              ->
  87       pp_uri out a; pp_xss out e c xss
  88    | C.MutInd (a, m, xss)          ->
  89       pp_uri out a; out (Printf.sprintf "/%u" m);
  90       pp_xss out e c xss
  91    | C.MutConstruct (a, m, n, xss) ->
  92       pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
  93       pp_xss out e c xss
  94    | C.Cast (v, w)                 ->
  95       out "type "; pp_term out e c w; out " contains "; pp_term out e c v
  96    | C.Appl vs                     ->
  97       xiter out "(" " @ " ")" (pp_term out e c) vs
  98    | C.MutCase (a, m, w, v, vs)    ->
  99       out "match "; pp_term out e c v;
 100       out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
 101       out " to "; pp_term out e c w;
 102       xiter out " cases " " | " "" (pp_term out e c) vs
 103    | C.Prod (s, w, t)             ->
 104       out "forall "; pp_name out s; out " of "; pp_term out e c w;
 105       out " in "; pp_term out e (abst s w :: c) t
 106    | C.Lambda (s, w, t)            ->
 107       out "fun "; pp_name out s; out " of "; pp_term out e c w;
 108       out " in "; pp_term out e (abst s w :: c) t
 109    | C.LetIn (s, v, w, t)          ->
 110       out "let "; pp_name out s;
 111       out " def "; pp_term out e c v; out " of "; pp_term out e c w;
 112       out " in "; pp_term out e (abbr s v w :: c) t
 113    | C.Fix (i, fs)                 ->
 114       let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
 115       let c' = List.fold_left map c fs in
 116       let map (s, i, w, v) =
 117          out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
 118          out " of "; pp_term out e c w;
 119       in
 120       xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
 121    | C.CoFix (i, fs)                 ->
 122       let map c (s, w, v) = abbr (C.Name s) v w :: c in
 123       let c' = List.fold_left map c fs in
 124       let map (s, w, v) =
 125          out s; pp_term out e c' v;
 126          out " of "; pp_term out e c w;
 127       in
 128       xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
 129
 130 and pp_xss out e c xss =
 131    let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
 132    xiter out "[" "; " "]" map xss
 133
 134 (* fresh name generator *****************************************************)
 135
 136 let split name =
 137    let rec aux i =
 138       if i <= 0 then assert false else
 139       let c = name.[pred i] in
 140       if c >= '0' && c <= '9' then aux (pred i)
 141       else Str.string_before name i, Str.string_after name i
 142    in
 143    let before, after = aux (String.length name) in
 144    let i = if after = "" then -1 else int_of_string after in
 145    before, i
 146
 147 let join (s, i) =
 148    C.Name (if i < 0 then s else s ^ string_of_int i)
 149
 150 let mk_fresh_name context (name, k) =
 151    let rec aux i = function
 152       | []                            -> name, i
 153       | Some (C.Name s, _) :: entries ->
 154          let m, j = split s in
 155          if m = name && j >= i then aux (succ j) entries else aux i entries
 156       | _ :: entries                  -> aux i entries
 157    in
 158    join (aux k context)
 159
 160 let mk_fresh_name context = function
 161    | C.Anonymous -> C.Anonymous
 162    | C.Name s    -> mk_fresh_name context (split s)
 163
 164 (* helper functions *********************************************************)
 165
 166 let rec list_fold_right_cps g map l a =
 167    match l with
 168       | []       -> g a
 169       | hd :: tl ->
 170          let h a = map g hd a in
 171          list_fold_right_cps h map tl a
 172
 173 let rec list_fold_left_cps g map a = function
 174    | []       -> g a
 175    | hd :: tl ->
 176       let h a = list_fold_left_cps g map a tl in
 177       map h a hd
 178
 179 let rec list_map_cps g map = function
 180    | []       -> g []
 181    | hd :: tl ->
 182       let h hd =
 183          let g tl = g (hd :: tl) in
 184          list_map_cps g map tl
 185       in
 186       map h hd
 187
 188 let identity x = x
 189
 190 let compose f g x = f (g x)
 191
 192 let fst3 (x, _, _) = x
 193
 194 let refine c t =
 195    try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
 196    with e ->
 197       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
 198       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
 199       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
 200       raise e
 201
 202 let get_type msg c t =
 203    let log s =
 204       prerr_endline ("TC: " ^ s);
 205       prerr_endline ("TC: context: " ^ Pp.ppcontext c);
 206       prerr_string "TC: term   : "; pp_term prerr_string [] c t;
 207       prerr_newline (); prerr_endline ("TC: location: " ^ msg)
 208    in
 209    try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
 210       | TC.TypeCheckerFailure s as e ->
 211         log ("failure: " ^ Lazy.force s); raise e
 212       | TC.AssertFailure s as e      ->
 213         log ("assert : " ^ Lazy.force s); raise e
 214
 215 let get_tail c t =
 216    match PEH.split_with_whd (c, t) with
 217       | (_, hd) :: _, _ -> hd
 218       | _               -> assert false
 219
 220 let is_proof c t =
 221    match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
 222       | C.Sort C.Prop -> true
 223       | C.Sort _      -> false
 224       | _             -> assert false
 225
 226 let is_sort = function
 227    | C.Sort _ -> true
 228    | _        -> false
 229
 230 let is_unsafe h (c, t) = true
 231
 232 let is_not_atomic = function
 233    | C.Sort _
 234    | C.Rel _
 235    | C.Const _
 236    | C.Var _
 237    | C.MutInd _
 238    | C.MutConstruct _ -> false
 239    | _                -> true
 240
 241 let is_atomic t = not (is_not_atomic t)
 242
 243 let get_ind_type uri tyno =
 244    match E.get_obj Un.default_ugraph uri with
 245       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
 246       | _                                           -> assert false
 247
 248 let get_ind_names uri tno =
 249 try
 250    let ts = match E.get_obj Un.default_ugraph uri with
 251       | C.InductiveDefinition (ts, _, _, _), _ -> ts
 252       | _                                      -> assert false
 253    in
 254    match List.nth ts tno with
 255       | (_, _, _, cs) -> List.map fst cs
 256 with Invalid_argument _ -> failwith "get_ind_names"
 257
 258 let get_default_eliminator context uri tyno ty =
 259    let _, (name, _, _, _) = get_ind_type uri tyno in
 260    let ext = match get_tail context (get_type "get_def_elim" context ty) with
 261       | C.Sort C.Prop      -> "_ind"
 262       | C.Sort C.Set       -> "_rec"
 263       | C.Sort (C.CProp _) -> "_rect"
 264       | C.Sort (C.Type _)  -> "_rect"
 265       | t                  ->
 266          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
 267          assert false
 268    in
 269    let buri = UM.buri_of_uri uri in
 270    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
 271    C.Const (uri, [])
 272
 273 let get_ind_parameters c t =
 274    let ty = get_type "get_ind_pars 1" c t in
 275    let ps = match get_tail c ty with
 276       | C.MutInd _                  -> []
 277       | C.Appl (C.MutInd _ :: args) -> args
 278       | _                           -> assert false
 279    in
 280    let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
 281       | C.Sort C.Prop -> 0
 282       | C.Sort _      -> 1
 283       | _             -> assert false
 284    in
 285    ps, disp
 286
 287 let cic = D.deannotate_term
 288
 289 let occurs c ~what ~where =
 290    let result = ref false in
 291    let equality c t1 t2 =
 292       let r = Ut.alpha_equivalence t1 t2 in
 293       result := !result || r; r
 294    in
 295    let context, what, with_what = c, [what], [C.Rel 0] in
 296    let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
 297    !result
 298
 299 let name_of_uri uri tyno cno =
 300    let get_ind_type tys tyno =
 301       let s, _, _, cs = List.nth tys tyno in s, cs
 302    in
 303    match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
 304       | C.Variable (s, _, _, _, _), _, _                     -> s
 305       | C.Constant (s, _, _, _, _), _, _                     -> s
 306       | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
 307          let s, _ = get_ind_type tys i in s
 308       | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
 309          let _, cs = get_ind_type tys i in
 310          let s, _ = List.nth cs (pred j) in s
 311       | _                                                    -> assert false
 312
 313 (* Ensuring Barendregt convenction ******************************************)
 314
 315 let rec add_entries map c = function
 316    | []       -> c
 317    | hd :: tl ->
 318       let sname, w = map hd in
 319       let entry = Some (Cic.Name sname, C.Decl w) in
 320       add_entries map (entry :: c) tl
 321
 322 let get_sname c i =
 323    try match List.nth c (pred i) with
 324       | Some (Cic.Name sname, _) -> sname
 325       | _                        -> assert false
 326    with
 327       | Failure _          -> assert false
 328       | Invalid_argument _ -> assert false
 329
 330 let cic_bc c t =
 331    let get_fix_decl (sname, i, w, v) = sname, w in
 332    let get_cofix_decl (sname, w, v) = sname, w in
 333    let rec bc c = function
 334       | C.LetIn (name, v, ty, t) ->
 335          let name = mk_fresh_name c name in
 336          let entry = Some (name, C.Def (v, ty)) in
 337          let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
 338          C.LetIn (name, v, ty, t)
 339       | C.Lambda (name, w, t) ->
 340          let name = mk_fresh_name c name in
 341          let entry = Some (name, C.Decl w) in
 342          let w, t = bc c w, bc (entry :: c) t in
 343          C.Lambda (name, w, t)
 344       | C.Prod (name, w, t) ->
 345          let name = mk_fresh_name c name in
 346          let entry = Some (name, C.Decl w) in
 347          let w, t = bc c w, bc (entry :: c) t in
 348          C.Prod (name, w, t)
 349       | C.Appl vs ->
 350          let vs = List.map (bc c) vs in
 351          C.Appl vs
 352       | C.MutCase (uri, tyno, u, v, ts) ->
 353          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 354          C.MutCase (uri, tyno, u, v, ts)
 355       | C.Cast (t, u) ->
 356          let t, u = bc c t, bc c u in
 357          C.Cast (t, u)
 358       | C.Fix (i, fixes) ->
 359          let d = add_entries get_fix_decl c fixes in
 360          let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
 361          let fixes = List.map bc_fix fixes in
 362          C.Fix (i, fixes)
 363       | C.CoFix (i, cofixes) ->
 364          let d = add_entries get_cofix_decl c cofixes in
 365          let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
 366          let cofixes = List.map bc_cofix cofixes in
 367          C.CoFix (i, cofixes)
 368       | t -> t
 369    in
 370    bc c t
 371
 372 let acic_bc c t =
 373    let get_fix_decl (id, sname, i, w, v) = sname, cic w in
 374    let get_cofix_decl (id, sname, w, v) = sname, cic w in
 375    let rec bc c = function
 376       | C.ALetIn (id, name, v, ty, t) ->
 377          let name = mk_fresh_name c name in
 378          let entry = Some (name, C.Def (cic v, cic ty)) in
 379          let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
 380          C.ALetIn (id, name, v, ty, t)
 381       | C.ALambda (id, name, w, t) ->
 382          let name = mk_fresh_name c name in
 383          let entry = Some (name, C.Decl (cic w)) in
 384          let w, t = bc c w, bc (entry :: c) t in
 385          C.ALambda (id, name, w, t)
 386       | C.AProd (id, name, w, t) ->
 387          let name = mk_fresh_name c name in
 388          let entry = Some (name, C.Decl (cic w)) in
 389          let w, t = bc c w, bc (entry :: c) t in
 390          C.AProd (id, name, w, t)
 391       | C.AAppl (id, vs) ->
 392          let vs = List.map (bc c) vs in
 393          C.AAppl (id, vs)
 394       | C.AMutCase (id, uri, tyno, u, v, ts) ->
 395          let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
 396          C.AMutCase (id, uri, tyno, u, v, ts)
 397       | C.ACast (id, t, u) ->
 398          let t, u = bc c t, bc c u in
 399          C.ACast (id, t, u)
 400       | C.AFix (id, i, fixes) ->
 401          let d = add_entries get_fix_decl c fixes in
 402          let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
 403          let fixes = List.map bc_fix fixes in
 404          C.AFix (id, i, fixes)
 405       | C.ACoFix (id, i, cofixes) ->
 406          let d = add_entries get_cofix_decl c cofixes in
 407          let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
 408          let cofixes = List.map bc_cofix cofixes in
 409          C.ACoFix (id, i, cofixes)
 410       | C.ARel (id1, id2, i, sname) ->
 411          let sname = get_sname c i in
 412          C.ARel (id1, id2, i, sname)
 413       | t -> t
 414    in
 415    bc c t