helm/matita/matitaEngine.ml

   1
   2 open Printf
   3 open MatitaTypes
   4
   5 let debug = true ;;
   6 let debug_print = if debug then prerr_endline else ignore ;;
   7
   8 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   9   * names as long as they are available, then it fallbacks to name generation
  10   * using FreshNamesGenerator module *)
  11 let namer_of names =
  12   let len = List.length names in
  13   let count = ref 0 in
  14   fun metasenv context name ~typ ->
  15     if !count < len then begin
  16       let name = Cic.Name (List.nth names !count) in
  17       incr count;
  18       name
  19     end else
  20       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  21
  22 let tactic_of_ast = function
  23   | TacticAst.Intros (_, None, names) ->
  24       (* TODO Zack implement intros length *)
  25       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  26   | TacticAst.Intros (_, Some num, names) ->
  27       (* TODO Zack implement intros length *)
  28       PrimitiveTactics.intros_tac ~howmany:num
  29         ~mk_fresh_name_callback:(namer_of names) ()
  30   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  31   | TacticAst.Assumption _ -> Tactics.assumption
  32   | TacticAst.Contradiction _ -> Tactics.contradiction
  33   | TacticAst.Exists _ -> Tactics.exists
  34   | TacticAst.Fourier _ -> Tactics.fourier
  35   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  36   | TacticAst.Left _ -> Tactics.left
  37   | TacticAst.Right _ -> Tactics.right
  38   | TacticAst.Ring _ -> Tactics.ring
  39   | TacticAst.Split _ -> Tactics.split
  40   | TacticAst.Symmetry _ -> Tactics.symmetry
  41   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  42   | TacticAst.Apply (_, term) -> Tactics.apply term
  43   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  44   | TacticAst.Exact (_, term) -> Tactics.exact term
  45   | TacticAst.Cut (_, term) -> Tactics.cut term
  46   | TacticAst.Elim (_, term, _) ->
  47       (* TODO Zack implement "using" argument *)
  48       (* old: Tactics.elim_intros_simpl term *)
  49       Tactics.elim_intros term
  50   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  51   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  52   | TacticAst.Auto (_,num) ->
  53       AutoTactic.auto_tac ~num (MatitaDb.instance ())
  54   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  55 (*
  56   (* TODO Zack a lot more of tactics to be implemented here ... *)
  57   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  58   | TacticAst.Change of 'term * 'term * 'ident option
  59   | TacticAst.Decompose of 'ident * 'ident list
  60   | TacticAst.Discriminate of 'ident
  61   | TacticAst.Fold of reduction_kind * 'term
  62   | TacticAst.Injection of 'ident
  63   | TacticAst.Replace_pattern of 'term pattern * 'term
  64 *)
  65   | TacticAst.LetIn (loc,term,name) ->
  66       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
  67   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
  68       ProofEngineTypes.mk_tactic
  69       (fun (((_,metasenv,_,_),goal) as status) ->
  70          let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  71          let where, also_in_hypotheses =
  72            if ident = "goal" then
  73              ty, false
  74            else
  75              let hyp =
  76                try
  77                  List.find (function
  78                    | Some (Cic.Name name,entry) when name = ident -> true
  79                    | _ -> false)
  80                  context
  81                with
  82                  Not_found ->
  83                    raise (ProofEngineTypes.Fail
  84                             (ident ^ " is not an hypothesis"))
  85              in
  86              (match hyp with
  87              | Some (_, Cic.Decl term) -> term
  88              | Some (_, Cic.Def (term,ty)) -> term
  89              | None -> assert false),true
  90          in
  91          let pointers = CicUtil.select ~term:where ~context:path in
  92           (match reduction_kind with
  93           | `Normalize ->
  94               ProofEngineTypes.apply_tactic
  95                 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
  96                 status
  97           | `Reduce ->
  98               ProofEngineTypes.apply_tactic
  99                 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
 100                 status
 101           | `Simpl ->
 102               ProofEngineTypes.apply_tactic
 103                 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
 104                 status
 105           | `Whd ->
 106               ProofEngineTypes.apply_tactic
 107                 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
 108                 status))
 109   | TacticAst.Reduce (_,reduction_kind,opts) ->
 110       let terms, also_in_hypotheses =
 111         match opts with
 112         | Some (l,`Goal) -> Some l, false
 113         | Some (l,`Everywhere) -> Some l, true
 114         | None -> None, false
 115       in
 116       (match reduction_kind with
 117       | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
 118       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
 119       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
 120       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
 121   | TacticAst.Rewrite (_,dir,t,ident) ->
 122       if dir = `Left then
 123         EqualityTactics.rewrite_tac ~term:t
 124       else
 125         EqualityTactics.rewrite_back_tac ~term:t
 126   | _ -> assert false
 127
 128 let eval_tactical status tac =
 129   let apply_tactic tactic =
 130     let (proof, goals) =
 131       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
 132     in
 133     let new_status =
 134       match goals with
 135       | [] ->
 136           let (_,metasenv,_,_) = proof in
 137           (match metasenv with
 138           | [] -> Proof proof
 139           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
 140       | ng::_ -> Incomplete_proof (proof, ng)
 141     in
 142     { status with proof_status = new_status }
 143   in
 144   let rec tactical_of_ast = function
 145     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
 146     | TacticAst.Fail loc -> Tacticals.fail
 147     | TacticAst.Do (loc, num, tactical) ->
 148         Tacticals.do_tactic num (tactical_of_ast tactical)
 149     | TacticAst.IdTac loc -> Tacticals.id_tac
 150     | TacticAst.Repeat (loc, tactical) ->
 151         Tacticals.repeat_tactic (tactical_of_ast tactical)
 152     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 153         Tacticals.seq (List.map tactical_of_ast tacticals)
 154     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 155         Tacticals.thens (tactical_of_ast tactical)
 156           (List.map tactical_of_ast tacticals)
 157     | TacticAst.Tries (loc, tacticals) ->
 158         Tacticals.try_tactics
 159           (List.map (fun t -> "", tactical_of_ast t) tacticals)
 160     | TacticAst.Try (loc, tactical) ->
 161         Tacticals.try_tactic (tactical_of_ast tactical)
 162   in
 163   apply_tactic (tactical_of_ast tac)
 164
 165 let eval_coercion status coercion =
 166   let coer_uri,coer_ty =
 167     match coercion with
 168     | Cic.Const (uri,_)
 169     | Cic.Var (uri,_) ->
 170         let o,_ =
 171           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 172         in
 173         (match o with
 174         | Cic.Constant (_,_,ty,_,_)
 175         | Cic.Variable (_,_,ty,_,_) ->
 176             uri,ty
 177         | _ -> assert false)
 178     | Cic.MutConstruct (uri,t,c,_) ->
 179         let o,_ =
 180           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 181         in
 182         (match o with
 183         | Cic.InductiveDefinition (l,_,_,_) ->
 184             let (_,_,_,cl) = List.nth l t in
 185             let (_,cty) = List.nth cl c in
 186               uri,cty
 187         | _ -> assert false)
 188     | _ -> assert false
 189   in
 190   (* we have to get the source and the tgt type uri
 191    * in Coq syntax we have already their names, but
 192    * since we don't support Funclass and similar I think
 193    * all the coercion should be of the form
 194    * (A:?)(B:?)T1->T2
 195    * So we should be able to extract them from the coercion type
 196    *)
 197   let extract_last_two_p ty =
 198     let rec aux = function
 199       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
 200       | Cic.Prod( _, src, tgt) -> src, tgt
 201       | _ -> assert false
 202     in
 203     aux ty
 204   in
 205   let ty_src,ty_tgt = extract_last_two_p coer_ty in
 206   let context = [] in
 207   let src_uri =
 208     let ty_src = CicReduction.whd context ty_src in
 209     UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
 210   in
 211   let tgt_uri =
 212     let ty_tgt = CicReduction.whd context ty_tgt in
 213     UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
 214   in
 215   let new_coercions =
 216     (* also adds them to the Db *)
 217     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
 218   in
 219   let status =
 220     List.fold_left (
 221       fun s (uri,o,ugraph) ->
 222         match o with
 223         | Cic.Constant (_,Some body, ty, params, attrs) ->
 224             MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
 225         | _ -> assert false
 226     ) status new_coercions
 227   in
 228   {status with proof_status = No_proof}
 229
 230 let eval_command status cmd =
 231   match cmd with
 232   | TacticAst.Set (loc, name, value) -> set_option status name value
 233   | TacticAst.Qed loc ->
 234       let uri, metasenv, bo, ty =
 235         match status.proof_status with
 236         | Proof (Some uri, metasenv, body, ty) ->
 237             uri, metasenv, body, ty
 238         | Proof (None, metasenv, body, ty) ->
 239             command_error
 240               ("Someone allows to start a thm without giving the "^
 241                "name/uri. This should be fixed!")
 242         | _-> command_error "You can't qed an uncomplete theorem"
 243       in
 244       let suri = UriManager.string_of_uri uri in
 245       if metasenv <> [] then
 246         command_error "Proof not completed! metasenv is not empty!";
 247       let proved_ty,ugraph =
 248         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 249       in
 250       let b,ugraph =
 251         CicReduction.are_convertible [] proved_ty ty ugraph
 252       in
 253       if not b then
 254         command_error
 255           ("The type of your proof is not convertible with the "^
 256           "type you've declared!");
 257       MatitaLog.message (sprintf "%s defined" suri);
 258       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 259       {status with proof_status = No_proof }
 260   | TacticAst.Record (loc, params, name, ty, fields) ->
 261       let suri = MatitaMisc.qualify status name ^ ".ind" in
 262       let record_spec = (suri, params, ty, fields) in
 263       let status = MatitaSync.add_record_def record_spec status in
 264       {status with proof_status = No_proof }
 265   | TacticAst.Inductive (loc, dummy_params, types) ->
 266       (* dummy_params are not real params, it is a list of nothing, and the only
 267        * semantic content is the len, that is leftno (note: leftno and
 268        * paramaters have nothing in common).
 269        *)
 270       let suri =
 271         match types with
 272         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 273         | _ -> assert false
 274       in
 275       let uri = UriManager.uri_of_string suri in
 276       let leftno = List.length dummy_params in
 277       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 278       let ugraph =
 279         CicTypeChecker.typecheck_mutual_inductive_defs uri
 280           (types, [], leftno) CicUniv.empty_ugraph
 281       in
 282       let status =
 283         MatitaSync.add_inductive_def ~uri ~types ~leftno ~ugraph status
 284       in
 285       {status with proof_status = No_proof }
 286   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 287       let uri =
 288         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 289       in
 290       let goalno = 1 in
 291       let metasenv, body =
 292         match status.proof_status with
 293         | Intermediate metasenv ->
 294             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 295         | _-> assert false
 296       in
 297       let initial_proof = (Some uri, metasenv, body, ty) in
 298       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 299   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 300       let uri =
 301         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 302       in
 303       let metasenv = MatitaMisc.get_proof_metasenv status in
 304       let (body_type, ugraph) =
 305         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 306       in
 307       let (subst, metasenv, ugraph) =
 308         CicUnification.fo_unif metasenv [] body_type ty ugraph
 309       in
 310       if metasenv <> [] then
 311         command_error (
 312           "metasenv not empty while giving a definition with body: " ^
 313           CicMetaSubst.ppmetasenv metasenv []) ;
 314       let body = CicMetaSubst.apply_subst subst body in
 315       let ty = CicMetaSubst.apply_subst subst ty in
 316       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
 317       {status with proof_status = No_proof}
 318   | TacticAst.Theorem (_, _, None, _, _) ->
 319       command_error "The grammar should avoid having unnamed theorems!"
 320   | TacticAst.Coercion (loc, coercion) ->
 321       eval_coercion status coercion
 322   | TacticAst.Alias (loc, spec) ->
 323       match spec with
 324       | TacticAst.Ident_alias (id,uri) ->
 325           {status with aliases =
 326             DisambiguateTypes.Environment.add
 327               (DisambiguateTypes.Id id)
 328               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 329               status.aliases }
 330       | TacticAst.Symbol_alias (symb, instance, desc) ->
 331           {status with aliases =
 332             DisambiguateTypes.Environment.add
 333               (DisambiguateTypes.Symbol (symb,instance))
 334               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 335               status.aliases }
 336       | TacticAst.Number_alias (instance,desc) ->
 337           {status with aliases =
 338             DisambiguateTypes.Environment.add
 339               (DisambiguateTypes.Num instance)
 340               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 341
 342 let eval_executable status ex =
 343   match ex with
 344   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 345   | TacticAst.Command (_, cmd) -> eval_command status cmd
 346   | TacticAst.Macro (_, mac) ->
 347       command_error (sprintf "The macro %s can't be in a script"
 348         (TacticAstPp.pp_macro_cic mac))
 349
 350 let eval_comment status c = status
 351
 352 let eval status st =
 353   match st with
 354   | TacticAst.Executable (_,ex) -> eval_executable status ex
 355   | TacticAst.Comment (_,c) -> eval_comment status c
 356
 357 let disambiguate_term status term =
 358   let (aliases, metasenv, cic, _) =
 359     match
 360       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 361         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 362         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 363     with
 364     | [x] -> x
 365     | _ -> assert false
 366   in
 367   let proof_status =
 368     match status.proof_status with
 369     | No_proof -> Intermediate metasenv
 370     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 371         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 372     | Intermediate _ -> Intermediate metasenv
 373     | Proof _ -> assert false
 374   in
 375   let status =
 376     { status with
 377         aliases = aliases;
 378         proof_status = proof_status }
 379   in
 380   status, cic
 381
 382 let disambiguate_closedtypes status terms =
 383   let term = CicAst.pack terms in
 384   let status, term = disambiguate_term status term in
 385   status, CicUtil.unpack term
 386
 387 let disambiguate_tactic status = function
 388   | TacticAst.Transitivity (loc, term) ->
 389       let status, cic = disambiguate_term status term in
 390       status, TacticAst.Transitivity (loc, cic)
 391   | TacticAst.Apply (loc, term) ->
 392       let status, cic = disambiguate_term status term in
 393       status, TacticAst.Apply (loc, cic)
 394   | TacticAst.Absurd (loc, term) ->
 395       let status, cic = disambiguate_term status term in
 396       status, TacticAst.Absurd (loc, cic)
 397   | TacticAst.Exact (loc, term) ->
 398       let status, cic = disambiguate_term status term in
 399       status, TacticAst.Exact (loc, cic)
 400   | TacticAst.Cut (loc, term) ->
 401       let status, cic = disambiguate_term status term in
 402       status, TacticAst.Cut (loc, cic)
 403   | TacticAst.Elim (loc, term, Some term') ->
 404       let status, cic1 = disambiguate_term status term in
 405       let status, cic2 = disambiguate_term status term' in
 406       status, TacticAst.Elim (loc, cic1, Some cic2)
 407   | TacticAst.Elim (loc, term, None) ->
 408       let status, cic = disambiguate_term status term in
 409       status, TacticAst.Elim (loc, cic, None)
 410   | TacticAst.ElimType (loc, term) ->
 411       let status, cic = disambiguate_term status term in
 412       status, TacticAst.ElimType (loc, cic)
 413   | TacticAst.Replace (loc, what, with_what) ->
 414       let status, cic1 = disambiguate_term status what in
 415       let status, cic2 = disambiguate_term status with_what in
 416       status, TacticAst.Replace (loc, cic1, cic2)
 417   | TacticAst.Change (loc, what, with_what, ident) ->
 418       let status, cic1 = disambiguate_term status what in
 419       let status, cic2 = disambiguate_term status with_what in
 420       status, TacticAst.Change (loc, cic1, cic2, ident)
 421 (*
 422   (* TODO Zack a lot more of tactics to be implemented here ... *)
 423   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 424   | TacticAst.Change of 'term * 'term * 'ident option
 425   | TacticAst.Decompose of 'ident * 'ident list
 426   | TacticAst.Discriminate of 'ident
 427   | TacticAst.Fold of reduction_kind * 'term
 428   | TacticAst.Injection of 'ident
 429   | TacticAst.Replace_pattern of 'term pattern * 'term
 430 *)
 431   | TacticAst.LetIn (loc,term,name) ->
 432       let status, term = disambiguate_term status term in
 433       status, TacticAst.LetIn (loc,term,name)
 434   | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
 435       let path = Disambiguate.interpretate [] status.aliases path in
 436       status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
 437   | TacticAst.Reduce (loc, reduction_kind, opts) ->
 438       let status, opts =
 439         match opts with
 440         | None -> status, None
 441         | Some (l,pat) ->
 442             let status, l =
 443               List.fold_right (fun t (status,acc) ->
 444                 let status',t' = disambiguate_term status t in
 445                 status', t'::acc)
 446               l (status,[])
 447             in
 448             status, Some (l, pat)
 449       in
 450       status, TacticAst.Reduce (loc, reduction_kind, opts)
 451   | TacticAst.Rewrite (loc,dir,t,ident) ->
 452       let status, term = disambiguate_term status t in
 453       status, TacticAst.Rewrite (loc,dir,term,ident)
 454   | TacticAst.Intros (loc, num, names) ->
 455       status, TacticAst.Intros (loc, num, names)
 456   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 457   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 458   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 459   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 460   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 461   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 462   | TacticAst.Left loc -> status, TacticAst.Left loc
 463   | TacticAst.Right loc -> status, TacticAst.Right loc
 464   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 465   | TacticAst.Split loc -> status, TacticAst.Split loc
 466   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 467   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 468   | x ->
 469       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 470       assert false
 471
 472 let rec disambiguate_tactical status = function
 473   | TacticAst.Tactic (loc, tactic) ->
 474       let status, tac = disambiguate_tactic status tactic in
 475       status, TacticAst.Tactic (loc, tac)
 476   | TacticAst.Do (loc, num, tactical) ->
 477       let status, tac = disambiguate_tactical status tactical in
 478       status, TacticAst.Do (loc, num, tac)
 479   | TacticAst.Repeat (loc, tactical) ->
 480       let status, tac = disambiguate_tactical status tactical in
 481       status, TacticAst.Repeat (loc, tac)
 482   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 483       let status, tacticals = disambiguate_tacticals status tacticals in
 484       let tacticals = List.rev tacticals in
 485       status, TacticAst.Seq (loc, tacticals)
 486   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 487       let status, tactical = disambiguate_tactical status tactical in
 488       let status, tacticals = disambiguate_tacticals status tacticals in
 489       status, TacticAst.Then (loc, tactical, tacticals)
 490   | TacticAst.Tries (loc, tacticals) ->
 491       let status, tacticals = disambiguate_tacticals status tacticals in
 492       status, TacticAst.Tries (loc, tacticals)
 493   | TacticAst.Try (loc, tactical) ->
 494       let status, tactical = disambiguate_tactical status tactical in
 495       status, TacticAst.Try (loc, tactical)
 496   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 497       status, tac
 498
 499 and disambiguate_tacticals status tacticals =
 500   let status, tacticals =
 501     List.fold_left
 502       (fun (status, tacticals) tactical ->
 503         let status, tac = disambiguate_tactical status tactical in
 504         status, tac :: tacticals)
 505       (status, [])
 506       tacticals
 507   in
 508   let tacticals = List.rev tacticals in
 509   status, tacticals
 510
 511 let disambiguate_inddef status params indTypes =
 512   let add_pi binders t =
 513     List.fold_right
 514       (fun (name, ast) acc ->
 515         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 516       binders t
 517   in
 518   let ind_binders =
 519     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 520   in
 521   let binders = ind_binders @ params in
 522   let asts = ref [] in
 523   let add_ast ast = asts := ast :: !asts in
 524   let paramsno = List.length params in
 525   let indbindersno = List.length ind_binders in
 526   List.iter
 527     (fun (name, _, typ, constructors) ->
 528       add_ast (add_pi params typ);
 529       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 530     indTypes;
 531   let status, terms = disambiguate_closedtypes status !asts in
 532   let terms = ref (List.rev terms) in
 533   let get_term () =
 534     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 535   in
 536   let uri =
 537     match indTypes with
 538     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 539     | _ -> assert false
 540   in
 541   let mutinds =
 542     let counter = ref 0 in
 543     List.map
 544       (fun _ ->
 545         incr counter;
 546         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 547       indTypes
 548   in
 549   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 550   let cicIndTypes =
 551     List.fold_left
 552       (fun acc (name, inductive, typ, constructors) ->
 553         let cicTyp = get_term () in
 554         let cicConstructors =
 555           List.fold_left
 556             (fun acc (name, _) ->
 557               let typ =
 558                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 559               in
 560               (name, typ) :: acc)
 561             [] constructors
 562         in
 563         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 564       [] indTypes
 565   in
 566   let cicIndTypes = List.rev cicIndTypes in
 567   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 568
 569 let disambiguate_record status params ty fields =
 570   let packed =
 571     List.fold_right
 572       (fun (name,ast) acc ->
 573         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 574     (params @ ["",ty] @ fields) (CicAst.Sort `Type)
 575   in
 576   prerr_endline (CicAstPp.pp_term packed);
 577   let status, packed = disambiguate_term status packed in
 578   let rec split t = function
 579     | [] -> [],t
 580     | (n,_)::tl ->
 581         match t with
 582         | Cic.Prod (_, src, tgt) ->
 583             let l, t = split tgt tl in
 584             (n, src) :: l, t
 585         | _-> assert false
 586   in
 587   let params, t = split packed params in
 588   let ty, t =
 589     match t with
 590     | Cic.Prod (_ , ty, t) -> ty, t
 591     | _ -> assert false
 592   in
 593   let fields, _ =
 594     split (let t,_,_ = CicMetaSubst.delift_rels [] [] 1 t in t) fields
 595   in
 596   params, ty, fields
 597
 598 let disambiguate_command status = function
 599   | TacticAst.Record(loc, params,name,ty,fields) ->
 600       let params, ty, fields =
 601         disambiguate_record status params ty fields
 602       in
 603       status, TacticAst.Record(loc, params, name, ty, fields)
 604   | TacticAst.Inductive (loc, params, types) ->
 605       let (status, (uri, (ind_types, vars, paramsno))) =
 606         disambiguate_inddef status params types
 607       in
 608       let rec mk_list = function
 609         | 0 -> []
 610         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 611       in
 612       (* once we've built the cic inductive types we no longer need terms
 613          corresponding to parameters, but we need the leftno, and we encode
 614          it as the length of dummy_params
 615       *)
 616       let dummy_params = mk_list paramsno in
 617       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 618   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 619       let status, ty = disambiguate_term status ty in
 620       let status, body =
 621         match body with
 622         | None -> status, None
 623         | Some body ->
 624             let status, body = disambiguate_term status body in
 625             status, Some body
 626       in
 627       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 628   | TacticAst.Coercion (loc, term) ->
 629       let status, term = disambiguate_term status term in
 630       status, TacticAst.Coercion (loc,term)
 631   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 632       status, cmd
 633   | TacticAst.Alias _ as x -> status, x
 634
 635 let disambiguate_executable status ex =
 636   match ex with
 637   | TacticAst.Tactical (loc, tac) ->
 638       let status, tac = disambiguate_tactical status tac in
 639       status, (TacticAst.Tactical (loc, tac))
 640   | TacticAst.Command (loc, cmd) ->
 641       let status, cmd = disambiguate_command status cmd in
 642       status, (TacticAst.Command (loc, cmd))
 643   | TacticAst.Macro (_, mac) ->
 644       command_error (sprintf "The macro %s can't be in a script"
 645         (TacticAstPp.pp_macro_ast mac))
 646
 647 let disambiguate_comment status c =
 648   match c with
 649   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 650   | TacticAst.Code (loc,ex) ->
 651         let status, ex = disambiguate_executable status ex in
 652         status, TacticAst.Code (loc,ex)
 653
 654 let disambiguate_statement status statement =
 655   match statement with
 656   | TacticAst.Comment (loc,c) ->
 657         let status, c = disambiguate_comment status c in
 658         status, TacticAst.Comment (loc,c)
 659   | TacticAst.Executable (loc,ex) ->
 660         let status, ex = disambiguate_executable status ex in
 661         status, TacticAst.Executable (loc,ex)
 662
 663 let eval_ast status ast =
 664   let status,st = disambiguate_statement status ast in
 665   (* this disambiguation step should be deferred to support tacticals *)
 666   eval status st
 667
 668 let eval_from_stream status str cb =
 669   let stl = CicTextualParser2.parse_statements str in
 670   List.fold_left
 671     (fun status ast -> cb status ast;eval_ast status ast) status
 672   stl
 673
 674 let eval_string status str =
 675   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 676
 677 let default_options () =
 678   let options =
 679     StringMap.add "baseuri"
 680       (String
 681         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 682       no_options
 683   in
 684   let options =
 685     StringMap.add "basedir"
 686       (String (Helm_registry.get "matita.basedir" ))
 687       options
 688   in
 689   options
 690
 691 let initial_status =
 692   lazy {
 693     aliases = DisambiguateTypes.empty_environment;
 694     proof_status = No_proof;
 695     options = default_options ();
 696     objects = [];
 697   }
 698
 699