+ | GrafiteParser.NoInclusionPerformed mafilename ->
+ let root, buri, _, tgt =
+ try Librarian.baseuri_of_script ~include_paths mafilename
+ with Librarian.NoRootFor _ ->
+ HLog.error ("The included file '"^mafilename^"' has no root file,");
+ HLog.error "please create it.";
+ raise (Failure ("No root file for "^mafilename))
+ in
+ let b = MatitacLib.Make.make root [tgt] in
+ if b then
+ try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
+ raise
+ (Failure ("Including: "^tgt^
+ "\nNothing to do... did you run matitadep?"))
+ else raise (Failure ("Compiling: " ^ tgt))
+;;
+
+let pp_eager_statement_ast =
+ GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+
+(* naive implementation of procedural proof script generation,
+ * starting from an applicatiove *auto generated) proof.
+ * this is out of place, but I like it :-P *)
+let cic2grafite context menv t =
+ (* indents a proof script in a stupid way, better than nothing *)
+ let stupid_indenter s =
+ let next s =
+ let idx_square_o = try String.index s '[' with Not_found -> -1 in
+ let idx_square_c = try String.index s ']' with Not_found -> -1 in
+ let idx_pipe = try String.index s '|' with Not_found -> -1 in
+ let tok =
+ List.sort (fun (i,_) (j,_) -> compare i j)
+ [idx_square_o,'[';idx_square_c,']';idx_pipe,'|']
+ in
+ let tok = List.filter (fun (i,_) -> i <> -1) tok in
+ match tok with
+ | (i,c)::_ -> Some (i,c)
+ | _ -> None
+ in
+ let break_apply n s =
+ let tab = String.make (n+1) ' ' in
+ Pcre.replace ~templ:(".\n" ^ tab ^ "apply") ~pat:"\\.apply" s
+ in
+ let rec ind n s =
+ match next s with
+ | None ->
+ s
+ | Some (position, char) ->
+ try
+ let s1, s2 =
+ String.sub s 0 position,
+ String.sub s (position+1) (String.length s - (position+1))
+ in
+ match char with
+ | '[' -> break_apply n s1 ^ "\n" ^ String.make (n+2) ' ' ^
+ "[" ^ ind (n+2) s2
+ | '|' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^
+ "|" ^ ind n s2
+ | ']' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^
+ "]" ^ ind (n-2) s2
+ | _ -> assert false
+ with
+ Invalid_argument err ->
+ prerr_endline err;
+ s
+ in
+ ind 0 s
+ in
+ let module PT = CicNotationPt in
+ let module GA = GrafiteAst in
+ let pp_t context t =
+ let names =
+ List.map (function Some (n,_) -> Some n | None -> None) context
+ in
+ CicPp.pp t names
+ in
+ let sort_of context t =
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux' menv context t
+ CicUniv.oblivion_ugraph
+ in
+ let sort,_ = CicTypeChecker.type_of_aux' menv context ty
+ CicUniv.oblivion_ugraph
+ in
+ match sort with
+ | Cic.Sort Cic.Prop -> true
+ | _ -> false
+ with
+ CicTypeChecker.TypeCheckerFailure _ ->
+ HLog.error "auto proof to sript transformation error"; false
+ in
+ let floc = HExtlib.dummy_floc in
+ (* minimalisti cic.term -> pt.term *)
+ let print_term c t =
+ let rec aux c = function
+ | Cic.Rel _
+ | Cic.MutConstruct _
+ | Cic.MutInd _
+ | Cic.Const _ as t ->
+ PT.Ident (pp_t c t, None)
+ | Cic.Appl l -> PT.Appl (List.map (aux c) l)
+ | Cic.Implicit _ -> PT.Implicit `JustOne
+ | Cic.Lambda (Cic.Name n, s, t) ->
+ PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Decl s)::c) t)
+ | Cic.Prod (Cic.Name n, s, t) ->
+ PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Decl s)::c) t)
+ | Cic.LetIn (Cic.Name n, s, ty, t) ->
+ PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
+ | Cic.Meta _ -> PT.Implicit `JustOne
+ | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
+ | Cic.Sort Cic.Set -> PT.Sort `Set
+ | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
+ | Cic.Sort Cic.Prop -> PT.Sort `Prop
+ | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
+ in
+ aux c t
+ in
+ (* prints an applicative proof, that is an auto proof.
+ * don't use in the general case! *)
+ let rec print_proof context = function
+ | Cic.Rel _
+ | Cic.Const _ as t ->
+ [GA.Executable (floc,
+ GA.Tactic (floc,
+ Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
+ | Cic.Appl (he::tl) ->
+ let tl = List.map (fun t -> t, sort_of context t) tl in
+ let subgoals =
+ HExtlib.filter_map (function (t,true) -> Some t | _ -> None) tl
+ in
+ let args =
+ List.map (function | (t,true) -> Cic.Implicit None | (t,_) -> t) tl