-let collect_arities_from_formulae f =
- let rec collect_arities_from_formulae = function
- | A.Disjunction (a,b) ->
- collect_arities_from_formulae a @ collect_arities_from_formulae b
- | A.NegAtom a
- | A.Atom a -> collect_arities_from_atom [a]
- in
- HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
-;;
-
-let is_formulae_1eq_negated f =
- let atom = atom_of_formula f in
- match atom with
- | [A.NotEq (l,r)] -> true
- | _ -> false
-;;
-
-let collect_fv_1stord_from_formulae f =
- let arities = collect_arities_from_formulae f in
- let fv = collect_fv_from_formulae f in
- List.map fst
- (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
-;;
-
-let rec convert_formula fv no_arities context f =
- let atom = atom_of_formula f in
- let t = convert_atom (fv = []) atom in
- let rec build_ctx n = function
- | [] -> t
- | hp::tl ->
- PT.Binder
- (`Forall,
- (mk_ident ("H" ^ string_of_int n),
- Some (convert_formula [] true [] hp)),
- build_ctx (n+1) tl)
- in
- let arities = if no_arities then [] else collect_arities atom context in
- build_ctx_for_arities true arities (build_ctx 0 context)
-;;
-
-let check_if_atom_is_negative = function
- | A.True -> false
- | A.False -> true
- | A.Proposition _ -> false
- | A.Predicate _ -> false
- | A.Eq _ -> false
- | A.NotEq _ -> true
-;;
-
-let rec check_if_formula_is_negative = function
- | A.Disjunction (a,b) ->
- check_if_formula_is_negative a && check_if_formula_is_negative b
- | A.NegAtom a -> not (check_if_atom_is_negative a)
- | A.Atom a -> check_if_atom_is_negative a
-;;
-
-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;PT.Implicit;
- PT.Implicit;PT.Implicit]);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
- | A.Comment s ->
- let s = String.sub s 1 (String.length s - 1) in
- let s =
- if s.[String.length s - 1] = '\n' then
- String.sub s 0 (String.length s - 1)
- else
- s
- in
- statements @ [GA.Comment (floc,GA.Note (floc,s))],
- context
- | A.Inclusion (s,_) ->
- statements @ [
- GA.Comment (
- floc, GA.Note (
- floc,"Inclusion of: " ^ s))], context
- | A.AnnotatedFormula (name,kind,f,_,_) ->
- match kind with
- | A.Axiom
- | A.Hypothesis ->
- statements, f::context
- | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
- statements, f::context
- | A.Negated_conjecture ->
- let ueq_case = is_formulae_1eq_negated f in
- let fv = collect_fv_1stord_from_formulae f in
- let old_f = f in
- let f =
- PT.Binder
- (`Forall,
- (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))),
- convert_formula fv false context f)
- in
- let o = PT.Theorem (`Theorem,name,f,None) in
- (statements @
- [ GA.Executable(floc,GA.Command(floc,
- (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
- if ng then
- ng_generate_tactics fv ueq_case context
- (let atom = atom_of_formula old_f in collect_arities atom context)
- else generate_tactics fv ueq_case),
- context
- | A.Definition
- | A.Lemma
- | A.Theorem
- | A.Conjecture
- | A.Lemma_conjecture
- | A.Plain
- | A.Unknown -> assert false
-;;