helm/matita/matitaEngine.ml

   1
   2 open Printf
   3
   4 open MatitaTypes
   5
   6
   7 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   8   * names as long as they are available, then it fallbacks to name generation
   9   * using FreshNamesGenerator module *)
  10 let namer_of names =
  11   let len = List.length names in
  12   let count = ref 0 in
  13   fun metasenv context name ~typ ->
  14     if !count < len then begin
  15       let name = Cic.Name (List.nth names !count) in
  16       incr count;
  17       name
  18     end else
  19       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  20
  21 let tactic_of_ast = function
  22   | TacticAst.Intros (_, _, names) ->
  23       (* TODO Zack implement intros length *)
  24       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  25   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  26   | TacticAst.Assumption _ -> Tactics.assumption
  27   | TacticAst.Contradiction _ -> Tactics.contradiction
  28   | TacticAst.Exists _ -> Tactics.exists
  29   | TacticAst.Fourier _ -> Tactics.fourier
  30   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  31   | TacticAst.Left _ -> Tactics.left
  32   | TacticAst.Right _ -> Tactics.right
  33   | TacticAst.Ring _ -> Tactics.ring
  34   | TacticAst.Split _ -> Tactics.split
  35   | TacticAst.Symmetry _ -> Tactics.symmetry
  36   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  37   | TacticAst.Apply (_, term) -> Tactics.apply term
  38   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  39   | TacticAst.Exact (_, term) -> Tactics.exact term
  40   | TacticAst.Cut (_, term) -> Tactics.cut term
  41   | TacticAst.Elim (_, term, _) ->
  42       (* TODO Zack implement "using" argument *)
  43       Tactics.elim_intros_simpl term
  44   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  45   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  46   | TacticAst.Auto (_,num) ->
  47       AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
  48   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  49 (*
  50   (* TODO Zack a lot more of tactics to be implemented here ... *)
  51   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  52   | TacticAst.Change of 'term * 'term * 'ident option
  53   | TacticAst.Decompose of 'ident * 'ident list
  54   | TacticAst.Discriminate of 'ident
  55   | TacticAst.Fold of reduction_kind * 'term
  56   | TacticAst.Injection of 'ident
  57   | TacticAst.LetIn of 'term * 'ident
  58   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
  59   | TacticAst.Replace_pattern of 'term pattern * 'term
  60 *)
  61   | TacticAst.Rewrite (_,dir,t,ident) ->
  62       if dir = `Left then
  63         EqualityTactics.rewrite_tac ~term:t
  64       else
  65         EqualityTactics.rewrite_back_tac ~term:t
  66   | _ -> assert false
  67
  68 let eval_tactical status tac =
  69   let apply_tactic tactic =
  70     let (proof, goals) =
  71       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
  72     in
  73     let new_status =
  74       match goals with
  75       | [] ->
  76           let (_,metasenv,_,_) = proof in
  77           (match metasenv with
  78           | [] -> Proof proof
  79           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
  80       | ng::_ -> Incomplete_proof (proof, ng)
  81     in
  82     { status with proof_status = new_status }
  83   in
  84   let rec tactical_of_ast = function
  85     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
  86     | TacticAst.Fail loc -> Tacticals.fail
  87     | TacticAst.Do (loc, num, tactical) ->
  88         Tacticals.do_tactic num (tactical_of_ast tactical)
  89     | TacticAst.IdTac loc -> Tacticals.id_tac
  90     | TacticAst.Repeat (loc, tactical) ->
  91         Tacticals.repeat_tactic (tactical_of_ast tactical)
  92     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
  93         Tacticals.seq (List.map tactical_of_ast tacticals)
  94     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
  95         Tacticals.thens (tactical_of_ast tactical)
  96           (List.map tactical_of_ast tacticals)
  97     | TacticAst.Tries (loc, tacticals) ->
  98         Tacticals.try_tactics
  99           (List.map (fun t -> "", tactical_of_ast t) tacticals)
 100     | TacticAst.Try (loc, tactical) ->
 101         Tacticals.try_tactic (tactical_of_ast tactical)
 102   in
 103   apply_tactic (tactical_of_ast tac)
 104
 105 let eval_command status cmd =
 106   match cmd with
 107   | TacticAst.Set (loc, name, value) -> set_option status name value
 108   | TacticAst.Qed loc ->
 109       let uri, metasenv, bo, ty =
 110         match status.proof_status with
 111         | Proof (Some uri, metasenv, body, ty) ->
 112             uri, metasenv, body, ty
 113         | Proof (None, metasenv, body, ty) ->
 114             command_error
 115               ("Someone allows to start a thm without giving the "^
 116                "name/uri. This should be fixed!")
 117         | _-> command_error "You can't qed an uncomplete theorem"
 118       in
 119       let suri = UriManager.string_of_uri uri in
 120       if metasenv <> [] then
 121         command_error "Proof not completed! metasenv is not empty!";
 122       let proved_ty,ugraph =
 123         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 124       in
 125       let b,ugraph =
 126         CicReduction.are_convertible [] proved_ty ty ugraph
 127       in
 128       if not b then
 129         command_error
 130           ("The type of your proof is not convertible with the "^
 131           "type you've declared!");
 132       MatitaLog.message (sprintf "%s defined" suri);
 133       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 134       {status with proof_status = No_proof }
 135   | TacticAst.Inductive (loc, dummy_params, types) ->
 136       (* dummy_params are not real params, it is a list of nothing, and the only
 137        * semantic content is the len, that is leftno (note: leftno and pamaters
 138        * have nothing in common).
 139        *)
 140       let suri =
 141         match types with
 142         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 143         | _ -> assert false
 144       in
 145       let uri = UriManager.uri_of_string suri in
 146       let leftno = List.length dummy_params in
 147       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 148       let ugraph =
 149         CicTypeChecker.typecheck_mutual_inductive_defs uri
 150           (types, [], leftno) CicUniv.empty_ugraph
 151       in
 152         MatitaSync.add_inductive_def
 153           ~uri ~types ~params:[] ~leftno ~ugraph status;
 154   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 155       let uri =
 156         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 157       in
 158       let goalno = 1 in
 159       let metasenv, body =
 160         match status.proof_status with
 161         | Intermediate metasenv ->
 162             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 163         | _-> assert false
 164       in
 165       let initial_proof = (Some uri, metasenv, body, ty) in
 166       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 167   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 168       let uri =
 169         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 170       in
 171       let metasenv = MatitaMisc.get_proof_metasenv status in
 172       let (body_type, ugraph) =
 173         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 174       in
 175       let (subst, metasenv, ugraph) =
 176         CicUnification.fo_unif metasenv [] body_type ty ugraph
 177       in
 178       if metasenv <> [] then
 179         command_error
 180           "metasenv not empty while giving a definition with body";
 181       let body = CicMetaSubst.apply_subst subst body in
 182       let ty = CicMetaSubst.apply_subst subst ty in
 183       MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
 184   | TacticAst.Theorem (_, _, None, _, _) ->
 185       command_error "The grammas should avoid having unnamed theorems!"
 186   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 187   | TacticAst.Alias (loc, spec) ->
 188       match spec with
 189       | TacticAst.Ident_alias (id,uri) ->
 190           {status with aliases =
 191             DisambiguateTypes.Environment.add
 192               (DisambiguateTypes.Id id)
 193               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 194               status.aliases }
 195       | TacticAst.Symbol_alias (symb, instance, desc) ->
 196           {status with aliases =
 197             DisambiguateTypes.Environment.add
 198               (DisambiguateTypes.Symbol (symb,instance))
 199               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 200               status.aliases }
 201       | TacticAst.Number_alias (instance,desc) ->
 202           {status with aliases =
 203             DisambiguateTypes.Environment.add
 204               (DisambiguateTypes.Num instance)
 205               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 206
 207 let eval_executable status ex =
 208   match ex with
 209   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 210   | TacticAst.Command (_, cmd) -> eval_command status cmd
 211   | TacticAst.Macro (_, mac) ->
 212       command_error (sprintf "The macro %s can't be in a script"
 213         (TacticAstPp.pp_macro_cic mac))
 214
 215 let eval_comment status c = status
 216
 217 let eval status st =
 218   match st with
 219   | TacticAst.Executable (_,ex) -> eval_executable status ex
 220   | TacticAst.Comment (_,c) -> eval_comment status c
 221
 222 let disambiguate_term status term =
 223   let (aliases, metasenv, cic, _) =
 224     match
 225       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 226         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 227         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 228     with
 229     | [x] -> x
 230     | _ -> assert false
 231   in
 232   let proof_status =
 233     match status.proof_status with
 234     | No_proof -> Intermediate metasenv
 235     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 236         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 237     | Intermediate _ -> Intermediate metasenv
 238     | Proof _ -> assert false
 239   in
 240   let status =
 241     { status with
 242         aliases = aliases;
 243         proof_status = proof_status }
 244   in
 245   status, cic
 246
 247 let disambiguate_terms status terms =
 248   let term = CicAst.pack terms in
 249   let status, term = disambiguate_term status term in
 250   status, CicUtil.unpack term
 251
 252 let disambiguate_tactic status = function
 253   | TacticAst.Transitivity (loc, term) ->
 254       let status, cic = disambiguate_term status term in
 255       status, TacticAst.Transitivity (loc, cic)
 256   | TacticAst.Apply (loc, term) ->
 257       let status, cic = disambiguate_term status term in
 258       status, TacticAst.Apply (loc, cic)
 259   | TacticAst.Absurd (loc, term) ->
 260       let status, cic = disambiguate_term status term in
 261       status, TacticAst.Absurd (loc, cic)
 262   | TacticAst.Exact (loc, term) ->
 263       let status, cic = disambiguate_term status term in
 264       status, TacticAst.Exact (loc, cic)
 265   | TacticAst.Cut (loc, term) ->
 266       let status, cic = disambiguate_term status term in
 267       status, TacticAst.Cut (loc, cic)
 268   | TacticAst.Elim (loc, term, Some term') ->
 269       let status, cic1 = disambiguate_term status term in
 270       let status, cic2 = disambiguate_term status term' in
 271       status, TacticAst.Elim (loc, cic1, Some cic2)
 272   | TacticAst.Elim (loc, term, None) ->
 273       let status, cic = disambiguate_term status term in
 274       status, TacticAst.Elim (loc, cic, None)
 275   | TacticAst.ElimType (loc, term) ->
 276       let status, cic = disambiguate_term status term in
 277       status, TacticAst.ElimType (loc, cic)
 278   | TacticAst.Replace (loc, what, with_what) ->
 279       let status, cic1 = disambiguate_term status what in
 280       let status, cic2 = disambiguate_term status with_what in
 281       status, TacticAst.Replace (loc, cic1, cic2)
 282   | TacticAst.Change (loc, what, with_what, ident) ->
 283       let status, cic1 = disambiguate_term status what in
 284       let status, cic2 = disambiguate_term status with_what in
 285       status, TacticAst.Change (loc, cic1, cic2, ident)
 286 (*
 287   (* TODO Zack a lot more of tactics to be implemented here ... *)
 288   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 289   | TacticAst.Change of 'term * 'term * 'ident option
 290   | TacticAst.Decompose of 'ident * 'ident list
 291   | TacticAst.Discriminate of 'ident
 292   | TacticAst.Fold of reduction_kind * 'term
 293   | TacticAst.Injection of 'ident
 294   | TacticAst.LetIn of 'term * 'ident
 295   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
 296   | TacticAst.Replace_pattern of 'term pattern * 'term
 297 *)
 298   | TacticAst.Rewrite (loc,dir,t,ident) ->
 299       let status, term = disambiguate_term status t in
 300       status, TacticAst.Rewrite (loc,dir,term,ident)
 301   | TacticAst.Intros (loc, num, names) ->
 302       status, TacticAst.Intros (loc, num, names)
 303   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 304   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 305   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 306   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 307   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 308   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 309   | TacticAst.Left loc -> status, TacticAst.Left loc
 310   | TacticAst.Right loc -> status, TacticAst.Right loc
 311   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 312   | TacticAst.Split loc -> status, TacticAst.Split loc
 313   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 314   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 315   | x ->
 316       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 317       assert false
 318
 319 let rec disambiguate_tactical status = function
 320   | TacticAst.Tactic (loc, tactic) ->
 321       let status, tac = disambiguate_tactic status tactic in
 322       status, TacticAst.Tactic (loc, tac)
 323   | TacticAst.Do (loc, num, tactical) ->
 324       let status, tac = disambiguate_tactical status tactical in
 325       status, TacticAst.Do (loc, num, tac)
 326   | TacticAst.Repeat (loc, tactical) ->
 327       let status, tac = disambiguate_tactical status tactical in
 328       status, TacticAst.Repeat (loc, tac)
 329   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 330       let status, tacticals = disambiguate_tacticals status tacticals in
 331       let tacticals = List.rev tacticals in
 332       status, TacticAst.Seq (loc, tacticals)
 333   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 334       let status, tactical = disambiguate_tactical status tactical in
 335       let status, tacticals = disambiguate_tacticals status tacticals in
 336       status, TacticAst.Then (loc, tactical, tacticals)
 337   | TacticAst.Tries (loc, tacticals) ->
 338       let status, tacticals = disambiguate_tacticals status tacticals in
 339       status, TacticAst.Tries (loc, tacticals)
 340   | TacticAst.Try (loc, tactical) ->
 341       let status, tactical = disambiguate_tactical status tactical in
 342       status, TacticAst.Try (loc, tactical)
 343   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 344       status, tac
 345
 346 and disambiguate_tacticals status tacticals =
 347   let status, tacticals =
 348     List.fold_left
 349       (fun (status, tacticals) tactical ->
 350         let status, tac = disambiguate_tactical status tactical in
 351         status, tac :: tacticals)
 352       (status, [])
 353       tacticals
 354   in
 355   let tacticals = List.rev tacticals in
 356   status, tacticals
 357
 358 let disambiguate_inddef status params indTypes =
 359   let add_pi binders t =
 360     List.fold_right
 361       (fun (name, ast) acc ->
 362         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 363       binders t
 364   in
 365   let ind_binders =
 366     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 367   in
 368   let binders = ind_binders @ params in
 369   let asts = ref [] in
 370   let add_ast ast = asts := ast :: !asts in
 371   let paramsno = List.length params in
 372   let indbindersno = List.length ind_binders in
 373   List.iter
 374     (fun (name, _, typ, constructors) ->
 375       add_ast (add_pi params typ);
 376       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 377     indTypes;
 378   let status, terms = disambiguate_terms status !asts in
 379   let terms = ref (List.rev terms) in
 380   let get_term () =
 381     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 382   in
 383   let uri =
 384     match indTypes with
 385     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 386     | _ -> assert false
 387   in
 388   let mutinds =
 389     let counter = ref 0 in
 390     List.map
 391       (fun _ ->
 392         incr counter;
 393         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 394       indTypes
 395   in
 396   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 397   let cicIndTypes =
 398     List.fold_left
 399       (fun acc (name, inductive, typ, constructors) ->
 400         let cicTyp = get_term () in
 401         let cicConstructors =
 402           List.fold_left
 403             (fun acc (name, _) ->
 404               let typ =
 405                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 406               in
 407               (name, typ) :: acc)
 408             [] constructors
 409         in
 410         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 411       [] indTypes
 412   in
 413   let cicIndTypes = List.rev cicIndTypes in
 414   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 415
 416 let disambiguate_command status = function
 417   | TacticAst.Inductive (loc, params, types) ->
 418       let (status, (uri, (ind_types, vars, paramsno))) =
 419         disambiguate_inddef status params types
 420       in
 421       let rec mk_list = function
 422         | 0 -> []
 423         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 424       in
 425       (* once we've built the cic inductive types we no longer need terms
 426          corresponding to parameters, but we need the leftno, and we encode
 427          it as the length of dummy_params
 428       *)
 429       let dummy_params = mk_list paramsno in
 430       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 431   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 432       let status, ty = disambiguate_term status ty in
 433       let status, body =
 434         match body with
 435         | None -> status, None
 436         | Some body ->
 437             let status, body = disambiguate_term status body in
 438             status, Some body
 439       in
 440       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 441   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 442   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 443       status, cmd
 444   | TacticAst.Alias _ as x -> status, x
 445
 446 let disambiguate_executable status ex =
 447   match ex with
 448   | TacticAst.Tactical (loc, tac) ->
 449       let status, tac = disambiguate_tactical status tac in
 450       status, (TacticAst.Tactical (loc, tac))
 451   | TacticAst.Command (loc, cmd) ->
 452       let status, cmd = disambiguate_command status cmd in
 453       status, (TacticAst.Command (loc, cmd))
 454   | TacticAst.Macro (_, mac) ->
 455       command_error
 456         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 457                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 458
 459 let disambiguate_comment status c =
 460   match c with
 461   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 462   | TacticAst.Code (loc,ex) ->
 463         let status, ex = disambiguate_executable status ex in
 464         status, TacticAst.Code (loc,ex)
 465
 466 let disambiguate_statement status statement =
 467   match statement with
 468   | TacticAst.Comment (loc,c) ->
 469         let status, c = disambiguate_comment status c in
 470         status, TacticAst.Comment (loc,c)
 471   | TacticAst.Executable (loc,ex) ->
 472         let status, ex = disambiguate_executable status ex in
 473         status, TacticAst.Executable (loc,ex)
 474
 475 let eval_ast status ast =
 476   let status,st = disambiguate_statement status ast in
 477   (* this disambiguation step should be deferred to support tacticals *)
 478   eval status st
 479
 480 let eval_from_stream status str =
 481   let st = CicTextualParser2.parse_statement str in
 482   eval_ast status st
 483
 484 let eval_string status str =
 485   eval_from_stream status (Stream.of_string str)
 486
 487 let default_options () =
 488   let options =
 489     StringMap.add "baseuri"
 490       (String
 491         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 492       no_options
 493   in
 494   let options =
 495     StringMap.add "basedir"
 496       (String (Helm_registry.get "matita.basedir" ))
 497       options
 498   in
 499   options
 500
 501 let initial_status =
 502   lazy {
 503     aliases = DisambiguateTypes.empty_environment;
 504     proof_status = No_proof;
 505     options = default_options ();
 506     coercions = [];
 507     objects = [];
 508   }
 509