lisp-runtime/extract/lisp_extractLib.sml

401   val params = listSyntax.dest_list args |> fst
402   val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` params
404   val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
408   val tm = mk_abs(args_var,subst (mk_els params args_var) lhs)
417   val f = foldr mk_abs goal params
418   val forall_goal = foldr mk_forall goal params
428           \\ METIS_TAC []) |> SPECL params
483   fun params [] ty = []
484     | params [v] ty = [v]
485     | params (v::vs) ty = let
490            map (fn x => sumSyntax.mk_inr(x,t1)) (params vs t2) end
491   val ps = params xs input_ty
743   val params = params1 @ rev (free_vars tm)
744   val fun_ty = foldr (fn (x,y) => mk_fun_ty (type_of x) y) ``:SExp # ^ty`` params
746   val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
760   val side_fun_ty = foldr (fn (x,y) => mk_fun_ty (type_of x) y) ``:bool`` params
762   val side_lhs = foldl (fn (x,y) => mk_comb(y,x)) side_new_fun params
776   val f = foldr mk_abs goal params
777   val forall_goal = foldr mk_forall goal params
790           \\ FULL_SIMP_TAC std_ss (get_assum_clauses())) |> SPECL params
806           \\ METIS_TAC []) |> SPECL params
812   val f = foldr mk_abs goal params
813   val forall_goal = foldr mk_forall goal params
827           \\ FULL_SIMP_TAC std_ss clause_rw) |> SPECL params
841           \\ METIS_TAC clause_rw) |> SPECL params
868     val params = xs |> tl |> map (fst o dest_var)
870     val strs = listSyntax.mk_list(map fromMLstring params,``:string``)
873     in (name,params,def,ind,body,rw,x1) end;
875   val xs = ps |> map (fn (name,params,def,ind,body,rw,x1) => x1)
885     val (name,params,def,ind,body,rw,x1) = el 1 ps
887   fun prove_corr (name,params,def,ind,body,rw,x1) = let
911     val params = listSyntax.dest_list args |> fst
912     val ty = foldr (fn (x,y) => mk_sexp_fun_ty y) ``:SExp`` params
914     val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params
918     val tm = mk_abs(args_var,subst (mk_els params args_var) lhs)
925     val f = foldr mk_abs goal params
926     val forall_goal = foldr mk_forall goal params
934             \\ REPEAT STRIP_TAC \\ METIS_TAC [isTrue_INTRO]) |> SPECL params