+let ng_generate_tactics fv ueq_case context arities =
+ [ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
+ @
+ (HExtlib.list_mapi
+ (fun (name,_) _->
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+ GA.NDot(floc)])))
+ arities)
+ @
+ (HExtlib.list_mapi
+ (fun _ i->
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
+ context)
+ @
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.NTactic(floc,
+ [GA.NApply (floc,
+ PT.Appl
+ [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+ PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NPos (floc,[2])]))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.NTactic(floc, [
+ if (*ueq_case*) true then
+ GA.NAuto (floc,(
+ HExtlib.list_mapi
+ (fun _ i ->
+ mk_ident ("H" ^ string_of_int i))
+ context
+ ,[]))
+ else
+ GA.NAuto (floc,([],[
+ "depth",string_of_int 5;
+ "width",string_of_int 5;
+ "size",string_of_int 20;
+ "timeout",string_of_int 10;
+ ]))
+ ;
+ GA.NSemicolon(floc)]));
+(*
+ GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))
+*)
+ ]@
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
+ GA.NSkip floc; GA.NMerge floc]))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+ GA.NSemicolon(floc)]))]@
+ [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
+;;
+
+let generate_tactics fv ueq_case =
+ [GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Exists floc),GA.Branch floc));
+ GA.Executable(floc,GA.Tactic(floc, None,
+ (GA.Pos (floc,[2]))))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.Tactic(floc, Some (
+ if true (*ueq_case*) then
+ GA.AutoBatch (floc,([],["paramodulation","";
+ "timeout",string_of_int !paramod_timeout]))
+ else
+ GA.AutoBatch (floc,([],[
+ "depth",string_of_int 5;
+ "width",string_of_int 5;
+ "size",string_of_int 20;
+ "timeout",string_of_int 10;
+ ]))
+ ),
+ GA.Semicolon(floc)));
+ GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))
+ ]@
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
+ GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
+ (GA.Merge floc)))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
+ GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
+;;
+
+let convert_ast ng statements context = function