miz3/miz3_of_hol.ml

   1 needs "miz3.ml";;
   2
   3 type script_step =
   4 | Tac of string * tactic
   5 | Par of script_step list list;;
   6
   7 type prooftree =
   8 | Prooftree of goal * (string * tactic) * prooftree list
   9 | Open_goal of goal;;
  10
  11 let read_script filename lemmaname =
  12   let rec check_semisemi l =
  13     match l with
  14     | ";"::";"::_ -> true
  15     | " "::l' -> check_semisemi l'
  16     | _ -> false in
  17   let file = open_in filename in
  18   let lemma_string = "let "^lemmaname^" = prove" in
  19   let n = String.length lemma_string in
  20   let rec read_script1 () =
  21     let s = input_line file in
  22     if String.length s >= n & String.sub s 0 n = lemma_string
  23       then (explode s)@"\n"::read_script2 () else read_script1 ()
  24   and read_script2 () =
  25     let l = explode (input_line file) in
  26     if check_semisemi (rev l) then l else l@"\n"::read_script2 () in
  27   let l = read_script1 () in
  28   close_in file;
  29   l;;
  30
  31 let rec tokenize l =
  32   match l with
  33   | [] -> []
  34   | c::l' ->
  35       let l1,l23 = if isalnum c then many (some isalnum) l else [c],l' in
  36       let l2,l3 = many (some isspace) l23 in
  37       (implode l1,if l2 = [] then "" else " ")::tokenize l3;;
  38
  39 let parse_script l =
  40   let rec parse_statement s l =
  41     match l with
  42     | ("`",_)::(",",_)::l' -> s,l'
  43     | (x,y)::l' -> parse_statement (s^x^y) l'
  44     | [] -> failwith "parse_statement" in
  45   let rec parse_tactic b n s y' l =
  46     match l with
  47     | ("\\",y)::l' when not b -> parse_tactic b n (s^y'^"\\\\") y l'
  48     | (x,y)::l' ->
  49         if n = 0 & (x = "THEN" or x = "THENL" or x = ";" or x = "]" or x = ")")
  50         then (Tac(s,exec_tactic s)),l else
  51           let n' = if x = "[" or x = "(" then n + 1 else
  52             if x = "]" or x = ")" then n - 1 else n in
  53           let x',b' =
  54             if x = "`" then
  55               if b then "(parse_term \"",(not b) else "\")",(not b)
  56             else x,b in
  57           parse_tactic b' n' (s^y'^x') y l'
  58     | [] -> failwith "parse_tactic" in
  59   let rec parse_tactics tacs l =
  60     let tac,l' = parse_tactic true 0 "" "" l in
  61     parse_tactics1 (tac::tacs) l'
  62   and parse_tactics1 tacs l =
  63     match l with
  64     | ("THEN",_)::l' -> parse_tactics tacs l'
  65     | ("THENL",_)::("[",_)::l' ->
  66         let tac,l'' = parse_par_tactics [] l' in
  67         parse_tactics1 (tac::tacs) l''
  68     | _ -> (rev tacs),l
  69   and parse_par_tactics tacss l =
  70     let tacs,l' = parse_tactics [] l in
  71     match l' with
  72     | (";",_)::l'' -> parse_par_tactics (tacs::tacss) l''
  73     | ("]",_)::l'' -> (Par (rev (tacs::tacss))),l''
  74     | _ -> failwith "parse_par_tactics" in
  75   match l with
  76   | ("let",_)::_::("=",_)::("prove",_)::("(",_)::("`",_)::l' ->
  77       let s,l'' = parse_statement "" l' in
  78       let tacs,l''' = parse_tactics [] l'' in
  79      (match l''' with
  80       | [")",_; ";",_; ";",_] -> parse_term s,tacs
  81       | _ -> failwith "parse_script")
  82   | _ -> failwith "parse_script";;
  83
  84 let read_script1 filename lemmaname =
  85   parse_script (tokenize (read_script filename lemmaname));;
  86
  87 let tactic_of_script l =
  88   let rec tactic_of_script1 l =
  89     match l with
  90     | [] -> ALL_TAC
  91     | [Tac(_,tac)] -> tac
  92     | (Tac(_,tac))::l' -> tactic_of_script1 l' THEN tac
  93     | (Par ll)::l' ->
  94         tactic_of_script1 l' THENL (map (tactic_of_script1 o rev) ll) in
  95   tactic_of_script1 (rev l);;
  96
  97 let run_script (tm,l) = prove(tm,tactic_of_script l);;
  98
  99 let prooftree_of_script g l =
 100   let rec prooftrees_of gltl tl =
 101     match gltl with
 102     | [] -> []
 103     | (gl,t)::rst ->
 104         let tl1,tl' = chop_list (length gl) tl in
 105         (t tl1)::prooftrees_of rst tl' in
 106   let prooftree_of_script2 t gltl =
 107     flat (map fst gltl),(fun tl -> t (prooftrees_of gltl tl)) in
 108   let rec prooftree_of_script1 g l =
 109     match l with
 110     | [] -> [g],(function [t] -> t | _ -> failwith "prooftree_of_script1")
 111     | (Tac(s,tac))::l' ->
 112         let gl,t = prooftree_of_script1 g l' in
 113         let gltl = map (fun g' -> let _,x,_ = tac g' in
 114           x,(fun tl -> Prooftree(g',(s,tac),tl))) gl in
 115         prooftree_of_script2 t gltl
 116     | (Par ll)::l' ->
 117         let gl,t = prooftree_of_script1 g l' in
 118         let gltl = map2 prooftree_of_script1 gl (map rev ll) in
 119         prooftree_of_script2 t gltl in
 120   let gl,t = prooftree_of_script1 g (rev l) in
 121   t (map (fun x -> Open_goal x) gl);;
 122
 123 let goal_of_prooftree t =
 124   match t with
 125   | Prooftree(g,_,_) -> g
 126   | Open_goal(g) -> g;;
 127
 128 let rec step_of_prooftree prefix n context t =
 129   let frees_of_goal (asl,w) =
 130     union (flat (map (frees o concl o snd) asl)) (frees w) in
 131   let rec extra_ass ass' ass =
 132     if subset ass' ass then [] else (hd ass')::(extra_ass (tl ass') ass) in
 133   let rec lets prefix l =
 134     match l with
 135     | [] -> []
 136     | t::_ ->
 137         let l',l'' = partition ((=) (type_of t) o type_of) l in
 138         step_of_substep prefix (Let l')::lets prefix l'' in
 139   let rec intros prefix n ass =
 140     match ass with
 141     | [] -> [],n,[]
 142     | a::ass' ->
 143         let steps,n',context = intros prefix (n + 1) ass' in
 144         let lab = string_of_int n in
 145         (step_of_substep prefix (Assume(a,[lab]))::steps),
 146         n',((a,lab)::context) in
 147   let shift_labels steps =
 148     let labels = rev (labels_of_steps [] [] steps) in
 149     let labels' =
 150       map ((fun s -> [s],[string_of_int (int_of_string s - 1)]) o hd o fst)
 151         labels in
 152       snd (renumber_steps labels' [] steps) in
 153   let rec steps_of_prooftrees prefix n context (asl,_ as g) tl =
 154     match tl with
 155     | [] -> [],[],n,context
 156     | t'::tl' ->
 157         let (asl',w' as g') = goal_of_prooftree t' in
 158         let prefix' = prefix^(!proof_indent) in
 159         let ll =
 160           lets prefix' (subtract (frees_of_goal g') (frees_of_goal g)) in
 161         let vars = flat (map (function (_,_,Let l) -> l | _ -> []) ll) in
 162         let ass =
 163           extra_ass (map (concl o snd) asl') (map (concl o snd) asl) in
 164         let w'' = list_mk_forall(vars, itlist (curry mk_imp) ass w') in
 165         try
 166           let lab = assoc w'' context in
 167           let steps,labs,n',context' =
 168             steps_of_prooftrees prefix n context g tl' in
 169           steps,Label lab::labs,n',context'
 170         with Failure "find" ->
 171           if vars = [] & ass = [] then
 172             let steps,just,n',context' =
 173               steps_of_prooftree prefix n context t' in
 174             try
 175               let lab = assoc w'' context' in
 176               let steps',labs,n'',context'' =
 177                 steps_of_prooftrees prefix n' context' g tl' in
 178               (steps@steps'),Label lab::labs,n'',context''
 179             with Failure "find" ->
 180               let lab = string_of_int n' in
 181               let steps',labs,n'',context'' =
 182                 steps_of_prooftrees prefix (n' + 1)
 183                   ((w',lab)::context') g tl' in
 184               (steps@
 185                [rewrap_step (step_of_substep prefix (Have(w'',[lab],just)))]@
 186                steps'),Label lab::labs,n'',context''
 187           else
 188             let lab = string_of_int n in
 189             let steps,n',context' = intros prefix' (n + 1) ass in
 190             let steps',just,n'',context'' =
 191               steps_of_prooftree prefix' n' (rev context'@context) t' in
 192             let qed = [rewrap_step (step_of_substep prefix (Qed just))] in
 193             let steps'',n''' =
 194               if steps' = [] then (steps'@qed),n'' else
 195               match last steps' with
 196               | _,_,Have(w''',_,Proof(_,steps''',_)) when w''' = w' ->
 197                  (butlast steps'@
 198                   map (outdent (String.length !proof_indent))
 199                     (shift_labels steps''')),n''
 200               | _ -> (steps'@qed),n'' in
 201             let steps''',labs,n'''',context''' =
 202               steps_of_prooftrees prefix n''' ((w'',lab)::context'') g tl' in
 203             (step_of_substep prefix
 204               (Have(w'',[lab],
 205                Proof (Some (step_of_substep prefix Bracket_proof),
 206                  (ll@steps@steps''), None)))::
 207             steps'''),Label lab::labs,n'''',context'''
 208   and steps_of_prooftree prefix n context t =
 209     match t with
 210     | Prooftree((_,w as g),(s,tac),tl) ->
 211         let steps,f_labs,n',context' =
 212           steps_of_prooftrees prefix n context g tl in
 213         let b_labs = map ((fun x -> Label x) o C assoc context o concl o snd)
 214           (rev (fst g)) in
 215         steps,By((Tactic(s,K tac))::b_labs,f_labs,false),n',context'
 216     | Open_goal(g) -> [],By([Hole],[],false),n,context in
 217   let prefix' = prefix^(!proof_indent) in
 218   match t with
 219   | Prooftree((_,w as g),_,_) ->
 220       let steps,_,_,_ =
 221         steps_of_prooftrees prefix n context g [t] in
 222      (match last steps with
 223       | _,_,Have(_,_,just) ->
 224           step_of_substep prefix (Have(w,[string_of_int n],
 225             if length steps = 1 then just else
 226             let steps',_,_,_ =
 227               steps_of_prooftrees prefix' (n + 1) context g [t] in
 228             Proof (Some (step_of_substep prefix Bracket_proof),
 229               (butlast steps'@
 230             [rewrap_step (step_of_substep prefix (Qed just))]), None)))
 231       | _ -> failwith "step_of_prooftree")
 232   | _ -> failwith "step_of_prooftree";;
 233
 234 let miz3_of_hol filename lemmaname =
 235   let tm,l = read_script1 filename lemmaname in
 236   step_of_prooftree "" 1 [] (prooftree_of_script ([],tm) l);;
 237