helm/interface/cicReduction.ml

   1 exception CicReductionInternalError;;
   2 exception WrongUriToInductiveDefinition;;
   3
   4 let fdebug = ref 1;;
   5 let debug t env s =
   6  let rec debug_aux t i =
   7   let module C = Cic in
   8   let module U = UriManager in
   9    CicPp.ppobj (C.Variable ("DEBUG",
  10     C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
  11      C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
  12       C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
  13        C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
  14         C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
  15          C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
  16           C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
  17            C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
  18             C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
  19              t
  20             )
  21            )
  22           )
  23          )
  24         )
  25        )
  26       )
  27      )
  28     )
  29     )) ^ "\n" ^ i
  30  in
  31   if !fdebug = 0 then
  32    begin
  33     print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
  34     flush stdout
  35    end
  36 ;;
  37
  38 exception Impossible of int;;
  39 exception ReferenceToDefinition;;
  40 exception ReferenceToAxiom;;
  41 exception ReferenceToVariable;;
  42 exception ReferenceToCurrentProof;;
  43 exception ReferenceToInductiveDefinition;;
  44
  45 (* takes a well-typed term *)
  46 let whd =
  47  let rec whdaux l =
  48   let module C = Cic in
  49   let module S = CicSubstitution in
  50    function
  51       C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
  52     | C.Var _ as t -> if l = [] then t else C.Appl (t::l)
  53     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
  54     | C.Sort _ as t -> t (* l should be empty *)
  55     | C.Implicit as t -> t
  56     | C.Cast (te,ty) -> whdaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
  57     | C.Prod _ as t -> t (* l should be empty *)
  58     | C.Lambda (name,s,t) as t' ->
  59        (match l with
  60            [] -> t'
  61          | he::tl -> whdaux tl (S.subst he t)
  62            (* when name is Anonimous the substitution should be superfluous *)
  63        )
  64     | C.Appl (he::tl) -> whdaux (tl@l) he
  65     | C.Appl [] -> raise (Impossible 1)
  66     | C.Const (uri,cookingsno) as t ->
  67        (match CicCache.get_cooked_obj uri cookingsno with
  68            C.Definition (_,body,_,_) -> whdaux l body
  69          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
  70          (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *)
  71          | C.Variable _ -> if l = [] then t else C.Appl (t::l)
  72          | C.CurrentProof (_,_,body,_) -> whdaux l body
  73          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
  74        )
  75     | C.Abst _ as t -> t (*CSC l should be empty ????? *)
  76     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
  77     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
  78     | C.MutCase (mutind,cookingsno,i,_,term,pl) as t ->
  79        let decofix =
  80         function
  81            C.CoFix (i,fl) as t ->
  82             let (_,_,body) = List.nth fl i in
  83              let body' =
  84               let counter = ref (List.length fl) in
  85                List.fold_right
  86                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
  87                 fl
  88                 body
  89              in
  90               whdaux [] body'
  91          | C.Appl (C.CoFix (i,fl) :: tl) ->
  92             let (_,_,body) = List.nth fl i in
  93              let body' =
  94               let counter = ref (List.length fl) in
  95                List.fold_right
  96                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
  97                 fl
  98                 body
  99              in
 100               whdaux tl body'
 101          | t -> t
 102        in
 103         (match decofix (whdaux [] term) with
 104             C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1))
 105           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
 106              let (arity, r, num_ingredients) =
 107               match CicCache.get_obj mutind with
 108                  C.InductiveDefinition (tl,ingredients,r) ->
 109                    let (_,_,arity,_) = List.nth tl i
 110                    and num_ingredients =
 111                     List.fold_right
 112                      (fun (k,l) i ->
 113                        if k < cookingsno then i + List.length l else i
 114                      ) ingredients 0
 115                    in
 116                     (arity,r,num_ingredients)
 117                | _ -> raise WrongUriToInductiveDefinition
 118              in
 119               let ts =
 120                let num_to_eat = r + num_ingredients in
 121                 let rec eat_first =
 122                  function
 123                     (0,l) -> l
 124                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 125                   | _ -> raise (Impossible 5)
 126                 in
 127                  eat_first (num_to_eat,tl)
 128               in
 129                whdaux (ts@l) (List.nth pl (j-1))
 130          | C.Abst _| C.Cast _ | C.Implicit ->
 131             raise (Impossible 2) (* we don't trust our whd ;-) *)
 132          | _ -> t
 133        )
 134     | C.Fix (i,fl) as t ->
 135        let (_,recindex,_,body) = List.nth fl i in
 136         let recparam =
 137          try
 138           Some (List.nth l recindex)
 139          with
 140           _ -> None
 141         in
 142          (match recparam with
 143              Some recparam ->
 144               (match whdaux [] recparam with
 145                   C.MutConstruct _
 146                 | C.Appl ((C.MutConstruct _)::_) ->
 147                    let body' =
 148                     let counter = ref (List.length fl) in
 149                      List.fold_right
 150                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 151                       fl
 152                       body
 153                    in
 154                     (* Possible optimization: substituting whd recparam in l *)
 155                     whdaux l body'
 156                | _ -> if l = [] then t else C.Appl (t::l)
 157              )
 158           | None -> if l = [] then t else C.Appl (t::l)
 159          )
 160     | C.CoFix (i,fl) as t ->
 161        (*CSC vecchio codice
 162        let (_,_,body) = List.nth fl i in
 163         let body' =
 164          let counter = ref (List.length fl) in
 165           List.fold_right
 166            (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 167            fl
 168            body
 169         in
 170          whdaux l body'
 171        *)
 172        if l = [] then t else C.Appl (t::l)
 173  in
 174   whdaux []
 175 ;;
 176
 177 (* t1, t2 must be well-typed *)
 178 let are_convertible t1 t2 =
 179  let module U = UriManager in
 180  let rec aux t1 t2 =
 181   debug t1 [t2] "PREWHD";
 182   (* this trivial euristic cuts down the total time of about five times ;-) *)
 183   (* this because most of the time t1 and t2 are "sintactically" the same   *)
 184   if t1 = t2 then
 185    true
 186   else
 187    begin
 188     let module C = Cic in
 189      let t1' = whd t1
 190      and t2' = whd t2 in
 191      debug t1' [t2'] "POSTWHD";
 192      (*if !fdebug = 0 then ignore(Unix.system "read" );*)
 193       match (t1',t2') with
 194          (C.Rel n1, C.Rel n2) -> n1 = n2
 195        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
 196        | (C.Meta n1, C.Meta n2) -> n1 = n2
 197        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
 198        | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
 199           aux s1 s2 && aux t1 t2
 200        | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
 201           aux s1 s2 && aux t1 t2
 202        | (C.Appl l1, C.Appl l2) ->
 203           (try
 204             List.fold_right2 (fun  x y b -> aux x y && b) l1 l2 true
 205            with
 206             Invalid_argument _ -> false
 207           )
 208        | (C.Const (uri1,_), C.Const (uri2,_)) ->
 209            (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *)
 210            (*CSC: mentre sono delirante, quindi ...                          *)
 211            (* WARNING: it is really important that the two cookingsno are not *)
 212            (* checked for equality. This allows not to cook an object with no *)
 213            (* ingredients only to update the cookingsno. E.g: if a term t has *)
 214            (* a reference to a term t1 which does not depend on any variable  *)
 215            (* and t1 depends on a term t2 (that can't depend on any variable  *)
 216            (* because of t1), then t1 cooked at every level could be the same *)
 217            (* as t1 cooked at level 0. Doing so, t2 will be extended in t     *)
 218            (* with cookingsno 0 and not 2. But this will not cause any trouble*)
 219            (* if here we don't check that the two cookingsno are equal.       *)
 220            U.eq uri1 uri2
 221        | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
 222            (* WARNIG: see the previous warning *)
 223            U.eq uri1 uri2 && i1 = i2
 224        | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
 225            (* WARNIG: see the previous warning *)
 226            U.eq uri1 uri2 && i1 = i2 && j1 = j2
 227        | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
 228           C.MutCase (uri2,_,i2,outtype2,term2,pl2)) ->
 229            (* WARNIG: see the previous warning *)
 230            (* aux outtype1 outtype2 should be true if aux pl1 pl2 *)
 231            U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 &&
 232             aux term1 term2 &&
 233             List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true
 234        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 235           i1 = i2 &&
 236            List.fold_right2
 237             (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
 238               b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2)
 239             fl1 fl2 true
 240        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 241           i1 = i2 &&
 242            List.fold_right2
 243             (fun (_,ty1,bo1) (_,ty2,bo2) b ->
 244               b && aux ty1 ty2 && aux bo1 bo2)
 245             fl1 fl2 true
 246        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
 247        | (C.Implicit, _) | (_, C.Implicit) ->
 248           raise (Impossible 3) (* we don't trust our whd ;-) *)
 249        | (_,_) -> false
 250    end
 251  in
 252   aux t1 t2
 253 ;;