helm/gTopLevel/proofEngine.ml

   1 type binder_type =
   2    Declaration
   3  | Definition
   4 ;;
   5
   6 type metas_context = (int * Cic.term) list;;
   7
   8 type context = (binder_type * Cic.name * Cic.term) list;;
   9
  10 type sequent = context * Cic.term;;
  11
  12 let proof = ref (None : (metas_context * Cic.term * Cic.term) option);;
  13 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
  14 (* Note: the sequent is redundant: it can be computed from the type of the   *)
  15 (* metavariable and its context in the proof. We keep it just for efficiency *)
  16 (* because computing the context of a term may be quite expensive.           *)
  17 let goal = ref (None : (int * sequent) option);;
  18
  19 exception NotImplemented
  20
  21 (*CSC: Funzione che deve sparire!!! *)
  22 let cic_context_of_context =
  23  List.map
  24   (function
  25       Declaration,_,t -> t
  26     | Definition,_,_ -> raise NotImplemented
  27   )
  28 ;;
  29
  30 let refine_meta meta term newmetasenv =
  31  let (metasenv,bo,ty) =
  32   match !proof with
  33      None -> assert false
  34    | Some (metasenv,bo,ty) -> metasenv,bo,ty
  35  in
  36   let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
  37   let rec aux =
  38    let module C = Cic in
  39     function
  40        C.Rel _ as t -> t
  41      | C.Var _ as t  -> t
  42      | C.Meta meta' when meta=meta' -> term
  43      | C.Meta _ as t -> t
  44      | C.Sort _ as t -> t
  45      | C.Implicit as t -> t
  46      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  47      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
  48      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
  49      | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
  50      | C.Appl l -> C.Appl (List.map aux l)
  51      | C.Const _ as t -> t
  52      | C.Abst _ as t -> t
  53      | C.MutInd _ as t -> t
  54      | C.MutConstruct _ as t -> t
  55      | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  56         C.MutCase (sp,cookingsno,i,aux outt, aux t,
  57          List.map aux pl)
  58      | C.Fix (i,fl) ->
  59         let substitutedfl =
  60          List.map
  61           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
  62            fl
  63         in
  64          C.Fix (i, substitutedfl)
  65      | C.CoFix (i,fl) ->
  66         let substitutedfl =
  67          List.map
  68           (fun (name,ty,bo) -> (name, aux ty, aux bo))
  69            fl
  70         in
  71          C.CoFix (i, substitutedfl)
  72   in
  73    let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in
  74    let bo' = aux bo in
  75     proof := Some (metasenv'',bo',ty)
  76 ;;
  77
  78 (* Returns the first meta whose number is above the number of the higher meta. *)
  79 let new_meta () =
  80  let metasenv =
  81   match !proof with
  82      None -> assert false
  83    | Some (metasenv,_,_) -> metasenv
  84  in
  85   let rec aux =
  86    function
  87       None,[] -> 1
  88     | Some n,[] -> n
  89     | None,(n,_)::tl -> aux (Some n,tl)
  90     | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  91   in
  92    1 + aux (None,metasenv)
  93 ;;
  94
  95 (* metas_in_term term                                                *)
  96 (* Returns the ordered list of the metas that occur in [term].       *)
  97 (* Duplicates are removed. The implementation is not very efficient. *)
  98 let metas_in_term term =
  99  let module C = Cic in
 100   let rec aux =
 101    function
 102       C.Rel _
 103     | C.Var _ -> []
 104     | C.Meta n -> [n]
 105     | C.Sort _
 106     | C.Implicit -> []
 107     | C.Cast (te,ty) -> (aux te) @ (aux ty)
 108     | C.Prod (_,s,t) -> (aux s) @ (aux t)
 109     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
 110     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
 111     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
 112     | C.Const _
 113     | C.Abst _
 114     | C.MutInd _
 115     | C.MutConstruct _ -> []
 116     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 117        (aux outt) @ (aux t) @
 118         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
 119     | C.Fix (i,fl) ->
 120         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 121     | C.CoFix (i,fl) ->
 122         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 123   in
 124    let metas = aux term in
 125     let rec elim_duplicates =
 126      function
 127         [] -> []
 128       | he::tl ->
 129          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
 130     in
 131      elim_duplicates metas
 132 ;;
 133
 134 (* perforate context term ty                                                 *)
 135 (* replaces the term [term] in the proof with a new metavariable whose type  *)
 136 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
 137 (* could be easily computed; so the only reasons to have it as an argument   *)
 138 (* are efficiency reasons.                                                   *)
 139 let perforate context term ty =
 140  let module C = Cic in
 141   let newmeta = new_meta () in
 142    match !proof with
 143       None -> assert false
 144     | Some (metasenv,bo,gty) ->
 145        (* We push the new meta at the end of the list for pretty-printing *)
 146        (* purposes: in this way metas are ordered.                        *)
 147        let metasenv' = metasenv@[newmeta,ty] in
 148        let rec aux =
 149         function
 150            (* Is == strong enough? *)
 151            t when t == term -> C.Meta newmeta
 152          | C.Rel _ as t -> t
 153          | C.Var _ as t  -> t
 154          | C.Meta _ as t -> t
 155          | C.Sort _ as t -> t
 156          | C.Implicit as t -> t
 157          | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 158          | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
 159          | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
 160          | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
 161          | C.Appl l -> C.Appl (List.map aux l)
 162          | C.Const _ as t -> t
 163          | C.Abst _ as t -> t
 164          | C.MutInd _ as t -> t
 165          | C.MutConstruct _ as t -> t
 166          | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 167             C.MutCase (sp,cookingsno,i,aux outt, aux t,
 168              List.map aux pl)
 169          | C.Fix (i,fl) ->
 170             let substitutedfl =
 171              List.map
 172               (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 173                fl
 174             in
 175              C.Fix (i, substitutedfl)
 176          | C.CoFix (i,fl) ->
 177             let substitutedfl =
 178              List.map
 179               (fun (name,ty,bo) -> (name, aux ty, aux bo))
 180                fl
 181             in
 182              C.CoFix (i, substitutedfl)
 183        in
 184         let bo' = aux bo in
 185         (* It may be possible that some metavariables occurred only in *)
 186         (* the term we are perforating and they now occurs no more. We *)
 187         (* get rid of them, collecting the really useful metavariables *)
 188         (* in metasenv''.                                              *)
 189          let newmetas = metas_in_term bo' in
 190           let metasenv'' =
 191            List.filter (function (n,_) -> List.mem n newmetas) metasenv'
 192           in
 193            proof := Some (metasenv'',bo',gty) ;
 194            goal := Some (newmeta,(context,ty)) ;
 195            newmeta
 196 ;;
 197
 198 (************************************************************)
 199 (*                  Some easy tactics.                      *)
 200 (************************************************************)
 201
 202 exception Fail of string;;
 203
 204 let intros () =
 205  let module C = Cic in
 206  let module R = CicReduction in
 207   let metasenv =
 208    match !proof with
 209       None -> assert false
 210     | Some (metasenv,_,_) -> metasenv
 211   in
 212   let (metano,context,ty) =
 213    match !goal with
 214       None -> assert false
 215     | Some (metano,(context,ty)) -> metano,context,ty
 216   in
 217    let newmeta = new_meta () in
 218     let rec collect_context =
 219      function
 220         C.Cast (te,_)   -> collect_context te
 221       | C.Prod (n,s,t)  ->
 222          let (ctx,ty,bo) = collect_context t in
 223           ((Declaration,n,s)::ctx,ty,C.Lambda(n,s,bo))
 224       | C.LetIn (n,s,t) ->
 225          let (ctx,ty,bo) = collect_context t in
 226           ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
 227       | _ as t -> [], t, (C.Meta newmeta)
 228     in
 229      let revcontext',ty',bo' = collect_context ty in
 230       let context'' = (List.rev revcontext') @ context in
 231        refine_meta metano bo' [newmeta,ty'] ;
 232        goal := Some (newmeta,(context'',ty'))
 233 ;;
 234
 235 (* The term bo must be closed in the current context *)
 236 let exact bo =
 237  let module T = CicTypeChecker in
 238  let module R = CicReduction in
 239   let metasenv =
 240    match !proof with
 241       None -> assert false
 242     | Some (metasenv,_,_) -> metasenv
 243   in
 244   let (metano,context,ty) =
 245    match !goal with
 246       None -> assert false
 247     | Some (metano,(context,ty)) ->
 248        assert (ty = List.assoc metano metasenv) ;
 249        (* Invariant: context is the actual context of the meta in the proof *)
 250        metano,context,ty
 251   in
 252    (*CSC: deve sparire! *)
 253    let context = cic_context_of_context context in
 254     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
 255      begin
 256       refine_meta metano bo [] ;
 257       goal := None
 258      end
 259     else
 260      raise (Fail "The type of the provided term is not the one expected.")
 261 ;;
 262
 263 (* The term bo must be closed in the current context *)
 264 let apply term =
 265  let module T = CicTypeChecker in
 266  let module R = CicReduction in
 267  let module C = Cic in
 268   let metasenv =
 269    match !proof with
 270       None -> assert false
 271     | Some (metasenv,_,_) -> metasenv
 272   in
 273   let (metano,context,ty) =
 274    match !goal with
 275       None -> assert false
 276     | Some (metano,(context,ty)) ->
 277        assert (ty = List.assoc metano metasenv) ;
 278        (* Invariant: context is the actual context of the meta in the proof *)
 279        metano,context,ty
 280   in
 281    (*CSC: deve sparire! *)
 282    let ciccontext = cic_context_of_context context in
 283     let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
 284      let mgul  = Array.to_list mgu in
 285      let mgutl = Array.to_list mgut in
 286      let applymetas_to_metas =
 287       let newmeta = new_meta () in
 288        (* WARNING: here we are using the invariant that above the most *)
 289        (* recente new_meta() there are no used metas.                  *)
 290        Array.init (List.length mgul) (function i -> newmeta + i) in
 291       (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!!                         *)
 292       (* Here we assume that either a META has been instantiated with *)
 293       (* a close term or with itself.                                 *)
 294       let uninstantiatedmetas =
 295        List.fold_right2
 296         (fun bo ty newmetas ->
 297           match bo with
 298              Cic.Meta i ->
 299               let newmeta = applymetas_to_metas.(i) in
 300                (*CSC: se ty contiene metas, queste hanno il numero errato!!! *)
 301                let ty_with_newmetas =
 302                 (* Substitues (META n) with (META (applymetas_to_metas.(n))) *)
 303                 let rec aux =
 304                  function
 305                     C.Rel _
 306                   | C.Var _ as t  -> t
 307                   | C.Meta n -> C.Meta (applymetas_to_metas.(n))
 308                   | C.Sort _
 309                   | C.Implicit as t -> t
 310                   | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 311                   | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
 312                   | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
 313                   | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
 314                   | C.Appl l -> C.Appl (List.map aux l)
 315                   | C.Const _ as t -> t
 316                   | C.Abst _ -> assert false
 317                   | C.MutInd _
 318                   | C.MutConstruct _ as t -> t
 319                   | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 320                      C.MutCase (sp,cookingsno,i,aux outt, aux t,
 321                       List.map aux pl)
 322                   | C.Fix (i,fl) ->
 323                      let substitutedfl =
 324                       List.map
 325                        (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 326                         fl
 327                      in
 328                       C.Fix (i, substitutedfl)
 329                   | C.CoFix (i,fl) ->
 330                      let substitutedfl =
 331                       List.map
 332                        (fun (name,ty,bo) -> (name, aux ty, aux bo))
 333                         fl
 334                      in
 335                       C.CoFix (i, substitutedfl)
 336                 in
 337                  aux ty
 338                in
 339                 (newmeta,ty_with_newmetas)::newmetas
 340            | _ -> newmetas
 341         ) mgul mgutl []
 342       in
 343       let mgul' =
 344        List.map
 345         (function
 346             Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i))
 347           | _ as t -> t
 348         ) mgul in
 349        let bo' =
 350         if List.length mgul' = 0 then
 351          term
 352         else
 353          Cic.Appl (term::mgul')
 354        in
 355         refine_meta metano bo' uninstantiatedmetas ;
 356         match uninstantiatedmetas with
 357            (n,ty)::tl -> goal := Some (n,(context,ty))
 358          | [] -> goal := None
 359 ;;