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