diff --git a/main.ml b/main.ml index 12ca508..b62bbc2 100644 --- a/main.ml +++ b/main.ml @@ -206,113 +206,134 @@ while !subgoals <> [] do let f = !fill_holes in match tactic with - | Intro var -> ( + | Intro var -> ( match ty with - | TImpl (ty1, ty2) -> ( + | TImpl (ty1, ty2) -> ( subgoals := List.tl !subgoals; subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals; fill_holes := fun holes -> match holes with - | h :: hs -> f (LFun (var, ty1, h) :: hs) - | _ -> raise TrouException + | h :: hs -> f (LFun (var, ty1, h) :: hs) + | _ -> raise TrouException ) - | _ -> raise (TacticException(tactic, "Cannot intro when the goal is no implication.")) + | _ -> raise (TacticException(tactic, "Cannot intro when the goal is not an implication.")) ) - | Intros [] -> () - | Intros (t :: ts) -> ( - applyTactic (Intro t); - applyTactic (Intros ts) - ) - | Assumption -> ( + | Intros [] -> () + | Intros (t :: ts) -> ( + applyTactic (Intro t); + applyTactic (Intros ts) + ) + | Assumption -> ( let rec explore = function - | (var, hyp) :: _ when hyp = ty -> ( + | (var, hyp) :: _ when hyp = ty -> ( subgoals := List.tl !subgoals; fill_holes := fun holes -> f ((LVar var) :: holes) ) - | [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal.")) - | _ :: hyps -> explore hyps + | [] -> raise (TacticException (tactic, "Cannot find such an assumption.")) + | _ :: hyps -> explore hyps in explore hyps ) - | Apply var -> ( + | Apply var -> ( match find_hyp var with - | Some (TImpl (t1, t2)) when t2 = ty -> ( + | Some (TImpl (t1, t2)) when t2 = ty -> ( subgoals := List.tl !subgoals; subgoals := (t1, hyps) :: !subgoals; fill_holes := function - | hole :: holes -> f ((LApp (LVar var, hole)) :: holes) - | [] -> raise TrouException + | hole :: holes -> f ((LApp (LVar var, hole)) :: holes) + | [] -> raise TrouException ) - | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist.")) - | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is no implication.")) + | None -> raise (TacticException ( + tactic, + "Cannot apply hypotesis " ^ var ^ " as it does not exist." + )) + | _ -> raise (TacticException ( + tactic, + "Cannot apply hypotesis " ^ var ^ " as it is not an implication." + )) ) - | Elim var -> ( + | Elim var -> ( match find_hyp var with - | Some TFalse -> ( + | Some TFalse -> ( subgoals := List.tl !subgoals; fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) - ) - | Some TAnd(tl,tr) -> ( - subgoals := List.tl !subgoals; - subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals; - fill_holes := fun holes -> match holes with - | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r) - | _ -> raise TrouException ) - | Some TOr(tl,tr) -> ( + | Some TAnd(tl,tr) -> ( subgoals := List.tl !subgoals; - subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals; + subgoals := (TImpl (tl, TImpl (tr, ty)), hyps) :: !subgoals; fill_holes := fun holes -> match holes with - | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r) - | _ -> raise TrouException + | h::r -> f ((LApp (LApp (h, LFst (LVar var)), LSnd (LVar var))) :: r) + | _ -> raise TrouException ) - | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist.")) - | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is neither an implication, nor a /\\ or a \\/")) + | Some TOr(tl,tr) -> ( + subgoals := List.tl !subgoals; + subgoals := (TImpl (tl, ty), hyps) :: (TImpl (tr, ty), hyps) :: !subgoals; + fill_holes := fun holes -> match holes with + | hl::hr::r -> f (LCase (LVar var, hl, hr) :: r) + | _ -> raise TrouException + ) + | None -> raise (TacticException ( + tactic, + "Cannot apply hypotesis " ^ var ^ " as it does not exist." + )) + | _ -> raise (TacticException ( + tactic, + "Cannot apply hypotesis " ^ var ^ " as it is neither an implication, a /\\ nor a \\/" + )) ) - (* Pour montrer A, on montre B -> A et B *) - | Cut tint -> ( + (* Pour montrer A, on montre B -> A et B *) + | Cut tint -> ( subgoals := List.tl !subgoals; subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals; fill_holes := function - | pf :: px :: s -> f ((LApp (pf, px)) :: s) - | _ -> raise TrouException + | pf :: px :: s -> f ((LApp (pf, px)) :: s) + | _ -> raise TrouException ) - | Split -> ( + | Split -> ( match ty with - | TAnd(t1,t2) -> ( + | TAnd(t1,t2) -> ( subgoals := List.tl !subgoals; subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals; fill_holes := fun holes -> match holes with - | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs) - | _ -> raise TrouException + | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs) + | _ -> raise TrouException ) - | _ -> raise (TacticException(tactic,"Cannot split as the goal is no /\\ clause")) + | _ -> raise (TacticException (tactic, "Cannot split as the goal is not a /\\")) ) - | Left -> ( + | Left -> ( match ty with - | TOr(tl,tr) -> ( + | TOr(tl,tr) -> ( subgoals := List.tl !subgoals; subgoals := (tl, hyps) :: !subgoals; fill_holes := fun holes -> match holes with - | hl :: hs -> f (LIg(hl,tr) :: hs) - | _ -> raise TrouException + | hl :: hs -> f (LIg(hl,tr) :: hs) + | _ -> raise TrouException ) - | _ -> raise (TacticException(tactic,"Cannot prove left as the goal is no \\/ clause")) + | _ -> raise (TacticException (tactic, "Cannot apply left as the goal is not a \\/")) ) - | Right -> ( + | Right -> ( match ty with - | TOr(tl,tr) -> ( + | TOr(tl,tr) -> ( subgoals := List.tl !subgoals; subgoals := (tr, hyps) :: !subgoals; fill_holes := fun holes -> match holes with - | hr :: hs -> f (LId(hr,tl) :: hs) - | _ -> raise TrouException + | hr :: hs -> f (LId(hr,tl) :: hs) + | _ -> raise TrouException ) - | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause")) + | _ -> raise (TacticException (tactic, "Cannot apply right as the goal is not a \\/")) ) - | Exact l -> ( + | Exact l -> ( if not (typecheck hyps l ty) then - raise (TacticException(tactic,"λ-term "^(string_of_lam l)^" cannot be typed with "^(string_of_ty ty)^" as its type is "^(match (computeType [] l) with None -> "None" | Some t -> string_of_ty t))) + let ty_str = match computeType [] l with + | None -> "None" + | Some t -> string_of_ty t + in + raise (TacticException ( + tactic, + "λ-term " ^ (string_of_lam l) ^ + " can't be typed with " ^ (string_of_ty ty) ^ + " as its type is " ^ ty_str + )) else ( subgoals := List.tl !subgoals; fill_holes := fun holes -> f (l::holes) @@ -329,10 +350,16 @@ while !subgoals <> [] do with | TacticException(t,s) -> Printf.printf "\027[31mCannot apply the tactic: %s\027[0m\n" s; - if(is_interactive) then applyUntilWorking () else raise (TacticException(t,s)) + if is_interactive then + applyUntilWorking () + else + raise (TacticException (t,s)) | TacticParseException -> Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n"; - if(is_interactive) then applyUntilWorking () else raise TacticParseException + if is_interactive then + applyUntilWorking () + else + raise TacticParseException | e -> Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n"; raise e